Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -88,8 +88,10 @@ The graph has eleven lanes: SCM compatibility · namespace · P-derive · observ
- [ ] **InferredTree carries only derived facts: the all-derived carrier lands** — Separate source and inferred carriers so candidate-equals-source is not even well-typed as a grounding proof: every fact on the inferred carrier traces to a derivation or the node refuses. Branch/Match/Loop (the three real inference paths) migrate first; the validate_then_compile door and its lens roster stay. A well-formed node with no derived facts cannot inhabit the carrier. Why: InferredTree becomes a trustworthy proof boundary; every lens consuming it stops reading facts that were never derived; the self-host frontier stops reading greener than it is. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **Every node kind derives or refuses: the generic acceptance arm deletes** — The remaining derivation rules beyond Branch/Match/Loop: each v2 node kind either derives into the inferred carrier or its acceptance is a typed compile refusal — the generic accept-anything arm deletes. Coverage is counted per kind, so the frontier shrinks to zero or to named FrontierAccepted rows each carrying a trigger. Why: The last self-certification residue: any kind without a rule is currently accepted on well-formedness alone, which is the recovered defect class in its most general form. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **Realization per target: an operation cannot compile for T without exactly one realization** — The realized carrier adds target realization: every executable operation in a program accepted for target T has exactly one compatible realization row for T, refused target-relatively otherwise. gunbc#7485 explicitly leaves this open; it consumes the primitive-identity join (realization rows are its per-target facts) and the derivation-coverage node (a realized tree is derived-then-realized, never source-then-realized). Why: The gunbc#7479 shape at its root: a costed-but-unrealized primitive currently compiles and fails at dispatch; the gate moves that to a located target-relative refusal. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: v2-node-kind-derivation-coverage, primitive-identity-join
- [ ] **Write the closing check for: One primitive identity: definition, per-target realization, and cost as three facts on one key** — One executable check states when this is done, transcribed from the node's own bar: A costed-but-unrealized primitive refuses target-relatively; a realized-but-undefined name cannot be keyed; existing corpus calls all still resolve. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **One primitive identity: definition, per-target realization, and cost as three facts on one key** — PrimitiveDefinition (invocation forms, receiver domain, parameters, result), PrimitiveRealization per target, PrimitiveCostModel — joined by one identity so a call cannot compile for target T without exactly one compatible definition and realization, and interpreter/emitter dispatch derive from realization rows instead of five independently-writable name sets (registry map, PrimitiveContract rows, algebra templates, interpreter arms, per-target templates). Why: Closes the gunbc#7479 CLASS rather than the specimen: filter_map had a cost contract, no seed method, and a green compile. Unlocks the method ambiguity wall (sameness becomes decidable) and un-narrows the method-existence wall — the measured length/count/size dispatch fork on gunbc#7484 is why per-receiver checking stalls at kernel receivers today. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **Method ambiguity refuses: more than one resolution is a located error once primitive identity defines sameness** — The method-existence wall closes cardinality zero; this closes more-than-one — two distinct primitive identities (or a primitive and a user fn) resolving for one receiver/method pair refuse with both candidates named. Gated on primitive-identity-join because ambiguity is decidable only when sameness is: the length/count/size dispatch aliases make one method look like three today (the gunbc#7484 measured fork), so an ambiguity check before the join would refuse legitimate corpus or silently pick. Why: The silent-first-hit dispatch class: today arm order decides which of two candidates runs — an unstated tiebreak the census cannot even measure until sameness is defined. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: primitive-identity-join, method-zero-resolution-general-wall
- [ ] **Write the closing check for: Interpreter primitive roster: the fifth surface becomes readable from .dag** — One executable check states when this is done, transcribed from the node's own bar: A new dispatch arm without a roster row refuses; a roster row without a matching arm refuses; fold_list via eval_call intercept and lookup dual-realization join through derived census. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **Interpreter primitive roster: the fifth surface becomes readable from .dag** — Land interpreter-primitive-roster across all six v1_interpreter dispatch sites (eval_builtin_inner, eval_algebra_method_inner, eval_call, try_v2_std_collection_map_primitive_grounding, try_parse_table_memo_dispatch, eval_method_call lookup short-circuit — 158 arms / 169 spellings). clever-crab-111 macro authority: eval_builtin_inner arms expand from interpreter_free_call_arm_spellings with construction wall (arm without roster entry unwritable). primitive_surface_census_derived absorbs InterpreterDispatch instead of primitive_interpreter_dispatch_measurement_rows. Prerequisite for primitive-identity-join terminal acceptance. Why: Closes the fifth blind spot in D1 mutation control across all six dispatch sites. Dissolves MeasurementOnly specimen rows into derived surfaces. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **One primitive identity: definition, per-target realization, and cost as three facts on one key** — PrimitiveDefinition (identity + PrimitiveSemanticContract), PrimitiveInvocationSurface, PrimitiveRealization per RealizationTarget, PrimitiveCostFact, and PrimitiveTraversalOrderFact — five separate carriers joined by PrimitiveIdentity, never one mega-row. TERMINAL acceptance: every primitive-bearing surface across all five authorities (registry, PrimitiveContract rows, algebra templates, interpreter dispatch, emit handlers) joins exactly one identity; population-wide join and realization refusals are the closing contract. D0 is a first slice only — not the closing contract. Namespace supplies declaration identity; this node supplies semantic primitive identity across invocation and realization. Why: Proves the determinism denominator is open (#7532 honest rung) and begins closing it: four surfaces feed primitive_surface_census_derived at runtime; mutation control is CLOSED on AlgebraTemplate and EmitHandler, PARTIAL on BuiltinRegistry and PrimitiveContractRow (parallel hand rosters — primitive_d0_derived_surface_drift_audit_note), NOT DISCOVERED on InterpreterDispatch. fold_list spelling fork and index_by registry+algebra dual absence are named specimens proving the denominator is not closed. Unlocks method ambiguity wall and D1 determinism consumption through PrimitiveIdentity rather than raw symbol. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **Method ambiguity refuses: more than one resolution is a located error once primitive identity defines sameness** — The method-existence wall closes cardinality zero; this closes more-than-one — two distinct primitive identities (or a primitive and a user fn) resolving for one receiver/method pair refuse with both candidates named. Gated on primitive-identity-join because ambiguity is decidable only when sameness is: the length/count/size dispatch aliases make one method look like three today (the gunbc#7484 measured fork), so an ambiguity check before the join would refuse legitimate corpus or silently pick. Why: The silent-first-hit dispatch class: today arm order decides which of two candidates runs — an unstated tiebreak the census cannot even measure until sameness is defined. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: primitive-identity-join, method-zero-resolution-general-wall
- [ ] **Determinism denominator closure: every primitive carries one traversal-order classification** — v2.std.determinism and v2.lens.determinism consume std.primitive_identity: every PrimitiveDefinition carries exactly one PrimitiveTraversalOrderFact, unclassified refuses, HostUnspecifiedOrder derives a determinism root, aliases resolve through PrimitiveIdentity not raw symbol. Adding a new invokable primitive realization without a traversal-order fact reds before any caller uses it. Why: Dissolves the interim two-root registry (#7532) into a closed denominator — the gate can tell an alias from a distinct operation, and keys/values false-positive class is eliminated by identity not spelling. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **Write the closing check for: The capability audit: sole_constructor completeness, then seal the proof-carriers** — One executable check states when this is done, transcribed from the node's own bar: Refined authored outside the sealing module refuses at compile in every probed form; refine remains the only inhabitation path; a probe form that does NOT refuse is a counted audit finding, never silently absorbed. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
- [ ] **The capability audit: sole_constructor completeness, then seal the proof-carriers** — The language ALREADY has a construction wall: sole_constructor rejects cross-module construction with SoleConstructorViolation and carries a sealed-record specimen (post-merge review of gunbc#7486 refuted this node's earlier premise that no private/sealed/opaque capability exists). What is UNVERIFIED is its completeness: generic carriers (does type Refined<B> sole_constructor hold across instantiation?), every construction form (literals, casts like as TransportScript, coproduct variants, default values), and behavior under module_skips_direct_call_arg_check. Audit by falsification first; extend sole_constructor or ground the reference-grant algebra (the parked visibility-grants design) only where the audit reds. Why: Every capability-kind ceiling resolves together — either sole_constructor suffices (cheap: seal Refined, delete the stub-pack forge arm) or its named gaps price the visibility-grants work honestly instead of by assumption. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
2 changes: 2 additions & 0 deletions dag/gunbc/publication_grant.dag
Original file line number Diff line number Diff line change
Expand Up @@ -76,11 +76,13 @@ data public_file_publish_grants: List<PublicFilePublishGrant> = [
public_file_publish_grant(path: "dag/gunbc/publication_grant.dag"),
public_file_publish_grant(path: "dag/gunbc/roadmap_presentation.dag"),
public_file_publish_grant(path: "dag/gunbc/source_integration_proof_kernel.dag"),
public_file_publish_grant(path: "dag/std/primitive_identity.dag"),
public_file_publish_grant(path: "dag/test/claim/acquisition_mechanism_witness_test.dag"),
public_file_publish_grant(path: "dag/test/claim/advertising_interface_witness_test.dag"),
public_file_publish_grant(path: "dag/test/claim/crm_stage_vocabulary_witness_test.dag"),
public_file_publish_grant(path: "dag/test/claim/heal_revalidation_integration_witness_test.dag"),
public_file_publish_grant(path: "dag/test/claim/heal_revalidation_witness_test.dag"),
public_file_publish_grant(path: "dag/test/claim/primitive_identity_join_witness_test.dag"),
public_file_publish_grant(path: "dag/test/claim/roadmap_presentation_witness_test.dag"),
public_file_publish_grant(path: "dag/test/claim/source_integration_proof_kernel_acceptance_test.dag"),
public_file_publish_grant(path: "dag/test/claim/source_integration_proof_kernel_model_witness_test.dag"),
Expand Down
Loading
Loading