Effect4

Open workopen

The open part of the plan: 11 planned goals, and 26 theorems proved modulo them. A goal's docstring, written with its statement, says why its proof waits. A chain shows how a theorem reaches a goal. Each step is an edge of the plan, from a node to a node its proof reaches first.

once_placed_pushes_onceopen:Effect4.Program.FinalizerRun.once_placed_pushes_once

Control-source uniqueness obligation of the at-most-once claim. A once-placed source pushes its finalizer frame at most once across all fibers. Consumer: the atomic cleanup-log claim. It supplies no finalizer progress.

Module
Effect4.Laws.Program.FinalizerRun
Claims
once-placed-finalizer
Requirements
R11
∀ (p : Effect4.Program.NativeEff) (table : Effect4.Program.RowTable) (cf : Nat) … (14 lines)
∀ (p : Effect4.Program.NativeEff) (table : Effect4.Program.RowTable) (cf : Nat)
  (m : Effect4.Program.NativeMachine) (q : List Nat),
  Eq (Effect4.Program.OncePlaced (Effect4.Program.Node.eff p) q) Bool.true →
    Effect4.Program.Guard.Reachable p table cf m →
      instLENat.le
        (List.countP (Effect4.Program.FinalizerRun.registeredAt q)
          (m.trace
            (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
              Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
            (Effect4.FrameFiber Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
              Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
            (Effect4.FrameEvent Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
              Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)))
        1

countdown_parks_positionalopen:Effect4.Program.Typed.Evaluating.countdown_parks_positional

A positional countdown's park (fiberPre's positional arm of awaitAll and awaitAllFailFast: a tuple certificate of per-target exit columns, which Layer.merge's siblings use): as Evaluating.countdown_parks, the record resuming with the exits at the tuple of the targets' columns. Planned: J's countdown payload holds one pair of columns for every target, so it cannot type this record; a positional payload must carry the columns in the targets' order. J then admits a stale or a duplicate countdown firing that would append past them (seat B's finding, 2026-10-12). Neither rc.112 nor 4.0.1 fires a target's observer twice (fiberAwaitAll, internal/effect.ts:779-813, the same text in 4.0.1), so the proof needs J to say that each countdown key has at most one firing to come. Consumer: awaitAllParks, awaitAllFailFastParks.

Module
Effect4.Laws.Program.Typed.Commands.Clauses.Park
Claims
step-loop-preserves, step-deliver-preserves, typed-state-admitted, decision-keeps-typed, m7-exits-typed, m7-stores-typed, m7-never-halts, m7-admitted, m7-exit-handles-valid, obs-typed-admitted, m7-results-exit-hasty
Requirements
R1, R6, R9
∀ {root : Effect4.Program.Typed.ProgramSource} {rootTy : Effect4.Program.EffTy} … (93 lines)
∀ {root : Effect4.Program.Typed.ProgramSource} {rootTy : Effect4.Program.EffTy}
  {w : Effect4.Program.Typed.World} {m : Effect4.Program.Sched.RState}
  {rest : List Effect4.Program.Sched.RCmd} {f : Effect4.Program.Sched.RFiber} {y : Bool},
  Effect4.Program.Typed.Evaluating root rootTy w m rest f y →
    Eq (Effect4.Program.Typed.raceRegistrationR f.frame.current) Option.none →
      Eq (Effect4.Program.Sched.externalRequestR f.frame.current) Option.none →
        ∀ {targets : List Effect4.FiberId} (failFast : Bool) {exits : List Effect4.Machine.ExitV}
          {target : Effect4.FiberId} {remaining : List Effect4.FiberId},
          Eq
              (Effect4.Machine.countdownWalk
                { fibers := m.fibers, races := m.races, nextId := m.nextId,
                  nextToken := instHAdd.hAdd m.nextToken 1, nextRace := m.nextRace,
                  middlewareInstalled := m.middlewareInstalled, armed := m.armed, state := m.state,
                  trace := m.trace, stuck := m.stuck, forks := m.forks }
                targets List.nil)
              { fst := exits, snd := Option.some { fst := target, snd := remaining } } →
            (∀ (id : Effect4.FiberId),
                List.instMembership.mem targets id → instLTNat.lt id.value m.nextId) →
              ∀ (cols : Effect4.FiberId → Prod Effect4.Program.Ty Effect4.Program.Ty),
                (∀ (id : Effect4.FiberId),
                    List.instMembership.mem targets id →
                      Effect4.Program.Typed.FiberColumnsBelow w id (cols id).fst (cols id).snd) →
                  ∀ (next' : Effect4.Machine.ExitV → Effect4.Program.Sched.RProgram)
                    (row : Effect4.Machine.Env.Requirement) (flag : Bool),
                    Effect4.Machine.Env.Context.Satisfies f.context.services row →
                      (∀ (ty : Effect4.Program.EffTy),
                          Eq (w.Γ f.id) (Option.some ty) →
                            Effect4.Program.Typed.MHostStack root w
                              (Effect4.Machine.RunMachine.update m f) f.id
                              {
                                fst :=
                                  Effect4.Program.Typed.AmbientPosition.result
                                    {
                                        fst :=
                                          Effect4.Program.EffTy.pure
                                            (Effect4.Program.Ty.tuple
                                              (List.map (fun t => (cols t).fst.exitOf (cols t).snd)
                                                targets)),
                                        snd := { fst := row, snd := row } }.fst
                                    {
                                          fst :=
                                            Effect4.Program.EffTy.pure
                                              (Effect4.Program.Ty.tuple
                                                (List.map
                                                  (fun t => (cols t).fst.exitOf (cols t).snd)
                                                  targets)),
                                          snd := { fst := row, snd := row } }.snd.fst
                                    {
                                          fst :=
                                            Effect4.Program.EffTy.pure
                                              (Effect4.Program.Ty.tuple
                                                (List.map
                                                  (fun t => (cols t).fst.exitOf (cols t).snd)
                                                  targets)),
                                          snd := { fst := row, snd := row } }.snd.snd,
                                snd := f.frame.interruptible }
                              (Effect4.Program.Typed.finalPos ty flag)
                              (List.cons (Effect4.Program.Sched.ScopeFrame.answer next')
                                f.frame.stack)) →
                        (∀ (M : Effect4.Program.Sched.RState) (g : Effect4.Program.Sched.RFiber)
                            (edits :
                              List
                                (Effect4.Machine.FiberEdit Effect4.Machine.Err
                                  Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)),
                            Eq g.frame.current f.frame.current →
                              Eq
                                (Effect4.Program.Sched.prepareIterR
                                  { machine := M, fiber := g, yielding := y,
                                    outcome := Effect4.Machine.Outcome.parked, nested := List.nil,
                                    edits := edits })
                                { machine := M, fiber := g, yielding := y,
                                  outcome := Effect4.Machine.Outcome.parked, nested := List.nil,
                                  edits := edits }) →
                          Effect4.Program.Typed.SettlesTyped root rootTy w f.id rest
                            (Effect4.Program.Sched.prepareIterR
                              { machine := Effect4.Program.Typed.countdownMachine m target f.id,
                                fiber :=
                                  Effect4.Program.Typed.countdownFiber root f next'
                                    { token := m.nextToken, remaining := remaining,
                                      collected := exits,
                                      resumeWith := Effect4.Machine.Resume.exitsValue,
                                      failFast := failFast },
                                yielding := y,
                                outcome :=
                                  Effect4.Machine.FiberAction.outcomeOf
                                    (Effect4.Program.Typed.countdownMachine m target f.id)
                                    Bool.true,
                                nested := List.nil,
                                edits :=
                                  List.cons
                                    (Effect4.Machine.FiberEdit.observe target
                                      (Effect4.Machine.Observer.countdown f.id m.nextToken))
                                    List.nil })

Proved modulo this goal (10), each by its shortest chain of nearest nodes:

request_leadsopen:Effect4.Run.CallTree.request_leads

A live native request retains a local call position reached under submitted exits. Consumer: request_in_tree, then the original routing clause. The unresolved obligation includes arbitrary budget cuts and every permitted control decision. The existing local agreement theorem supplies the subsequent call-tree observation.

Module
Effect4.Laws.Run.CallTree
Claims
recorded-call-tree-prefix
Requirements
R5, R6, R10
∀ (s : Effect4.Run), … (41 lines)
∀ (s : Effect4.Run),
  s.Reached →
    Eq (Effect4.Program.Denote.StraightRows s.built.table s.built.program) Bool.true →
      Eq (Effect4.Run.CallTree.NoCauseHandler s.built.program) Bool.true →
        Effect4.Program.SourceScope.ExternalOnly s.built.program →
          Effect4.Program.SourceScope.ConcreteReplies s.built.table →
            ∀ (call : Effect4.Api.HostSession.Call) (token : Nat),
              Eq (Effect4.Program.requestOf s.machine call.fiber token)
                  (Option.some { fst := call.op, snd := call.request }) →
                Exists fun i =>
                  Exists fun row =>
                    Exists fun tape =>
                      Exists fun frame =>
                        Exists fun stores =>
                          And (Eq call.op (Effect4.Program.NativeOp.external i))
                            (And
                              (Eq (Effect4.Program.externalRow s.built.table i) (Option.some row))
                              (And
                                (∀ (ex : Effect4.Machine.ExitV),
                                  List.instMembership.mem tape ex →
                                    Exists fun reply =>
                                      And
                                        (List.instMembership.mem s.journal
                                          (Effect4.Api.Runner.Command.submit reply))
                                        (Eq reply.completion
                                          (Effect4.Machine.Completion.ofExit ex)))
                                (And
                                  (Effect4.Program.Agreement.Leads
                                    (Effect4.Run.CallTree.admittedTapeHost s.built.table)
                                    s.built.program
                                    (Effect4.Program.Agreement.Pos.live
                                      (Effect4.Program.Agreement.fiberOf
                                        (Effect4.Program.compile s.built.program
                                          s.budget.compileFuel)
                                        List.nil)
                                      Effect4.Machine.Stores.empty)
                                    tape (Effect4.Program.Agreement.Pos.live frame stores) List.nil)
                                  (And
                                    (Eq (Effect4.Program.Agreement.IsCall frame.current) Bool.true)
                                    (Eq (Effect4.Program.Agreement.callOf frame.current)
                                      (Option.some { fst := i, snd := call.request }))))))

Proved modulo this goal (3), each by its shortest chain of nearest nodes:

log_debitsopen:Test.Dogfood.Scenario.Atomic.Cleanup.log_debits

Cleanup-log provenance obligation of the original claim. Every logged identity comes from its request's finalizer, with at most one write per start. Reach: actual admitted histories, including interruption and incomplete commands. Consumer: cleaned; the static placement proof alone does not establish this property.

Module
Test.Dogfood.Scenario.Atomic.Cleanup
Claims
—
Requirements
R4, R11
∀ (b : Effect4.Api.Built) (m : Effect4.Program.NativeMachine), … (25 lines)
∀ (b : Effect4.Api.Built) (m : Effect4.Program.NativeMachine),
  Eq
      (Effect4.Api.Author.build
        (Test.Dogfood.Scenario.Atomic.shop Test.Dogfood.Scenario.Atomic.Fault.none))
      (Except.ok b) →
    Effect4.Run.HistoryOf b Test.Dogfood.Scenario.Atomic.budget.compileFuel m →
      And
        (∀ (i : Nat),
          List.instMembership.mem (Test.Dogfood.Scenario.Atomic.Store.observeM m).cleaned i →
            List.instMembership.mem Test.Dogfood.Scenario.Atomic.requests i)
        (∀ (i : Nat),
          List.instMembership.mem Test.Dogfood.Scenario.Atomic.requests i →
            instLENat.le (List.count i (Test.Dogfood.Scenario.Atomic.Store.observeM m).cleaned)
              (List.countP
                (Effect4.Program.FinalizerRun.startedAt
                  (Test.Dogfood.Scenario.Atomic.Cleanup.requestPath i))
                (m.trace
                  (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
                    Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
                  (Effect4.FrameFiber Effect4.Program.EffName Effect4.Program.EffThunk
                    Effect4.Machine.Val Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                    Effect4.Machine.Ann)
                  (Effect4.FrameEvent Effect4.Program.EffName Effect4.Program.EffThunk
                    Effect4.Machine.Val Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                    Effect4.Machine.Ann))))

Proved modulo this goal (2), each by its shortest chain of nearest nodes:

shop_stagesopen:Test.Dogfood.Scenario.Atomic.Store.shop_stages

The stages exist (program-specific; new). Every machine of every history of the shop admits a stage assignment that fits its observation.

Placement. Concept store-typing, requirement R4. Question: the scenario clauses counted and committed, whose step this is. Consumers: Atomic.counted, Atomic.committed; with a cleaned stage per request it also serves cleans_once (R11, another seat's). Reach: the built shop, every compile budget, every control history. Not established: that a request decides (progress), anything of a lowered run. Route (README.md, section S2): the shop's per-fiber positions, by the fiber-local residual law (G2), and one check per write site and per interruption.

Module
Test.Dogfood.Scenario.Atomic.Store
Claims
—
Requirements
R4
∀ (b : Effect4.Api.Built), … (10 lines)
∀ (b : Effect4.Api.Built),
  Eq
      (Effect4.Api.Author.build
        (Test.Dogfood.Scenario.Atomic.shop Test.Dogfood.Scenario.Atomic.Fault.none))
      (Except.ok b) →
    ∀ (compileFuel : Nat) (m : Effect4.Program.NativeMachine),
      Effect4.Run.ControlHistory b compileFuel m →
        Exists fun g =>
          Test.Dogfood.Scenario.Atomic.Store.StagesFit g
            (Test.Dogfood.Scenario.Atomic.Store.observeM m)

Proved modulo this goal (3), each by its shortest chain of nearest nodes:

jobs_stepopen:Test.Dogfood.Scenario.QueueWorkers.Assertions.jobs_step

Machine-to-model preservation for held_within_fed at an actual funded command boundary. It needs the queue-cell writer census, admitted take replies and once-entered continuations. Consumer: jobs_boundary, then the first clause. It establishes no rest or progress claim.

Module
Test.Dogfood.Scenario.QueueWorkers.Assertions
Claims
—
Requirements
R10, R12
∀ (total : Nat) (b : Effect4.Api.Built) (s : Effect4.Run) (c : Effect4.Api.Runner.Command),
  Eq (Effect4.Api.Author.build (Test.Dogfood.Scenario.QueueWorkers.crew total)) (Except.ok b) →
    Test.Dogfood.Scenario.QueueWorkers.Assertions.Basis b s →
      Test.Dogfood.Scenario.QueueWorkers.Assertions.Jobs s →
        Eq (s.rowReads c) Bool.true → Test.Dogfood.Scenario.QueueWorkers.Assertions.Jobs (s.step c)

Proved modulo this goal (4), each by its shortest chain of nearest nodes:

logs_historyopen:Test.Dogfood.Scenario.QueueWorkers.Assertions.logs_history

The remaining cleanup writer obligation on the original actual history. Each observed identity spends a release start at its own source acquisition. Consumer: cleanup_step, then the unchanged releases_once; no progress or release order follows.

Module
Test.Dogfood.Scenario.QueueWorkers.Assertions
Claims
—
Requirements
R10, R11
∀ (total compileFuel : Nat) (b : Effect4.Api.Built) (machine : Effect4.Program.NativeMachine), … (27 lines)
∀ (total compileFuel : Nat) (b : Effect4.Api.Built) (machine : Effect4.Program.NativeMachine),
  Eq (Effect4.Api.Author.build (Test.Dogfood.Scenario.QueueWorkers.crew total)) (Except.ok b) →
    Effect4.Run.HistoryOf b compileFuel machine →
      And
        (∀ (value : Effect4.Machine.Val),
          List.instMembership.mem (Test.Dogfood.Scenario.QueueWorkers.Assertions.log machine)
              value →
            Exists fun i =>
              And (List.instMembership.mem (List.cons 1 (List.cons 2 (List.cons 3 List.nil))) i)
                (Eq value (Effect4.Store.Val.nat i)))
        (∀ (i : Nat),
          List.instMembership.mem (List.cons 1 (List.cons 2 (List.cons 3 List.nil))) i →
            instLENat.le
              (List.count (Effect4.Store.Val.nat i)
                (Test.Dogfood.Scenario.QueueWorkers.Assertions.log machine))
              (List.countP
                (Effect4.Program.ReleaseTrace.releaseAt
                  (Test.Dogfood.Scenario.QueueWorkers.Assertions.acquirePath i))
                (machine.trace
                  (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
                    Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
                  (Effect4.FrameFiber Effect4.Program.EffName Effect4.Program.EffThunk
                    Effect4.Machine.Val Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                    Effect4.Machine.Ann)
                  (Effect4.FrameEvent Effect4.Program.EffName Effect4.Program.EffThunk
                    Effect4.Machine.Val Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                    Effect4.Machine.Ann))))

Proved modulo this goal (3), each by its shortest chain of nearest nodes:

rest_stepopen:Test.Dogfood.Scenario.QueueWorkers.Assertions.rest_step

Rest preservation for fed_accounted and queue_settled at an actual command boundary. It needs committed delivery custody, interrupted withdrawal and queue wake-to-wait correspondence. Consumer: rest_script, then the two rest clauses. It establishes no fairness or liveness claim.

Module
Test.Dogfood.Scenario.QueueWorkers.Assertions
Claims
—
Requirements
R10, R12
∀ (total : Nat) (b : Effect4.Api.Built) (s : Effect4.Run) (c : Effect4.Api.Runner.Command),
  Eq (Effect4.Api.Author.build (Test.Dogfood.Scenario.QueueWorkers.crew total)) (Except.ok b) →
    Test.Dogfood.Scenario.QueueWorkers.Assertions.Basis b s →
      Test.Dogfood.Scenario.QueueWorkers.Assertions.Jobs s →
        Test.Dogfood.Scenario.QueueWorkers.Assertions.Rest s →
          Eq (s.rowReads c) Bool.true →
            Test.Dogfood.Scenario.QueueWorkers.Assertions.Rest (s.step c)

Proved modulo this goal (3), each by its shortest chain of nearest nodes:

cleanup_keepsopen:Test.Dogfood.Scenario.Timeout.cleanup_keeps

Cleanup keeps the committed count. Under every script the observation satisfies Observation.cleanupKeeps. Each attempt that ended stands once in the cleanup log, with the count its finalizer saw: its own number. So an interruption by the timer takes no committed count back. Reach: the program fetch, every script of the driver's alphabet, the battery's budgets. It is a statement about the log and the count cell: it counts writes by identity. It does not count a finalizer's invocations, and it does not establish that a finalizer runs. It states no cut inside a masked region: the attempt has none. Concept scope-lifetime-finalization, R11. Consumer: the timeout scenario. Its controls are finite runs, and the seat's receipt records a bounded search.

Module
Test.Dogfood.Scenario.Timeout
Claims
—
Requirements
R6, R11
Test.Dogfood.Scenario.Timeout.CleanupKeeps

Proved modulo this goal (1), each by its shortest chain of nearest nodes:

retries_declaredopen:Test.Dogfood.Scenario.Timeout.retries_declared

Only returned declared failures retry. Each later attempt follows a completed timeout form that returns a declared typed failure. The client starts at most four attempts. Reach: fetch, the battery's budgets, and every plain script. The observation keeps host reply application separate from the form's complete returned exit. The selected entrant identifies its attempt or timer role at the actual exit observer. The statement establishes no fairness, physical deadline, or general law of either form. Concept: translation-simulation, R10. Consumer: the timeout scenario.

Module
Test.Dogfood.Scenario.Timeout
Claims
—
Requirements
R6, R10
Test.Dogfood.Scenario.Timeout.RetriesDeclared

Proved modulo this goal (1), each by its shortest chain of nearest nodes:

logs_stepopen:Test.Dogfood.Scenario.Workers.Assertions.logs_step

Store preservation obligation of releases_once. Reach: the second allocated reference in actual crew histories at every command boundary. It needs the cell's writer census and the value captured at each acquisition source. It proves no host behavior; consumer: step and then history.

Module
Test.Dogfood.Scenario.Workers.Assertions
Claims
—
Requirements
R6, R11
∀ (total cf : Nat) (b : Effect4.Api.Built) (m : Effect4.Program.NativeMachine)
  (x : Prod Nat Effect4.Program.NativeDecision),
  Eq (Effect4.Api.Author.build (Test.Dogfood.Scenario.Workers.crew total)) (Except.ok b) →
    Test.Dogfood.Scenario.Workers.Assertions.Holds b cf m →
      Effect4.Run.Accepted b.table (Effect4.Api.HostSession.callTable b.program b.table) m x.snd →
        Test.Dogfood.Scenario.Workers.Assertions.LogDebits (Effect4.Run.stepBy b m x)

Proved modulo this goal (2), each by its shortest chain of nearest nodes: