[codex] Implement PR11.10d container proof closure

docs/PR11.x-series-proposed.md

@@ -2057,17 +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.
-- Absorb all new container fixtures into the blocking proof inventory
-  with zero unnamed uncovered fixtures.
-- Update the verification matrix and proof inventory.
+- 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 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
 

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, "<pattern>")` /

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",
     ),
 ]
 

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,