Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
210 changes: 210 additions & 0 deletions src/v2/test/claim/generated_conformance_floor_test.dag
Original file line number Diff line number Diff line change
@@ -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<TestClaim>) -> 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()
}
Loading