From 0beae56f0bed9faa0d62aa3d08490bfa84514d6d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 11:53:24 -0400 Subject: [PATCH] WIP: R3 gate #10: l7 algebraic laws witnessed --- docs/r3-program-plan.md | 4 +- .../r3_verification_l7_algebraic_laws.dag | 13 ++++-- .../r3_verification_l4_l7_l5_skeleton_test.rs | 42 +++++++++++++++---- 3 files changed, 46 insertions(+), 13 deletions(-) diff --git a/docs/r3-program-plan.md b/docs/r3-program-plan.md index f4f8e1d0a8c..14f5402fc28 100644 --- a/docs/r3-program-plan.md +++ b/docs/r3-program-plan.md @@ -179,7 +179,7 @@ Mgrs author per-gate spec citing the (a)/(b)/(c) satisfaction; closure-ledger en |---|---|---| | T-Tier3-Dissolution | `tier3_*_mirror_dissolved` (state-check) | + `tier3_dissolution_demonstration_executes` — at least one Tier3-mirror-consumer .dag program runs end-to-end via Evaluator | | T-LensProducer-Retirement | retirement gates (state-check) | + `lens_producer_retirement_executable_witness` (per PB Mgr poke-hole 2026-05-06 F3 — reframed from `_demonstration`) — execution-ready witness DEFERRED to Row-4 equivalence receipt landing per `docs/design-pb-runtime-interpreter.md` §5.1 + convergence matrix; near-term demo = retirement state-check + doc receipts; "demonstration" status re-promotes when Row-4 + Item 4 receipts exist | -| T-V-L4-L7-Direct | `l4_emit_eval_match` (**§1.8 #9** — **CONSUMER_LANDED** on Rust/Int W1 slice; **not §1.8 PASSING** until full certification corpus per `r3-structure.md` §Acceptance); `l7_algebraic_laws_witnessed` still staged (closure bar = exhaustive L4 corpus + per-(algebra, inhabitant, law) L7 coverage per `r3-structure.md` §"Lane structure") | Executable seeds + §1.7 corpus rule: slice **Pass** receipts ≠ acceptance **PASSING**; full lane demonstration remains gated on corpus exhaustion + L7 | +| T-V-L4-L7-Direct | `l4_emit_eval_match` (**§1.8 #9** — **CONSUMER_LANDED** on Rust/Int W1 slice; **not §1.8 PASSING** until full certification corpus per `r3-structure.md` §Acceptance); `l7_algebraic_laws_witnessed` (**§1.8 #10** — **CONSUMER_LANDED** on bounded `AlgebraicLaw` `Int` slice per §1.8 ledger Notes; **not §1.8 PASSING** until exhaustive per-(algebra, inhabitant, law) L7 coverage per `r3-structure.md` §"Lane structure") | Executable seeds + §1.7 corpus rule: slice **Pass** receipts ≠ acceptance **PASSING**; full lane demonstration remains gated on corpus exhaustion + exhaustive L7 | | T-V-L5-Corpus | `l5_cross_target_consistency` ✓ | (existing) | | T-FixedPoint | `pb_self_compile_fixed_point` ✓ | (existing) | | T-Numeric-Construction | substrate-shape gates only | + `numeric_construction_demonstration` — end-to-end program using `Int<32>` + `Real<64>` round-trip executes | @@ -233,7 +233,7 @@ This principle is NOT a separate lane; it's a per-lane gate-shape requirement ap | 7 | `regen_lens_dot_rs_retired` | state-check | T-LensProducer-Retirement | DECLARED | gated on PB-1 bin-shim emit pattern | | 8 | `sg0_non_test_zero` | state-check | T-LensProducer-Retirement | DECLARED | SG-0 T-PB-A non-test ratchet = 0 (`EXPECTED_HAND_AUTHORED_NON_TEST` + `EXPECTED_HAND_AUTHORED_FRAGMENTS`) | | 9 | `l4_emit_eval_match` | structural-fold | T-V-L4-L7-Direct | **CONSUMER_LANDED** — executable consumer exists; §Acceptance corpus coverage **incomplete** (§1.7 corpus-quantified rule) | **Slice-1 receipt (evidence, non-closure):** three Rust/Int W1 `DifferentialEquals` certification seeds Pass in CI (`r3_verification_l4_emit_eval_match.dag`, suite `r3_verification_l4_l7_direct_suite`, harness `r3_verification_l4_l7_l5_skeleton_test.rs`; canonical claim `l4_emit_eval_match`). **PASSING** = every certification-corpus program per `r3-structure.md` §Acceptance. **Ledger phrase:** per-program emit ↔ eval algebraic equality | -| 10 | `l7_algebraic_laws_witnessed` | alg-law-witness | T-V-L4-L7-Direct | DECLARED (skeleton/staged) | exhaustive per-(algebra, inhabitant, law) coverage | +| 10 | `l7_algebraic_laws_witnessed` | alg-law-witness | T-V-L4-L7-Direct | **CONSUMER_LANDED** — bounded `AlgebraicLaw` runner receipts on honest additive/multiplicative `Int` lenses (`src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag`; canonical `TestClaim.name` `l7_algebraic_laws_witnessed`; integration `r3_verification_l4_l7_l5_skeleton_test.rs`) | **PASSING** = exhaustive per-(algebra, inhabitant, law) §Acceptance coverage per `r3-structure.md` (distributivity / lattice absorption / non-`AlgebraicLawKind` laws remain substrate §P1); slice receipts ≠ ledger closure | | 11 | `tc1_eta_equivalence_executable` | DimensionReport-typed | T-V-L4-L7-Direct | **DECLARED through R3** (scaffold authored PR #2184 with NotYetImplemented sentinel per Director (C-modified) ratification at #828). **AMENDED 2026-05-09 per Director (a)-disposition**: E3.c #1970 closed superseded-by-deferral; TC1 V1 strict-fire cannot reach PASSING absent #1972 substrate canvas-tier work, which is HELD-CANVAS-DEFERRED past R3 per Substrate Mgr Path-A confirmation 2026-05-08. Gate #11 stays DECLARED through R3 close; R3-close evidence routes through the Pattern A second-mover audit slice and is not load-bearing for R3-thesis honest-close arithmetic (97 enumerated - 1 canvas-deferred {#11} = 96 R3-load-bearing per §1.5). Prior phrasing ("flips DECLARED -> CONSUMER_LANDED -> PASSING in one move on Evaluator E3.c merge") superseded; strict-fire flip moves to a fresh post-R3 issue after #1972. | runtime prereq: G1.a static-rep OR G1.b generic + eta relation; #1972 canvas-tier substrate post-R3 | | 12 | `tc2_church_rosser_executable` | DimensionReport-typed | T-V-L4-L7-Direct | DECLARED (NEW 2026-05-06) | runtime prereq: second strategy/input order + strategy-keyed report | | 13 | `tc3_pattern_a_second_mover_executable` | DimensionReport-typed | T-V-L4-L7-Direct | DECLARED (NEW 2026-05-06) | runtime prereq: Descent execution proof (E5) + eval-step producer | diff --git a/src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag b/src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag index 8614f0f4943..1a958c44083 100644 --- a/src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag +++ b/src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag @@ -54,10 +54,15 @@ data r3_verification_l7_algebraic_laws_skeleton: TestClaim = { // `Identity`). Lattice meet/join **associativity/commutativity** tags are **not** green-lit here on // `Int` `+` (that would read as lattice laws without meet/join carriers). Bounded-lattice / // Boolean-algebra / free-monoid identity placeholders likewise stay **out** of the passing matrix. -data r3_l7_semigroup_associativity: TestClaim = { - name: "r3_l7_semigroup_associativity", +// +// §1.8 gate #10 canonical `TestClaim.name` / declaration id (`docs/r3-program-plan.md`): bounded +// `AlgebraicLaw::Associativity` on honest `Int` `+` (Semigroup slice). **PASSING** on the §Acceptance +// ledger remains exhaustive per-(algebra, inhabitant, law) coverage per `r3-structure.md`; this row +// is the executable consumer hook matching gate id `l7_algebraic_laws_witnessed`. +data l7_algebraic_laws_witnessed: TestClaim = { + name: "l7_algebraic_laws_witnessed", source: "fn r3_l7_semigroup_associativity_op(a: Int, b: Int) -> Int = a + b\n", - file_name: "r3_l7_semigroup_associativity.v3", + file_name: "l7_algebraic_laws_witnessed.v3", predicate: AlgebraicLaw(Associativity, r3_l7_semigroup_associativity_op), requires: [] } @@ -195,7 +200,7 @@ data r3_verification_l7_algebra_skeleton_suite: TestSuite = { data r3_verification_l7_algebra_matrix_suite: TestSuite = { name: "r3_verification_l7_algebra_matrix_suite", claims: [ - r3_l7_semigroup_associativity, + l7_algebraic_laws_witnessed, r3_l7_monoid_identity, r3_l7_commutative_monoid_commutativity, r3_l7_group_identity, diff --git a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs index 06d0d969bcb..01ebc98694f 100644 --- a/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs +++ b/src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs @@ -6,11 +6,13 @@ //! (`docs/r3-program-plan.md` §1.7 corpus-quantified rule — ledger **PASSING** awaits full corpus). //! Plus a mixed-lineage `NotYetImplemented` control. Lane 1 L7 exercises bounded `Associativity`, //! `Commutativity`, and `Identity` operational witnesses on **honest additive vs multiplicative `Int` -//! lenses** (`+` vs `*`). The L7 matrix suite locks claims whose **Int lens semantics match the -//! tagged obligation** (e.g. multiplicative `Identity` uses `*`); lattice / Boolean / free-monoid -//! obligations and lattice meet/join law tags stay **out** of the passing matrix until faithful -//! carriers exist (`dsl/std/algebra.dag`, INVARIANTS §P1 / MODELING M9); see fixture **Receipt limits** -//! — this is not ROADMAP exhaustive L7 closure. Lane 2 / L5 rows remain intentionally deferred where noted. +//! lenses** (`+` vs `*`). Canonical §1.8 gate **#10** `l7_algebraic_laws_witnessed` maps to the matrix +//! lead row (`AlgebraicLaw::Associativity` on `Int` `+`). The L7 matrix suite locks claims whose **Int +//! lens semantics match the tagged obligation** (e.g. multiplicative `Identity` uses `*`); lattice / +//! Boolean / free-monoid obligations and lattice meet/join law tags stay **out** of the passing +//! matrix until faithful carriers exist (`dsl/std/algebra.dag`, INVARIANTS §P1 / MODELING M9); see +//! fixture **Receipt limits** — slice receipts ≠ ROADMAP exhaustive L7 closure. Lane 2 / L5 rows +//! remain intentionally deferred where noted. //! Matrix: `docs/briefs/r3-v-l7-algebra-coverage-matrix.md`. use std::sync::OnceLock; @@ -43,11 +45,12 @@ const L7_FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/r3_verification_l7_algebraic_laws.dag"; const L7_SUITE: &str = "r3_verification_l7_algebra_skeleton_suite"; const L7_CLAIM: &str = "r3_verification_l7_algebraic_laws_skeleton"; +const L7_GATE_CLAIM: &str = "l7_algebraic_laws_witnessed"; const L7_MATRIX_SUITE: &str = "r3_verification_l7_algebra_matrix_suite"; /// Claims wired into [`L7_MATRIX_SUITE`] — honest **additive vs multiplicative Int** slices only /// (`+` vs `*`); no lattice / monoid inhabitant rows (see fixture receipt limits). const L7_MATRIX_PASS_CLAIMS: &[&str] = &[ - "r3_l7_semigroup_associativity", + L7_GATE_CLAIM, "r3_l7_monoid_identity", "r3_l7_commutative_monoid_commutativity", "r3_l7_group_identity", @@ -227,7 +230,32 @@ fn r3_verification_l7_algebraic_law_identity_skeleton_passes_bounded_witness() { }); } -/// Bounded-runner receipt for [`L7_MATRIX_SUITE`] only — **not** exhaustive `l7_algebraic_laws_witnessed` / ROADMAP coverage. +/// §1.8 gate #10 canonical claim id — bounded `AlgebraicLaw::Associativity` on `Int` `+` (matrix lead row). +#[test] +fn l7_algebraic_laws_witnessed_passes_bounded_associativity_witness() { + run_on_larger_stack(|| { + let dag = cached_compile(L7_FIXTURE, L7_FIXTURE_PATH, &L7_DAG); + let claim_decl = dag.declaration_by_name(L7_GATE_CLAIM).unwrap_or_else(|| { + panic!("missing `{L7_GATE_CLAIM}` in {L7_FIXTURE_PATH}"); + }); + let claim = TestClaimValue::from_declaration(claim_decl).unwrap_or_else(|reason| { + panic!("`{L7_GATE_CLAIM}` should lower to a structural TestClaim: {reason}"); + }); + assert_eq!( + claim.claim_name, L7_GATE_CLAIM, + "canonical gate claim name must match §1.8 gate id" + ); + let evaluation = TestRunner::new(dag).run_claim(&claim); + assert_eq!(evaluation.claim_name, L7_GATE_CLAIM); + assert!( + matches!(evaluation.result, ClaimResult::Pass), + "expected AlgebraicLaw::Associativity bounded witness Pass on Int `+`, got {:?}", + evaluation.result + ); + }); +} + +/// Bounded-runner receipt for [`L7_MATRIX_SUITE`] only — **not** exhaustive §Acceptance / ROADMAP coverage. /// /// One [`TestRunner::run_suite`] covers every [`L7_MATRIX_PASS_CLAIMS`] row (including semigroup /// associativity and commutative-monoid commutativity) plus embedded-source `a + b` / `a * b`