B1-5..B1-20: distill remaining code behaviors into specs (rendering.allium, post/media/task/generation/editor specs)

This commit is contained in:
2026-05-30 14:33:19 +02:00
parent dfb2f8870b
commit 723a7ec1f7
11 changed files with 354 additions and 22 deletions

View File

@@ -36,6 +36,7 @@ surface TaskRuntimeSurface {
TaskWorkCompleted(task)
TaskWorkFailed(task, error_message)
ProgressReported(task, value, message)
FinishedTaskEvictionDue()
}
surface TaskSurface {
@@ -54,6 +55,8 @@ surface TaskSurface {
config {
max_concurrent: Integer = 3
progress_throttle: Duration = 250.milliseconds
finished_task_ttl: Duration = 1.hour
recent_finished_limit: Integer = 10
}
invariant MaxConcurrency {
@@ -112,6 +115,23 @@ invariant ProgressThrottled {
-- At most one progress event per 250ms per task
}
invariant FinishedTaskRetention {
-- The status snapshot surfaces only the most recent finished tasks:
-- completed/failed/cancelled tasks beyond config.recent_finished_limit
-- (newest first) are not shown.
let finished = Tasks where status in {completed, failed, cancelled}
-- At most config.recent_finished_limit finished tasks are reported.
}
rule EvictFinishedTasks {
when: FinishedTaskEvictionDue()
-- Periodic sweep (every config.finished_task_ttl). A finished task whose
-- finished_at is older than config.finished_task_ttl is dropped from state.
for task in Tasks where status in {completed, failed, cancelled}:
if now - task.finished_at >= config.finished_task_ttl:
ensures: not exists task
}
-- External tasks: lifecycle controlled by caller (e.g., renderer-side scripts)
rule RegisterExternalTask {
when: RegisterExternalTaskRequested(name)