diff --git a/src/v2/test/lens_application/sg_claims_test.dag b/src/v2/test/lens_application/sg_claims_test.dag index 25a4c60eb7e..85f7a94e44c 100644 --- a/src/v2/test/lens_application/sg_claims_test.dag +++ b/src/v2/test/lens_application/sg_claims_test.dag @@ -9,10 +9,6 @@ data lens_application_synthesis_root_declaration: DeclarationId = DeclarationId path: lens_application_synthesis_root_path } -test fn lens_application_introspect_advisory_holds() -> Bool { - apply_lens_introspect_rejection_is_advisory_claim_holds() -} - fn lens_application_synthesis_gap_enforce_rejects() -> Bool { match apply_advisory_lens( lens: decision_tree_synthesis_advisory_lens, @@ -31,10 +27,6 @@ fn lens_application_synthesis_gap_enforce_rejects() -> Bool { } } -test fn lens_application_synthesis_gap_polynomial_holds() -> Bool { - synthesis_gap_poly_lens_non_empty() -} - test fn lens_application_synthesis_gap_enforce_rejection_holds() -> Bool { lens_application_synthesis_gap_enforce_rejects() } diff --git a/src/v2/test/lens_cost/bounded_summation_test.dag b/src/v2/test/lens_cost/bounded_summation_test.dag index 8c8b2840b5b..2af7f8e829b 100644 --- a/src/v2/test/lens_cost/bounded_summation_test.dag +++ b/src/v2/test/lens_cost/bounded_summation_test.dag @@ -63,10 +63,14 @@ fn bounded_summation_projects_to_linear() -> Bool { } } -test fn bounded_summation_expr_authority_holds() -> Bool { +fn bounded_summation_expr_authority() -> Bool { bounded_summation_is_representable() && bounded_summation_projects_to_linear() } +test fn bounded_summation_expr_authority_holds() -> Bool { + bounded_summation_expr_authority() +} + test fn zero_body_loop_projects_to_zero_red_control() -> Bool { match normalize_cost_expr_to_symbolic( expr: cost_loop_expr( @@ -92,7 +96,7 @@ data claim_bounded_summation: TestClaim = EqualsClaim { label: "lens_cost/bounded_summation: CostSum with grounded binder is representable and projects to linear SymbolicCost", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), lhs: bounded_summation_bound_leaf, - rhs: if bounded_summation_expr_authority_holds() { + rhs: if bounded_summation_expr_authority() { bounded_summation_bound_leaf } else { Node { diff --git a/src/v2/test/lens_cost/p9_llvm_instruction_cost_registry_owner_test.dag b/src/v2/test/lens_cost/p9_llvm_instruction_cost_registry_owner_test.dag index 549417cd5d2..e7441e8abbb 100644 --- a/src/v2/test/lens_cost/p9_llvm_instruction_cost_registry_owner_test.dag +++ b/src/v2/test/lens_cost/p9_llvm_instruction_cost_registry_owner_test.dag @@ -28,5 +28,5 @@ fn p9_registry_canonical_row_count() -> Int { } test fn p9_registry_owner_receipt_holds() -> Bool { - p9_registry_fn_names_unique() && p9_registry_canonical_row_count() == 1 + p9_registry_canonical_row_count() == 1 } diff --git a/src/v2/test/lens_idempotency/sg_claims_test.dag b/src/v2/test/lens_idempotency/sg_claims_test.dag deleted file mode 100644 index 78af82e19e4..00000000000 --- a/src/v2/test/lens_idempotency/sg_claims_test.dag +++ /dev/null @@ -1,8 +0,0 @@ -module v2.test.lens_idempotency.sg_claims - - - -data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -test fn lens_idempotency_write_effect_holds() -> Bool { - idempotency_write_effect_claim_holds() -} diff --git a/src/v2/test/lens_structural_resolution/binds_to_resolved_test.dag b/src/v2/test/lens_structural_resolution/binds_to_resolved_test.dag index f35d544fd81..b119b302165 100644 --- a/src/v2/test/lens_structural_resolution/binds_to_resolved_test.dag +++ b/src/v2/test/lens_structural_resolution/binds_to_resolved_test.dag @@ -75,4 +75,3 @@ test fn binds_to_resolved_claim_holds() -> Bool { } } -data binds_to_resolved_claim_passes: Bool = binds_to_resolved_claim_holds() diff --git a/src/v2/workflow/floor_grandfathered_roster.dag b/src/v2/workflow/floor_grandfathered_roster.dag index e87a7e6230d..d55df8e92ff 100644 --- a/src/v2/workflow/floor_grandfathered_roster.dag +++ b/src/v2/workflow/floor_grandfathered_roster.dag @@ -180,6 +180,18 @@ data floor_grandfathered_removals: List = [ identity: "test.claim.bare_name_fork_lens_witness_test.two_declarations_of_one_name_inside_the_subject_are_not_a_fork_with_itself" as NonEmptyStr, deleted_in: "gunbc#11286: the declaration-grained lens it exercised (gunbc.bare_name_fork_lens) is deleted with its check instrument, after the floor's bare-name invariant was repointed at the read-grained detector (claim_scope_for, AmbiguousBareNameRead); the coverage this row carried -- a fork of one bare name across two declarers -- is not the defect, and the defect's own red is test.claim.bare_name_ambiguity_wall_witness_test" as NonEmptyStr, }, + WitnessDeleted { + identity: "v2.test.lens_application.sg_claims.lens_application_introspect_advisory_holds" as NonEmptyStr, + deleted_in: "it only re-asserted the enrolled v2.test.lens_application.apply_lens_introspect_rejection_is_advisory.apply_lens_introspect_rejection_is_advisory_claim_holds by calling it, and no code may reference a test fn (owner ruling 2026-09-16/17); the fact stays asserted by that claim" as NonEmptyStr, + }, + WitnessDeleted { + identity: "v2.test.lens_application.sg_claims.lens_application_synthesis_gap_polynomial_holds" as NonEmptyStr, + deleted_in: "it only re-asserted the enrolled v2.test.lens_synthesis.synthesis_gap_polynomial.synthesis_gap_poly_lens_non_empty by calling it, and no code may reference a test fn (owner ruling 2026-09-16/17); the fact stays asserted by that claim" as NonEmptyStr, + }, + WitnessDeleted { + identity: "v2.test.lens_idempotency.sg_claims.lens_idempotency_write_effect_holds" as NonEmptyStr, + deleted_in: "it only re-asserted the enrolled v2.test.lens_idempotency.write_effect.idempotency_write_effect_claim_holds by calling it, and no code may reference a test fn (owner ruling 2026-09-16/17); the fact stays asserted by that claim" as NonEmptyStr, + }, WitnessDeleted { identity: "v2.test.claim.generated_conformance_floor.generated_lbe_conj_snapshot_passes" as NonEmptyStr, deleted_in: "gunbc test-reference cleanup (gates, generated, compiler, imports area): a test fn that only re-asserted the enrolled test data v2.test.generated.language_behavior_equivalence.witness_lbe_conj_snapshot_pass; the fact stays enrolled at its declaration" as NonEmptyStr,