Residual Program Typingconcept:residual-program-typing

instantiated-formationclaim:instantiated-formation

Successful row template use checks instantiated map keys and deferred error columns

instantiated-formation: a successful row use retains the actual bindings, the request's and then the binder term's (bindTerm), and strict formation of every substituted column. Typing consumes this through rowTy. This is a static property; it makes no host reply or execution claim.

Module

Effect4.Laws.Program.Template

∀ {row : Effect4.Program.Row} {request : Effect4.Program.Ty} {use : Option Effect4.Program.TermUse}
  {ty : Effect4.Program.EffTy},
  Eq (Effect4.Program.rowTy row request use) (Option.some ty) →
    Exists fun σ =>
      Exists fun bindings =>
        And
          (Eq (Effect4.Program.Bounds.matchB List.nil row.request.normalize request.normalize)
            (Option.some σ))
          (And (Eq (Effect4.Program.bindTerm σ use) (Except.ok bindings))
            (Effect4.Program.Formation.Formed
              (Effect4.Program.Formation.instantiatedSites row bindings)))

seq-typedclaim:seq-typed

The seqR compatibility lemma: denoteR sequences with typed continuations

The seqR compatibility lemma. A first program typed at mid, a value continuation typed at ty at every later world on every value that fits mid's answer column, and equal error columns: the sequence denoteR builds is typed at ty. A failure of the first program skips the continuation and must fit ty's error column, which the equal columns give. The instance of seqGuard_typed at seqR.

Module

Effect4.Laws.Program.Typed.Seq

Literature

ATTAPL, ch. 3, pp. 87–136 (adaptedResult)

∀ (root : Effect4.Program.Typed.ProgramSource) {w : Effect4.Program.Typed.World}
  {mid ty : Effect4.Program.EffTy} {a : Effect4.Program.Sched.RProgram}
  {k : Effect4.Machine.Val → Effect4.Program.Sched.RProgram},
  Effect4.Program.Typed.TypedProg root w mid a →
    (∀ (w' : Effect4.Program.Typed.World),
        w.leHost w' →
          ∀ (v : Effect4.Machine.Val),
            Effect4.Program.Typed.Fits w' v mid.answer →
              Effect4.Program.Typed.TypedProg root w' ty (k v)) →
      Eq mid.error ty.error →
        Effect4.Program.Typed.TypedProg root w ty
          (Effects.Program.bind
            (Effect4.Program.Sched.guardR Effect4.Program.Sched.GuardKind.onSuccess a)
            (Effect4.Program.Sched.seqR k))

close-typedclaim:close-typed

Closing a typed program with unguard preserves typing

Closing keeps the type. Closing a typed program with unguard is typed at the same type: every leaf becomes a closing marker carrying the leaf's exit.

Module

Effect4.Laws.Program.Typed.Seq

Literature

deVilhenaPottier2021, audit P8 (proofTechnique)

∀ (root : Effect4.Program.Typed.ProgramSource) {w : Effect4.Program.Typed.World}
  {T : Effect4.Program.EffTy} {a : Effect4.Program.Sched.RProgram},
  Effect4.Program.Typed.TypedProg root w T a →
    ∀ (g : Effect4.Machine.ExitV → Effect4.Program.Sched.RProgram),
      Effect4.Program.Typed.TypedProg root w T
        (Effects.Program.bind a fun ex =>
          Effects.Program.vis (Sum.inr (Effect4.Program.Sched.FiberOp.unguard ex)) g)

sound-at-app-signatureclaim:sound-at-app-signature

Meaning, loop and run soundness at an application's signature: any table, service declarations at fresh codes, by C3's reflection (R1)

run_typed (the machine) at an application's signature (R1).

Module

Effect4.Laws.Program.SoundAnySignature

∀ (t : Effect4.Program.RowTable) (s : List (Prod Effect4.ServiceKey Effect4.Program.Ty)),
  (∀ (entry : Prod Effect4.ServiceKey Effect4.Program.Ty),
      List.instMembership.mem s entry → { rows := t }.FreshCode entry) →
    ∀ (e : Effect4.Program.NativeEff) (ty : Effect4.Program.EffTy) (fuel : Nat),
      Eq (Effect4.Program.Denote.Straight e) Bool.true →
        Eq (Effect4.Program.effTy { rows := t, services := s }.signature List.nil e)
            (Option.some ty) →
          instLENat.le (Effect4.Program.Agreement.depth e) fuel →
            instLENat.le (instHAdd.hAdd (instHMul.hMul 2 (Effect4.Program.Agreement.steps e)) 6)
                fuel →
              And (Eq (Effect4.Api.run e fuel).outcome Effect4.Api.Outcome.finished)
                (Exists fun ex =>
                  And (Eq (Effect4.Api.run e fuel).exit (Option.some ex))
                    (Effect4.Program.Denote.ExitHasTy ty.answer ty.error
                      (Effect4.Api.run e fuel).stores ex))

straight-meaning-typedclaim:straight-meaning-typed

Typed straight programs return ExitHasTy from the empty environment and stores

A typed straight program's meaning has its type. From the empty stores, the exit is a valid value of the answer type or a cause inside the error type.

Module

Effect4.Laws.Program.MeaningSound

∀ (e : Effect4.Program.NativeEff) (t : Effect4.Program.EffTy),
  Eq (Effect4.Program.Denote.Straight e) Bool.true →
    Eq (Effect4.Program.effTy Effect4.Program.nativeSignature List.nil e) (Option.some t) →
      Effect4.Program.Denote.ExitHasTy t.answer t.error
        (Effect4.Program.Denote.meaning e List.nil Effect4.Machine.Stores.empty).snd
        (Effect4.Program.Denote.meaning e List.nil Effect4.Machine.Stores.empty).fst

denote-typedclaim:denote-typed

The denotation of a checked program is TypedProg at its certificate (M5)

M5's fundamental property (decisions rows 148 and 349, denotesTyped): at every source whose layer references are well formed, a checked point denotes a program typed by the ambient judgment at every world whose service table is the source's and every row holding its requirement row. The arms by induction on fuel (childDenotes_upto), the layer family's by provideLayerArm.

Module

Effect4.Laws.Program.Typed.LayerArm

Literature

XiaEtAl2020, audit P37 (definitionUsed)

∀ (root : Effect4.Program.Typed.ProgramSource), Effect4.Program.Typed.DenotesTyped root

Register record E4-TYPED-CE-020 (REPAIRED)

| `E4-TYPED-CE-020` | REPAIRED 2026-10-01 (seat D2, merged `aabb1b5e`: `DenotesTyped` takes row 170's premise `layerRefsWF`, discharged at the load by `layerRefsWF_of_typeOf`); SEEDED 2026-10-01 (seat D2) | `DenotesTyped` is false at a root whose layer reference targets a reference | Codex's candidate (`docs/research/2026-10-01-landing/codex-second-eyes/2016-d1-review.md`): three `provideLayer`s of `Test.Program.TypedSplit.key` with unit bodies, the last `.ref [1,0,0]` to `.ref [0,0]`; the point `[1,1]` is `PointTyped` at `pure unit` through `Eff.expandIn`, the run's `.ref` arm answers `badShapeExit` (reading, not compiled) | decisions row 170: the premise `layerRefsWF` on `DenotesTyped`, discharged at the load from `typeOfProgram` |

Register record E4-TYPED-CE-021 (REPAIRED)

| `E4-TYPED-CE-021` | REPAIRED 2026-10-01 (seat D2, merged `aabb1b5e`: `PointTyped` carries the completed view, row 175 (a)); SEEDED 2026-10-01 (seat D2) | `DenotesTyped` is false at a point whose completed view holds an exit the world refuses, because `PointTyped` never reads `point.completed` | seat D2's witness: the corpus program `awaitFiber.value`, point `[1]`, env `[fiber 1]`, completed `[(1, success "x")]`, world `Γ 1 = pure nat`; `PointTyped` at `pure (exitOf nat never)`, the denotation `.pure (success (exitOk "x"))` refused | decisions row 175 (ruled): `PointTyped` carries the completed view |

Register record E4-TYPED-CE-022 (REPAIRED)

| `E4-TYPED-CE-022` | REPAIRED 2026-10-01 (seat D2, merged `aabb1b5e`: `DenotesTyped` ranges over worlds whose service table is the source's, row 175); SEEDED 2026-10-01 (seat D2) | `DenotesTyped` is false at a world whose service table differs from the checker's | seat D2's witness: `.service ⟨4,4⟩` (native carrier `nat`) at a world with `serviceTy := fun _ => none` and a context holding `str "x"` under the key | decisions row 175 (ruled): `DenotesTyped` ranges over worlds whose service table is the source's |

Register record E4-TYPED-CE-023 (REPAIRED)

| `E4-TYPED-CE-023` | REPAIRED 2026-10-02 (seat L: built layers answer the fiber-context image, decisions row 176 (b), `f8571cf0`, merged `9a2b7651`; the layer family's arm proved at every source, `provideLayerArm`, `8c9464b6`, merged `71b1c9c1`); SEEDED 2026-10-02 (seat L, `c1c05314`, merged `3f9c2a77`; D2's reserved id) | `DenotesTyped` holds at a typed `provideLayer` point whose memo lookup hits | `memoSrc`, `provideLayer (effect K (succeed 7)) false (succeed unit)` checked at `pure unit`: the hit answers a fiber-context image, which fits `Ty.context` and which the build's reader `Env.decode` refuses, so `addCurrentMemoMapR` answers `badShapeExit`; `old_memo_refuted : ¬ DenotesTyped memoSrc`, kernel-checked at `c1c05314` over the old helpers (`Test/Program/LayerDenotation.lean`; the history control `hit_image_refused_old` stays) | decisions row 176 (b) (ruled): a build answers `builtContext`, every reader is `Val.context?`; row 187 types the memo rows so a guard keeps the hit's type |

Register record E4-TYPED-CE-031 (REPAIRED)

| `E4-TYPED-CE-031` | REPAIRED 2026-10-02 (seat L, L1 `569d3d69`, merged `71b1c9c1`: `orDie` resolves its inner layer on both machines, `resolveLayerWith` and `denoteLayerWith`'s `orDie` arm; the controls `orDie_runs`, `chain_runs` and their reference twins); SEEDED 2026-10-02 (seat L, `c1c05314`, merged `3f9c2a77`) | `ProvideLayerArm` and `DenotesTyped` hold at a well-formed program with a layer reference under `orDie` | `orDieSrc`: `layerRefsWF` admits `orDie (ref t)` and the checker types the expansion, where the reference is its target's term, while the run compiled `orDie`'s inner term directly, the wrong shape at every fuel; `orDie_arm_refuted : ¬ ProvideLayerArm orDieSrc`, `orDie_denotes_refuted`, kernel-checked at `c1c05314` over the old arms | decisions row 185 (owner, 2026-10-02): `orDie` builds its inner layer as it resolves (`Layer.ts:3327-3328`, `self.build(memoMap, scope)`) |

invocation-armclaim:invocation-arm

An invocation of a checked definition block denotes TypedProg at the declared row: the body at its point, its type widened to the declaration (M5's arm, decisions row 328, G3)

An invocation (decisions row 328, goal G3; the arm of denote-typed): the counted step, then the definition's body at its path, its one variable the request's value. The checker types the invocation by the definition's declared row (invoke_hasTy), which the declaration's formation keeps closed: the request's value fits the declared request and the node's type is the declared columns (rowTy_closed_some). The body is typed at its point by the block's typing (BodiesTyped), one unit of fuel lighter (Point.redirect), and its type widens to the declared columns (DefDecl.admits). Its consumer is perform_arm.

Module

Effect4.Laws.Program.Typed.Denotation

∀ {root : Effect4.Program.Typed.ProgramSource} {w : Effect4.Program.Typed.World}
  {p : Effect4.Program.Point} {ty : Effect4.Program.EffTy}
  {available : Effect4.Machine.Env.Requirement} {k : Nat} {r : Effect4.Program.Term} {f : Nat},
  Eq p.fuel (instHAdd.hAdd f 1) →
    Eq ((Effect4.Program.Node.eff root.program).at_ p.path)
        (Option.some
          (Effect4.Program.Node.eff
            (Effect4.Program.Eff.perform (Effect4.Program.NativeOp.call k) r))) →
      Effect4.Program.Typed.PointTyped root w p ty →
        Eq w.serviceTy root.sig.serviceTy →
          Effect4.Program.Typed.BodiesTyped root →
            (∀ (c : Effect4.Program.NativeEff) (path : List Nat),
                Eq ((Effect4.Program.Node.eff root.program).at_ path)
                    (Option.some (Effect4.Program.Node.eff c)) →
                  Effect4.Program.Typed.ChildDenotes root f c path) →
              Effect4.Row.Subset ty.requires available →
                Effect4.Program.Typed.AmbientProg root w available
                  (Effect4.Program.Typed.AmbientPosition.result
                    { fst := ty, snd := { fst := available, snd := available } }.fst
                    { fst := ty, snd := { fst := available, snd := available } }.snd.fst
                    { fst := ty, snd := { fst := available, snd := available } }.snd.snd)
                  (Effect4.Program.Sched.denoteR root.program
                    (Effect4.Program.Eff.perform (Effect4.Program.NativeOp.call k) r) p)

rebuild-admissionclaim:rebuild-admission

Successful rebuilding checks the exact candidate under the retained host table and row names (Built.rebuild)

Successful rebuilding retains the host setup and checks exactly the candidate. The returned Built.admitted certificate is indexed by those program and table fields.

Module

Effect4.Laws.Program.Author

∀ {before after : Effect4.Api.Built} {candidate : Effect4.Api.Program},
  Eq (before.rebuild candidate) (Except.ok after) →
    And (Eq after.program candidate)
      (And (Eq after.table before.table) (Eq after.rowNames before.rowNames))

denote-typed-layer-freeclaim:denote-typed-layer-free

M5 on the layer-free fragment: every arm but provideLayer's, assembled by induction on fuel

M5 on the layer-free fragment: a program none of whose nodes is a provideLayer satisfies the fundamental property; the layer family's arm cannot be reached there (provideLayerArm_of_layerFree).

Module

Effect4.Laws.Program.Typed.Assembly

Literature

XiaEtAl2020, audit P37 (definitionUsed)

∀ (root : Effect4.Program.Typed.ProgramSource),
  Effect4.Program.Typed.LayerFree root.program → Effect4.Program.Typed.DenotesTyped root

load-typed-layer-freeclaim:load-typed-layer-free

The typed load on the layer-free fragment: a checked program loads into J (M5's load connector, the marker premise discharged)

The typed load on the layer-free fragment: a checked program none of whose nodes is a provideLayer loads into J (denotesTyped_of_layerFree, then the load connector).

Module

Effect4.Laws.Program.Typed.Commands.Finish

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy)
  (fuel compileFuel : Nat),
  Effect4.Program.Typed.LayerFree root.program →
    Effect4.Program.Typed.LoadsTyped root rootTy fuel compileFuel

provide-layer-armclaim:provide-layer-arm

The layer family's arm: a layer build at an admitted layer point answers the built context at the layer's checked error type, and the provide protocol around it is typed (decisions rows 176 (b), 185-187)

ProvideLayerArm holds at every source: the hypothesis the assembly was conditional on.

Module

Effect4.Laws.Program.Typed.LayerArm

∀ (root : Effect4.Program.Typed.ProgramSource), Effect4.Program.Typed.ProvideLayerArm root

Register record E4-TYPED-CE-023 (REPAIRED)

| `E4-TYPED-CE-023` | REPAIRED 2026-10-02 (seat L: built layers answer the fiber-context image, decisions row 176 (b), `f8571cf0`, merged `9a2b7651`; the layer family's arm proved at every source, `provideLayerArm`, `8c9464b6`, merged `71b1c9c1`); SEEDED 2026-10-02 (seat L, `c1c05314`, merged `3f9c2a77`; D2's reserved id) | `DenotesTyped` holds at a typed `provideLayer` point whose memo lookup hits | `memoSrc`, `provideLayer (effect K (succeed 7)) false (succeed unit)` checked at `pure unit`: the hit answers a fiber-context image, which fits `Ty.context` and which the build's reader `Env.decode` refuses, so `addCurrentMemoMapR` answers `badShapeExit`; `old_memo_refuted : ¬ DenotesTyped memoSrc`, kernel-checked at `c1c05314` over the old helpers (`Test/Program/LayerDenotation.lean`; the history control `hit_image_refused_old` stays) | decisions row 176 (b) (ruled): a build answers `builtContext`, every reader is `Val.context?`; row 187 types the memo rows so a guard keeps the hit's type |

Register record E4-TYPED-CE-031 (REPAIRED)

| `E4-TYPED-CE-031` | REPAIRED 2026-10-02 (seat L, L1 `569d3d69`, merged `71b1c9c1`: `orDie` resolves its inner layer on both machines, `resolveLayerWith` and `denoteLayerWith`'s `orDie` arm; the controls `orDie_runs`, `chain_runs` and their reference twins); SEEDED 2026-10-02 (seat L, `c1c05314`, merged `3f9c2a77`) | `ProvideLayerArm` and `DenotesTyped` hold at a well-formed program with a layer reference under `orDie` | `orDieSrc`: `layerRefsWF` admits `orDie (ref t)` and the checker types the expansion, where the reference is its target's term, while the run compiled `orDie`'s inner term directly, the wrong shape at every fuel; `orDie_arm_refuted : ¬ ProvideLayerArm orDieSrc`, `orDie_denotes_refuted`, kernel-checked at `c1c05314` over the old arms | decisions row 185 (owner, 2026-10-02): `orDie` builds its inner layer as it resolves (`Layer.ts:3327-3328`, `self.build(memoMap, scope)`) |

load-typedclaim:load-typed

M5: a lawful, checked, closed source with an empty requirement row loads into J

M5 (loadsTyped): a lawful, checked, closed source whose requirement row is empty loads into J at the initial world, at every fuel and compile budget.

Module

Effect4.Laws.Program.Typed.LayerArm

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy)
  (fuel compileFuel : Nat), Effect4.Program.Typed.LoadsTyped root rootTy fuel compileFuel

load-typed-checkedclaim:load-typed-checked

The typed load for every checked program: M5 with no lawful-signature or closed-row premise

The typed load for a checked closed program: row 117's empty requirement row applies at the load. The source's lawful-signature premise is not read here.

Module

Effect4.Laws.Program.Typed.LayerArm

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy)
  (fuel compileFuel : Nat),
  Eq (Effect4.Program.typeOfProgram root.sig.signature root.program) (Option.some rootTy) →
    Eq rootTy.requires Effect4.Machine.Env.Requirement.empty →
      Exists fun w =>
        Effect4.Program.Typed.MachineTyped root rootTy w
          (Effect4.Program.Sched.loadR root.program fuel compileFuel)

bind-closedclaim:bind-closed

TypedProg is closed under bind

Red control: TypedProg is not closed under bind. closeAtNat is typed at nat, toUnit is typed at unit on every exit at every later world, and their sequence is not typed at unit: the marker's exit must fit the current type.

Module

Test.Program.TypedProgBindRed

Literature

deVilhenaPottier2021, audit P8 (excludedFeature)

∀ (root : Effect4.Program.Typed.ProgramSource) (w : Effect4.Program.Typed.World),
  Exists fun mid =>
    Exists fun ty =>
      Exists fun p =>
        Exists fun k =>
          And (Effect4.Program.Typed.TypedProg root w mid p)
            (And
              (∀ (w' : Effect4.Program.Typed.World),
                w.leHost w' →
                  ∀ (ex : Effect4.Machine.ExitV),
                    Effect4.Program.Typed.ExitOk w' mid ex →
                      Effect4.Program.Typed.TypedProg root w' ty (k ex))
              (Not (Effect4.Program.Typed.TypedProg root w ty (Effects.Program.bind p k))))

Register record E4-TYPED-CE-030 (REPAIRED)

| `E4-TYPED-CE-030` | REPAIRED 2026-10-01 (seat D2, merged `aabb1b5e`: every guard shape has its compatibility lemma); SEEDED 2026-10-01 (coordinator; the red controls landed with decisions row 148, in the battery under the gate's ceiling) | `TypedProg` is closed under bind: a program typed at `mid` and a continuation typed at `ty` at every later world on every exit `ExitOk` admits at `mid` make a sequence typed at `ty` | `Test/Program/TypedProgBindRed.lean`: `typedProg_not_bind_closed` (`:32`; a closing marker's exit must fit the current type), `bind_not_typed` and `guard_bind_not_closed` (a first program whose only closing marker sits inside a guard body does not bind either); green control `seq_sample` | no bind rule: M5 sequences per construct (`seq_typed`, `src/Effect4/Laws/Program/Typed/Seq.lean:59`, with `close_typed`); the `onFailure`, `all` and `onExit` shapes beside it, landed by seat D2 (`catchGuard_typed`, `allGuard_typed`, `onExit_typed`, the general `guardBind_typed`; decisions row 148) |

guard-bind-typedclaim:guard-bind-typed

The guard compatibility lemma: a guarded program bound into its arms is typed (the general form of seq_typed, row 148)

The guard compatibility lemma (the general form of seq_typed, decisions row 148): a first program typed at mid, a continuation typed at ty at every later world on every exit the guard's arm takes and mid admits, and every exit the arm does not take admitted at ty: the guarded sequence is typed at ty. Every guard denoteR builds has this shape (guardR kind a, bound to a continuation); the body closes by close_typed.

Module

Effect4.Laws.Program.Typed.Seq

∀ (root : Effect4.Program.Typed.ProgramSource) {w : Effect4.Program.Typed.World}
  {mid ty : Effect4.Program.EffTy} {kind : Effect4.Program.Sched.GuardKind}
  {a : Effect4.Program.Sched.RProgram} {K : Effect4.Machine.ExitV → Effect4.Program.Sched.RProgram},
  Effect4.Program.Typed.TypedProg root w mid a →
    (∀ (w' : Effect4.Program.Typed.World),
        w.leHost w' →
          ∀ (ex : Effect4.Machine.ExitV),
            Eq (kind.hasExitArm ex) Bool.true →
              Effect4.Program.Typed.ExitOk w' mid ex →
                Effect4.Program.Typed.TypedProg root w' ty (K ex)) →
      (∀ (w' : Effect4.Program.Typed.World),
          w.leHost w' →
            ∀ (ex : Effect4.Machine.ExitV),
              Effect4.Program.Typed.ExitOk w' mid ex →
                Eq (kind.hasExitArm ex) Bool.false → Effect4.Program.Typed.ExitOk w' ty ex) →
        Effect4.Program.Typed.TypedProg root w ty
          (Effects.Program.bind (Effect4.Program.Sched.guardR kind a) K)

on-failure-typedclaim:on-failure-typed

The onFailure shape (catchCause, catchIf, orDie, a finalizer's cleanup) is typed

The onFailure shape (catchCause, catchIf, orDie, a finalizer's cleanup): the continuation at every failure mid admits; a success skips it and must fit ty's answer column, below which mid's is.

Module

Effect4.Laws.Program.Typed.Seq

∀ (root : Effect4.Program.Typed.ProgramSource) {w : Effect4.Program.Typed.World}
  {mid ty : Effect4.Program.EffTy} {a : Effect4.Program.Sched.RProgram}
  {K : Effect4.Machine.ExitV → Effect4.Program.Sched.RProgram},
  Effect4.Program.Typed.TypedProg root w mid a →
    Eq (mid.answer.subN ty.answer) Bool.true →
      (∀ (w' : Effect4.Program.Typed.World),
          w.leHost w' →
            ∀
              (c :
                Effect4.Cause Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId
                  Effect4.Machine.Ann),
              Effect4.Program.Typed.ExitOk w' mid (Effect4.Exit.failure c) →
                Effect4.Program.Typed.TypedProg root w' ty (K (Effect4.Exit.failure c))) →
        Effect4.Program.Typed.TypedProg root w ty
          (Effects.Program.bind
            (Effect4.Program.Sched.guardR Effect4.Program.Sched.GuardKind.onFailure a) K)

all-guard-typedclaim:all-guard-typed

The all and onExit guard shapes (exit, matchCause, a finalizer's boundary) are typed

The all and onExit shapes (exit, matchCause, a finalizer's boundary): a guard whose arm takes every exit runs the continuation on every exit mid admits; nothing skips.

Module

Effect4.Laws.Program.Typed.Seq

∀ (root : Effect4.Program.Typed.ProgramSource) {w : Effect4.Program.Typed.World}
  {mid ty : Effect4.Program.EffTy} {kind : Effect4.Program.Sched.GuardKind},
  (∀ (ex : Effect4.Machine.ExitV), Eq (kind.hasExitArm ex) Bool.true) →
    ∀ {a : Effect4.Program.Sched.RProgram}
      {K : Effect4.Machine.ExitV → Effect4.Program.Sched.RProgram},
      Effect4.Program.Typed.TypedProg root w mid a →
        (∀ (w' : Effect4.Program.Typed.World),
            w.leHost w' →
              ∀ (ex : Effect4.Machine.ExitV),
                Effect4.Program.Typed.ExitOk w' mid ex →
                  Effect4.Program.Typed.TypedProg root w' ty (K ex)) →
          Effect4.Program.Typed.TypedProg root w ty
            (Effects.Program.bind (Effect4.Program.Sched.guardR kind a) K)

on-exit-typedclaim:on-exit-typed

The onExit shape onExitR builds: the body and the finalizer at their types

The onExit shape (onExitR, DenoteR.lean): the body typed at b, below the result in both columns, and the finalizer typed at f on every exit b admits, its error column below the result's: the region is typed at the result. The guard's arm takes every exit (allGuard_typed); each runs the finalizer's boundary (finalizer_typed).

Module

Effect4.Laws.Program.Typed.Seq

∀ (root : Effect4.Program.Typed.ProgramSource) {w : Effect4.Program.Typed.World}
  {b f ty : Effect4.Program.EffTy} {body : Effect4.Program.Sched.RProgram}
  {fin : Effect4.Machine.ExitV → Effect4.Program.Sched.RProgram} {flag : Bool},
  Eq (b.answer.subN ty.answer) Bool.true →
    Eq (b.error.subN ty.error) Bool.true →
      Eq (f.error.subN ty.error) Bool.true →
        Effect4.Program.Typed.TypedProg root w b body →
          (∀ (w' : Effect4.Program.Typed.World),
              w.leHost w' →
                ∀ (ex : Effect4.Machine.ExitV),
                  Effect4.Program.Typed.ExitOk w' b ex →
                    Effect4.Program.Typed.TypedProg root w' f (fin ex)) →
            Effect4.Program.Typed.TypedProg root w ty (Effect4.Program.Sched.onExitR body fin flag)

scoped-body-substitution-boundaryclaim:scoped-body-substitution-boundary

A restore site is one node that binds nothing, with its checked body at child 0: both saved choices run that one body in the node's environment; a typed point at the node denotes a typed program, its saved term evaluates to an image, and its body's point is typed at the node's type; a saved value passed as data keeps its choice and holds no handle; the mask's builder is the program's own expansion over bind (decisions rows 245, 246; the restore node's half of the claim; no agreement with a target)

The restore node's body (the claim scoped-body-substitution-boundary, for the mask; concept residual-program-typing, requirement R4; decisions rows 245 and 246).

Reach: the checker at any signature and path; the compile at a positive budget; the typed state at a source whose layer references are well formed and a world whose service table is the source's (denotesTyped). It does not establish agreement with a target. The claim's second half, a later constructor that binds a scope, has no statement: the mask adds none. Its consumers are the Queue's waiting wrapper and the Semaphore's protected permit, which descend into a restore site's body by bodyTyped.

Module

Effect4.Laws.Program.Typed.Mask

Effect4.Program.Typed.RestoreBodyBoundary

admitted-source-lawfulclaim:admitted-source-lawful

An admitted program's signature, its row table and its service declarations, is lawful: program admission runs admitSig (the bridge from admission to the typed state)

The bridge (proved; claim admitted-source-lawful). An admitted program's signature is lawful: admission ran admitSig (decisions row 21), and admitSig_ok_iff reads its ok as LawfulSig. E4-TYPED-CE-041's three witnesses, which the table-indexed admission admitted, are refused now (Test/Counterexamples/Program/AdmissionUnserved.lean).

Module

Effect4.Laws.Program.Typed.AdmittedSource

∀ {program : Effect4.Program.NativeEff} {app : Effect4.Program.SigApp}
  (a : Effect4.Program.AdmittedProgram program app), Effect4.Program.LawfulSig app

Register record E4-TYPED-CE-041 (REPAIRED)

| `E4-TYPED-CE-041` | REPAIRED 2026-10-04 (seat S, branch `seat/sigapp`: decisions row 21's slice, step 2; `lawfulSig_of_admitted` has no premise, `[propext, Quot.sound]`); SEEDED 2026-10-04 (Claude, the Σ_app slice survey; kernel-checked by `decide +kernel`) | A program the API admits denotes a lawful source: `AdmittedProgram program table` implies `LawfulSig ⟨table, []⟩`, the premise of M5–M7 (`ProgramSource.lawful`) | `Test/Counterexamples/Program/AdmissionUnserved.lean`, one witness per clause the API did not check: a row requiring the key at service code 30, which no built-in carrier serves, performed by the program; a row whose answer mentions an unbound parameter; a parameter under a union head. Each was admitted by `admitProgram` and refused by `admitSig`. Repaired: `admitProgram` refuses each with the refusal `admitSig` gives (`refused`: `.signature (.unservedKey 0 appKey)`; `refused_unscoped`: `.signature (.row 0 .notWellScoped)`; `refused_union`: `.signature (.row 0 (.templateNotAdmissible "request"))`; `decide +kernel`), `not_lawful` stays, and each old acceptance is a red control under `#guard_msgs (error)`; the green controls admit clause 1's program once the application declares the key's carrier (`admitted_served`) and type a read of the declared service at its carrier (`admitted_reads_declared`, against `refused_reads_undeclared`) | decisions row 21's slice, step 2 (`docs/research/2026-10-04-claude-lead/sigapp-slice-plan.md`): program admission runs the signature's located refusal (`admitSig`, `src/Effect4/Program/SigApp.lean`) at `AdmittedProgram program app`, whose certificate holds `admitSig app = .ok ()`; the bridge `lawfulSig_of_admitted` is `admitSig_ok_iff` read off that field, and the premise `AdmissionGap` is deleted |