diff --git a/src/v2/test/claim/generated_conformance_floor_test.dag b/src/v2/test/claim/generated_conformance_floor_test.dag new file mode 100644 index 00000000000..6b6d8c914f0 --- /dev/null +++ b/src/v2/test/claim/generated_conformance_floor_test.dag @@ -0,0 +1,210 @@ +// Floor gate for testgen generated output (docs/plans/testgen-oracle.md ยง4.1, faces #1+#2). +// +// Face #1 (coverage by illusion): every module under src/v2/compiler/generated/ has zero +// `test fn` and is not `*_test.dag`, so the witness floor discovered+ran NONE of them โ€” the +// only execution path was the ungated Rust subset. This file surfaces the witnesses the +// generator ALREADY emits into the floor by naming them in a discovered `*_test.dag`, one +// `test fn` per generated witness. No new generator logic: each `test fn` is a single +// reference to the generated authority (single-representation โ€” the generated decl IS the +// fact, this is only its floor entry point). +// +// Face #2 (parallel-representation drift): the generated modules call the live generator +// (`v2.lens.testgen.testgen_emit_*`) at evaluation time rather than freezing its output, so +// compiling + running them here makes any generator/generated drift unwritable โ€” a record-shape +// fork (the ๐ŸŸก `NatAlgebraLawObligation โ‡„ AlgebraLawSubject` risk) fails the floor as a compile +// error or a RED witness, the same closure CiYamlGate gives ci.yml. +// +// Falsifier: revert/break any generated witness or a generator emit shape it exercises โ‡’ the +// matching `test fn` goes RED in the floor. + +module v2.test.claim.generated_conformance_floor + +import v2.std.logic { Bool } +import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.verification { TestClaim } + +import v2.test.generated.algebra_law_conformance { + generated_algebra_law_sample_count_is_three, + generated_nat_add_left_identity_claim, + generated_nat_add_associativity_claim, + generated_nat_mul_annihilator_claim +} +import v2.test.generated.coproduct_exhaustiveness { + witness_coproduct_exhaustiveness_diagnostic_claim, + witness_coproduct_exhaustiveness_uses_generated_anchor, + witness_coproduct_exhaustiveness_all_variants_emit, + witness_coproduct_exhaustiveness_generator_count +} +import v2.test.generated.refinement_preservation { + witness_refinement_preserves_nonempty_list_base, + witness_refinement_preservation_subject_anchor, + witness_refinement_preservation_scheduler_emits_one_generator, + claim_refinement_nonempty_list_base_preserved +} +import v2.test.generated.language_behavior_equivalence { + witness_lbe_conj_snapshot_pass, + witness_lbe_disj_snapshot_pass, + witness_lbe_transform_snapshot_pass, + witness_testgen_schedules_three_lbe_generators, + witness_dag_surface_language_identity +} +import v2.test.generated.witness_validity { + row_witness_validity_constraint_satisfaction_holds, + row_witness_validity_property_symbol_mismatch, + row_witness_validity_evidence_node_mismatch, + row_witness_validity_rule_not_realized +} +import v2.test.generated.idempotent_operation_conformance { + generated_label_only_skip_pins_rejection, + witness_read_idempotent_operation_run_non_pass, + witness_upsert_idempotent_operation_run_non_pass, + witness_delete_idempotent_operation_run_non_pass, + witness_create_if_absent_idempotent_operation_run_non_pass, + generated_idempotent_operation_sample_count_is_four, + generated_idempotent_operation_scheduled_subject_count_is_four, + generated_idempotent_operation_run_count_is_four +} +import v2.test.generated.testgen_category_wishlist { + pending_non_tautological_generator_count_is_three, + dispatched_non_tautological_generator_count_is_four +} + +// A generated claim row is well-formed iff the live generator emitted it (Accepted), not a +// Rejected emit. Discriminating: break the generator's emit and the row flips to Rejected โ‡’ RED. +fn generated_claim_emitted(o: Outcome) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +// --- AlgebraLawConformance (structural โ€” nat_declared_algebra_law_obligations) --- +test fn generated_algebra_law_sample_count_holds() -> Bool { + generated_algebra_law_sample_count_is_three() +} + +test fn generated_algebra_law_left_identity_emits() -> Bool { + generated_claim_emitted(o: generated_nat_add_left_identity_claim) +} + +test fn generated_algebra_law_associativity_emits() -> Bool { + generated_claim_emitted(o: generated_nat_add_associativity_claim) +} + +test fn generated_algebra_law_annihilator_emits() -> Bool { + generated_claim_emitted(o: generated_nat_mul_annihilator_claim) +} + +// --- CoproductExhaustiveness --- +test fn generated_coproduct_exhaustiveness_is_diagnostic() -> Bool { + witness_coproduct_exhaustiveness_diagnostic_claim +} + +test fn generated_coproduct_exhaustiveness_anchor_holds() -> Bool { + witness_coproduct_exhaustiveness_uses_generated_anchor +} + +test fn generated_coproduct_exhaustiveness_all_variants_emit() -> Bool { + witness_coproduct_exhaustiveness_all_variants_emit +} + +test fn generated_coproduct_exhaustiveness_generator_count_holds() -> Bool { + witness_coproduct_exhaustiveness_generator_count +} + +// --- RefinementPreservation --- +test fn generated_refinement_preserves_nonempty_list_base() -> Bool { + witness_refinement_preserves_nonempty_list_base +} + +test fn generated_refinement_subject_anchor_holds() -> Bool { + witness_refinement_preservation_subject_anchor +} + +test fn generated_refinement_scheduler_emits_one_generator() -> Bool { + witness_refinement_preservation_scheduler_emits_one_generator +} + +test fn generated_refinement_claim_emits() -> Bool { + generated_claim_emitted(o: claim_refinement_nonempty_list_base_preserved) +} + +// --- LanguageBehaviorEquivalence --- +test fn generated_lbe_conj_snapshot_passes() -> Bool { + witness_lbe_conj_snapshot_pass +} + +test fn generated_lbe_disj_snapshot_passes() -> Bool { + witness_lbe_disj_snapshot_pass +} + +test fn generated_lbe_transform_snapshot_passes() -> Bool { + witness_lbe_transform_snapshot_pass +} + +test fn generated_lbe_schedules_three_generators() -> Bool { + witness_testgen_schedules_three_lbe_generators +} + +test fn generated_lbe_dag_surface_language_identity() -> Bool { + witness_dag_surface_language_identity +} + +// --- WitnessValidity (RoundTripClaim โ€” emission Accepted; run Deferred until eval lands) --- +test fn generated_witness_validity_constraint_satisfaction_emits() -> Bool { + generated_claim_emitted(o: row_witness_validity_constraint_satisfaction_holds) +} + +test fn generated_witness_validity_property_symbol_mismatch_emits() -> Bool { + generated_claim_emitted(o: row_witness_validity_property_symbol_mismatch) +} + +test fn generated_witness_validity_evidence_node_mismatch_emits() -> Bool { + generated_claim_emitted(o: row_witness_validity_evidence_node_mismatch) +} + +test fn generated_witness_validity_rule_not_realized_emits() -> Bool { + generated_claim_emitted(o: row_witness_validity_rule_not_realized) +} + +// --- IdempotentOperationConformance --- +test fn generated_idempotent_label_only_skip_pins_rejection() -> Bool { + generated_label_only_skip_pins_rejection +} + +test fn generated_idempotent_read_run_non_pass() -> Bool { + witness_read_idempotent_operation_run_non_pass +} + +test fn generated_idempotent_upsert_run_non_pass() -> Bool { + witness_upsert_idempotent_operation_run_non_pass +} + +test fn generated_idempotent_delete_run_non_pass() -> Bool { + witness_delete_idempotent_operation_run_non_pass +} + +test fn generated_idempotent_create_if_absent_run_non_pass() -> Bool { + witness_create_if_absent_idempotent_operation_run_non_pass +} + +test fn generated_idempotent_sample_count_holds() -> Bool { + generated_idempotent_operation_sample_count_is_four() +} + +test fn generated_idempotent_scheduled_subject_count_holds() -> Bool { + generated_idempotent_operation_scheduled_subject_count_is_four() +} + +test fn generated_idempotent_run_count_holds() -> Bool { + generated_idempotent_operation_run_count_is_four() +} + +// --- TestgenCategoryWishlist --- +test fn generated_wishlist_pending_count_holds() -> Bool { + pending_non_tautological_generator_count_is_three() +} + +test fn generated_wishlist_dispatched_count_holds() -> Bool { + dispatched_non_tautological_generator_count_is_four() +}