From a9b755a7d0cbd6277d06b5da385fb2468590daf3 Mon Sep 17 00:00:00 2001 From: Codex Date: Fri, 3 Apr 2026 22:43:56 +0000 Subject: [PATCH 1/2] Implement PR11.10d container proof closure --- docs/PR11.x-series-proposed.md | 7 +++-- docs/emitted_output_verification_matrix.md | 36 ++++++++++++++++++++++ scripts/_lib/proof_inventory.py | 9 +++++- scripts/run_proofs.py | 17 ++++++++++ 4 files changed, 66 insertions(+), 3 deletions(-) diff --git a/docs/PR11.x-series-proposed.md b/docs/PR11.x-series-proposed.md index 1f5c7efe..f7d6d1c0 100644 --- a/docs/PR11.x-series-proposed.md +++ b/docs/PR11.x-series-proposed.md @@ -2065,8 +2065,11 @@ Standard-library proof checkpoint for the container surface. dereference through the implementation layer. - Add companion emission templates for the container instantiation pattern if the existing template set does not cover the new shapes. -- Absorb all new container fixtures into the blocking proof inventory - with zero unnamed uncovered fixtures. +- Close the parent container checkpoint as the explicit union of the + proof-backed `PR11.10a`, `PR11.10b`, and `PR11.10c` manifests. +- Allow named documented runtime-only exclusions when GNATprove still + rejects an admitted witness for tool-specific reasons, but keep zero + unnamed uncovered fixtures in the proof inventory. - Update the verification matrix and proof inventory. ### Dependency diff --git a/docs/emitted_output_verification_matrix.md b/docs/emitted_output_verification_matrix.md index 8e62b54e..c4a05555 100644 --- a/docs/emitted_output_verification_matrix.md +++ b/docs/emitted_output_verification_matrix.md @@ -104,6 +104,7 @@ subset remain outside the current surface; see | PR11.8g.1 build-surface proof-expansion set | `tests/build/pr118c2_package_pre_task.safe`, `tests/build/pr118d1_for_of_string_build.safe`, `tests/build/pr118d1_string_case_build.safe`, `tests/build/pr118d1_string_order_build.safe`, `tests/build/pr118d_bounded_string_array_component_build.safe`, `tests/build/pr118d_bounded_string_index_build.safe`, `tests/build/pr118d_bounded_string_tick_build.safe`, `tests/build/pr118d_for_of_fixed_build.safe`, `tests/build/pr118d_for_of_growable_build.safe`, `tests/build/pr118d_for_of_heap_element_build.safe` | PR11.8g.1 also widens the blocking lane across proof-friendly emitted build/package representatives. The live emitted surface now includes a named post-PR11.8d build subset rather than leaving these fixtures in an implicit “accepted but not proved” bucket. | yes | yes | yes | yes | yes | none | no | | Heap-backed runtime-backed string/growable surface | `tests/positive/pr118d_bounded_string.safe`, `tests/positive/pr118d_character_quote_literal.safe`, `tests/positive/pr118d_growable_array.safe`, `tests/positive/pr118d_string_length_attribute.safe`, `tests/positive/pr118d_string_mutable_object.safe`, `tests/build/pr118d1_growable_to_fixed_guard_build.safe`, `tests/build/pr118d_bounded_string_build.safe`, `tests/build/pr118d_bounded_string_field_build.safe`, `tests/build/pr118d_fixed_to_growable_build.safe`, `tests/build/pr118d_growable_to_fixed_literal_build.safe`, `tests/build/pr118d_growable_to_fixed_slice_build.safe` | PR11.8g.2 moved string/growable runtime support onto the shared proved runtime seam. PR11.8g.4 then made that seam generically honest by weakening shared `Safe_Array_RT` to length-only facts and routing non-heap growable-array component types through the stronger `Safe_Array_Identity_Ops` + `Safe_Array_Identity_RT` path where element-preservation is actually justified. | yes | yes | yes | yes | yes | none | no | | Fixed-width binary emitted surface | `tests/positive/pr118c_binary_boolean_logic.safe`, `tests/positive/pr118c_binary_conversion_wrap.safe`, `tests/positive/pr118c_binary_inline_object.safe`, `tests/positive/pr118c_binary_named_type.safe`, `tests/positive/pr118c_binary_param_return.safe`, `tests/positive/pr118c_binary_shift.safe` | PR11.8i.1 completes the second emitted-proof expansion pass by absorbing the remaining fixed-width binary fixtures into the blocking proof manifest alongside the earlier case-dispatch representative. The emitted numeric surface is now explicit and fully covered rather than tracked as post-PR11.8g.1 cleanup debt. | yes | yes | yes | yes | yes | none | no | +| Built-in container checkpoint surface | `tests/positive/pr1110a_optional_guarded.safe`, `tests/positive/pr1110b_list_basics.safe`, `tests/positive/pr1110c_map_basics.safe`, plus the build-backed `pr1110a*`, `pr1110b*`, and `pr1110c*` fixtures in `scripts/_lib/proof_inventory.py` | PR11.10a/PR11.10b/PR11.10c close the shipped optional/list/map surface under blocking emitted proof manifests, and PR11.10d ratifies that union as the parent container checkpoint. The only retained gap is the named runtime-only witness `tests/build/pr1110b_list_empty_build.safe`, which remains an explicit proof exclusion rather than an unnamed coverage hole. | yes | yes | yes | yes | yes | named documented exclusion for the empty-list `pop_last` witness only | no | | Shared `IO` seam representative | `tests/positive/pr118c1_print.safe` | `print` now lowers through the shared standard-library `IO` package instead of per-unit generated wrappers. PR11.8g.2 includes that seam in the blocking emitted-proof lane, so emitted packages no longer rely on excluded `_safe_io` helper bodies. | yes | yes | yes | yes | yes | none | no | ## PR10.2 Rule 5 Boundary Closure @@ -320,6 +321,41 @@ all-proved-only policy as the earlier checkpoints, including the linked-list observer and accumulator traversal representatives after PR11.8f.1's structural cursor-loop lowering. +## PR11.10 Container Checkpoint Corpus + +PR11.10d closes the parent container milestone as the explicit union of the +three shipped container wedges: + +- `PR11.10a` optional checkpoint: + - `tests/positive/pr1110a_optional_guarded.safe` + - `tests/build/pr1110a_optional_string_build.safe` + - `tests/build/pr1110a_optional_growable_build.safe` +- `PR11.10b` list checkpoint: + - `tests/positive/pr1110b_list_basics.safe` + - `tests/positive/pr1110b_disjoint_mut_indices.safe` + - `tests/build/pr1110b_list_build.safe` + - `tests/build/pr1110b_list_string_build.safe` + - `tests/build/pr1110b_list_growable_build.safe` +- `PR11.10c` map checkpoint: + - `tests/positive/pr1110c_map_basics.safe` + - `tests/build/pr1110c_map_build.safe` + - `tests/build/pr1110c_map_string_build.safe` + - `tests/build/pr1110c_map_list_build.safe` + +This exact parent checkpoint is mirrored in `scripts/_lib/proof_inventory.py` +and summarized by `python3 scripts/run_proofs.py` as `PR11.10d checkpoint`. + +The parent checkpoint is closed under the same all-proved-only policy as the +earlier emitted checkpoints. It keeps one named runtime-only exclusion: + +- `tests/build/pr1110b_list_empty_build.safe` + +That empty-list `pop_last` witness remains in the runtime/build lane, but its +statically empty lowering still triggers GNATprove ineffectual-branch warnings +under `--warnings=error`. The fixture is therefore retained as an explicit +proof exclusion with documented owner/reason metadata rather than treated as an +unnamed coverage hole. + ## Emitted GNATprove Warning Suppression Inventory The emitter generates narrowly scoped `pragma Warnings (GNATprove, Off, "")` / diff --git a/scripts/_lib/proof_inventory.py b/scripts/_lib/proof_inventory.py index e1029c2f..3bebb6a9 100644 --- a/scripts/_lib/proof_inventory.py +++ b/scripts/_lib/proof_inventory.py @@ -199,6 +199,13 @@ class EmittedProofExclusion: ] +PR11_10D_CHECKPOINT_FIXTURES = ( + PR11_10A_CHECKPOINT_FIXTURES + + PR11_10B_CHECKPOINT_FIXTURES + + PR11_10C_CHECKPOINT_FIXTURES +) + + PR11_8I1_CHECKPOINT_FIXTURES = [ "tests/positive/pr115_case_terminator.safe", "tests/positive/pr115_var_basic.safe", @@ -300,7 +307,7 @@ class EmittedProofExclusion: path="tests/build/pr1110b_list_empty_build.safe", reason="runtime-only empty pop_last witness; static empty-length lowering triggers GNATprove ineffectual-branch warnings", owner="runtime-regression-only", - milestone="PR11.10b", + milestone="PR11.10d", ), ] diff --git a/scripts/run_proofs.py b/scripts/run_proofs.py index 9b38df67..7335ee9d 100644 --- a/scripts/run_proofs.py +++ b/scripts/run_proofs.py @@ -31,6 +31,7 @@ PR11_10A_CHECKPOINT_FIXTURES, PR11_10B_CHECKPOINT_FIXTURES, PR11_10C_CHECKPOINT_FIXTURES, + PR11_10D_CHECKPOINT_FIXTURES, PROOF_COVERAGE_ROOTS, iter_proof_coverage_paths, ) @@ -80,6 +81,7 @@ def validate_manifests() -> None: validate_manifest("PR11.10a checkpoint manifest", PR11_10A_CHECKPOINT_FIXTURES) validate_manifest("PR11.10b checkpoint manifest", PR11_10B_CHECKPOINT_FIXTURES) validate_manifest("PR11.10c checkpoint manifest", PR11_10C_CHECKPOINT_FIXTURES) + validate_manifest("PR11.10d checkpoint manifest", PR11_10D_CHECKPOINT_FIXTURES) validate_manifest("emitted proof regression manifest", EMITTED_PROOF_REGRESSION_FIXTURES) validate_manifest("emitted proof manifest", EMITTED_PROOF_FIXTURES) validate_manifest( @@ -219,6 +221,8 @@ def main() -> int: checkpoint_10b_failures: list[tuple[str, str]] = [] checkpoint_10c_passed = 0 checkpoint_10c_failures: list[tuple[str, str]] = [] + checkpoint_10d_passed = 0 + checkpoint_10d_failures: list[tuple[str, str]] = [] regression_passed = 0 regression_failures: list[tuple[str, str]] = [] @@ -303,6 +307,13 @@ def main() -> int: toolchain=toolchain, ) + checkpoint_10d_passed = ( + checkpoint_10a_passed + checkpoint_10b_passed + checkpoint_10c_passed + ) + checkpoint_10d_failures = ( + checkpoint_10a_failures + checkpoint_10b_failures + checkpoint_10c_failures + ) + total_passed = ( companion_passed + checkpoint_a_passed @@ -414,6 +425,12 @@ def main() -> int: title="PR11.10c checkpoint", trailing_blank_line=True, ) + print_summary( + passed=checkpoint_10d_passed, + failures=checkpoint_10d_failures, + title="PR11.10d checkpoint", + trailing_blank_line=True, + ) print_summary( passed=regression_passed, failures=regression_failures, From 66a2a41409d6be0cbabf085313e0cc0b7befc9e3 Mon Sep 17 00:00:00 2001 From: Codex Date: Fri, 3 Apr 2026 22:51:44 +0000 Subject: [PATCH 2/2] Clarify PR11.10d checkpoint scope --- docs/PR11.x-series-proposed.md | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/docs/PR11.x-series-proposed.md b/docs/PR11.x-series-proposed.md index f7d6d1c0..60af6251 100644 --- a/docs/PR11.x-series-proposed.md +++ b/docs/PR11.x-series-proposed.md @@ -2057,20 +2057,18 @@ Standard-library proof checkpoint for the container surface. ### Scope -- Add blocking proof fixtures for `optional T`, `list of T`, and - `map of (K, V)` covering construction, access, mutation, and - scope-exit cleanup. -- Prove that container operations preserve the D27 rules: no overflow - in length/index arithmetic, no out-of-bounds access, no null - dereference through the implementation layer. -- Add companion emission templates for the container instantiation - pattern if the existing template set does not cover the new shapes. -- Close the parent container checkpoint as the explicit union of the +- Ratify the parent container checkpoint as the explicit union of the proof-backed `PR11.10a`, `PR11.10b`, and `PR11.10c` manifests. +- Treat those shipped fixtures as the authoritative proof-backed + coverage for the admitted `optional`, `list`, and `map` surface, + including the D27 obligations they already exercise. - Allow named documented runtime-only exclusions when GNATprove still rejects an admitted witness for tool-specific reasons, but keep zero unnamed uncovered fixtures in the proof inventory. -- Update the verification matrix and proof inventory. +- Update the proof runner, verification matrix, and proof inventory so + the parent checkpoint and its named exclusions are stated explicitly. +- Leave the companion/template side unchanged unless a concrete + container modeling gap is discovered while refreshing the checkpoint. ### Dependency