From ff78d3e8adf001959614b90e6412a9a57a46985b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 30 Jun 2026 22:31:39 +0000 Subject: [PATCH] lens: add Witness API + perturb-RED witness for medium_structure_containment MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Gate PR-A step 1 only: execution-proven Holds→Violates flip on canonical scan roots via medium_structure_containment_witness fed by live medium_structure_leak_facts read-back. medium_structure_project.rs retirement (HAND[] delete) deferred per loyal-bee MIXED split — separate from this diff. Co-authored-by: Cursor --- src/v2/lens/medium_structure_containment.dag | 50 +++++++++++++++++++ .../scanner/perturb_red_test.dag | 42 ++++++++++++++++ .../perturb_red/plant.dag | 12 +++++ 3 files changed, 104 insertions(+) create mode 100644 src/v2/test/claim/medium_structure_containment/scanner/perturb_red_test.dag create mode 100644 src/v2/test/fixture/medium_structure_scan/perturb_red/plant.dag diff --git a/src/v2/lens/medium_structure_containment.dag b/src/v2/lens/medium_structure_containment.dag index ca4f6e0a95a..3aca6f167b8 100644 --- a/src/v2/lens/medium_structure_containment.dag +++ b/src/v2/lens/medium_structure_containment.dag @@ -11,8 +11,16 @@ import v2.std.algebra { list_snoc_item } import v2.std.collection { List } +import v2.std.diagnostic { + AmbiguousIntent, + Diagnostic, + Textual, + Unavailable, + WholeFile +} import v2.std.logic { Bool } import v2.std.text { Char, String } +import v2.std.witness { Holds, Violates, Witness } type MediumLeakFace = InlineSyntaxLiteral @@ -273,6 +281,48 @@ fn medium_structure_containment_clean_live( ) } +fn medium_structure_containment_witness_diagnostic() -> Diagnostic { + Diagnostic { + reason: ^medium_structure_containment_leak_detected, + at: Textual { file: ^medium_structure_containment_lens_file, extent: WholeFile }, + correction: Unavailable { reason: AmbiguousIntent } + } +} + +fn medium_structure_containment_witness( + emit_roots: List, + check_roots: List +) -> Witness { + if medium_structure_containment_clean_live( + emit_roots: emit_roots, + check_roots: check_roots + ) { + Holds { value: true } + } else { + Violates { diagnostic: medium_structure_containment_witness_diagnostic() } + } +} + +fn medium_structure_containment_canonical_witness() -> Witness { + medium_structure_containment_witness( + emit_roots: medium_emit_side_scan_roots, + check_roots: medium_check_side_scan_roots + ) +} + +fn medium_structure_check_roots_with_perturb(perturb_roots: List) -> List { + list_append(left: medium_check_side_scan_roots, right: perturb_roots) +} + +fn medium_structure_containment_canonical_with_check_perturb_witness( + perturb_roots: List +) -> Witness { + medium_structure_containment_witness( + emit_roots: medium_emit_side_scan_roots, + check_roots: medium_structure_check_roots_with_perturb(perturb_roots: perturb_roots) + ) +} + data construction_justification: ConstructionJustification = ConstructionJustification { class: WallAfterGrounding { dissolves_to: RealizationDispatch } } diff --git a/src/v2/test/claim/medium_structure_containment/scanner/perturb_red_test.dag b/src/v2/test/claim/medium_structure_containment/scanner/perturb_red_test.dag new file mode 100644 index 00000000000..d7b34ad2179 --- /dev/null +++ b/src/v2/test/claim/medium_structure_containment/scanner/perturb_red_test.dag @@ -0,0 +1,42 @@ +module v2.test.medium_structure_containment.scanner.perturb_red + +import v2.lens.medium_structure_containment { + medium_structure_containment_canonical_witness, + medium_structure_containment_canonical_with_check_perturb_witness, + medium_structure_leak_count_live, + medium_emit_side_scan_roots, + medium_structure_check_roots_with_perturb +} +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.text { String } +import v2.std.witness { Holds, Violates } + +data perturb_red_scan_roots: List = [ + "src/v2/test/fixture/medium_structure_scan/perturb_red" +] + +test fn medium_structure_canonical_read_back_holds() -> Bool { + match medium_structure_containment_canonical_witness() { + Holds { value: _ } => true + Violates { diagnostic: _ } => false + } +} + +test fn medium_structure_canonical_perturb_flips_violates() -> Bool { + match medium_structure_containment_canonical_with_check_perturb_witness( + perturb_roots: perturb_red_scan_roots + ) { + Holds { value: _ } => false + Violates { diagnostic: _ } => true + } +} + +test fn medium_structure_perturb_red_leak_count_positive() -> Bool { + medium_structure_leak_count_live( + emit_roots: medium_emit_side_scan_roots, + check_roots: medium_structure_check_roots_with_perturb( + perturb_roots: perturb_red_scan_roots + ) + ) > 0 +} diff --git a/src/v2/test/fixture/medium_structure_scan/perturb_red/plant.dag b/src/v2/test/fixture/medium_structure_scan/perturb_red/plant.dag new file mode 100644 index 00000000000..c96af8a60b2 --- /dev/null +++ b/src/v2/test/fixture/medium_structure_scan/perturb_red/plant.dag @@ -0,0 +1,12 @@ +module v2.test.fixture.medium_structure_scan.perturb_red_plant +import v2.std.logic { Bool } +import v2.std.text { String } + +fn expected_ci_yml() -> String { + "runs-on: linux\n" +} + +fn perturb_red_check_side_leak() -> Bool { + let yaml = expected_ci_yml() + string_contains(s: yaml, pattern: "runs-on") +}