From 533d92bdf4e27814a415f9df9020f0115d96efcf Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 20 Jul 2026 05:12:55 +0000 Subject: [PATCH 1/3] WIP: ci_floor_cutover OVERLAP-START: build + execute the PROACTIVE VERIFICATI --- dag/gunbc/proactive_verification_ledger.dag | 260 ++++++++++++++++++ ...roactive_verification_ledger_transport.dag | 50 ++++ ...ctive_verification_ledger_witness_test.dag | 38 +++ 3 files changed, 348 insertions(+) create mode 100644 dag/gunbc/proactive_verification_ledger.dag create mode 100644 dag/tools/proactive_verification_ledger_transport.dag create mode 100644 src/v2/test/claim/proactive_verification_ledger_witness_test.dag diff --git a/dag/gunbc/proactive_verification_ledger.dag b/dag/gunbc/proactive_verification_ledger.dag new file mode 100644 index 00000000000..cd8ea5f0569 --- /dev/null +++ b/dag/gunbc/proactive_verification_ledger.dag @@ -0,0 +1,260 @@ +module gunbc.proactive_verification_ledger + +import std.types { String, Int, List } +import v2.std.node { Symbol } +import v2.std.algebra { filter, fold_list, length } + +data proactive_verification_ledger_law: String = "The PROACTIVE VERIFICATION LEDGER (operator no-soak ruling 2026-07-20; v1_deletion_plan ^v1_delete): enumerated executed receipts that gate v1_delete — never calendar soak, never elapsed-time claims. Each row is ONE deliberate run with a typed execution shape and an honest overlap disposition (ExecutableNow | KnownRedPendingUnquarantine | BlockedOnCiFloorCutover). Green-by-execution means every row ran and passed; a pending row is counted, not absorbed. Spine receipts (whole-corpus cold v1-vs-v2 witness parity, compile-clean parity, regen behavioral fixed point) plus one row per emit_host family equals_eval agreement witness. Dissolve-on: ci_floor_cutover routes native + the ledger is all ExecutableNow green — then v1_quarantine may proceed." + +type VerificationReceiptKind + = WholeCorpusWitnessParityCold + | CompileCleanParity + | RegenBehavioralFixedPoint + | FamilyEqualsEval + +type VerificationExecutionShape + = ClaimWitness { entry: String, function: String } + | FalsifierPredictOnlyBatch + | CompileCleanGate + | RegenVerifyGate + +type VerificationDisposition + = ExecutableNow + | KnownRedPendingUnquarantine + | BlockedOnCiFloorCutover + +type VerificationLedgerRow { + id: Symbol, + kind: VerificationReceiptKind, + title: String, + execution: VerificationExecutionShape, + disposition: VerificationDisposition, + dissolve_trigger: String +} + +data spine_witness_parity_recipe: String = "claim_executor --source-root dag --source-root src/v2 --plan-entry src/v2/workflow/ci_floor_plan.dag --plan-function gunbc_falsifier_batches --batch-index 0 (SelectionPredictOnly whole-corpus cold affected-set falsifier; zero unexplained divergence vs predict-only expectations)" + +data spine_compile_clean_recipe: String = "claim_executor batch-1 dag_compile_clean_gate (--target dag whole-tree; same authority as gunbc_ci_floor_batches)" + +data spine_regen_recipe: String = "regen_stage0 --emit-fresh target/v2-emit-fresh-realize --write-manifest target/v2-emit-fresh-realize/roster_manifest.txt --verify (RegenVerifyGate transport)" + +data proactive_verification_spine_rows: List = [ + VerificationLedgerRow { + id: ^whole_corpus_witness_parity_cold, + kind: WholeCorpusWitnessParityCold, + title: "Whole-corpus cold v1-vs-v2 witness parity (falsifier predict-only batch; zero unexplained divergence)", + execution: FalsifierPredictOnlyBatch, + disposition: BlockedOnCiFloorCutover, + dissolve_trigger: "ci_floor_cutover lands native routing; falsifier cold sweep records zero divergence rows" + }, + VerificationLedgerRow { + id: ^compile_clean_parity, + kind: CompileCleanParity, + title: "Compile-clean parity (whole-tree --target dag gate)", + execution: CompileCleanGate, + disposition: BlockedOnCiFloorCutover, + dissolve_trigger: "ci_floor_cutover; whole-tree compile-clean gate green on v2-emitted execution path" + }, + VerificationLedgerRow { + id: ^regen_behavioral_fixed_point, + kind: RegenBehavioralFixedPoint, + title: "Regen behavioral fixed point (regen_stage0 --verify two-generation equivalence)", + execution: RegenVerifyGate, + disposition: BlockedOnCiFloorCutover, + dissolve_trigger: "emitter_fixed_point + ci_floor_cutover; regen_verify gate green by execution" + } +] + +data proactive_verification_family_rows: List = [ + VerificationLedgerRow { + id: ^family_equals_add, + kind: FamilyEqualsEval, + title: "emit_host_add interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag", + function: "emit_host_add_equals_eval_holds" + }, + disposition: ExecutableNow, + dissolve_trigger: "ledger all-green at v1_delete" + }, + VerificationLedgerRow { + id: ^family_equals_match, + kind: FamilyEqualsEval, + title: "emit_host_match interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_match_equals_eval_test.dag", + function: "emit_host_match_equals_eval_holds" + }, + disposition: ExecutableNow, + dissolve_trigger: "ledger all-green at v1_delete" + }, + VerificationLedgerRow { + id: ^family_equals_loop, + kind: FamilyEqualsEval, + title: "emit_host_loop interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag", + function: "emit_host_loop_equals_eval_holds" + }, + disposition: ExecutableNow, + dissolve_trigger: "ledger all-green at v1_delete" + }, + VerificationLedgerRow { + id: ^family_equals_classical_not_ingested, + kind: FamilyEqualsEval, + title: "emit_host_classical_not_ingested interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_classical_not_ingested_equals_eval_test.dag", + function: "emit_host_classical_not_ingested_equals_eval_holds" + }, + disposition: ExecutableNow, + dissolve_trigger: "ledger all-green at v1_delete" + }, + VerificationLedgerRow { + id: ^family_equals_module, + kind: FamilyEqualsEval, + title: "emit_host_module interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_module_equals_eval_test.dag", + function: "emit_host_module_add_equals_eval_holds" + }, + disposition: ExecutableNow, + dissolve_trigger: "ledger all-green at v1_delete" + }, + VerificationLedgerRow { + id: ^family_equals_produced_module, + kind: FamilyEqualsEval, + title: "emit_host_produced_module interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_produced_module_equals_eval_test.dag", + function: "emit_host_produced_module_add_equals_eval_holds" + }, + disposition: ExecutableNow, + dissolve_trigger: "ledger all-green at v1_delete" + }, + VerificationLedgerRow { + id: ^family_equals_fold_closure, + kind: FamilyEqualsEval, + title: "emit_host_fold_closure interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_fold_closure_equals_eval_test.dag", + function: "emit_host_fold_closure_equals_eval_holds" + }, + disposition: KnownRedPendingUnquarantine, + dissolve_trigger: "eval gains closure-arg support; known_red_probe row deletes on green (swift-stag-662 / jolly-dove-581)" + }, + VerificationLedgerRow { + id: ^family_equals_field_access, + kind: FamilyEqualsEval, + title: "emit_host_field_access interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_field_access_equals_eval_test.dag", + function: "emit_host_field_access_equals_eval_holds" + }, + disposition: KnownRedPendingUnquarantine, + dissolve_trigger: "emit_host_field_access transport lands; known_red_probe wet rows delete (swift-stag-662)" + }, + VerificationLedgerRow { + id: ^family_equals_complement, + kind: FamilyEqualsEval, + title: "emit_host_complement interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_complement_equals_eval_test.dag", + function: "emit_host_complement_equals_eval_holds" + }, + disposition: KnownRedPendingUnquarantine, + dissolve_trigger: "emit_host_complement transport lands; known_red_probe wet rows delete (swift-stag-662)" + }, + VerificationLedgerRow { + id: ^family_equals_meet, + kind: FamilyEqualsEval, + title: "emit_host_meet interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_meet_join_equals_eval_test.dag", + function: "emit_host_meet_equals_eval_holds" + }, + disposition: KnownRedPendingUnquarantine, + dissolve_trigger: "meet_join equals_eval debt cleared (emit_host_meet_join_equals_eval_test.dag)" + }, + VerificationLedgerRow { + id: ^family_equals_join, + kind: FamilyEqualsEval, + title: "emit_host_join interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_meet_join_equals_eval_test.dag", + function: "emit_host_join_equals_eval_holds" + }, + disposition: KnownRedPendingUnquarantine, + dissolve_trigger: "meet_join equals_eval debt cleared (emit_host_meet_join_equals_eval_test.dag)" + }, + VerificationLedgerRow { + id: ^family_equals_variant_construct, + kind: FamilyEqualsEval, + title: "emit_host_variant_construct interpreted==native equals_eval", + execution: ClaimWitness { + entry: "src/v2/test/claim/execution/emit_host_variant_construct_equals_eval_test.dag", + function: "emit_host_variant_construct_equals_eval_holds" + }, + disposition: KnownRedPendingUnquarantine, + dissolve_trigger: "variant_construct equals_eval debt cleared (emit_host_variant_construct_equals_eval_test.dag)" + } +] + +fn proactive_verification_ledger_rows() -> List { + concat(proactive_verification_spine_rows, proactive_verification_family_rows) +} + +fn ledger_row_disposition_is(row: VerificationLedgerRow, d: VerificationDisposition) -> Bool { + match row.disposition { + ExecutableNow => + match d { ExecutableNow => true, KnownRedPendingUnquarantine => false, BlockedOnCiFloorCutover => false } + KnownRedPendingUnquarantine => + match d { ExecutableNow => false, KnownRedPendingUnquarantine => true, BlockedOnCiFloorCutover => false } + BlockedOnCiFloorCutover => + match d { ExecutableNow => false, KnownRedPendingUnquarantine => false, BlockedOnCiFloorCutover => true } + } +} + +fn ledger_rows_with_disposition(d: VerificationDisposition) -> List { + filter(xs: proactive_verification_ledger_rows(), predicate: fn(row) { + ledger_row_disposition_is(row: row, d: d) + }) +} + +fn ledger_spine_row_count() -> Int { + length(xs: proactive_verification_spine_rows) +} + +fn ledger_family_row_count() -> Int { + length(xs: proactive_verification_family_rows) +} + +fn ledger_total_row_count() -> Int { + length(xs: proactive_verification_ledger_rows()) +} + +fn ledger_executable_now_count() -> Int { + length(xs: ledger_rows_with_disposition(d: ExecutableNow)) +} + +fn ledger_known_red_count() -> Int { + length(xs: ledger_rows_with_disposition(d: KnownRedPendingUnquarantine)) +} + +fn ledger_blocked_count() -> Int { + length(xs: ledger_rows_with_disposition(d: BlockedOnCiFloorCutover)) +} + +fn ledger_has_spine_kind(kind: VerificationReceiptKind) -> Bool { + fold_list( + xs: proactive_verification_spine_rows, + empty: false, + cons: fn(acc, row) { acc || (row.kind == kind) } + ) +} + +fn ledger_all_spine_kinds_present() -> Bool { + ledger_has_spine_kind(kind: WholeCorpusWitnessParityCold) + && ledger_has_spine_kind(kind: CompileCleanParity) + && ledger_has_spine_kind(kind: RegenBehavioralFixedPoint) +} diff --git a/dag/tools/proactive_verification_ledger_transport.dag b/dag/tools/proactive_verification_ledger_transport.dag new file mode 100644 index 00000000000..39b13706559 --- /dev/null +++ b/dag/tools/proactive_verification_ledger_transport.dag @@ -0,0 +1,50 @@ +module tools.proactive_verification_ledger_transport + +import gunbc.ci_layer_roots { witness_layer_roots } +import gunbc.proactive_verification_ledger { + VerificationLedgerRow, + VerificationExecutionShape, + ClaimWitness, + ExecutableNow, + ledger_rows_with_disposition +} +import tools.host_prelude { ClaimRun, run_gunbc_claims } +import tools.regen_verify_transport { run_regen_verify } +import v2.std.algebra { fold_list } +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.text { String } + +fn claim_run_from_row(row: VerificationLedgerRow) -> ClaimRun { + match row.execution { + ClaimWitness { entry: e, function: f } => + ClaimRun { entry: e, function: f } + FalsifierPredictOnlyBatch => + ClaimRun { entry: "", function: "" } + CompileCleanGate => + ClaimRun { entry: "", function: "" } + RegenVerifyGate => + ClaimRun { entry: "", function: "" } + } +} + +fn run_ledger_claim_row(row: VerificationLedgerRow) -> Bool { + match row.execution { + ClaimWitness { entry: e, function: f } => + run_gunbc_claims( + source_roots: witness_layer_roots, + claims: [ClaimRun { entry: e, function: f }] + ) + FalsifierPredictOnlyBatch => false + CompileCleanGate => false + RegenVerifyGate => run_regen_verify() + } +} + +fn run_executable_ledger_rows() -> Bool { + fold_list( + xs: ledger_rows_with_disposition(d: ExecutableNow), + empty: true, + cons: fn(acc, row) { acc && run_ledger_claim_row(row: row) } + ) +} diff --git a/src/v2/test/claim/proactive_verification_ledger_witness_test.dag b/src/v2/test/claim/proactive_verification_ledger_witness_test.dag new file mode 100644 index 00000000000..d542377a90e --- /dev/null +++ b/src/v2/test/claim/proactive_verification_ledger_witness_test.dag @@ -0,0 +1,38 @@ +module v2.test.claim.proactive_verification_ledger_witness + +import gunbc.proactive_verification_ledger { + WholeCorpusWitnessParityCold, + CompileCleanParity, + RegenBehavioralFixedPoint, + FamilyEqualsEval, + ledger_all_spine_kinds_present, + ledger_blocked_count, + ledger_executable_now_count, + ledger_family_row_count, + ledger_known_red_count, + ledger_spine_row_count, + ledger_total_row_count +} +import tools.proactive_verification_ledger_transport { run_executable_ledger_rows } +import v2.std.logic { Bool } + +data proactive_verification_ledger_witness_note: String = "OVERLAP-START receipt (sunny-lynx-241, operator no-soak 2026-07-20): the proactive verification ledger is enumerated on the carrier (dag/gunbc/proactive_verification_ledger.dag) and overlap-executable rows run green by execution. Spine rows (whole-corpus falsifier cold, compile-clean, regen fixed point) are honestly BlockedOnCiFloorCutover until that milestone lands — never calendar soak. Known-red family equals_eval rows are counted, not silently skipped. v1_delete gates on ALL rows ExecutableNow or un-quarantined green." + +test fn proactive_verification_ledger_enumeration_holds() -> Bool { + ledger_spine_row_count() == 3 + && ledger_family_row_count() == 12 + && ledger_total_row_count() == 15 + && ledger_all_spine_kinds_present() == true + && ledger_blocked_count() == 3 + && ledger_known_red_count() == 6 + && ledger_executable_now_count() == 6 +} + +test fn proactive_verification_ledger_overlap_execution_holds() -> Bool { + run_executable_ledger_rows() +} + +test fn proactive_verification_ledger_witnesses() -> Bool { + proactive_verification_ledger_enumeration_holds() + && proactive_verification_ledger_overlap_execution_holds() +} From da11d8da7a8c47f50686ea0a8a43569c9c8e9a77 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 20 Jul 2026 05:21:19 +0000 Subject: [PATCH 2/3] Model the proactive verification ledger as typed .dag rows (overlap-start). Enumerates 12 executed-receipt rows (3 spine + 9 witness-realization families) with honest disposition tracking per the operator no-soak ruling: overlap-executable family equals_eval receipts run green by execution; spine and known-red rows stay OutcomePending until ci_floor_cutover / #6912 / fold eval arc land. Co-authored-by: Cursor --- dag/gunbc/proactive_verification_ledger.dag | 114 ++++++++---------- ...roactive_verification_ledger_transport.dag | 18 +-- ...ctive_verification_ledger_witness_test.dag | 18 ++- 3 files changed, 59 insertions(+), 91 deletions(-) diff --git a/dag/gunbc/proactive_verification_ledger.dag b/dag/gunbc/proactive_verification_ledger.dag index cd8ea5f0569..fbc434f2411 100644 --- a/dag/gunbc/proactive_verification_ledger.dag +++ b/dag/gunbc/proactive_verification_ledger.dag @@ -4,7 +4,7 @@ import std.types { String, Int, List } import v2.std.node { Symbol } import v2.std.algebra { filter, fold_list, length } -data proactive_verification_ledger_law: String = "The PROACTIVE VERIFICATION LEDGER (operator no-soak ruling 2026-07-20; v1_deletion_plan ^v1_delete): enumerated executed receipts that gate v1_delete — never calendar soak, never elapsed-time claims. Each row is ONE deliberate run with a typed execution shape and an honest overlap disposition (ExecutableNow | KnownRedPendingUnquarantine | BlockedOnCiFloorCutover). Green-by-execution means every row ran and passed; a pending row is counted, not absorbed. Spine receipts (whole-corpus cold v1-vs-v2 witness parity, compile-clean parity, regen behavioral fixed point) plus one row per emit_host family equals_eval agreement witness. Dissolve-on: ci_floor_cutover routes native + the ledger is all ExecutableNow green — then v1_quarantine may proceed." +data proactive_verification_ledger_law: String = "The PROACTIVE VERIFICATION LEDGER (operator no-soak ruling 2026-07-20; v1_deletion_plan ^v1_delete): enumerated executed receipts that gate v1_delete — never calendar soak, never elapsed-time claims. Each row is ONE deliberate run with a typed execution shape, an overlap disposition (ExecutableNow | KnownRedPendingUnquarantine | BlockedOnCiFloorCutover), and an execution outcome (OutcomeGreen | OutcomePending | OutcomeRed) recorded only after a real run — never fabricated. Spine: (1) whole-corpus cold v1-vs-v2 witness parity — falsifier predict-only cadence, zero unexplained divergence (every divergence typed/located/counted, never absorbed); (2) compile-clean parity; (3) regen behavioral fixed point. Families: nine witness-realization equals_eval receipts (#6879 partition); fold_closure appends when the eval arc lands it — 8 of 9 green once #6912 merges. Dissolve-on: ci_floor_cutover + ledger all OutcomeGreen." type VerificationReceiptKind = WholeCorpusWitnessParityCold @@ -23,6 +23,11 @@ type VerificationDisposition | KnownRedPendingUnquarantine | BlockedOnCiFloorCutover +type VerificationExecutionOutcome + = OutcomeGreen + | OutcomePending { reason: String } + | OutcomeRed { reason: String } + type VerificationLedgerRow { id: Symbol, kind: VerificationReceiptKind, @@ -32,20 +37,22 @@ type VerificationLedgerRow { dissolve_trigger: String } -data spine_witness_parity_recipe: String = "claim_executor --source-root dag --source-root src/v2 --plan-entry src/v2/workflow/ci_floor_plan.dag --plan-function gunbc_falsifier_batches --batch-index 0 (SelectionPredictOnly whole-corpus cold affected-set falsifier; zero unexplained divergence vs predict-only expectations)" +data spine_witness_parity_recipe: String = "claim_executor --source-root dag --source-root src/v2 --plan-entry src/v2/workflow/ci_floor_plan.dag --plan-function gunbc_falsifier_batches (batch 0 = SelectionPredictOnly whole-corpus cold affected-set falsifier; zero unexplained divergence vs predict-only expectations — a rerun-everything arm is the absorbing-fallback hard reject)" data spine_compile_clean_recipe: String = "claim_executor batch-1 dag_compile_clean_gate (--target dag whole-tree; same authority as gunbc_ci_floor_batches)" data spine_regen_recipe: String = "regen_stage0 --emit-fresh target/v2-emit-fresh-realize --write-manifest target/v2-emit-fresh-realize/roster_manifest.txt --verify (RegenVerifyGate transport)" +data family_partition_note: String = "Nine witness-realization families (#6879 kernel partition): add (serial kernel), match+loop+fold_closure (lane 3), field_access+complement (lane 2), meet_join+variant_construct+classical_not_ingested (lane 4). Emitter clean across all nine — gaps are eval/harness-side. #6912 unblocks field_access, complement, meet_join, variant_construct equals_eval; fold_closure remains KnownRedPendingUnquarantine until closure-arg eval lands." + data proactive_verification_spine_rows: List = [ VerificationLedgerRow { id: ^whole_corpus_witness_parity_cold, kind: WholeCorpusWitnessParityCold, - title: "Whole-corpus cold v1-vs-v2 witness parity (falsifier predict-only batch; zero unexplained divergence)", + title: "Whole-corpus cold v1-vs-v2 witness parity (falsifier predict-only batch)", execution: FalsifierPredictOnlyBatch, disposition: BlockedOnCiFloorCutover, - dissolve_trigger: "ci_floor_cutover lands native routing; falsifier cold sweep records zero divergence rows" + dissolve_trigger: "ci_floor_cutover; falsifier cold sweep records zero unexplained divergence rows" }, VerificationLedgerRow { id: ^compile_clean_parity, @@ -69,10 +76,10 @@ data proactive_verification_family_rows: List = [ VerificationLedgerRow { id: ^family_equals_add, kind: FamilyEqualsEval, - title: "emit_host_add interpreted==native equals_eval", + title: "emit_host_add family equals_eval agreement", execution: ClaimWitness { entry: "src/v2/test/claim/execution/emit_host_add_equals_eval_test.dag", - function: "emit_host_add_equals_eval_holds" + function: "emit_host_add_equals_eval_all_holds" }, disposition: ExecutableNow, dissolve_trigger: "ledger all-green at v1_delete" @@ -80,10 +87,10 @@ data proactive_verification_family_rows: List = [ VerificationLedgerRow { id: ^family_equals_match, kind: FamilyEqualsEval, - title: "emit_host_match interpreted==native equals_eval", + title: "emit_host_match family equals_eval agreement", execution: ClaimWitness { entry: "src/v2/test/claim/execution/emit_host_match_equals_eval_test.dag", - function: "emit_host_match_equals_eval_holds" + function: "emit_host_match_equals_eval_all_holds" }, disposition: ExecutableNow, dissolve_trigger: "ledger all-green at v1_delete" @@ -91,10 +98,10 @@ data proactive_verification_family_rows: List = [ VerificationLedgerRow { id: ^family_equals_loop, kind: FamilyEqualsEval, - title: "emit_host_loop interpreted==native equals_eval", + title: "emit_host_loop family equals_eval agreement", execution: ClaimWitness { entry: "src/v2/test/claim/execution/emit_host_loop_equals_eval_test.dag", - function: "emit_host_loop_equals_eval_holds" + function: "emit_host_loop_equals_eval_all_holds" }, disposition: ExecutableNow, dissolve_trigger: "ledger all-green at v1_delete" @@ -102,7 +109,7 @@ data proactive_verification_family_rows: List = [ VerificationLedgerRow { id: ^family_equals_classical_not_ingested, kind: FamilyEqualsEval, - title: "emit_host_classical_not_ingested interpreted==native equals_eval", + title: "emit_host_classical_not_ingested family equals_eval agreement", execution: ClaimWitness { entry: "src/v2/test/claim/execution/emit_host_classical_not_ingested_equals_eval_test.dag", function: "emit_host_classical_not_ingested_equals_eval_holds" @@ -110,93 +117,60 @@ data proactive_verification_family_rows: List = [ disposition: ExecutableNow, dissolve_trigger: "ledger all-green at v1_delete" }, - VerificationLedgerRow { - id: ^family_equals_module, - kind: FamilyEqualsEval, - title: "emit_host_module interpreted==native equals_eval", - execution: ClaimWitness { - entry: "src/v2/test/claim/execution/emit_host_module_equals_eval_test.dag", - function: "emit_host_module_add_equals_eval_holds" - }, - disposition: ExecutableNow, - dissolve_trigger: "ledger all-green at v1_delete" - }, - VerificationLedgerRow { - id: ^family_equals_produced_module, - kind: FamilyEqualsEval, - title: "emit_host_produced_module interpreted==native equals_eval", - execution: ClaimWitness { - entry: "src/v2/test/claim/execution/emit_host_produced_module_equals_eval_test.dag", - function: "emit_host_produced_module_add_equals_eval_holds" - }, - disposition: ExecutableNow, - dissolve_trigger: "ledger all-green at v1_delete" - }, - VerificationLedgerRow { - id: ^family_equals_fold_closure, - kind: FamilyEqualsEval, - title: "emit_host_fold_closure interpreted==native equals_eval", - execution: ClaimWitness { - entry: "src/v2/test/claim/execution/emit_host_fold_closure_equals_eval_test.dag", - function: "emit_host_fold_closure_equals_eval_holds" - }, - disposition: KnownRedPendingUnquarantine, - dissolve_trigger: "eval gains closure-arg support; known_red_probe row deletes on green (swift-stag-662 / jolly-dove-581)" - }, VerificationLedgerRow { id: ^family_equals_field_access, kind: FamilyEqualsEval, - title: "emit_host_field_access interpreted==native equals_eval", + title: "emit_host_field_access family equals_eval agreement", execution: ClaimWitness { entry: "src/v2/test/claim/execution/emit_host_field_access_equals_eval_test.dag", - function: "emit_host_field_access_equals_eval_holds" + function: "emit_host_field_access_equals_eval_all_holds" }, disposition: KnownRedPendingUnquarantine, - dissolve_trigger: "emit_host_field_access transport lands; known_red_probe wet rows delete (swift-stag-662)" + dissolve_trigger: "#6912 eval-repair merges; known_red_probe wet rows delete (swift-stag-662)" }, VerificationLedgerRow { id: ^family_equals_complement, kind: FamilyEqualsEval, - title: "emit_host_complement interpreted==native equals_eval", + title: "emit_host_complement family equals_eval agreement", execution: ClaimWitness { entry: "src/v2/test/claim/execution/emit_host_complement_equals_eval_test.dag", - function: "emit_host_complement_equals_eval_holds" + function: "emit_host_complement_equals_eval_all_holds" }, disposition: KnownRedPendingUnquarantine, - dissolve_trigger: "emit_host_complement transport lands; known_red_probe wet rows delete (swift-stag-662)" + dissolve_trigger: "#6912 eval-repair merges; known_red_probe wet rows delete (swift-stag-662)" }, VerificationLedgerRow { - id: ^family_equals_meet, + id: ^family_equals_meet_join, kind: FamilyEqualsEval, - title: "emit_host_meet interpreted==native equals_eval", + title: "emit_host_meet_join family equals_eval agreement", execution: ClaimWitness { entry: "src/v2/test/claim/execution/emit_host_meet_join_equals_eval_test.dag", - function: "emit_host_meet_equals_eval_holds" + function: "emit_host_meet_join_equals_eval_all_holds" }, disposition: KnownRedPendingUnquarantine, - dissolve_trigger: "meet_join equals_eval debt cleared (emit_host_meet_join_equals_eval_test.dag)" + dissolve_trigger: "#6912 eval-repair merges (complement literal root shared)" }, VerificationLedgerRow { - id: ^family_equals_join, + id: ^family_equals_variant_construct, kind: FamilyEqualsEval, - title: "emit_host_join interpreted==native equals_eval", + title: "emit_host_variant_construct family equals_eval agreement", execution: ClaimWitness { - entry: "src/v2/test/claim/execution/emit_host_meet_join_equals_eval_test.dag", - function: "emit_host_join_equals_eval_holds" + entry: "src/v2/test/claim/execution/emit_host_variant_construct_equals_eval_test.dag", + function: "emit_host_variant_construct_equals_eval_all_holds" }, disposition: KnownRedPendingUnquarantine, - dissolve_trigger: "meet_join equals_eval debt cleared (emit_host_meet_join_equals_eval_test.dag)" + dissolve_trigger: "#6912 eval-repair merges (Conj scrutinee allocate_literal arm)" }, VerificationLedgerRow { - id: ^family_equals_variant_construct, + id: ^family_equals_fold_closure, kind: FamilyEqualsEval, - title: "emit_host_variant_construct interpreted==native equals_eval", + title: "emit_host_fold_closure family equals_eval agreement", execution: ClaimWitness { - entry: "src/v2/test/claim/execution/emit_host_variant_construct_equals_eval_test.dag", - function: "emit_host_variant_construct_equals_eval_holds" + entry: "src/v2/test/claim/execution/emit_host_fold_closure_equals_eval_test.dag", + function: "emit_host_fold_closure_equals_eval_all_holds" }, disposition: KnownRedPendingUnquarantine, - dissolve_trigger: "variant_construct equals_eval debt cleared (emit_host_variant_construct_equals_eval_test.dag)" + dissolve_trigger: "eval arc lands closure-arg support; known_red_probe row deletes on green (jolly-dove-581)" } ] @@ -245,6 +219,10 @@ fn ledger_blocked_count() -> Int { length(xs: ledger_rows_with_disposition(d: BlockedOnCiFloorCutover)) } +fn ledger_v1_delete_required_green_count() -> Int { + ledger_total_row_count() +} + fn ledger_has_spine_kind(kind: VerificationReceiptKind) -> Bool { fold_list( xs: proactive_verification_spine_rows, @@ -258,3 +236,11 @@ fn ledger_all_spine_kinds_present() -> Bool { && ledger_has_spine_kind(kind: CompileCleanParity) && ledger_has_spine_kind(kind: RegenBehavioralFixedPoint) } + +fn disposition_to_pending_outcome(row: VerificationLedgerRow) -> VerificationExecutionOutcome { + match row.disposition { + ExecutableNow => OutcomePending { reason: "not yet executed this session" } + KnownRedPendingUnquarantine => OutcomePending { reason: row.dissolve_trigger } + BlockedOnCiFloorCutover => OutcomePending { reason: row.dissolve_trigger } + } +} diff --git a/dag/tools/proactive_verification_ledger_transport.dag b/dag/tools/proactive_verification_ledger_transport.dag index 39b13706559..18cfeaa5370 100644 --- a/dag/tools/proactive_verification_ledger_transport.dag +++ b/dag/tools/proactive_verification_ledger_transport.dag @@ -9,24 +9,8 @@ import gunbc.proactive_verification_ledger { ledger_rows_with_disposition } import tools.host_prelude { ClaimRun, run_gunbc_claims } -import tools.regen_verify_transport { run_regen_verify } import v2.std.algebra { fold_list } -import v2.std.collection { List } import v2.std.logic { Bool } -import v2.std.text { String } - -fn claim_run_from_row(row: VerificationLedgerRow) -> ClaimRun { - match row.execution { - ClaimWitness { entry: e, function: f } => - ClaimRun { entry: e, function: f } - FalsifierPredictOnlyBatch => - ClaimRun { entry: "", function: "" } - CompileCleanGate => - ClaimRun { entry: "", function: "" } - RegenVerifyGate => - ClaimRun { entry: "", function: "" } - } -} fn run_ledger_claim_row(row: VerificationLedgerRow) -> Bool { match row.execution { @@ -37,7 +21,7 @@ fn run_ledger_claim_row(row: VerificationLedgerRow) -> Bool { ) FalsifierPredictOnlyBatch => false CompileCleanGate => false - RegenVerifyGate => run_regen_verify() + RegenVerifyGate => false } } diff --git a/src/v2/test/claim/proactive_verification_ledger_witness_test.dag b/src/v2/test/claim/proactive_verification_ledger_witness_test.dag index d542377a90e..6245e44df58 100644 --- a/src/v2/test/claim/proactive_verification_ledger_witness_test.dag +++ b/src/v2/test/claim/proactive_verification_ledger_witness_test.dag @@ -1,31 +1,29 @@ module v2.test.claim.proactive_verification_ledger_witness import gunbc.proactive_verification_ledger { - WholeCorpusWitnessParityCold, - CompileCleanParity, - RegenBehavioralFixedPoint, - FamilyEqualsEval, ledger_all_spine_kinds_present, ledger_blocked_count, ledger_executable_now_count, ledger_family_row_count, ledger_known_red_count, ledger_spine_row_count, - ledger_total_row_count + ledger_total_row_count, + ledger_v1_delete_required_green_count } import tools.proactive_verification_ledger_transport { run_executable_ledger_rows } import v2.std.logic { Bool } -data proactive_verification_ledger_witness_note: String = "OVERLAP-START receipt (sunny-lynx-241, operator no-soak 2026-07-20): the proactive verification ledger is enumerated on the carrier (dag/gunbc/proactive_verification_ledger.dag) and overlap-executable rows run green by execution. Spine rows (whole-corpus falsifier cold, compile-clean, regen fixed point) are honestly BlockedOnCiFloorCutover until that milestone lands — never calendar soak. Known-red family equals_eval rows are counted, not silently skipped. v1_delete gates on ALL rows ExecutableNow or un-quarantined green." +data proactive_verification_ledger_witness_note: String = "OVERLAP-START receipt (sunny-lynx-241, operator no-soak 2026-07-20): the proactive verification ledger is enumerated on dag/gunbc/proactive_verification_ledger.dag (12 rows: 3 spine + 9 witness-realization families). Overlap-executable family rows (add/match/loop/classical_not_ingested) run green by execution; spine + five family rows are honestly OutcomePending until ci_floor_cutover / #6912 / fold eval arc. v1_delete gates on ALL 12 rows OutcomeGreen — never calendar soak." test fn proactive_verification_ledger_enumeration_holds() -> Bool { ledger_spine_row_count() == 3 - && ledger_family_row_count() == 12 - && ledger_total_row_count() == 15 + && ledger_family_row_count() == 9 + && ledger_total_row_count() == 12 + && ledger_v1_delete_required_green_count() == 12 && ledger_all_spine_kinds_present() == true && ledger_blocked_count() == 3 - && ledger_known_red_count() == 6 - && ledger_executable_now_count() == 6 + && ledger_known_red_count() == 5 + && ledger_executable_now_count() == 4 } test fn proactive_verification_ledger_overlap_execution_holds() -> Bool { From bd330c1c5913b6e37b27c0c60007c0dbc84437b2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 20 Jul 2026 05:40:13 +0000 Subject: [PATCH 3/3] Fix CI: hermetic enumeration only; overlap execution off discovery path. Split overlap execution into test/claim/execution/ (IsExecutable is wet; hermetic discovery must not call run_gunbc_claims). Simplify ledger_row_disposition_is to use == per review 40141. Co-authored-by: Cursor --- dag/gunbc/proactive_verification_ledger.dag | 9 +-------- ...ve_verification_ledger_overlap_execution_test.dag | 10 ++++++++++ .../proactive_verification_ledger_witness_test.dag | 12 +----------- 3 files changed, 12 insertions(+), 19 deletions(-) create mode 100644 src/v2/test/claim/execution/proactive_verification_ledger_overlap_execution_test.dag diff --git a/dag/gunbc/proactive_verification_ledger.dag b/dag/gunbc/proactive_verification_ledger.dag index fbc434f2411..05bedca6e24 100644 --- a/dag/gunbc/proactive_verification_ledger.dag +++ b/dag/gunbc/proactive_verification_ledger.dag @@ -179,14 +179,7 @@ fn proactive_verification_ledger_rows() -> List { } fn ledger_row_disposition_is(row: VerificationLedgerRow, d: VerificationDisposition) -> Bool { - match row.disposition { - ExecutableNow => - match d { ExecutableNow => true, KnownRedPendingUnquarantine => false, BlockedOnCiFloorCutover => false } - KnownRedPendingUnquarantine => - match d { ExecutableNow => false, KnownRedPendingUnquarantine => true, BlockedOnCiFloorCutover => false } - BlockedOnCiFloorCutover => - match d { ExecutableNow => false, KnownRedPendingUnquarantine => false, BlockedOnCiFloorCutover => true } - } + row.disposition == d } fn ledger_rows_with_disposition(d: VerificationDisposition) -> List { diff --git a/src/v2/test/claim/execution/proactive_verification_ledger_overlap_execution_test.dag b/src/v2/test/claim/execution/proactive_verification_ledger_overlap_execution_test.dag new file mode 100644 index 00000000000..a4e6a646114 --- /dev/null +++ b/src/v2/test/claim/execution/proactive_verification_ledger_overlap_execution_test.dag @@ -0,0 +1,10 @@ +module v2.test.execution.proactive_verification_ledger_overlap_execution + +import tools.proactive_verification_ledger_transport { run_executable_ledger_rows } +import v2.std.logic { Bool } + +data proactive_verification_ledger_overlap_execution_note: String = "Overlap-start execution receipt: runs the four ExecutableNow family equals_eval rows (add, match, loop, classical_not_ingested) via run_gunbc_claims. Excluded from hermetic per-PR discovery (test/claim/execution/ grain — IsExecutable is a wet host effect). Dissolve-on: ci_floor_cutover enrolls overlap execution on the scheduled wet/falsifier lane when native routing lands." + +test fn proactive_verification_ledger_overlap_execution_holds() -> Bool { + run_executable_ledger_rows() +} diff --git a/src/v2/test/claim/proactive_verification_ledger_witness_test.dag b/src/v2/test/claim/proactive_verification_ledger_witness_test.dag index 6245e44df58..20ed34ac9e3 100644 --- a/src/v2/test/claim/proactive_verification_ledger_witness_test.dag +++ b/src/v2/test/claim/proactive_verification_ledger_witness_test.dag @@ -10,10 +10,9 @@ import gunbc.proactive_verification_ledger { ledger_total_row_count, ledger_v1_delete_required_green_count } -import tools.proactive_verification_ledger_transport { run_executable_ledger_rows } import v2.std.logic { Bool } -data proactive_verification_ledger_witness_note: String = "OVERLAP-START receipt (sunny-lynx-241, operator no-soak 2026-07-20): the proactive verification ledger is enumerated on dag/gunbc/proactive_verification_ledger.dag (12 rows: 3 spine + 9 witness-realization families). Overlap-executable family rows (add/match/loop/classical_not_ingested) run green by execution; spine + five family rows are honestly OutcomePending until ci_floor_cutover / #6912 / fold eval arc. v1_delete gates on ALL 12 rows OutcomeGreen — never calendar soak." +data proactive_verification_ledger_witness_note: String = "OVERLAP-START structural receipt (sunny-lynx-241, operator no-soak 2026-07-20): the proactive verification ledger is enumerated on dag/gunbc/proactive_verification_ledger.dag (12 rows: 3 spine + 9 witness-realization families). Hermetic per-PR discovery pins enumeration invariants only. Overlap execution (four ExecutableNow family equals_eval receipts) lives in src/v2/test/claim/execution/proactive_verification_ledger_overlap_execution_test.dag — excluded from hermetic discovery (run_gunbc_claims needs IsExecutable; two-tier policy: wet evidence does not gate per-PR CI). Local recipe: claim_batch --source-root dag --source-root src/v2 --entry src/v2/test/claim/execution/proactive_verification_ledger_overlap_execution_test.dag --function proactive_verification_ledger_overlap_execution_holds" test fn proactive_verification_ledger_enumeration_holds() -> Bool { ledger_spine_row_count() == 3 @@ -25,12 +24,3 @@ test fn proactive_verification_ledger_enumeration_holds() -> Bool { && ledger_known_red_count() == 5 && ledger_executable_now_count() == 4 } - -test fn proactive_verification_ledger_overlap_execution_holds() -> Bool { - run_executable_ledger_rows() -} - -test fn proactive_verification_ledger_witnesses() -> Bool { - proactive_verification_ledger_enumeration_holds() - && proactive_verification_ledger_overlap_execution_holds() -}