From 9a16b979f83b6bc8390d3fb90b3e88902176f89b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 02:06:26 +0000 Subject: [PATCH 1/3] WIP: dependency fidelity --- docs/plans/dependency-fidelity-design.md | 2 +- docs/plans/enforcement-intent-design.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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) From 8a0222b0480eff852bc5a867f4fb145a67812142 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 02:19:51 +0000 Subject: [PATCH 2/3] WIP: dependency fidelity --- src/v2/lens/dependency_fidelity.dag | 56 ++++++++++++++++++++++++ src/v2/lens/dependency_fidelity_test.dag | 29 ++++++++++++ 2 files changed, 85 insertions(+) create mode 100644 src/v2/lens/dependency_fidelity.dag create mode 100644 src/v2/lens/dependency_fidelity_test.dag diff --git a/src/v2/lens/dependency_fidelity.dag b/src/v2/lens/dependency_fidelity.dag new file mode 100644 index 00000000000..4e0dc91da97 --- /dev/null +++ b/src/v2/lens/dependency_fidelity.dag @@ -0,0 +1,56 @@ +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 three-surface fidelity verdict (§3); each arm reports its located discrepancies into ONE verdict lattice. 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 FidelitySurface + = InputReachability + | OutputReachability + | InteractionFidelity + +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)) +} From b32bafe293173fd11bf5342a161dde9fba4c9a65 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 02:29:40 +0000 Subject: [PATCH 3/3] dependency-fidelity: delete unused FidelitySurface enum (review #6567) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reviewer (claude-opus-4-7 APPROVE) flagged FidelitySurface as declared with no producer/consumer — speculative dead scaffold (DESIGN §5 wall-now / §2 don't grow concepts ahead of a consumer). The §3 surface is already implicit in the FidelityDiscrepancy variant (input/output/interaction), and the design doc holds the three-surface concept, so the enum earned no place yet. Reintroduce with a consumer when the output-reachability / interaction arms land. Witnesses still green (clean_input_surface_is_faithful, one_unused_param_flips_to_discrepant). Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v2/lens/dependency_fidelity.dag | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/v2/lens/dependency_fidelity.dag b/src/v2/lens/dependency_fidelity.dag index 4e0dc91da97..449ebe56d6f 100644 --- a/src/v2/lens/dependency_fidelity.dag +++ b/src/v2/lens/dependency_fidelity.dag @@ -9,12 +9,7 @@ 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 three-surface fidelity verdict (§3); each arm reports its located discrepancies into ONE verdict lattice. 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 FidelitySurface - = InputReachability - | OutputReachability - | InteractionFidelity +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 }