Skip to content
Merged
Show file tree
Hide file tree
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
8 changes: 0 additions & 8 deletions src/v2/test/lens_application/sg_claims_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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()
}
8 changes: 6 additions & 2 deletions src/v2/test/lens_cost/bounded_summation_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand All @@ -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 {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
8 changes: 0 additions & 8 deletions src/v2/test/lens_idempotency/sg_claims_test.dag

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -75,4 +75,3 @@ test fn binds_to_resolved_claim_holds() -> Bool {
}
}

data binds_to_resolved_claim_passes: Bool = binds_to_resolved_claim_holds()
12 changes: 12 additions & 0 deletions src/v2/workflow/floor_grandfathered_roster.dag
Original file line number Diff line number Diff line change
Expand Up @@ -180,6 +180,18 @@ data floor_grandfathered_removals: List<GrandfatheredRemoval> = [
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,
Expand Down
Loading