Skip to content

Fix Swift recovery replay checkpoint correctness - #967

Merged
odvcencio merged 2 commits into
mainfrom
codex/swift-576-partial-correctness-20260824
Aug 24, 2026
Merged

Fix Swift recovery replay checkpoint correctness#967
odvcencio merged 2 commits into
mainfrom
codex/swift-576-partial-correctness-20260824

Conversation

@odvcencio

@odvcencio odvcencio commented Aug 24, 2026

Copy link
Copy Markdown
Owner

Summary

  • Replay recovery lookaheads from the exact skipped-prefix offset after all alignment proofs pass.
  • Record complete Swift scanner checkpoints across failed scans and incremental fast-forward.
  • Reset recovery and pooled scratch state at each required lifecycle boundary.

Correctness

The 20-byte let x = unsafe bar() witness now matches locked C.

These large witnesses still differ from locked C:

  • stdlib_FloatingPointToString.swift
  • stdlib_CollectionAlgorithms.swift

Keep issue #576 open.

All focused Docker gates pass. They cover:

  • The generic relex contract and scanner transitions
  • The pooled Swift minimal witness and clean-to-large sequence
  • Both large Swift telemetry witnesses
  • The pinned AWK recovery control
  • The parser memory contract

CI repair

External scanners now restore their start state after a terminal failed scan by default. Swift explicitly retains its required failed-scan state.

Generic relex rejects a synthetic end-of-file token before the source end. The Swift repair preserves a trailing custom_operator token.

Temporary CNode memo growth now restores an existing warm standard slab. A shorter retained slab stays short.

These exact private Docker gates pass:

  • Templ TestDispatcherArmCensusA0Manifest
  • Swift TestSwiftOptionalGenericCloseDoesNotStarveCustomOperator/trailing_after_function
  • Race TestCNodeMemoTemporaryTierLivesForParseOperation
  • Race TestMarkdownIncrementalScannerCertification/256KiB/replace/middle, with 73424/262341 bytes reused

Public continuous integration for exact head d5c38cd8a06be1ae2a980b0d081927bb20064baf is pending.

Performance

The original 20-seed randomized benchmark geometric mean improves 3.57 percent. Bytes per operation and allocations per operation stay unchanged.

One original warmed before sample uses 594240 KiB. One original warmed after sample uses 597160 KiB. The observed increase is 0.491384 percent.

For the CI repair, the primary trio median geomean changes by +1.242879 percent across 20 randomized seeds. Each p-value exceeds 0.60. Bytes and allocations per operation stay unchanged.

The repair's warmed large-witness sample changes from 565920 KiB to 565280 KiB.

- Replay deterministic finite automaton recovery tokens from the exact skipped-prefix offset only after span, state, and error-mode proofs succeed
- Preserve complete external scanner checkpoints across failed scans and incremental fast-forward so recovery and relex use the correct scanner state
- Reset recovery memo and merge scratch state at operation and pool boundaries to prevent stale state and undersized reservations from affecting later parses
- Add focused parser, scanner, pooled Swift parity, and checkpoint tests; document the verified minimal witness while keeping the larger issue #576 corpus mismatches open

Refs #576

Buckley-Change-Hash: sha256:b526b18c7bec50bf500aa7168627c37b3f42608df00dbe8f0b97131904899381
Buckley-Change-Stats: files=23 insertions=1184 deletions=113 binaries=0
- Restore external scanner state after failed scans by default, while supporting explicit state retention for scanners such as Swift.
- Reject synthetic end-of-file relex substitutions and limit Swift operator deferral to scopes with an unmatched opening angle.
- Preserve the standard recovery memo slab across temporary growth without expanding shorter retained slabs.
- Add regression coverage and document the parity, correctness, and performance results for the repair.

Refs #576

Buckley-Change-Hash: sha256:cd235a3257c774f7353d9f62de58b8b69dc95b19a6eb205a7175b1b8288c1db1
Buckley-Change-Stats: files=12 insertions=436 deletions=28 binaries=0
@odvcencio
odvcencio merged commit c25686c into main Aug 24, 2026
49 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant