FV: corrected-dependency SHA-256 constructor and Digest correspondence

The owner selected the corrected dependency on 2026-10-30 for the next SHA-256/Digest proof work, following #1095 and the source-target decision recorded on #1067.

The selected chain is sha2 0.10.9 -> digest 0.10.7 -> block-buffer 0.10.4 -> generic-array 0.14.7, with the exact correction already reviewed in #1090 (generic-array.patch SHA-256 58f09226434661ea5ee27f80979aa61390e1e83e76ddcb2fd0a368b057dec18d). This is a research-only target. The production dependency remains unchanged, and #1067 remains open for its original-source acceptance criterion.

Acceptance requires source-bound corrected constructor/default/generate behavior, actual corrected Digest caller composition with explicit target/configuration and dependencies, and streaming/length/padding/output correspondence. Component proofs and finite compatibility tests do not close full Digest or unrestricted-input obligations. Keep compiler/memory-model trust, callbacks, cross-tool refinement and cryptographic assumptions explicit.

The landed bounded batch authenticates the correction and runtime, verifies the actual U32/U64 byte-array constructor shapes and generated-byte order, checks initialized-prefix cleanup under deliberate generator panics, and inspects the corrected full caller's frontend feasibility. All default, uninitialized-memory, valid-value and unwind guards stay enabled. Negative controls must fail the intended consumer checks; setup failure or timeout is not accepted.

The constructor component landed through #1098 at 206bbd3113e7d2621ae246c5f1bde060ac1975c4 on 2026-10-30. Its merged tree exactly matches the final reviewed candidate. Astra ultra and Opus 5.5 xhigh both returned GO with all mandatory checks answered; no Kimi or optional extra reviewers were used. All six final-candidate PR workflows passed. All four post-merge workflows also passed on the exact merge commit, including general CI (QEMU and Miri), Lean FV, workflow security and recorded constructor evidence; the PR-only advisory dependency-review job is inapplicable/skipped on the push event. The retained proof outputs, causal controls, finite cleanup evidence, fresh replay entrypoint, 13 regression groups and CI authentication are published in contracts/verification/sha256-constructor/.

Accepted component evidence:

U32/U64 byte defaults: 313 properties (300 successful, 12 unreachable, one satisfied cover).
Arbitrary 64-byte observing generation: 265 properties (258 successful, six unreachable, one satisfied cover), including byte values, exactly 64 calls and increasing index order.
Byte corruption and reversed generation fail only their intended assertions. A paired U1 diagnostic passes for the correction and exposes initialization-check failures for the original dependency; no full original-source theorem is claimed.
Fresh isolated native and recursive-Miri cleanup runs pass all 110 finite cases. The wrong-prefix-drop control fails its intended assertion. Source inventories and actual Miri run-info bind the runs to the correct source. Superseded stale-cache cleanup receipts remain preserved without current evidence credit.

Remaining work keeps this issue open:

The source-preserving copy-on-write graph compiler is now accepted for private research after C1–C4 gates and all required implementation-review checks. Corrected full-caller translation completes in 66.21 active seconds; this is translation feasibility, not a proof. The first full-caller solver diagnostic has now completed on empty input and exposed an opaque raw-read model refusal before the digest assertions; see the 2026-10-31 diagnosis below. Full Digest composition remains open.
Complete corrected Digest composition, general source-level streaming/accumulated length/padding/output correspondence, unrestricted inputs and arbitrary closures remain open.
Compiler/memory-model soundness, alias/provenance and cross-tool correspondence remain explicit assumptions/gaps. Finite cleanup tests do not establish universal panic/unwind equivalence.
Optional follow-ups banked from review: a generator-value/write-position control; tighter checks of historical per-receipt resource limits and runner identity; separately retained collector traceback. These were not merge blockers. The older padding replay's terminal resource-check fix is tracked separately in FV: enforce terminal resource limits in the padding replay entrypoint #1099.

The published workflow authenticates recorded evidence and does not rerun a solver. Production dependencies remain unchanged, #1067 retains its original-source criterion, and no hardware or production adoption is authorized by this issue.

Local plan and exact receipts: /home/nicola/.local/state/pqsigner-research/easycrypt-full-digest-20261028/corrected-digest/. The existing 6 GiB aggregate research cap remains enforced. Parent research track: #100; original-source blocker: #1067.

Post-merge CI receipts: general CI, Lean FV, constructor evidence, workflow security. The earlier PR-only advisory dependency-review check remains unavailable because the repository Dependency graph is disabled; it was not counted as a successful individual check.

Translation-cost investigation (2026-10-30)

The first source-preserving diagnosis is complete. Initial compiler reachability
finishes in about 0.1 seconds; a bounded debugger stack sample places the delay
inside nested points-to fixpoint analysis and graph joins, before delayed-UB
instrumentation completes. The already-present upstream cyclic ancestor-walk
fix (#4898 in model-checking/kani) covers a later stage and does not resolve this
observed bottleneck.

Separate copy-elision-only and host opt-level2 comparisons also exhausted the
same 175 CPU-second budget. A shadow diagnostic that still recomputed every
result recorded 147,456 calls at its last sample, including 20,211 exact matches
among 26,650 eligible small input contexts. These are bounded sampling statistics,
not a universal reuse rate or a proof.

A bounded completed-context cache was then selected and independently reviewed
by Astra ultra and Opus 5.5 xhigh. Both gave architecture-only GO on plan commit
d7e12c2db3eb5bf857081ff3a2c9da8663bf037c, after the stopping rule and differential
controls were tightened. Its isolated implementation
27fdf04d308abc158c344714ecba385b2a431b8f passed all 50 compiler unit tests,
including 83,521 finite full-graph key pairs. Three weakened-key variants
(instance-only, omitted ancestors, dropped statics) failed the intended
wrong-hit assertions.

The sole full-caller feasibility trial still ended with SIGXCPU at 175 CPU
seconds (175.96 active seconds), before complete translation artifacts existed.
No solver ran. This candidate is stopped and unadopted; no longer retry or quota
tuning is authorized by that experiment's plan. Its mandatory C2 differential
and C4 compiler/consumer adoption gates were not completed, and no implementation
GO or compiler-soundness claim is made. The accepted installed compiler remains
unchanged. Source, logs, receipts and the experimental binary are retained; the
binary is compressed with a verified SHA-256 round trip under the existing
6 GiB aggregate research cap.

The next route must start from this evidence and a fresh bounded Phase A/B
selection. Full corrected Digest composition, streaming/length/padding/output
correspondence and the stated compiler/model assumptions remain open.

Copy-on-write representation candidate (2026-10-30)

Starting from the accepted analysis, a separate representation-only candidate
shares immutable per-node successor/ancestor sets and copies them before writes.
It contains none of the stopped completed-context cache and changes no analysis,
call-resolution, target-extraction, instrumentation, or model guards. C1 production candidate
efd9a763ae1da042800dcf6827fd33cef450e80d (tree
9021213b1a6da8ba3fa5bc3f7241bbe5e8e233a8) supplied the exact compiler subsequently accepted for private research in the final milestone below.

C1 passed all 49 compiler unit tests, including 83,521 finite join pairs,
4,624 extension cases and 1,156 query/closure cases. All five deliberate graph
mutation/change-flag controls failed their intended assertions. Package Clippy
passed; existing Cargo manifest notices remain in logs. Architecture review
records remain honest: Astra GO, Opus FIX with the coordinator's required flag
controls and memory-limit conditions subsequently evidenced; this is not an
implementation or adoption GO.

The first full-caller COW attempt was interrupted by the aggregate storage
reserve after code generation, before final metadata, and remains a failed
attempt. After retiring inactive regenerated build intermediates, one separately
selected retry used the identical source, compiler bytes, dependencies and
limits. It exited zero in 66.21 active seconds (64.78 child-execution seconds),
producing all required metadata, model, type/name maps, full instrumented MIR
and DOT output. Peak sampled RSS was about 865 MB. The limits remain 175/180 CPU
seconds, 180 active seconds, 16 MiB per output, 8 GiB address space and 6 GiB
aggregate research allocation. No full-caller solver ran.

C3 is complete: two original-compiler diagnostic runs first established
byte-identical full graphs (all keys and both adjacency directions) and complete
instrumented MIR for ten bounded fixtures. The COW diagnostic matches both
exactly. All verification-export fields also match after excluding timing fields
only. Five positive fixtures pass; the intended uninitialized-read and false-
assertion controls fail; existing boolean tracking, boxed-overlap and static-
reference limitations remain unchanged. The boolean tracking finding is banked
in #1101. Heap and static graph records are covered by refusal fixtures, not
claimed as positive heap/static proofs. Both diagnostic compilers use the same
observational emitter patch and are bound to their respective frozen bases.

The previously pending C4 Linux CPROVER regression/style/unit/lint/codegen/
warnings gates, fresh affected consumers and combined implementation review
are now complete; see the private-adoption milestone below.
The original full Digest caller never completed, so there is no full-caller
original/COW differential. Finite tests are not universal compiler soundness,
and one-shot/streaming self-consistency is not a functional SHA theorem.
The accepted installed compiler and production dependency remain unchanged.

Exact new evidence is retained under corrected-digest/full-caller-cow-v2/
and corrected-digest/cow-c3-v1/. Source, toolchains, current binaries, proof
artifacts and receipts were preserved during storage reclamation; explicit
manifests identify retired rebuildable library/build caches.

C4 and private compiler adoption (2026-10-30)

The final reviewed candidate is 8d9c52fedd0e1941d9c72ea6843adca104be5fbb, tree 0b4412adf7ec7e813c2d3da3b3c9e336bf5af75e, compared with 2a5a39e9c07e330b411e653331ef98582a729fcc. Its production compiler is the exact C1 binary, SHA-256 d757e0e42d5fd53a43f282dd7a9953f0daa7ae7512888e9d6c290dfe7d7a1401; the only subsequent source change is a license notice in the historical prototype patch. The original installed compiler is preserved, and no upstream write or production dependency change was made.

All 15 pinned Linux CPROVER suites completed, covering 1,628 regression cases, including 22 expected-failure cases. Source ignores and refusals remain explicit. Style, units, lint, warning/configuration and actual Firecracker codegen gates passed. Resumed suites authenticate each retained completed case and freshly executed remainder; their interrupted invocations retain failed status. The 44 exact-read and 17 auxiliary controls are separately classified.

All ten fresh padding/constructor consumer cases satisfy their unchanged published semantic checkers, including each intended negative and its exact failing property. Each run has distinct inputs/working directories and exact runtime bindings. The rejected 8-GiB padding attempt remains failed; the separately selected 16-GiB padding runs completed with kernel-reported maximum child RSS of 9.2–9.5 GB. Partial RSS sampling is documented as a lower bound, separate from kernel accounting and enforced limits. The existing 110 finite native/Miri cleanup cases were reused only after authenticating unchanged source, tools, runtime and the full Miri sysroot; they were not rerun or promoted to a universal unwind theorem.

Astra ultra returned GO on all seven implementation checks in 454 seconds. Opus 5.5 xhigh's original GAP is preserved: two focused follow-ups completed the missing diagnostic/resume provenance and consumer/resource/finite-reuse checks on the unchanged snapshot. The final scoped follow-up returned GO; combined Opus coverage now answers every original mandatory check. No blocker or mandatory gap remains. All legs stayed within the original 900-second/8-MiB hard bounds. No Kimi, optional reviewer, repeated full test suite, or accompanying proof replay was used. After review, all 9,467 frozen evidence files and 85 symlink texts still authenticated.

This accepts only the exact compiler for separately bounded private research. It establishes no functional SHA/full-Digest theorem, completed original full-caller differential, universal compiler soundness, production adoption or hardware decision. Full corrected Digest composition and the broader source/model/cross-tool boundaries remain open.

Non-blocking tooling observations are banked here for a later bounded slice: exclude stale ignored Python bytecode when loading proof checkers, and directly compare each recorded prlimit command with its structured resource limits. Current evidence was re-evaluated from source without bytecode-cache use, and all actual command limits were independently checked. These observations do not activate the deferred assurance sweep or require another solver campaign; #1099 separately tracks the older padding entrypoint's terminal resource check.

Exact adoption decision, immutable review reports and source/evidence identities: corrected-digest/cow-private-adoption-v1.json, cow-implementation-wave-v1/, cow-implementation-gap-wave-v1/, and cow-implementation-gap-wave-v2/ under the existing local research root. The 6 GiB aggregate cap remains in effect. Next: select the smallest useful corrected Digest source-composition slice; compilation alone does not authorize a full-caller solver run.

Actual corrected Digest admissibility and raw-read boundary (2026-10-31)

A bounded actual-caller diagnostic now executes both unchanged sha256_bytes and sha256_parts entry points against the independent standard empty-message digest. It uses the exact research correction, force-soft x86_64 configuration, all default/initialization/validity/unwind guards, fresh inputs/Cargo home/target, and the accepted COW compiler. Its offline dependencies match the selected consumer lockfile, including cfg-if 1.0.4 and libc 0.2.185. The older C2 compilation-only probe used cfg-if 1.0.5 and libc 0.2.191; it remains a separately scoped translation-feasibility receipt and is not transferred as proof evidence for the consumer dependency closure.

The new diagnostic terminated normally with verification failure after 160.60 active seconds, below its 180-second bound, with no resource stop and unchanged source/runtime. Exactly one of 2,436 non-cover properties failed: std::ptr::read::<MaybeUninit<GenericArray<u8,U64>>>::unsupported_construct.1, reporting Opaque transfer overlap is not proved disjoint or exact self-copy. Both digest-value assertions and the final reachability cover are unreachable. This is an explicit verifier-model coverage limitation, not a demonstrated digest mismatch or source-code memory-safety failure. The planned wrong-oracle control was not run because the positive admissibility prerequisite failed.

Source inspection localizes the refusal to kani-compiler/src/kani_middle/transform/check_uninit/opaque.rs: its conservative assignment rule supports known-disjoint locals and a restricted ordinary-reference case but refuses raw-pointer dereference to a fresh local. This is the original guard in the accepted model; it has not been removed or weakened.

A separate minimal reproduction confirms the distinction without the SHA/dependency stack. For arbitrary 64 input bytes, copying an initialized MaybeUninit<[u8;64]> through an ordinary reference passes the byte assertion and cover (5.13 seconds). Reading the same caller-owned initialized object through standard ptr::read produces exactly the same unsupported-transfer refusal, leaving the byte assertion and cover unreachable (1.83 seconds). Both small runs preserve all guards and the exact compiler/runtime. No compiler or library-model change has been made.

Next: select a narrowly scoped, reviewed transfer-model extension that can justify the needed raw read while preserving initialization state, validity, pointer and overlap checks. A blanket raw-pointer exemption or suppressing the refusal is not an acceptable closure. This changes the verifier's admitted operation subset and therefore needs its own architecture decision, causal controls and adoption gates before any full-Digest proof credit. The complete source-composition and unrestricted-input obligations remain open.

Exact plans, raw logs, complete property results and source/tool identities are retained under corrected-digest/digest-admissibility-v1/ and corrected-digest/opaque-raw-read-repro-v1/. Their assessment.json files record the failed full-caller result and the successful minimization separately. No result is promoted into a functional SHA theorem.

The narrow raw-return transfer candidate is implemented privately at 089bca6a3c8d2dafcd53bf637bb7334dd0ab1899; it is not adopted. Architecture review and coordinator reconciliation are recorded, preserving Astra GO and Opus FIX as their original verdicts. The selected route requires an exact raw-pointer argument to a MaybeUninit return plus distinct actual memory objects before metadata transfer.

The compiler and changed verification libraries rebuilt successfully. All 49 compiler unit tests pass. Four source-bound C1 controls have their intended outcomes:

Arbitrary 64-byte copy preserves destination and source, with reachable assertions/cover.
Partially initialized storage preserves its initialized prefix and source.
Reading the copied uninitialized suffix fails the intended initialization guards.
A misaligned MaybeUninit raw read fails the intended alignment guard before transfer.

Actual instrumented MIR contains the checked helper and source AddressOf path. The separate unchanged-compiler ordinary-u32 alignment limitation is banked as #1108; the opaque path's successful negative control is not a general alignment-model fix.

Remaining before C2: selector/exclusion and pointer/nested/ZST cases, exact-helper same-object tests, causal mutations, and relevant lint gates. The full Digest positive/wrong-oracle diagnostic has not been rerun. Broader upstream/affected-consumer gates and frozen implementation review remain required before any private adoption. No production dependency or upstream Kani change was made.

Local evidence: easycrypt-full-digest-20261028/corrected-digest/raw-read-c1-core-v1/assessment.json, candidate/runtime/build records alongside it. Storage remains under the existing 6 GiB cap; identical toolchain-file deduplication and verified inactive-cache archiving preserved all frozen inputs, runtimes and proof evidence.

C1 of the checked opaque raw-return candidate is complete on private compiler commit 089bca6a3c8d2dafcd53bf637bb7334dd0ab1899: 49 compiler unit tests; four core, 16 expanded and five explicit-MIR controls; 901,120 finite source-extracted helper transitions; three helper mutations and three actual compiled producer-omission controls; relevant compiler/library lint and formatting. Failed setup attempts and the earlier JSON log-size failure remain excluded from evidence.

The single fresh full-caller C2 diagnostic, with the selected corrected dependency closure and all guards enabled, hit its 300-active-second limit without a verdict. Its final solver log also reported memory exhaustion. It is not a passing proof, and the wrong-oracle control was not launched.

A separate, newly selected output-overhead diagnostic used the exact saved instrumented GOTO, all the same property/solver/unwind checks, and plain CBMC output. It returned in 130.07 s with exit 6, reporting 2,831 properties: 2,232 SUCCESS, 104 FAILURE and 495 ERROR. Of the failures, 103 are reachability queries; the one semantic failure is Kani's unsupported integer_min intrinsic in usize::min. The solver also exhausted memory under the unchanged 8 GiB address-space cap (observed peak RSS 7,540,883,456 bytes). Thus removing JSON traces alone does not close the resource problem; no partial successes are promoted to Digest proof credit.

The intrinsic refusal now reproduces in a standalone arbitrary-usize minimum test in 0.93 s, with exactly the same unsupported-intrinsic failure and all three outcome covers unreachable. The pinned Rust toolchain supplies its ordinary integer-minimum fallback, so the next bounded selection will compare source-preserving support routes before implementation. Full caller composition, the memory strategy, full upstream/consumer gates and final Astra/Opus review remain open. The new raw-return compiler is unadopted; production dependencies and the accepted private runtimes remain unchanged.

Evidence is retained under corrected-digest/: raw-read-c1-acceptance-v1.json, raw-read-c2-stop-v1.json, raw-read-output-diagnosis-v1/assessment.json, and raw-read-integer-min-repro-v1/assessment.json. Inactive generated caches were losslessly archived with complete hash roundtrips, reclaiming 255,930,368 bytes; installed runtime hashes remain unchanged. No upstream Kani writes or hardware actions.

The narrow integer_min extension has completed its local implementation and focused validation, with no private adoption yet.

Frozen compiler implementation: 144fa3d76894b473e621908d5862db33efb56c7d; final fixture-only candidate: 92b5208c67093e2c43b7be2c8847dfcd8463bd71, tree 5e47fd69ad12557ceb1993c19a003c54946a0b5b. Compiler SHA-256: f686950e9531aac30b7c3e3c3273afd6390f724eaff383fb0c8b22f71cef9597.
Both required architecture reviewers returned GO for bounded implementation. Their direct-call coverage and indirect char::min observations were incorporated.
The extension recognizes only two equal primitive integer operands with the same return type and an available, non-mandatory Rust fallback. It keeps the actual Rust body, pre-call initialization checks, normal-return destination initialization, and conservative alias union. Unexpected backend dispatch refuses explicitly.
Compiler build, 49 unit tests, Clippy, and relevant formatting passed. Sixteen positive controls pass across all 12 integer types, the character wrapper, a directly addressed call destination, and both exposed-pointer operand positions. Seven negative controls fail for their intended initialization, incorrect-oracle, or excluded integer_max reason. Actual direct-call MIR and signed/unsigned GOTO fallback bodies were inspected. Seven result-checker mutations were rejected.
One initial character test encountered the existing Option<char> niche-layout refusal in its validity oracle. That failed output is retained and excluded; the replacement checks the Unicode scalar range directly and passes with all guards. No safety credit is assigned to assertions or covers after deliberate UB in the negative controls.

The prior combined full-Digest timeout/memory failure remains not a proof. Next is a separately bounded memory selection, considering whether the two independent actual-wrapper diagnostics can be executed separately before introducing property partitioning. Separate wrapper evidence would not establish the old sequential composition or arbitrary-input SHA correctness. Existing combined C3 regression/runtime gates and C4 implementation review remain mandatory before adoption. Production signer/dependency source is unchanged by this private compiler work.

Local authoritative receipt: corrected-digest/integer-min-c1-acceptance-v1.json under the existing easycrypt-full-digest-20261028 research root. All raw evidence and runtimes are retained; current aggregate allocation is about 5.70 GiB under the 6 GiB cap.

The corrected-dependency track progressed through a fresh combined-caller compile (49.24 s) and a bounded property-partition prototype. The complete census is 2,830 static checks; 23 partitions were frozen without dropping checks or separating the two callers. The checker has 40-property monolithic/partition agreement, preserved-assumption and unwind controls, and 28 rejection mutations. Six source-location-free CBMC pointer checks are explicitly retained by exact complete metadata.

The first root partition finished in 69.96 s, with peak child RSS 3,904,086,016 bytes, instead of exhausting the prior 8 GiB address-space limit. It was rejected: both digest comparisons and the final cover were unreachable. The other partitions and wrong-oracle run were not launched. This is not a full-caller pass.

One separate causal query (60.86 s, same GOTO/guards) confirmed the path-cutting refusal: rotate_right::<u32> reaches the pinned Rust unchecked_funnel_shr fallback, which the initialization checker does not classify. Source inspection also identifies its nested disjoint_bitor fallback and the shift-range/disjointness preconditions that must remain checked. Next is a narrowly scoped, jointly reviewed proposal for those two u32 operations—not a blanket intrinsic fallback or a guard removal.

Private helper candidate: ed796af (unadopted). Local receipts: corrected-digest/partition-p1-acceptance-v2.json, partition-p2-stop-v1.json, partition-refusal-diagnostic-v1/assessment.json, and rotation-fallback-selection-v1.json under the retained easycrypt-full-digest-20261028 research root. The corrected dependency is already landed via #1098; full Digest correspondence and the combined compiler/runtime adoption gates remain open here.

Private compiler correction and full-caller checkpoint (2026-10-31):

The dependency correction remains merged in #1098. The follow-up private compiler now recognizes only the actual guarded u32 unchecked_funnel_shr and disjoint_bitor fallback bodies. The original Rust bodies, operand initialization checks, addressed-destination initialization and all-argument alias propagation remain in scope.

Focused evidence: 50 compiler unit tests, strict compiler Clippy/format checks, and 23 controls passed their intended outcomes (7 positives, 16 negatives). Eleven old-compiler comparisons confirm that the new checker rejects an unsupported-operation refusal as a substitute for the intended negative. Eighteen checker mutations were rejected. Actual MIR/GOTO and distinct-origin alias-transfer checks are recorded. This is focused evidence, not combined adoption.

The fresh original sequential combined fixed-empty caller compiled in 51.73 seconds. Preparation and census passed with 2,828 properties frozen into 23 partitions. The exact census delta is removal of the two old rotation/funnel unsupported-operation properties; no static property was added. Both original 32-byte oracle comparisons and the final cover remain.

The first partition then stopped with CBMC exit 6: out of memory during propositional reduction under the unchanged 8 GiB address-space cap (141.77 seconds, 8,123,875,328 bytes peak child RSS). Its 82 raw SUCCESS and 38 ERROR rows are diagnostic only: zero partitions accepted, full caller unverified. The remaining 22 partitions and wrong-oracle negative were not run. All 635 pinned inputs for that stage were reauthenticated; the failed run is retained.

Next is source-backed selection of a bounded memory alternative. No unchanged retry, post-result regrouping, easier replacement caller or negative run on this failed positive. The 6 GiB aggregate storage cap remains enforced. Existing C3 combined upstream/runtime/consumer gates and C4 Astra/Opus review still precede any private adoption. Production dependencies and cryptographic claims are unchanged; #1108 and deferred assurance #509 remain open.

Local receipts under ~/.local/state/pqsigner-research/easycrypt-full-digest-20261028/corrected-digest/: rotation-r1-acceptance-v1.json, rotation-r2-acceptance-v1.json, rotation-r3-stop-v1.json. Candidate fca31db21d2947e10e80925fa1246c378f6daefe, tree b34d416931d8de1fa29b09b05492755b8a887e5c; compiler SHA-256 384b35ab41b520b11e5711d8f00c9fef1491f640aaab97858ca0fc75171abd15.

Original full-caller memory checkpoint:

The selected --arrays-uf-always alternative did not resolve the resource limit. The exact retained positive GOTO (552b835e623cff98783d6e4698291c6b6ca820d5ca1f8674a89b9da7988613f3) produced the same complete 2,828 property records and unchanged 23-partition schedule. The first partition exhausted 8 GiB address space after 76.87 seconds, exit 6, peak child RSS 8,194,043,904 bytes. No SAT/UNSAT result or complete verification report was produced. Zero partitions accepted; the remaining 22 and full wrong-oracle negative did not run. All inputs and raw receipts were reauthenticated and retained.

Verbosity-8 evidence now records 46.23 seconds of symex, 1,951,287 SSA steps, 1,448,289 sliced assignments, 1,833 VCCs remaining after simplification, and 11.15 seconds of SSA conversion. This identifies the size of the workload, not the exact allocation that failed.

Nine finite encoding comparisons completed and agreed on all outcomes (18 solves, 18 censuses, 32.27 seconds). Only the Rust initialization control demonstrates a measured encoding change; its formula became larger. The initial C controls have no formula statistics, and no finite wrong-oracle control combines an intended failure with a measured encoding change. These controls do not establish a general encoding theorem or a full-caller proof.

The reviewed complete-schedule budget is now 4,320 active seconds per positive/conditional negative (24 commands × 180 seconds); process memory, per-command time and the 6 GiB aggregate storage cap stayed fixed for this attempt. The review's remaining wording ambiguity was reproduced and corrected as an editorial clarification; reports retain their actual reviewed identities.

Returning to source-backed selection for the same original sequential caller. No repeat of this failed encoding attempt, caller reduction, regrouping or negative on partial evidence. A bounded resource adjustment for the original default backend is being evaluated; it has not been implemented or run. The private compiler remains unadopted, with the existing C3/C4 gates and limitations #1108/#509 unchanged.

Receipt: ~/.local/state/pqsigner-research/easycrypt-full-digest-20261028/corrected-digest/array-a2-stop-v1.json; helper candidate b1c78883cc77fee8c06fbf2867297d24f326a3d4, tree edf20e78e84f013ac01f61ea87b10fca5841f035. The compiler binary and its actual build identity are unchanged from the preceding rotation correction.

The original full-caller diagnostic has now exercised the reviewed 16 GiB CBMC process envelope with the original default array encoding/Cadical.

Astra ultra and Opus 5.5 xhigh both returned architecture GO. Opus’s storage concern was reproduced; 119,091,200 bytes of inactive generated caches were reclaimed through hash/mode/roundtrip-verified archival, leaving the hard 6 GiB aggregate cap unchanged.
The new private helper passed 24 pre-launch refusal controls and retained the default 8 GiB limit for other commands. Live kernel receipts confirmed 16 GiB for CBMC; available memory before the first partition was 66,883,702,784 bytes. Existing compiler, driver, libraries, dependencies and prepared program remained byte-identical; no rebuild is claimed.
Fresh census: all 2,828 original property records and the exact 23 partition memberships/order matched. Both full digest comparisons, reachability checks, final cover, all static guards and dynamic unwind requirements remain required.
Partition 0 stopped at the 180-active-second time ceiling (184.13 seconds including cleanup/accounting), exit -9. Peak child RSS was 9,636,401,152 bytes. No out-of-memory message and no final SAT/UNSAT result appeared; zero partitions earned proof credit. The remaining 22 partitions and the conditional wrong-oracle negative did not run.
Recorded stages: symex 46.41 s, 1,951,287 SSA steps, 1,448,289 assignments sliced, 1,833 VCCs remaining, SSA conversion 11.66 s. Last stage message: “Running propositional reduction”; it does not establish that SAT search itself began.

Private helper candidate: 3efa8ca203e7771f34776a4a960617975add6ca7, tree c5334f60ed2250bfe5c38dc2bc7e51d1d3977128. Authenticated stop: corrected-digest/default-memory-m3-stop-v1.json; M1/M2 receipt: default-memory-m1-m2-acceptance-v1.json under the retained research root. Source/proof logs, failed attempts and installed runtimes are preserved.

#1097 remains open. Next is source-backed backend-stage diagnosis/selection, not an automatic further resource increase or retry. Full combined C3 upstream/runtime/consumer gates and C4 review remain mandatory before any private adoption; no general SHA theorem or production dependency adoption is claimed. #1108 and the deferred #509 scope remain unchanged.

Source-backed follow-up to the 16 GiB time stop:

Eleven finite default/array-refinement comparisons preserved their complete expected outcomes, including real array-refinement activity on positive and wrong-oracle symbolic-length C controls (26 new commands, 13 solves, 22.64 s; nine unchanged default baselines reused). This is finite compatibility evidence, not a full-caller proof or performance result.

The architecture review returned Astra GO / Opus FIX. Coordinator reproduction confirmed that the pinned source inherits U_NONE, not the plan’s asserted AUTO policy; both default and refinement factories retain it. All nine prior Rust/C controls needed only one refinement iteration per solve round. The 644/68 constraint activations occurred only in the synthetic variable-length C controls. The full caller’s applicability is still unestablished. Two bounded metadata renderings reached their fixed output ceiling, so neither establishes a complete type census.

The full refinement attempt is not selected or running. Its frozen plan/reports remain retained as research. The second finding requires explicit CaDiCaL/refinement final-round protocol checks if this candidate is later selected; those exact protocol lines were independently verified on all eleven finite logs, but no full runner has been implemented.

Reconciliation: corrected-digest/refinement-architecture-reconciliation-v1.json; finite acceptance: refinement-finite-acceptance-v1.json. #1097 and the original full-caller criterion remain open; C3/C4 remain required and no private adoption is claimed. Next investigation is the already-installed SMT backend, beginning with source/tool and bounded finite compatibility checks, without automatic resource escalation or another unsupported full-run retry.

Phase A SMT feasibility update; no original-caller SMT run or adoption yet.

The corrected dependency constructors remain merged in #1098. The original combined Digest caller and its complete property/partition requirements remain unchanged.

Both installed Z3 binaries (system 4.8.12 and opam 4.16.0) returned false SAT for two independently justified UNSAT bitvector-array cases, using constant arrays and lambda arrays. These controls expose the class documented in z3 reports sat on unsat problem with constant arrays Z3Prover/z3#9550. Both binaries are rejected for this backend experiment. Earlier full-caller attempts used CaDiCaL; they are not retrospectively relabelled as Z3 runs.
Acquired a standalone official Z3 5.3.3 release inside the existing accounting root, verified GitHub's published archive SHA-256, and pinned the binary and resolved libraries. Its source contains the #9572 base-value constraint. This is official-release provenance, not a reproducible source-build attestation. System installations remain unchanged.
The fixed binary returned UNSAT for both controls and matched all eleven authenticated default-backend cases: 368 static properties plus three dynamic unwinding obligations across the cases. Intended negative, reachability, and insufficient-unwind outcomes agree. All eleven default solves were reused.
A finite protocol control reproduced CBMC's external-child-status gap: a declared unsuccessful child (exit 23) returning unsat made CBMC exit 0 and label a known false assertion successful. This deliberately invalid diagnostic earns no proof credit. A legitimate Z3 UNSAT query followed by get-value exits 1 with a model-unavailable error, so a blanket nonzero-exit rejection also needs care.
Total new finite/diagnostic commands: 32, approximately 30.2 active seconds. Research allocation is approximately 6.317 billion bytes, below the unchanged 6,442,450,944-byte hard cap. Existing source, evidence, runtimes, and unrelated working-tree changes are preserved.

Next: prototype strict external-child command/query/output/exit receipts and targeted refusal controls, then select and review the bounded original-caller SMT architecture. No full caller is accepted from these finite comparisons; C3/C4 and the original combined-caller requirements remain open. The three tiny protocol-only diagnostics did not record a fresh MemAvailable preflight; they remain diagnostic-only, and the future run controls must enforce that preflight.

Local reconciliation: corrected-digest/smt-finite-reconciliation-v1.json under easycrypt-full-digest-20261028; raw inputs, outputs, and hashes are retained. Primary upstream references: Z3Prover/z3#9550 and Z3Prover/z3#9572.

The original-caller SMT candidate has reached Phase C S1; no full-caller SMT proof or private adoption is claimed.

Frozen architecture candidate: 859a1fc880bced2b59987d835b2461903a6a30b8, tree 291bcc03d0f282acd66d8637e062b0d127369d06 in the private Kani worktree. Astra ultra and Opus 5.5 xhigh both returned GO for bounded S1-S3 testing, with the explicit prelaunch gates still mandatory. Both completed inside the 15-minute limit; source identity and raw review hashes were checked.

Completed prototype evidence:

28 malformed-response mutations rejected; real SAT and UNSAT preserved, including Z3's legitimate nonzero exit after UNSAT/model requests.
Four existing complete C/Rust finite cases retained their expected outcomes. All 17 accepted external calls have exact query, command, status and separate output receipts.
The declared unsuccessful-child control now makes CBMC exit 6 rather than falsely succeed.
Process-lifecycle controls terminate a descendant ignoring SIGTERM after its parent exits and reject a timed-out run.

The coordinated S1 follow-ups are concrete: replace inherited SAT telemetry with exact SMT call accounting; enforce sufficient per-command and per-external-call disk reserves; record query byte size and construct counts before solving. SAT/UNSAT semantics still depend on the trusted pinned solver. Finite protocol validation does not independently certify them, and construct coverage/performance remain bounded by the executed evidence.

Lossless archival of inactive generated GOTO/MIR caches and compiler name maps reclaimed 205,512,704 bytes. Every archived member passed a full byte/mode round trip, all prior archives remain, and all 13,483 current bindings reauthenticated afterwards. Allocation is approximately 6.118 billion bytes, leaving approximately 324 MB beneath the unchanged 6,442,450,944-byte cap. An initial name-map schema preflight rejected null values before any deletion; the corrected preflight follows Kani's Option<InternedString> serialization and its failure receipt is preserved.

Next: finish S1 selected-path/full-driver integration and refusal controls, then authenticate and run the original complete positive only if all gates pass. The original 2,828-record census, exact 23-part schedule, both full oracles, conditional complete negative, and C3/C4 remain required. No caller reduction, cap increase, system installation change, production adoption or new EasyCrypt replay was performed.

Local owners: PQ1-SMT-BACKEND-PLAN.md, corrected-digest/smt-architecture-decision-v1.json, smt-architecture-reconciliation-v1.json, and smt-name-map-retention-postflight-v1.json under easycrypt-full-digest-20261028.

S1 integration passed on private helper candidate cbf5d613b4e08e1c4e75833548cee1be92fe1b74 (tree e162f7597b34ca609bf241956cebbad5c274a6b2). Four complete finite CBMC outcomes match their original baselines; 30 corrupted-receipt cases refuse; census, unsuccessful-child and descendant/timeout cleanup controls pass. Eight monitored commands took 16.91 seconds. The 15 accepted external calls contain 28 datatype declarations and no lambda/forall/exists operators; these remain finite compatibility controls with CBMC/Z3 trusted, not independent semantic certificates.

The exact original full positive then ran: prepared GOTO SHA-256 552b835e623cff98783d6e4698291c6b6ca820d5ca1f8674a89b9da7988613f3, fresh equality of all 2,828 property records, unchanged 23 partitions and pilot order [0,15,16]. Root partition 0 terminated with SIGXFSZ after 111.85 active seconds (114.03 seconds including census), at the existing 16 MiB per-file ceiling. Its retained SMT query prefix is exactly 16,777,216 bytes. Pinned CBMC source writes that temporary query before invoking the adapter; no external adapter receipt exists and Z3 was not reached. Zero partitions are accepted; the conditional wrong-oracle case did not run. All owned processes terminated and source/tool pins remain unchanged. Peak aggregate allocation was 6,162,964,480 bytes, below the fixed 6,442,450,944-byte cap.

Evidence is retained under corrected-digest/smt-controls-v1/, smt-s1-acceptance-v1.json, smt-digest-v1/positive/ and smt-s2-stop-v1.json. Prelaunch also restored one 63,687-byte finite preparation input from its authenticated lossless archive; original hash/mode and all preparation pins verify. No progress was lost.

Next is bounded source-backed query-transport/backend selection within the existing limits. This attempt does not authorize an unchanged retry, automatic ceiling increase, easier caller or adoption. Full original-caller completion and the combined C3/C4 gates remain open.

Streaming follow-up is complete and remains diagnostic-only. The installed native incremental backend aborts on the first existing array-copy fixture during conversion (extension_for_type); its fresh census agrees, but no native case is accepted. The two commands took 1.94 seconds and all owned processes terminated. Further native cases were stopped.

A separate legacy formula-output control exactly matches all 23,263 bytes of the first previously accepted real solver query. Chunked capture also round-trips a 22,020,096-byte stream in six files below the unchanged 16 MiB file ceiling. The initial control runner expected CBMC exit 6, but pinned caller source explicitly returns zero for --outfile; the corrected interpretation reauthenticated the same raw receipts without rerunning them. Zero here is emission status only.

One bounded original-caller emission then reached its 256 MiB raw-stream ceiling after 128.23 seconds. Its 64 lossless chunks occupy 46,274,291 compressed bytes, and their initial 16 MiB is identical to the original failed query prefix. Thus the complete legacy query exceeds 256 MiB; there is still no complete query or full SMT solver result. No solver ran during this measurement, no cap was raised, and all process groups terminated. Evidence: corrected-digest/smt-streaming-research-v1/reconciliation-v1.json. The private research root now has approximately 231 MB of headroom; required launch reserve remains a gate.

Private plan-only candidate b64248ec4b4884afefcd49f5aff3543ef6fb2996 (tree 1663d05a0e59258de2d8cb3486ad0b0bfac14f22) freezes PQ1-DEFAULT-TIME-PLAN.md: one proposed default/Cadical attempt allocating at most 600 active seconds to root partition 0, retaining 180 seconds for other partitions and the existing 4,320-second complete-case budget. Memory remains 16 GiB for that previously tested backend; file and aggregate caps stay unchanged. The exact original caller, prepared GOTO, all 2,828 properties and 23 memberships remain required. Fresh Astra ultra/Opus 5.5 xhigh architecture review, guard tests and restored storage headroom precede any new proof attempt. No escalation loop, smaller target, production change or adoption is authorized. C3/C4 and the full caller remain open.

The field-option architecture wave is terminal: Astra GO (186 s), Opus FIX (340 s), no missing reviewer answers or input drift. I reproduced the three stage blockers locally: insufficient whole-continuation storage budgeting, no explicit fresh smoke test combining the derived native fixture with the flag, and the need to authenticate failed-run costs separately from the successful-proof reader. There are 22 remaining positive parts (the review text counted 21).

The revised local plan is committed at 081c1ba3ff87019567b1eb12a4979dc272b7d561 (tree cc0305866f1c17702aebb5a662011e65c7f8ab94). It adds a 75,235,328-byte whole-campaign allocated-space gate, bounded lossless gzip for new logs, small in-memory control fixtures, the exact derived/native flag comparison, and an explicit failed-cost ledger reader with separate old/new totals. It still needs fresh architecture review before implementation.

I also deduplicated exactly seven byte-identical JSON fixtures from completed control runs, recovering 37,724,160 net allocated bytes before the final receipt. All paths, contents, owners and modes were preserved; no source, runtime or proof log changed. Post-dedup headroom was about 80.5 MB; the new storage gate must be measured again after review, rather than assumed satisfied.

Receipts: promoted-field-architecture-reconciliation-v1.json, promoted-field-fixture-dedup-v1.json, and promoted-post-lemma-research-v1/field-storage-feasibility-v1.json under the existing corrected-digest root. Full-case/finite costs and accepted obligations are unchanged. No full query, model adoption or limit increase occurred. The autonomous goal remains active; next is the bounded review of the revised plan.

F1 is implemented and frozen locally at 61d7acb2f0dda6ec8d698aab14c3f5abf7ff31ed (tree fd9c38b8f10283ae4f8d0507c93b9b76f17c005b). All four native field-option controls passed, including the exact derived fixture; six transport commands passed with 15 corruption/truncation/limit/failure refusals; all 77 admission controls passed. Admission reparses the original root and 692 finite maps, and preserves the exact failed/inventory-cost chain at 1186.41343192989 seconds. Synthetic schedule mutations now stay in memory.

New logs use bounded lossless gzip with raw/compressed hashes; allocated component and whole-campaign budgets are checked before writes/launch. Maximum estimated spec is 336319 bytes under 384 KiB; setup schedule is 5387172 bytes under its shared 6 MiB setup budget. The fresh storage preflight fits the unchanged aggregate cap. Astra ultra and Opus 5.5 xhigh are now reviewing the combined implementation under the required 900-second/8-MiB bounds. No full query has started and F2 remains unauthorized until that review closes; full negative, C3 and C4 remain open. Raw F1 evidence: corrected-digest/promoted-field-F1-v1; review: promoted-field-implementation-wave-v1.

The dependency/constructor correction is merged to master in #1098 at 206bbd3113e7d2621ae246c5f1bde060ac1975c4. The field-option F1 candidate earned 77 admission refusals plus native/transport controls and GO/GO implementation readiness. Its single F2 part-2 attempt then hit the unchanged 180-second active limit (182.48223003500607 seconds including cleanup). No additional full partition was accepted: root 0 remains the only accepted one, with 22 remaining. Accumulated full-case cost is 1368.8956619648961 seconds. No unchanged retry or limit increase is authorized.

That stopped attempt exposed incomplete gzip finalization; a separately reviewed local helper repair also closes #1117 and #1119. Final candidate 67728f89accd671f57f433a7de91e3982b26fbd6 / tree 94b6d2486efca4542c0f4740bde981cf7a0f61fc has GO/GO, eight finite children, fourteen refusal controls, exact input admission over 1098 pins, explicit unknown costs, interruption-safe byte reservations and honest received-prefix status. These are local diagnostic-helper readiness results, not full-proof or private-adoption authority. The old failed payload is unrecoverable; existing accepted proof evidence and all retained artifacts are preserved.

Remaining: select an evidence-backed next proof route; complete the original positive obligations before the conditional full negative; then current C3 regressions and C4 adoption. Fresh negative preparation still requires its existing 256 MiB reserve. Current allocation is about 6,374,445,056 bytes under the unchanged 6,442,450,944 cap. Raw records: promoted-field-positive-stop-reconciliation-v1.json and promoted-field-evidence-repair-decision-v1.json. No solver/compiler command ran during the repair campaign.

Bounded follow-up after the diagnostic-helper repairs: no additional full Digest query was run, and the constructor/dependency correction remains merged through #1098.

Two small, source-backed alternatives were assessed on the existing copied-array fixture:

Stock dereference caching: all 347 property statuses agree; SSA steps (26,755), variables (103,907), and clauses (142,516) are unchanged. Paired times were 0.8463 and 0.8506 seconds. Stopped after the first pair under the predeclared rule.
The already-installed CVC5 1.3.0 through CBMC's incremental SMT interface: all 347 property statuses agree, but the first fixture took 22.3382 seconds versus the fresh MiniSat baseline of 0.8463 seconds. Stopped after that case under the predeclared rule. The two negative fixtures were not run, and no complete external-solver protocol/adoption gate is claimed.

Neither option is selected for a full query. CBMC's experimental full slicer was also excluded on its explicit unsoundness warning, without executing it. The three finite commands consumed 24.0351 seconds; their complete raw logs, receipts and source identities are retained. They earn no full-caller proof credit.

The full-case ledger remains 1,368.8956619648961 active seconds, including failed attempts. Only root partition 0 is accepted; the other 22 partitions, conditional full negative, and required C3/C4 gates remain open. No caller/model/runtime modification, larger limit, unchanged full retry, or private adoption occurred. The measured aggregate was 6,375,157,760 bytes, leaving 67,293,184 bytes under the unchanged 6 GiB cap; all previous evidence is preserved.

Next is read-only feasibility of the required C3 compiler/runtime/consumer gates and their ordering, not another option sweep. Exact local assessment: corrected-digest/promoted-post-field-research-v1/next-route-assessment-v1.json, SHA-256 003015106db1d899b95b7db71340b18bacfb38ef7aae53780843b595a1446cdf.

Progress on the remaining C3 prerequisites, with no full-Digest retry or adoption:

Enrolled padding-raw-return-controls.expected on isolated candidate 57149142b906290c29536b747dee37e37cdd4178 (tree 624bacaffbd3e090bbc997a1a30520a2a3e4163f). The actual upstream expected-mode test passes. Independently reconciled all 955 checks and four covers against the complete export and raw results: both positives pass with reached covers; uninitialized-byte and misalignment negatives fail only their intended checks. All nine listed unsupported-operation guards succeed. The initial sparse-checkout census failure is preserved; no solver ran in that failed setup.
Built fresh no_core kani_core and playback kani_core/kani/std from the current model source, borrowing only authenticated unchanged macro/standard-library dependencies. These are small direct builds, not a complete cargo build-dev claim. The native playback positive consumes the supplied byte, and the wrong-byte control exits 101 at the exact intended assertion.
Preserved two setup stops honestly. The initial small-build script's extra no-warning criterion failed on two diagnostics also present in the prior accepted playback unit run. No warning was suppressed; the separate mandatory warning/lint gates remain open. A subsequent smoke link lacked the transitive macro search path; adding a macro-only directory fixed that concrete error without rebuilding any library. All variant attempts together consumed 0.370 active command seconds and about 6.43 MiB of retained output.

Raw-return evidence: corrected-digest/c3-raw-enrollment-v2/assessment-reconciled-v1.json, SHA-256 239b641c75b15ada77f901b62bd211ec98370051815dce4a008f21a68ba8a5d8.
Runtime preparation: corrected-digest/c3-playback-link-correction-v1/assessment.json, SHA-256 c77b01d6f11253e006564137f8e837a9bab5ba6e91f68848453a8ed41e7be20d.

The original runtime, accepted proof inputs and dirty canonical PQSigner checkout remain untouched. Aggregate research allocation is about 5.96 GiB, below the unchanged 6 GiB cap. No process remains running from this batch.

Still open: G1/G2 fixture enrollment, complete Linux CPROVER/build/style/unit/lint/warning/codegen and affected-consumer gates, complete full positive partition union and conditional negative, and combined C4 Astra/Opus review. The full proof remains at one accepted root partition of 23; none of these finite/runtime checks closes it. Next is the existing promoted-entry fixture enrollment and storage feasibility for the remaining C3 gates. No unchanged full query, larger limit, installation or private adoption is selected.

C3 enrollment progress: the 30 existing promoted-entry end-to-end/contract-mode fixtures are now enrolled and formatted on isolated candidate e87d8cd3a58e237733f709b6087c1f605e157404 (tree 14ca79b8cd198e449b63ccaa3866391b41fc6e19). Discovery finds all 30 plus the separately completed raw-return test.

Nine newly enrolled cases pass, with every property ID/status/description matching the prior complete evidence. The tenth (no_seed_indirect) stopped expected-mode on one predictable crate-name mismatch: case::no_seed_indirect.missing_definition.1 became promoted_entry_no_seed_indirect::no_seed_indirect.missing_definition.1. Both are SUCCESS with the same description; the other 87 properties and intended unsupported function-pointer failure are identical. The regression remains failed until its expectation is corrected. Inspection found the same namespace prefix in three not-yet-run contract fixtures (13 IDs total across four files). Twenty cases remain unrun.

Setup/postprocessing stops are preserved: compiletest dry-run reports the whole source-directory census before filtering; JSON result buckets may reorder identical IDs; completed-command reuse must retain its original environment paths. No completed solver case was repeated. All actual formatting/census/case commands so far total 14.46 active seconds.

The concrete diagnosis is retained in corrected-digest/c3-promoted-namespace-diagnosis-v1.json. One unpinned generated MIR diagnostic was retained as gzip after SHA-256 round-trip verification, reclaiming about 1.79 MiB; c3-promoted-mir-retention-v1/retention.json records restoration identity. Sources, runtime, raw property results and proof inputs remain intact. No active job remains.

Next: correct those exact property namespaces in an isolated snapshot, reuse the nine unchanged cases after authentication, and complete the failed enrollment check plus the remaining 20 within the original resource bounds. Full Digest, remaining C3 gates and combined C4 review remain open; no installation/adoption or full-query retry is selected.

C3 enrollment is now 27/30 complete. Candidate 154cf9e42a20c84aa0f6830c6c9dd797657d8bcb (tree e65519bd00a7eea3be278c5fb8a1eb71eb70e0ba) corrects 13 crate-name property prefixes in four expected files. No compiler, model, Rust fixture body, guard or expected status changed. Completed cases were reused only after exact source/expectation/tool and raw-result authentication.

The first contract fixture exposed a second portability issue in its expectations: absolute closure locations and crate-disambiguator symbols. Its complete 297-property map is identical to the prior map after the exact source-bound location mapping and crate/function identity mapping. The old/new contract annotation text and closure columns are identical; the two symbol spellings demangle to the same nested contract closure after the recorded crate rename. All statuses, failure causes and guards remain unchanged. The upstream expected-mode result remains failed; the two other contract fixtures have not run. This is an expectation correction still to do, not a passed regression or full-Digest proof.

Evidence: corrected-digest/c3-promoted-contract-portability-diagnosis-v1.json. All actual enrollment commands, including failed attempts, total 23.50 active seconds; no job remains running.

Storage stayed below the unchanged 6 GiB cap. Authenticated hardlink deduplication recovered about 4.56 MiB while preserving every source path, byte and Git identity. Shared immutable files must never be edited in place. Generated MIR diagnostics and four completed raw outputs were losslessly compressed with verified SHA-256 round trips and restoration manifests. The continuation checks decompressed raw bytes against their original accepted hashes; no progress was discarded.

Next: make the three contract expectations portable while retaining all guard/status/count checks and strict complete-map comparison, then finish the remaining three cases. Full Digest, the broader C3 gates and combined C4 review remain open. No runtime installation, private adoption, full-query retry or limit increase is selected.

C3 promoted-entry enrollment now has 30/30 expected-mode regressions with all 3,202 property rows reconciled on isolated candidate 3bd7633936a4da4b72116c20d5ed7bd07305087e (tree 9a363a22452b3e6687017380588a681bc83fc63c). This includes known negative/refusal outcomes; it is not 3,202 successful proof obligations or a full Digest theorem.

The last three contract fixtures pass after correcting path/symbol portability in their expectations. The supplementary complete-map checker binds exact source spans and demangled contract identities; eight corrupted-output controls are rejected. No Rust fixture body, compiler, model or runtime changed. The other 27 results were reused only after exact source, expectation, tool and raw-result authentication. Cumulative case/setup/format command time, including failed attempts, is 25.90 active seconds.

The final invocation still failed its retained-output bound: 6,594,560 bytes against 6,291,456. Its failed terminal receipt remains unchanged. A separate read-only reconciliation reauthenticated every property map and losslessly compressed three raw outputs plus generated graph diagnostics with SHA-256 round-trip checks. No solver was rerun. Retained enrollment output, including the reconciliation, is now 6,189,056 bytes. This does not retroactively mark the stopped invocation successful.

For remaining gate preparation, exact immutable tracked-source deduplication reclaimed 57,331,712 allocated bytes while preserving all paths, bytes, permissions, owners and clean Git identities across 21 research snapshots. Locks, runtime, generated files, proof inputs/outputs and the canonical PQ1 checkout were excluded. Shared source files must be replaced with independent inodes before any future edit. The research cap remains 6 GiB, with roughly 56 MiB usable above the mandatory 32 MiB reserve. Full restoration of the historical host/warning/script caches still does not fit; no large build was launched.

Exact receipts under corrected-digest/: c3-promoted-enrollment-reconciliation-v1/assessment.json, c3-gate-source-dedup-v1/assessment.json, and c3-remaining-gate-feasibility-v1.json. Next is bounded complete-source/check-only C3 gate preparation. Full upstream/consumer C3, the incomplete full Digest proof and combined C4 remain open; no private adoption, new full query, increased limit or additional review wave is authorized by these results.

C3 now has a complete source checkout and three passing style gates plus all 15 suite inventories on private candidate 55d238314c209978073a3e892b0f39e87f109026 (tree fe6cd0ef899ccd7b97e260de96657209ee495655). No compiler/model/runtime behavior changed, and no upstream Kani write or adoption occurred.

The checkout authenticates 5,560 tracked regular files and the exact Charon/Firecracker submodule commits. The excluded performance submodule remains uninitialized as in the earlier CPROVER gate setup. Source materialization used approximately 9 MiB by sharing authenticated immutable files; locks were copied independently.

The actual gates exposed two bounded corrections: the C lemma fixtures already had licensing text, but used block-comment syntax unsupported by the repository checker; their headers now use the accepted line-comment form with identical C bodies and line positions. Eleven private Python runners needed formatting. Complete AST comparison caught autopep8 attempting to move two imports before their required historical search-path setup; that output was rejected. Their original order is preserved with two targeted E402 annotations, and all eleven resulting ASTs equal the originals. Historical proof-input paths and shared source inodes were preserved.

Formatting, copyright and Python style are now passing. The 15 inventories contain 2,328 discovered cases: 1,661 unignored and 667 source-ignored. Relative to the accepted COW candidate, exactly 33 cases were added: integer-min and rotation fallbacks, the raw-return regression, and the 30 promoted-entry cases. There are no removed cases or changed ignore flags. This is discovery evidence, not execution of 1,661 tests.

All setup, style and discovery failures remain recorded. Discovery stopped at its retained-output limit after 14 suites. A SHA-256-verified metadata archive preserves 1,453 empty generated scratch directories, reclaiming about 5.7 MiB without removing any source, raw log, result or inventory file. Only the previously unrun fifteenth inventory was then executed. The failed batch was not relabelled successful. Total bounded gate/format-command time including failed attempts was 4.50 active seconds; source preparation and read-only reconciliation are separate.

Receipts: corrected-digest/c3-check-only-v5/assessment.json, inventory-delta.json, c3-python-style-correction-v1/assessment.json, and c3-discovery-empty-directory-retention-v1/assessment.json. Current aggregate allocation is 6,365,614,080 bytes under the unchanged 6 GiB cap. The next step is a separately bounded actual C3 execution batch with authenticated current runtime and measured workspace requirements. Full regression/unit/build/lint/warning/codegen/consumer gates, full Digest composition and combined C4 remain open. No solver ran in this check-only batch.

C3 progress on unchanged private candidate 55d238314c209978073a3e892b0f39e87f109026 (tree fe6cd0ef899ccd7b97e260de96657209ee495655). The corrected constructor dependency work remains merged via #1098; this comment does not expand that claim to full Digest correspondence.

11 of 15 upstream suite inventories are now complete: json-handler, firecracker, prusti, smack, coverage, kani-fixme, ui, std-checks, cargo-coverage, cargo-ui, and kani-docs. This comprises 278 ordinary suite pass outcomes and 22 upstream expected-panic outcomes. Firecracker's two tests are source-ignored; its actual project code-generation gate is still open. The 629 ignored entries in kani-fixme are regular tests excluded by that mode, not 629 distinct ignored source cases.

The expected-panic audit found 12 unchanged backend property censuses/statuses/descriptions, six inherited Rust frontend rejections, one inherited harness-selection refusal, one inherited CBMC type-mismatch rejection, and two pre-execution header panics. These last ten cases do not provide backend negative-proof evidence. All 22 match the prior behavior within the explicitly recorded source/executable-path mapping boundaries.

The original small-Cargo batch stopped after all five std checks passed because generated targets exceeded its 12 MiB workspace bound. Its failed status is preserved. All 183 generated target file paths were retained in a byte- and metadata-verified archive, recovering 11.5 MiB; source and raw result logs remained unchanged. Only the unstarted Cargo coverage/UI cases then ran, with completed targets archived between small groups. Documentation passed 6 cases before 3 setup failures exposed a missing offline proptest cache. The 7 unfinished cases completed with the existing correct cache; the first 6 were retained and not replayed. All failed attempts remain recorded. These suite commands used 112.95 active seconds in total, including the failed setup attempt.

Remaining suites: kani, expected, cargo-kani, script-based-pre. Full build/unit gates, both Clippy invocations, warnings, real Firecracker codegen, changed-runtime/affected-consumer controls, exact read/auxiliary/refusal checks and exact finite-evidence reuse still require completion before combined C4 review. No private adoption, production dependency change, or new full Digest query. The full Digest proof remains incomplete.

Source/runtime identities were reauthenticated; no owned compiler/solver job remains. Aggregate research allocation is 6,396,264,448 bytes against the unchanged 6 GiB cap, leaving about 12.0 MiB above the mandatory 32 MiB reserve. The next step is a measured storage plan for the remaining larger gates, not an unbudgeted launch.

Local receipt: corrected-digest/c3-eleven-suite-checkpoint-v1.json, SHA-256 fc986e8b81a8745bdd0e9018a6ee46578b9970e22a2cd06d8c67e73e8c197e4a. Canonical dirty PQ1 checkout preserved.

C3 update on unchanged candidate 55d238314c209978073a3e892b0f39e87f109026:

The full mandatory Kani suite finished in 521.41 active seconds: 627 passed, 1 failed, 23 source/mode-ignored. Source and tool pins remained unchanged, process-group cleanup completed, and the overall storage/time limits held. The suite is not accepted.

The sole failing case is kani/Vectors/any/push_slow.rs. Its raw output says Solver ran out of memory during propositional reduction. under the recorded 8 GiB address-space limit. The baseline had 400 SUCCESS and 6 UNREACHABLE properties; this run had 274 SUCCESS, 4 UNREACHABLE and 128 ERROR. All 406 property identifiers/descriptions, the selected Vec/C-model source files, VCC counts and SAT-size counts match the baseline. Matching counts do not establish byte-identical SAT instances. This is an incomplete solver result, not a verified counterexample or negative-control success. No unchanged retry, higher limit, harness weakening or private adoption was performed.

A harness-associated comparison of all 628 enabled cases found:

619 cases unchanged across property censuses/statuses/descriptions, harness verdicts and error diagnostics.
8 cases with only 9 additional UNREACHABLE first-entry guard properties, matching the planned promoted-entry extension. Every preexisting result in those cases remains unchanged. These unreachable rows do not provide reached-guard evidence; the separate G1/G2 obligations remain required.
1 unresolved solver-memory failure, as above.

I also scanned 602 retained stdout/stderr files from the eleven previously completed suite inventories for resource failures, including the newly observed solver-memory diagnostic; none were found.

Storage preparation deduplicated 1,354 byte-identical immutable vendor-source paths in 370 groups, recovering 53,923,840 bytes while preserving paths, contents, modes, owners and modification times. Runtime binaries, raw logs, archives and generated proof artifacts were excluded. Shared source files must be replaced with independent inodes before any future edit.

Still open: this Kani regression failure; the full expected, cargo-kani and script-based-pre suites; the previously listed build/unit/lint/warnings/real-Firecracker/consumer/reuse gates; and combined C4 review. Eleven of fifteen suites remain fully completed. Full Digest correspondence remains incomplete. No owned compiler or solver job is now running.

Next: a focused causal plan for the single memory failure and a measured storage plan for remaining gates. The failed run and all completed cases remain preserved; no automatic replay or limit increase is selected.

Classification receipt: corrected-digest/c3-kani-suite-v1/outcome-classification-v1.json, SHA-256 669e5e9f8d8a48d35b29f801e41122ca8b26b5aedfeceb6acba3ab09d0cd2e32.

The corrected-Digest candidate 55d238314c209978073a3e892b0f39e87f109026 (tree fe6cd0ef899ccd7b97e260de96657209ee495655) now has 12 of 15 upstream regression suite inventories complete. C3 and private adoption remain open.

The original full Kani run retains its honest result: 627 passed, one solver-memory failure, 23 ignored. A recorded Phase-B resource amendment selected one exact completion of kani/Vectors/any/push_slow.rs: CBMC soft/hard AS 16 GiB, compiler/driver soft AS 8 GiB with inherited hard limit 16 GiB, and 120 active seconds maximum. The same authenticated CBMC binary, default CaDiCaL solver, candidate, harness and verification arguments were used; the private shim records and forwards every argument unchanged. No aggregate disk-cap increase or full-suite replay occurred.

That completion passed in 31.2625 active seconds, with all 406 harness-associated property/status/description results identical to the prior successful baseline: 400 SUCCESS and six UNREACHABLE. Harness census, verdicts, summary and error diagnostics also match. The exact generated GOTO input was retained. Source/tool pins stayed fixed and the owned process group is empty. Full-suite plus completion time, including the failed case, is 552.6727 active seconds.

The combined Kani inventory is therefore 628 passing enabled cases and 23 explicit ignores. This combines the 627 preserved passes with the one completion; it does not relabel the original failed run as passing. Across the suite, 620 cases exactly match baseline outcomes; eight cases have only the nine previously classified added UNREACHABLE first-entry guard rows. Those rows remain no evidence of reached guard/seed behavior.

Remaining suites: expected, cargo-kani, script-based-pre. Full build/unit/Clippy/warnings/real Firecracker codegen and required consumer/reuse gates remain pending, followed by the mandatory combined Astra/Opus C4 review. The one-case memory amendment and original failure remain explicit review inputs. No full Digest retry, runtime adoption, production dependency change or end-to-end correspondence claim.

Evidence: corrected-digest/c3-push-slow-completion-v1/{plan.json,assessment.json,suite-reconciliation-v1.json} under the existing research root. The current storage preflight is recorded separately; the 6 GiB accounting cap, 32 MiB reserve and evidence-preservation rules remain in force. Further full-suite/build launches need a measured storage plan.

C3 milestone on unchanged candidate 55d238314c209978073a3e892b0f39e87f109026 (tree fe6cd0ef899ccd7b97e260de96657209ee495655): the full expected suite is now accepted, with 568 passed and 13 source-declared ignores, in 929.04 active command seconds. This completes 13 of 15 suite inventories; Cargo-Kani and script-based-pre remain.

Changed-outcome reconciliation retained every harness/property/status: 490 prior cases identical; 39 have only additive first-entry guards; 33 are newly enrolled regressions; two changed only printed type/definition IDs in the same unsupported failure; two added successful checks; two changed redundant delayed-check multiplicity. The last two are backed by source inspection, identical-condition MIR, unchanged intended failures/source locations, and the strict read gate. One unchanged-path diagnostic reproduced stable current maps; no nondeterminism claim or repeated solver retries. Shared-cache behavior is banked separately in #1126.

All 44 exact source/MIR read contracts pass on fresh suite outputs. All 30 promoted-entry controls / 3,202 properties match the earlier focused evidence after exact authenticated checkout-path substitution only. The unchanged 110 finite native/Miri cases were reauthenticated against 204 prepared input files and 89 runtime/tool files; no proof rerun was needed.

Preservation work before the suite recovered 56,078,336 net bytes by sharing byte-identical tracked Rust sources across clean frozen snapshots. Historical mtimes are explicitly recorded, current candidate mtimes and all source bytes/Git identities are unchanged, and future edits must replace shared inodes first. No raw proof logs, inputs, runtime binaries or full-caller timing target were removed.

Receipts remain under corrected-digest/c3-expected-suite-v1/ (assessment.json, outcome-reconciliation-v2.json, exact-read-controls/assessment.json, promoted-comparison-v2.json), plus c3-check-origin-mir-v1/ and c3-finite-reuse-v1/. A local classification-parser error was corrected without rerunning the compiler or solver; its failed version and stop receipt are retained.

Still open: the last two suite inventories, build/unit/Clippy/warning/real-Firecracker gates, remaining auxiliary and affected consumer checks, full Digest completeness, and combined C4. No private runtime adoption or new end-to-end proof claim. The dependency correction itself is already merged via #1098. Next: finish the small auxiliary checks while preflighting remaining build storage under the unchanged aggregate cap; no blind large restore or unchanged full-Digest retry.

Further C3 completion on unchanged 55d238314c209978073a3e892b0f39e87f109026:

Cargo-Kani: 72/72 passed, zero ignores; all 13,034 harness-associated property results and all compared verdict/summary/error maps match the accepted COW baseline. 152.63 active command seconds across all case commands. This completes 14/15 upstream suite inventories; script-based-pre remains.
17/17 auxiliary controls accepted: 16 operation/refusal contracts checked against fresh expected outputs, plus one fresh uninit-only zero-size control with the two independently pinned read failures, correct locations and the required reachable cover. These supplement the already accepted 44 exact-read contracts.
No source/runtime changes, private adoption or full-Digest proof claim. No live compiler/solver jobs.

The original Cargo runner stopped at its conservative archive-space preflight after 63 successful verification commands. Those results remain intact; 62 target archives were already complete. After sharing six remaining byte-identical frozen schedule aliases, the completed 63rd target was retained and only the nine never-run cases were executed. The original failed runner receipt is preserved. No compiler/solver command from the successful prefix was repeated, and neither the6GiB aggregate cap nor the62MiB suite workspace allowance increased.

Fresh evidence: corrected-digest/c3-cargo-kani-completion-v1/assessment.json binds all72 original case receipts and lossless target archives. c3-auxiliary-controls-v2/assessment.json binds all17 controls and retains the preceding comparison-only closure-path stop. Source sharing and exact immutable-manifest sharing preserved every path/content hash and recorded original per-path metadata; future edits require private inodes.

Remaining blocker for larger mandatory gates: allocation is6,400,978,944bytes against the6,442,450,944byte cap, leaving7,917,568bytes above the32MiB reserve. Historical host, warning and script target restore footprints are approximately107MB,78MB and261MB respectively (sizing evidence, not minimum fresh-build claims). The owner has been asked to select the prepared6-to7GiB resource amendment; it is not selected or active. Time/memory/concurrency limits, all preservation rules and the full-Digest no-retry boundary stay unchanged. Further large restores/builds await that explicit decision because the frozen plan forbids an implicit cap increase.

Still mandatory after resource selection: script-based-pre, build/unit/both Clippy/warnings/real-Firecracker/manifest-path gates, affected padding/constructor consumers and combined C4; full Digest remains independently incomplete. The dependency correction itself is already merged in #1098.

C3 checkpoint for unchanged candidate 55d238314c209978073a3e892b0f39e87f109026 (tree fe6cd0ef899ccd7b97e260de96657209ee495655):

The manifest-path gate passed, including its cleanup command, in 1.979 active seconds. This checks manifest resolution and selection of an empty harness; it proves zero program-safety properties.
Four script cases completed successfully: standalone and Cargo version reporting, compiler defaults, and unmatched-harness rejection. Their raw stdout is byte-identical to authenticated baseline results. Source and tool pins remain unchanged.
The five-case command stopped during mem-init-reinstrumentation after 2.000 active seconds at its selected 3 MiB local workspace limit. The 6 GiB aggregate cap and 32 MiB reserve were preserved. The command remains failed; the interrupted case receives no credit. Its generated artifacts and original stop receipt are retained. No compiler/solver command was rerun to reconcile the four completed cases.
Overall: 14/15 full suite inventories accepted; script-based-pre has 4/93 cases accepted, one interrupted, and 88 unattempted. The larger build, unit, lint, warning, real Firecracker codegen, affected consumer, and combined C4 gates remain open. Full Digest is still incomplete; there is no private adoption or broader proof claim.

No verification process is running. Allocation after reconciliation was 6,405,496,832 bytes, leaving approximately 3.2 MiB above the required reserve. The prepared 6-to-7 GiB amendment remains pending explicit owner selection. Larger gates have not been launched, and no source, raw evidence, proof input, archive, or installed runtime was removed.

Receipts under corrected-digest/: c3-manifest-path-v1/assessment.json, c3-script-small-prefix-v1/run/result.json, and c3-script-small-prefix-v1/completed-cases-reconciliation-v1.json.

Navigation Menu

Repository navigation

FV: corrected-dependency SHA-256 constructor and Digest correspondence #1097

Translation-cost investigation (2026-10-30)

Copy-on-write representation candidate (2026-10-30)

C4 and private compiler adoption (2026-10-30)

Actual corrected Digest admissibility and raw-read boundary (2026-10-31)

13 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

FV: corrected-dependency SHA-256 constructor and Digest correspondence #1097

Description

Translation-cost investigation (2026-10-30)

Copy-on-write representation candidate (2026-10-30)

C4 and private compiler adoption (2026-10-30)

Actual corrected Digest admissibility and raw-read boundary (2026-10-31)

Activity

Nicola-Ceornea commented on Oct 30, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

13 remaining items

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Oct 31, 2026

Nicola-Ceornea commented on Nov 1, 2026

Nicola-Ceornea commented on Nov 1, 2026

Nicola-Ceornea commented on Nov 1, 2026

Nicola-Ceornea commented on Nov 1, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions