diff --git a/docs/plans/dependency-fidelity-design.md b/docs/plans/dependency-fidelity-design.md index 62c5f2e35c0..e33abbddb26 100644 --- a/docs/plans/dependency-fidelity-design.md +++ b/docs/plans/dependency-fidelity-design.md @@ -1,6 +1,6 @@ # Dependency-Fidelity — making "CI green" mean *declared ≡ witnessed* -Status: design draft (operator-directed, 2026-07-14). Companion to the *enforcement-intent* thread (the same "ask once, compile forever" spine, made quantitative). Reasoned serially per DESIGN.md; each section is a consequence of the ones before it. +Status: design draft (operator-directed, 2026-07-14). Companion to the [*enforcement-intent* thread](enforcement-intent-design.md) (the same "ask once, compile forever" spine, made quantitative). Reasoned serially per DESIGN.md; each section is a consequence of the ones before it. --- diff --git a/docs/plans/enforcement-intent-design.md b/docs/plans/enforcement-intent-design.md index 0c9ca0904d5..936bb5466c4 100644 --- a/docs/plans/enforcement-intent-design.md +++ b/docs/plans/enforcement-intent-design.md @@ -1,6 +1,6 @@ # Enforcement intent — ask once, compile forever -*Status: draft for operator review (2026-07-02). Extends the standing threads "model §1's axioms + enforce the syllogism" and the intent-linearity draft; does not supersede either.* +*Status: draft for operator review (2026-07-02). Extends the standing threads "model §1's axioms + enforce the syllogism" and the intent-linearity draft; does not supersede either. Quantitative companion: [dependency-fidelity design](dependency-fidelity-design.md) — the same "ask once, compile forever" spine turned into a measured coverage law (CI-green ⟺ declared ≡ witnessed across an affected-set-scoped, mutation-adequate coverage set).* ## 1. The displaced cost (why this is on-dial) diff --git a/src/v2/lens/dependency_fidelity.dag b/src/v2/lens/dependency_fidelity.dag new file mode 100644 index 00000000000..449ebe56d6f --- /dev/null +++ b/src/v2/lens/dependency_fidelity.dag @@ -0,0 +1,51 @@ +module v2.lens.dependency_fidelity + +import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding } +import std.disposition { SingleAuthority } +import std.algebra { Empty } +import v2.std.algebra { is_empty, list_snoc_item } +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.node { Node, Symbol } +import v2.lens.unused_parameters { UnusedParameterFact, UnusedParametersFact } + +data law_note: String = "dependency-fidelity §2: correctness = declared dependency structure equals witnessed (by-execution) structure. This module is the single authority for the fidelity verdict; each arm reports its located discrepancies into ONE verdict lattice, and the FidelityDiscrepancy variant IS the §3 surface it lives on (UnreachedDeclaredInput = input-reachability, UnreachedDeclaredOutput = output-reachability, UnderClaimedEdge/OverClaimedCoupling = interaction fidelity). Input-reachability is consumed from v2.lens.unused_parameters (no re-mint, §3 single authority). Output-reachability and the under-claim/over-claim edge arms are staged slots (docs/plans/dependency-fidelity-design.md §5, §8)." + +type FidelityDiscrepancy + = UnreachedDeclaredInput { declaration: Node } + | UnreachedDeclaredOutput { arm: Symbol } + | UnderClaimedEdge { source: Node, dependent: Node } + | OverClaimedCoupling { left: Node, right: Node } + +type FidelityVerdict + = Faithful + | Discrepant { findings: List } + +fn verdict_from_discrepancies(findings: List) -> FidelityVerdict { + if is_empty(xs: findings) { + Faithful + } else { + Discrepant { findings: findings } + } +} + +fn verdict_is_faithful(v: FidelityVerdict) -> Bool { + match v { + Faithful => true + Discrepant { findings: _ } => false + } +} + +fn input_reachability_discrepancies(fact: UnusedParametersFact) -> List { + fold(fact.unused, init: Empty, f: fn(acc, u) { + list_snoc_item(xs: acc, item: UnreachedDeclaredInput { declaration: u.declaration }) + }) +} + +fn input_reachability_verdict(fact: UnusedParametersFact) -> FidelityVerdict { + verdict_from_discrepancies(findings: input_reachability_discrepancies(fact: fact)) +} + +data construction_justification: ConstructionJustification = ConstructionJustification { + class: WallAfterGrounding { dissolves_to: SingleAuthority } +} diff --git a/src/v2/lens/dependency_fidelity_test.dag b/src/v2/lens/dependency_fidelity_test.dag new file mode 100644 index 00000000000..61030b36bbf --- /dev/null +++ b/src/v2/lens/dependency_fidelity_test.dag @@ -0,0 +1,29 @@ +module v2.test.lens_dependency_fidelity.dependency_fidelity_test + +import v2.std.logic { Bool } +import std.algebra { Empty } +import v2.std.algebra { list_snoc_item } +import v2.std.node { Node, node_synthetic, TypeNode, Atom } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.lens.unused_parameters { UnusedParameterFact, UnusedParametersFact } +import v2.lens.dependency_fidelity { + input_reachability_verdict, + verdict_is_faithful +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn a_synthetic_param() -> Node { + node_synthetic(kind: TypeNode { connective: Atom { identity: ^p } }, children: Empty) +} + +test fn clean_input_surface_is_faithful() -> Bool { + return verdict_is_faithful(v: input_reachability_verdict(fact: UnusedParametersFact { unused: Empty })) +} + +test fn one_unused_param_flips_to_discrepant() -> Bool { + let fact = UnusedParametersFact { + unused: list_snoc_item(xs: Empty, item: UnusedParameterFact { declaration: a_synthetic_param() }) + } + return !verdict_is_faithful(v: input_reachability_verdict(fact: fact)) +}