test(self-host): Wave 1 gate 1 general body producer verification witnesses

src/v2/test/claim/body_lowering/wave1_gate1_normalize_add_helpers.dag

@@ -0,0 +1,108 @@
+module v2.test.claim.body_lowering.wave1_gate1_normalize_add_helpers
+
+import v2.compiler.normalize { normalize }
+import v2.compiler.parse { parse_module }
+import v2.compiler.resolve { resolve }
+import v2.compiler.tokenize { tokenize }
+import v2.extdeps.languages.dag { dag_language_model }
+import v2.std.collection { Absent, Optional, Present }
+import v2.std.diagnostic { Accepted, Rejected }
+import v2.std.logic { Bool }
+import v2.std.node {
+  Arrow,
+  ComputationNode,
+  Node,
+  Transform,
+  TypeNode,
+  well_formed
+}
+import v2.std.node_query { find_arrow_body_child }
+
+data wave1_gate1_add_module_source: String = "module add_probe\n\nfn add(x: Int, y: Int) -> Int { x + y }\n"
+
+fn wave1_gate1_find_arrow_in_module(root: Node) -> Optional<Node> {
+  match root.kind {
+    TypeNode { connective: Arrow } => Present { value: root }
+    _ =>
+      fold(root.children, init: Absent, f: fn(acc, e) {
+        match acc {
+          Present { value: _ } => acc
+          Absent => wave1_gate1_find_arrow_in_module(root: e.target)
+        }
+      })
+  }
+}
+
+fn wave1_gate1_normalized_add_module() -> Optional<Node> {
+  let lm = dag_language_model()
+  match tokenize(
+    text: wave1_gate1_add_module_source,
+    file: ^wave1_gate1_add_probe_file,
+    rules: lm.lex
+  ) {
+    Rejected { diagnostics: _ } => Absent
+    Accepted { value: ts, diagnostics: _ } =>
+      match parse_module(tokens: ts, grammar: lm.grammar) {
+        Rejected { diagnostics: _ } => Absent
+        Accepted { value: artifact, diagnostics: _ } =>
+          match normalize(parse_tree: artifact.tree) {
+            Rejected { diagnostics: _ } => Absent
+            Accepted { value: tree, diagnostics: _ } => Present { value: tree }
+          }
+      }
+  }
+}
+
+fn wave1_gate1_normalized_add_resolves_holds() -> Bool {
+  match wave1_gate1_normalized_add_module() {
+    Absent => false
+    Present { value: tree } =>
+      match resolve(tree: tree, lm: dag_language_model()) {
+        Accepted { value: _, diagnostics: _ } => true
+        Rejected { diagnostics: _ } => false
+      }
+  }
+}
+
+fn wave1_gate1_normalized_add_yields_arrow_transform_holds() -> Bool {
+  match wave1_gate1_normalized_add_module() {
+    Absent => false
+    Present { value: tree } =>
+      match wave1_gate1_find_arrow_in_module(root: tree) {
+        Absent => false
+        Present { value: arrow } =>
+          well_formed(n: arrow)
+            && match find_arrow_body_child(root: arrow) {
+              Accepted { value: body, diagnostics: _ } =>
+                match body.kind {
+                  ComputationNode { behavior: Transform } => true
+                  _ => false
+                }
+              Rejected { diagnostics: _ } => false
+            }
+      }
+  }
+}
+
+fn wave1_gate1_resolved_add_arrow_transform_holds() -> Bool {
+  match wave1_gate1_normalized_add_module() {
+    Absent => false
+    Present { value: tree } =>
+      match resolve(tree: tree, lm: dag_language_model()) {
+        Accepted { value: resolved, diagnostics: _ } =>
+          match wave1_gate1_find_arrow_in_module(root: resolved) {
+            Present { value: arrow } =>
+              match find_arrow_body_child(root: arrow) {
+                Accepted { value: body, diagnostics: _ } =>
+                  match body.kind {
+                    ComputationNode { behavior: Transform } => true
+                    _ => false
+                  }
+                Rejected { diagnostics: _ } => false
+              }
+            Absent => false
+          }
+        Rejected { diagnostics: _ } => false
+      }
+  }
+}

src/v2/test/claim/long/wave1_gate1_general_body_producer_witness_test.dag

@@ -0,0 +1,37 @@
+module v2.test.long.wave1_gate1_general_body_producer_witness
+
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import v2.std.logic { Bool }
+import v2.test.claim.body_lowering.wave1_gate1_normalize_add_helpers {
+  wave1_gate1_normalized_add_resolves_holds,
+  wave1_gate1_normalized_add_yields_arrow_transform_holds,
+  wave1_gate1_resolved_add_arrow_transform_holds
+}
+import v2.test.execution.emit_host_classical_not_ingested_equals_eval {
+  ingested_classical_not_arrow_has_match_holds,
+  ingested_classical_not_resolves_holds
+}
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+data wave1_gate1_long_witness_note: String = "Wave 1 exit gate 1 execution witnesses (long lane): full tokenize→parse_module→normalize→resolve ingest paths exceed the per-PR 5s fast-lane eval budget (gunbc_ci_fast_lane_rule_note). Proven here by execution: add fn_decl lowers to Arrow+Transform; classical_not lowers to Arrow+Match — without the fixture-bound MVP producer bridge. Fast compile-gate import closure lives in self_host/wave1_gate1_general_body_producer_witness_test.dag. Local recipe: claim_batch --source-root src/v2 --source-root dag --entry src/v2/test/claim/long/wave1_gate1_general_body_producer_witness_test.dag --function <name>."
+
+test fn wave1_gate1_ingested_add_normalize_yields_arrow_transform_holds() -> Bool {
+  wave1_gate1_normalized_add_yields_arrow_transform_holds()
+}
+
+test fn wave1_gate1_ingested_add_normalize_resolves_holds() -> Bool {
+  wave1_gate1_normalized_add_resolves_holds()
+}
+
+test fn wave1_gate1_ingested_add_resolved_arrow_transform_holds() -> Bool {
+  wave1_gate1_resolved_add_arrow_transform_holds()
+}
+
+test fn wave1_gate1_ingested_match_normalize_yields_match_holds() -> Bool {
+  ingested_classical_not_arrow_has_match_holds()
+}
+
+test fn wave1_gate1_ingested_match_resolves_holds() -> Bool {
+  ingested_classical_not_resolves_holds()
+}

src/v2/test/claim/self_host/wave1_gate1_general_body_producer_witness_test.dag

@@ -0,0 +1,26 @@
+module v2.test.claim.self_host.wave1_gate1_general_body_producer_witness
+
+import v2.compiler.body_producer {
+  body_producer_pick_kw_false,
+  body_producer_pick_kw_true
+}
+import v2.compiler.compile { always_required_lenses }
+import v2.compiler.self_host.frontier {
+  compiler_frontier_row_03_body_producer,
+  compiler_frontier_row_03_normalize
+}
+import v2.std.algebra { length }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+import v2.std.logic { Bool }
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+data wave1_gate1_witness_note: String = "Wave 1 exit gate 1 fast-lane witness (compile-gate + roster): import-closure resolution of 03_body_producer and 03_normalize. Full ingest execution proofs (add Transform, classical_not Match via tokenize→parse_module→normalize) live in long/wave1_gate1_general_body_producer_witness_test.dag — those witnesses exceed the 5s per-PR discovery budget. Not proven here: Stage D MVP producer subsumption, FLAG D binding-key re-grounding, frontier probe per-module receipts, or FLAG E dissolution of body_lowering_fold.dag."
+
+test fn wave1_gate1_body_producer_modules_import_resolve_holds() -> Bool {
+  (length(xs: always_required_lenses()) == 2)
+    && (body_producer_pick_kw_true == ^dag_token_kw_true)
+    && (body_producer_pick_kw_false == ^dag_token_kw_false)
+    && (compiler_frontier_row_03_body_producer.module_path == "src/v2/compiler/03_body_producer.dag")
+    && (compiler_frontier_row_03_normalize.module_path == "src/v2/compiler/03_normalize.dag")
+}