Semantics evidence
Effect4 makes 216 claims about Effect's runtime: 198 proved, 12 modulo, 1 goal, 1 refuted, 3 absent, 1 assumed.
A claim's evidence comes from its Lean declaration and is never written by hand (decisions row 203). The open work lists the planned goals that the remaining claims rest on, and why each waits.
Every witness uses no axiom beyond propext and Quot., or the page is not written. That ceiling covers the evidence shown here, not the whole library. A claim's English is written by hand. A placement that a declaration inherits from its module is provisional.
A register record links a claim to a historical attack. Read the whole row: an early status word may stand beside a later repair.
How to read a statusstatuses
- proved: a theorem whose proof rests on no planned goal.
- modulo: a theorem proved from planned goals; it names the goals it rests on.
- goal: a planned goal (
proof_goal), a statement whose proof is stillsorry; a claim whose statement is one. - open: a requirement with a node not yet proved, or a part not yet stated as a goal.
- refuted: a register record refutes the claim with a theorem.
- absent: no declaration states the claim yet; its row gives the reason.
- assumed: the claim is taken from an outside source, with its reason.
- missing: in the plan, a name that no node holds.
- Open work: 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.
- Store Typing: World-indexed semantic value membership (Fits) and store typings. 21 claims: 20 proved, 1 absent.
- Residual Program Typing: TypedProg, the protocol-indexed judgment on residual programs. 20 claims: 19 proved, 1 refuted.
- Scope Lifetime & Finalization: Lifetimes, finalizer registration, and LIFO unwinding. 16 claims: 15 proved, 1 goal.
- Reactive Scheduling: Multi-fiber execution, decision steps, and configuration invariants. 25 claims: 19 proved, 4 modulo, 2 absent.
- Exact Codecs: Invertible embeddings for JSON and Schema representations. 19 claims: 19 proved.
- Subtyping Algebra: Preorder laws, normalization, and join-semilattice on CTy. 13 claims: 13 proved.
- Initial Algebras & Folds: Free syntax objects, catamorphisms, and fold uniqueness. 33 claims: 33 proved.
- Context Requirements: Graded coeffects, requirement rows, and layer discharge. 8 claims: 8 proved.
- Host Session Protocol: Session automaton, external reply ingestion, and boundary capabilities. 12 claims: 11 proved, 1 assumed.
- Translation & Simulation: Semantic preservation, replay relations, and capstone M7. 49 claims: 41 proved, 8 modulo.
- Applicability decisions
- Placement: theorems of the registry's concept-named modules; auxiliary names and planned goals excluded
- Plan: The requirements and their nodes. A node is a planned goal (a theorem whose body is
sorry, declared byproof_goal) or a theorem a requirement names. Its status is derived from its proof, with goals as leaves (tools/ProofGraph/Plan., decisions row 203). The status is goal, modulo (proved from the goals it rests on), or proved. An edge goes from a node to the nodes its proof reaches first.lean - Acceptance programs: The rc.112 probe programs as acceptance tests (decisions row 206;
Test/Dogfood/README.). Each row is themd stageits battery declares, which a guard ties to the battery's own measurement, and the requirements itwaitsOn. A slice that moves a program edits both.