Generative TestClaim categories lane — formalize wishlist + dispatch non-tautological generators (per smart-lynx-142 framing 2026-05-22)

docs/design-testgen-generative-categories.md

@@ -0,0 +1,66 @@
+# Generative TestClaim Categories
+
+> Part of: `src/v4/TASKS.md` T-19, `src/v4/lens/testgen.dag`, `src/v4/std/verification.dag`, `TESTING.md`, `INVARIANTS.md`.
+>
+> Purpose: define the wishlist of TestClaim families that can be generated from existing substrate facts without producing tautological tests.
+
+## Rule
+
+A generated TestClaim must add evidence not already proven by the source row that scheduled it.
+
+Mechanical exclusion test: if the claim result can be proven from the scheduling row alone, without execution, an independent witness, a negative fixture, or a cross-target observation, the generator skips that row.
+
+This excludes `f(x) = f(x)`, type-conformance for already typechecked inputs, and identity laws copied directly from an algebra declaration with no sample, witness, or falsification path. Uncertain rows fail closed by not generating a claim.
+
+## Canonical Arms
+
+`src/v4/lens/testgen.dag` owns the closed `TestgenConcept` coproduct. This doc does not add a second category authority; it records which universally generated claim families route through each existing arm.
+
+| TestgenConcept arm | Source rows | Generated claim | Non-tautology basis | Mechanical skip |
+|---|---|---|---|---|
+| `LanguageBehaviorEquivalence` | Type-construction or modeled callable subject plus target language identity | Same typed input produces equivalent observed output across target models | Frozen I/O snapshot now; target-pair runtime observation once multi-target eval is live | Skip if the expected value is just the input row without a language-model observation |
+| `AlgebraLaw` | `data carrier: Algebra<T>` rows and law symbols | Law expression normalizes to the independently declared expected witness | Law witness or falsifying negative fixture, not the algebra row itself | Reject `lhs == rhs` at the generator boundary |
+| `DiagnosticExhaustiveness` | Diagnostic reasons and negative fixtures | Ill-formed input produces the declared typed diagnostic | Negative fixture, not a success-path restatement | Skip when there is no negative fixture or the expected diagnostic is only copied from the producer |
+| `LensApplicability` | Lens plus program subject | Lens observation over a program produces or rejects with the expected witness | Observation fixture, property checker, or negative fixture | Skip if the row only reruns the lens and compares its own emitted fact |
+| `BidirectionalRoundtrip` | Language production plus target identity | Encode/decode or parse/emit roundtrip preserves the independently declared value | Differential roundtrip through two directions | Skip identity productions with no distinct decode/encode step |
+| `TypeConstruction` | Connective or behavior construction subjects | Constructed node matches the structural witness or rejects arity errors | Construction witness or negative arity fixture | Skip type-conformance rows already proven by parsing/lowering alone |
+| `RefinementPreservation` | Refined value plus original base | Refinement preserves the accepted base value | Accepted refinement witness plus base projection | Skip if the refinement was not accepted or the projected base is only restated without the refined carrier |
+
+Operator wishlist examples route through those seven arms rather than extending the arm set: coproduct exhaustiveness is a `DiagnosticExhaustiveness` or `LensApplicability` family depending on whether the first slice is a missing-branch diagnostic or a branch-coverage lens observation; refinement preservation uses its canonical `RefinementPreservation` arm; witness validity and idempotent operation conformance route through `LensApplicability` until a later substrate change proves a more specific arm is needed.
+
+## Landed Slices
+
+`LanguageBehaviorEquivalence` is live in `src/v4/lens/testgen.dag` via `testgen_emit_language_behavior_equivalence_claim` and `testgen_scheduled_language_behavior_generators`. The generated corpus is `src/v4/test/claim/generated/language_behavior_equivalence.dag`; it carries three runner receipts through `run_test_claim` / `run_test_claim_assert`.
+
+`AlgebraLaw` now has a generator emission helper, `testgen_emit_algebra_law_claim`, and a first generated Nat corpus at `src/v4/test/claim/generated/algebra_law_conformance.dag`. The helper carries the canonical `AlgebraLawSubject` into both emitted equality terms; the sample rows route Nat values and operation results through `Zero` / `Succ` plus canonical `nat_add` / `nat_mul`, with only local expression-shape tags left as a bounded `feature:t19-nat-expression-node-encoding` bridge until a canonical Nat-expression `Node` encoder lands. The dispatch ledger therefore records AlgebraLaw as dispatched; remaining AlgebraLaw work is broadening from the Nat sample to all algebra carriers, not a pending category slot.
+
+`RefinementPreservation` is dispatched by `testgen_emit_refinement_preservation_claim` and the generated corpus at `src/v4/test/claim/generated/refinement_preservation.dag`. The dispatch ledger records the landed nonempty-list base-preservation slice; remaining work is broadening the corpus beyond that first refinement subject.
+
+`DiagnosticExhaustiveness` is dispatched by `testgen_emit_coproduct_exhaustiveness_claim` and the generated corpus at `src/v4/test/claim/generated/coproduct_exhaustiveness.dag`. The dispatch ledger records the landed coproduct-exhaustiveness diagnostic slice under `GeneratedCoproductExhaustiveness`; remaining diagnostic work is broadening beyond that first missing-variant fixture, not a pending category slot.
+
+`src/v4/test/claim/generated/testgen_category_wishlist.dag` records pending or dispatched rows through the canonical `Generator` shape: `kind`, `classification`, `anchor`, and `slot`. That file is a dispatch artifact, not a second authority for `TestgenConcept`; the closed seven-arm scheduling coproduct remains `src/v4/lens/testgen.dag`.
+
+## Worked Samples
+
+Cross-target LBE samples:
+
+- `ManualLbeConjDagSurface` checks a `Conj` type-node against the `.dag` language model surface snapshot.
+- `ManualLbeDisjDagSurface` checks a `Disj` type-node against the same language-model authority.
+- `ManualLbeTransformDagSurface` checks a `Transform` computation-node snapshot.
+
+Algebra-law samples:
+
+- `generated_nat_add_left_identity_claim` emits a Nat addition identity claim from the law symbol and expected witness node.
+- `generated_nat_add_associativity_claim` emits a Nat addition associativity claim.
+- `generated_nat_mul_annihilator_claim` emits a Nat multiplication zero-annihilator claim.
+
+## Dispatch Plan
+
+The next generator PRs should land one category at a time and include:
+
+- the generator function in `src/v4/lens/testgen.dag` or a tighter existing authority if the category already has one;
+- at least three generated TestClaim rows under `src/v4/test/claim/generated/`;
+- a structural test or script guard proving the rows are generated through the category emission helper;
+- an explicit tautology-skip path, preferably represented as a negative fixture or count witness.
+
+Recommended order by canonical arm: `LensApplicability` witness-validity instance, `LensApplicability` idempotent-operation instance, `DiagnosticExhaustiveness` generated-corpus broadening beyond the first coproduct-exhaustiveness slice, and `RefinementPreservation` generated-corpus broadening. Algebra-law broadening from the Nat sample to all algebra carriers can proceed in parallel under the existing `AlgebraLaw` arm.

scripts/check_t19_testgen_activation.py

@@ -20,6 +20,8 @@
 EFFECTS = ROOT / "src/v4/std/effects.dag"
 LBE_GENERATED = ROOT / "src/v4/test/claim/generated/language_behavior_equivalence.dag"
 LBE_MANIFEST = ROOT / "src/v4/test/claim/generated/lbe_anchor_manifest.dag"
+GENERATOR_WISHLIST = ROOT / "src/v4/test/claim/generated/testgen_category_wishlist.dag"
+ALGEBRA_GENERATED = ROOT / "src/v4/test/claim/generated/algebra_law_conformance.dag"
 COPRODUCT_EXHAUSTIVENESS_GENERATED = (
     ROOT / "src/v4/test/claim/generated/coproduct_exhaustiveness.dag"
 )
@@ -46,13 +48,21 @@ def _require_substrings(label: str, text: str, needles: tuple[str, ...]) -> None
         raise SystemExit(f"{label}: missing required substrings: {missing!r}")
 
 
+def _forbid_substrings(label: str, text: str, needles: tuple[str, ...]) -> None:
+    present = [n for n in needles if n in text]
+    if present:
+        raise SystemExit(f"{label}: forbidden substrings present: {present!r}")
+
+
 def main() -> None:
     for path in (
         TESTGEN,
         COPRODUCT_EXHAUSTIVENESS_GENERATED,
         EFFECTS,
         LBE_GENERATED,
         LBE_MANIFEST,
+        GENERATOR_WISHLIST,
+        ALGEBRA_GENERATED,
         REFINEMENT_GENERATED,
         REFINEMENT_MANIFEST,
         IDEMPOTENT_OPERATION_GENERATED,
@@ -64,6 +74,8 @@ def main() -> None:
     effects = _read(EFFECTS)
     lbe = _read(LBE_GENERATED)
     manifest = _read(LBE_MANIFEST)
+    wishlist = _read(GENERATOR_WISHLIST)
+    algebra = _read(ALGEBRA_GENERATED)
     coproduct_exhaustiveness = _read(COPRODUCT_EXHAUSTIVENESS_GENERATED)
     refinement = _read(REFINEMENT_GENERATED)
     refinement_manifest = _read(REFINEMENT_MANIFEST)
@@ -78,6 +90,18 @@ def main() -> None:
             "type FrozenLanguageBehaviorSnapshot",
             "type LanguageBehaviorIoMock",
             "fn testgen_emit_language_behavior_equivalence_claim",
+            "fn testgen_emit_algebra_law_claim",
+            "if lhs == rhs",
+            "t19_algebra_law_tautological_sides",
+            "type AlgebraLawCase { anchor: ClaimAnchorKey, subject: AlgebraLawSubject }",
+            "fn algebra_law_manual_claim_case(anchor: ManualAnchorKey) -> Outcome<AlgebraLawCase>",
+            "fn algebra_law_subject_for_manual_anchor(anchor: ManualAnchorKey) -> Outcome<AlgebraLawSubject>",
+            "t19_algebra_law_anchor_mismatch",
+            "match algebra_law_manual_claim_case(anchor: anchor)",
+            "match algebra_law_subject_for_manual_anchor(anchor: manual_anchor)",
+            "fn algebra_law_claim_term(subject: AlgebraLawSubject, expression: Node) -> Node",
+            "lhs: algebra_law_claim_term(subject: law_case.subject, expression: lhs)",
+            "rhs: algebra_law_claim_term(subject: law_case.subject, expression: rhs)",
             "fn testgen_emit_idempotent_operation_claim",
             "fn testgen_scheduled_language_behavior_generators",
             "fn testgen_scheduled_idempotent_operation_subjects",
@@ -97,7 +121,9 @@ def main() -> None:
             "coproduct_exhaustiveness_subject_testclaim_diagnostic",
             "coproduct_exhaustiveness_subject_testclaim_equals",
             "coproduct_exhaustiveness_subject_testclaim_roundtrip",
-            "coproduct_exhaustiveness_missing_variant",
+            "subject: DiagnosticExhaustivenessSubject",
+            "reason: subject.reason",
+            "d: coproduct_exhaustiveness_diagnostic(subject: subject, input: input)",
             "fn coproduct_exhaustiveness_anchor_omitted_variant",
             "variant: coproduct_exhaustiveness_anchor_omitted_variant(anchor: anchor)",
             "anchor: generated_claim_anchor(anchor: anchor)",
@@ -163,12 +189,80 @@ def main() -> None:
         ),
     )
 
+    _require_substrings(
+        "testgen_category_wishlist.dag",
+        wishlist,
+        (
+            "fn testgen_pending_non_tautological_generator_wishlist",
+            "fn testgen_dispatched_non_tautological_generators",
+            "kind: TestClaimCompilesClaimVariant",
+            "kind: TestClaimDiagnosticClaimVariant",
+            "kind: TestClaimEqualsClaimVariant",
+            "kind: TestClaimRoundTripClaimVariant",
+            "type TestgenOracleBasis",
+            "StructuralConstructionWitness",
+            "AlgebraLawWitness",
+            "DiagnosticNegativeFixture",
+            "LensObservationFixture",
+            "RoundTripDifferential",
+            "FrozenIoSnapshot",
+            "RefinementProjectionWitness",
+            "dispatch_key: Symbol",
+            "feature:t19-generator-oracle-basis-carrier",
+            "bound task: src/v4/TASKS.md#t-19-lenstestgendag--producer-of-testclaim-corpus-from-substrate",
+            "dissolve-on-arrival: delete TestgenOracleBasis",
+            "data claim_testgen_wishlist_formalized: TestClaim",
+            "generated_claim_anchor",
+            "GeneratedCoproductExhaustiveness",
+            "t19_coproduct_exhaustiveness_missing_variant",
+        ),
+    )
+
+    _require_substrings(
+        "algebra_law_conformance.dag",
+        algebra,
+        (
+            "testgen_emit_algebra_law_claim",
+            "Nat,",
+            "nat_add,",
+            "nat_mul",
+            "feature:t19-nat-expression-node-encoding",
+            "generated_nat_add_left_identity_claim",
+            "generated_nat_add_associativity_claim",
+            "generated_nat_mul_annihilator_claim",
+            "fn t19_generated_nat_add",
+            "fn t19_generated_nat_mul",
+            "operation: algebra_law_generated_nat_add_application",
+            "operation: algebra_law_generated_nat_mul_application",
+            "result: nat_add(a: t19_generated_nat_zero_value(), b: t19_generated_nat_one_value())",
+            "rhs: t19_generated_nat_one()",
+            "result: nat_mul(a: t19_generated_nat_zero_value(), b: t19_generated_nat_three_value())",
+            "rhs: t19_generated_nat_zero()",
+            "fn generated_algebra_law_claim_rows",
+            "length(xs: generated_algebra_law_claim_rows()) == 3",
+        ),
+    )
+    _forbid_substrings(
+        "algebra_law_conformance.dag",
+        algebra,
+        (
+            "nat_algebra_law_subject_symbol_add_operation",
+            "nat_algebra_law_subject_symbol_mul_operation",
+            "nat_algebra_law_subject_symbol_zero_value",
+            "nat_algebra_law_subject_symbol_one_value",
+            "nat_algebra_law_subject_symbol_two_value",
+            "nat_algebra_law_subject_symbol_three_value",
+        ),
+    )
+
     _require_substrings(
         "coproduct_exhaustiveness.dag",
         coproduct_exhaustiveness,
         (
             "fn generated_coproduct_exhaustiveness_claim() -> Outcome<TestClaim>",
             "testgen_emit_coproduct_exhaustiveness_claim",
+            "subject: DiagnosticExhaustivenessSubject",
+            "reason: t19_coproduct_exhaustiveness_missing_variant",
             "GeneratedCoproductExhaustiveness { omitted_variant: _ }",
             "witness_coproduct_exhaustiveness_diagnostic_claim",
             "witness_coproduct_exhaustiveness_uses_generated_anchor",
@@ -233,6 +327,42 @@ def main() -> None:
             "IdempotentOperationSubject must stay outside the closed seven-way TestgenConcept coproduct"
         )
 
+    pending_rows = wishlist.split("fn testgen_pending_non_tautological_generator_wishlist")[1].split(
+        "fn testgen_dispatched_non_tautological_generators"
+    )[0]
+    if pending_rows.count("TestgenWishlistRow {") != 3:
+        raise SystemExit("generator wishlist must carry exactly three pending non-dispatched rows")
+    for shipped_slot in ("slot: AlgebraLaw", "slot: DiagnosticExhaustiveness"):
+        if shipped_slot in pending_rows:
+            raise SystemExit(f"{shipped_slot} has generated rows and must stay out of pending wishlist rows")
+
+    dispatched_rows = wishlist.split("fn testgen_dispatched_non_tautological_generators")[1].split(
+        "fn pending_non_tautological_generator_count_is_three"
+    )[0]
+    if dispatched_rows.count("TestgenWishlistRow {") != 4:
+        raise SystemExit("generator wishlist must carry exactly four dispatched rows")
+    if (
+        "generator: dispatched_language_behavior_equivalence_generator()" not in dispatched_rows
+        or "generator: dispatched_algebra_law_generator()" not in dispatched_rows
+        or "generator: dispatched_diagnostic_exhaustiveness_generator()" not in dispatched_rows
+        or "generator: dispatched_refinement_preservation_generator()" not in dispatched_rows
+    ):
+        raise SystemExit("dispatched wishlist rows must include LBE, AlgebraLaw, DiagnosticExhaustiveness, and RefinementPreservation")
+    if "ManualNatAddAssociativity" not in wishlist:
+        raise SystemExit("dispatched AlgebraLaw wishlist row must carry the emitted algebra-law anchor")
+    if "GeneratedCoproductExhaustiveness" not in wishlist:
+        raise SystemExit("dispatched DiagnosticExhaustiveness wishlist row must carry the emitted generated anchor")
+    diagnostic_generator = wishlist.split("fn dispatched_diagnostic_exhaustiveness_generator")[1].split(
+        "fn wishlist_lens_applicability_generator"
+    )[0]
+    if "classification: TestClassification { tier: Tier1, layer: Unit }" not in diagnostic_generator:
+        raise SystemExit("dispatched DiagnosticExhaustiveness wishlist row must match emitted Tier1 classification")
+    if "ManualRefinementNonEmptyListBase" not in wishlist:
+        raise SystemExit("dispatched RefinementPreservation wishlist row must carry the emitted refinement anchor")
+
+    if algebra.count("data generated_nat_") < 3:
+        raise SystemExit("algebra-law generator must produce at least three sample TestClaim rows")
+
     _require_substrings(
         "effects.dag",
         effects,
@@ -259,7 +389,8 @@ def main() -> None:
 
     print(
         "OK: T-19 testgen activation "
-        "(LBE + refinement-preservation + idempotent-operation + coproduct-exhaustiveness generated receipts)."
+        "(LBE + algebra-law + refinement-preservation + idempotent-operation + "
+        "coproduct-exhaustiveness generated receipts)."
     )
 
 

scripts/v4-mvp1-e2e-gate.sh

@@ -27,7 +27,7 @@
 #
 # Env:
 #   V2_COMPILER   — path to v2-compiler binary (default: target/release/v2-compiler)
-#   MVP1_OUT_DIR  — compile output directory (default: /tmp/v4-mvp1-out)
+#   MVP1_OUT_DIR  — compile output directory (default: unique /tmp/v4-mvp1-out.XXXXXX)
 
 set -euo pipefail
 
@@ -50,10 +50,19 @@ if [[ ! -f "${entry_root}/add.dag" ]]; then
   exit 1
 fi
 
-out="${MVP1_OUT_DIR:-/tmp/v4-mvp1-out}"
-log="${MVP1_LOG:-/tmp/v4-mvp1.log}"
-rm -rf "$out"
-mkdir -p "$out"
+cleanup_out=""
+if [[ -n "${MVP1_OUT_DIR:-}" ]]; then
+  out="$MVP1_OUT_DIR"
+  rm -rf "$out"
+  mkdir -p "$out"
+else
+  out="$(mktemp -d "${TMPDIR:-/tmp}/v4-mvp1-out.XXXXXX")"
+  cleanup_out="$out"
+fi
+if [[ -n "$cleanup_out" ]]; then
+  trap 'rm -rf "$cleanup_out"' EXIT
+fi
+log="${MVP1_LOG:-${out}/v4-mvp1.log}"
 
 echo "=== MVP-1: compile ${entry_root}/add.dag (--target rust) ==="
 set +e
@@ -141,12 +150,20 @@ echo "=== MVP-1: cargo build mvp1_gate ==="
 )
 
 echo "=== MVP-1: cargo run mvp1_gate (assert add(2,3)==5) ==="
+set +e
 run_out="$(
   cd "$out"
   cargo run --quiet --bin mvp1_gate 2>&1
 )"
+run_status=$?
+set -e
 echo "$run_out"
 
+if [[ "$run_status" -ne 0 ]]; then
+  echo "error: MVP-1 cargo run exited $run_status (output above)" >&2
+  exit "$run_status"
+fi
+
 if ! grep -q 'mvp1-ok: add(2, 3) = 5' <<<"$run_out"; then
   echo "error: MVP-1 run did not print expected receipt (got above)" >&2
   exit 1