FV: verify corrected generic-array constructor contracts

.github/workflows/sha256-constructor-evidence.yml

@@ -0,0 +1,38 @@
+name: FV (recorded SHA-256 constructor evidence)
+
+on:
+  push:
+    branches: [master]
+    paths: &constructor_paths
+      - 'contracts/verification/sha256-constructor/**'
+      - 'contracts/verification/sha256-padding/**'
+      - 'sphincs-c10/src/hash.rs'
+      - 'sphincs-c10/src/params.rs'
+      - 'sphincs-c10/Cargo.toml'
+      - 'Cargo.lock'
+      - '.github/workflows/sha256-constructor-evidence.yml'
+  pull_request:
+    paths: *constructor_paths
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: constructor-evidence-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
+jobs:
+  recorded-evidence:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 5
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        with:
+          persist-credentials: false
+      - name: Check recorded evidence and source binding (no solver replay)
+        working-directory: contracts/verification/sha256-constructor
+        run: |
+          python3 check.py
+          python3 test_gate.py -v
+          python3 inputs.py "$RUNNER_TEMP/constructor-inputs"

contracts/verification/easycrypt/c10-port/RESEARCH-LIMITS.md

@@ -1241,8 +1241,27 @@ original complete `Digest` correspondence and existing hash postulates remain
 open; neither finite source checks nor these universal model theorems substitute
 for that link.
 
+**Corrected-dependency constructor component (2026-10-30).** The owner selected
+the exact previously reviewed `generic-array 0.14.7` correction as a research
+target. The isolated [`sha256-constructor` profile](../../sha256-constructor/README.md)
+checks U32/U64 zero defaults and, for every 64-byte input, the observing
+generator's returned bytes, call count and increasing index order. All semantic
+assertions and positive covers are reached. Byte corruption and reversed-order
+controls fail only their intended assertions. A paired U1 diagnostic exposes
+initialization-check failures in the original dependency and passes for the
+correction. All default, initialization, validity and unwind guards remain.
+
+The 110 native and recursive-Miri cleanup cases, including every injected panic
+index at U0/U1/U8/U32/U64, are finite evidence; an omitted-prefix-drop mutation
+is rejected. They are not universal panic/unwind or arbitrary-closure proofs.
+Both actual corrected full-caller code-generation diagnostics hit their compiler
+CPU bound without completing translation or running a solver. The new profile
+preserves their failures and the original large-control timeout honestly.
+Production dependencies, original-source #1067 and complete `Digest`
+correspondence remain unchanged/open. Issue #1097 tracks the corrected target.
+
 **Remaining backend boundary.** The word, complete-block, bounded initialized
-streaming and corrected-dependency padding results do not connect the existing
+streaming, corrected constructors and corrected-dependency padding results do not connect the existing
 `sha256_bytes`/`sha256_parts` postulates to an entire Rust `Digest` execution.
 General Rust streaming updates, source-level accumulated-length/padding composition,
 dispatch, unsafe conversions, accelerated backends, and the STM32 driver

contracts/verification/sha256-constructor/README.md

@@ -0,0 +1,177 @@
+# Corrected generic-array constructors for SHA-256 research
+
+This profile checks the exact `generic-array 0.14.7` correction preserved in
+the [padding profile](../sha256-padding/README.md). The owner selected that
+corrected dependency as a research proof target on 2026-10-30.
+[Issue #1097](https://github.com/EthereumPhone/PQ1/issues/1097) tracks this work;
+the original-dependency correspondence gap remains
+[#1067](https://github.com/EthereumPhone/PQ1/issues/1067).
+Production Cargo dependencies are unchanged.
+
+The correction writes each generated element through a raw pointer and only
+then advances the initialized prefix. Its `ArrayBuilder::drop` destroys only
+that prefix. Public `iter_position` and other constructors are outside the
+correction. The exact patch, original archive, compiler model and retained
+runtime are shared with the padding profile; this batch changes none of them.
+
+## Accepted scope
+
+The symbolic cases retain default, uninitialized-memory, valid-value and
+unwinding checks. The two main harnesses use unwind 65:
+
+- U32 and U64 byte defaults return all zero bytes, with the final-byte cover
+  reached. The complete output has 313 properties: 300 successful checks,
+  12 unreachable checks, and one satisfied cover.
+- For every input `[u8; 64]`, the observing generator returns those bytes in
+  order and is called exactly once at each index, in increasing order. All
+  byte/count/order assertions are reached and successful. There are 265
+  properties: 258 successful checks, six unreachable checks and one satisfied
+  edge-value cover. This is a contract for this observing generator, not for
+  arbitrary closures, element types or array lengths.
+
+Changing the first generated byte fails only the zero-value assertion.
+Reversing the generator's index fails only its order assertion. Later checks
+or covers made unreachable by those failing assertions are retained explicitly.
+Unsupported-operation failures, timeout, build failure or another failed
+assertion cannot satisfy either negative control.
+
+A separate paired U1 diagnostic passes for the correction and fails two
+initialization checks for the original dependency, at mutable-slice formation
+and mutable iteration. Its output assertion and cover still succeed, showing
+why checking output bytes alone is insufficient. This is an explicit boundary
+of the retained experimental model, not a settled statement about every Rust
+validity interpretation. A preceding U32/U64 original-source control exhausted
+1,800 active seconds without a complete result; it is preserved as an
+incomplete diagnostic and receives no negative-control credit.
+
+Cleanup has **finite** evidence: all 110 complete-or-panicking generator cases
+at U0/U1/U8/U32/U64 pass natively and under experimental recursive Miri. These
+check generator order and exact initialized-prefix destruction, including every
+injected stop index at those sizes. Omitting the first prefix destructor fails
+at the intended `initialized-prefix drop mismatch` assertion. This does not
+establish universal panic/unwind equivalence or arbitrary destructor behavior.
+The accepted cleanup runs use fresh target directories and isolated Cargo homes.
+Both positive logs contain exactly 105 intended panic-hook messages. The gate
+also binds the Miri run-info's working directory and input to the pinned v2
+source and checks its isolated compilation/runner path.
+
+## Remaining boundary
+
+These constructor results complement the separate padding, initialized
+streaming-step and list-level history proofs. They do not compose those results
+into complete Rust `Digest` execution, connect the length counter to every
+update, or prove the original dependency. Unrestricted slices, callbacks,
+alias/provenance semantics, cross-tool correspondence, hardware/accelerated
+backends and cryptographic security remain outside the claim.
+
+Two code-generation diagnostics exercised the actual corrected software
+callers: a paired one-shot/streaming root and a narrowed one-shot root. Both
+compilers received SIGXCPU at the inherited 175-second soft CPU bound before
+translation completed. Neither ran a solver or proved a caller property.
+The source, command, output and assessment are under `frozen/diagnostics`.
+The next complete-caller step needs a bounded translation-cost diagnosis;
+these incomplete experiments do not justify changing or suppressing guards.
+
+## Check the recorded evidence
+
+With Python 3.12+, GNU patch and git:
+
+```sh
+python3 check.py
+python3 test_gate.py -v
+python3 inputs.py /absolute/new/constructor-inputs
+```
+
+The gate authenticates the parent profile and its production-source/dependency
+closure, all frozen inputs, exact historical harness/manifest/lock identities,
+recorded tool inventory and complete raw property outputs. Every property
+identity, description and status is checked. Historical locations are checked
+against the complete saved census; replay permits dependency paths to move
+while preserving exact semantic assertion/cover locations in the harness.
+Finite cleanup output is checked separately from symbolic evidence.
+The CI workflow performs these recorded-evidence checks; **it does not run a
+solver or establish new proof evidence**.
+
+`inputs.py` reconstructs the archived packages and exact correction through the
+parent preparer, then applies the three declared single-edit controls. Archived
+`.rs.in` files are byte-identical source templates, materialized as `.rs` only
+in the isolated prepared crates. They are not enrolled in the default Kani
+runtime or its production harness census. Input validation independently
+reconstructs the files and rejects changed source or extra build scripts;
+editing a generated inventory cannot authorize different inputs.
+
+The historical symbolic runners independently reconstructed and compared
+dependency files before and after execution. Their result records pin project
+files and runtime tools; the main positive records did not separately serialize
+the complete dependency inventory. The superseded cleanup runner was weaker:
+it independently pinned only generic-array's `src/lib.rs`, and compared the
+remaining baseline package files against that same working directory. Its Miri
+cache also reused run-info for the earlier v1 source while the receipt named
+v2. Those invalidly attributed receipts remain under `frozen/diagnostics` and
+receive no current cleanup credit. The replacement commands independently
+reconstructed and inventoried all dependency files before and after execution,
+with fresh targets and Cargo homes. The gate reconstructs both inventories
+again. This is fresh replacement evidence, not retrospective authentication of
+the old executions.
+
+All four replacement baseline commands passed. Its collector then mishandled
+Miri's string-form argument list; a separate completion checked the unchanged
+inputs, tools and saved command/log identities without repeating execution.
+The receipt preserves that collector failure and its completion. The fresh
+run-info copy identifies `cleanup-v2`; both logs expose all intended panics.
+
+All six symbolic runs shared a serial Cargo compilation cache. The initial
+code-generation result and log are preserved and bound to the reused receipt
+digest, positive harness/tool identities and shared target path. The source
+controls changed their selected dependency or harness and rebuilt as needed;
+they reused compilation artifacts, never a prior solver verdict. The proofs
+therefore also trust Cargo's freshness decisions: not every translated artifact
+was independently inventoried before each solver run. Fresh replay uses a new
+target directory. Frozen runner source and present-day reconstruction preserve
+these boundaries rather than inventing a retrospective run inventory.
+Recorded output is evidence, not authentication of a historical host or a
+proof that Kani/Miri, the private compiler or their memory models are sound.
+The parent's source-to-binary and system-library trust boundaries still apply.
+
+## Fresh symbolic replay
+
+Use the retained tool paths described in the parent's
+[runtime instructions](../sha256-padding/README.md#fresh-replay-with-the-retained-runtime).
+No toolchain is installed or substituted. A newly rebuilt compiler needs its
+own evidence and review. The Rustup home embedded in the retained driver must
+match the original path.
+
+```sh
+python3 run.py \
+  --prepared "$CONSTRUCTOR_INPUTS" \
+  --kani-root "$CONSTRUCTOR_KANI_TREE" \
+  --rustup-home "$CONSTRUCTOR_RUSTUP_HOME" \
+  --rustup "$CONSTRUCTOR_RUSTUP_BINARY" \
+  --solver-bin "$CONSTRUCTOR_SOLVER_BIN" \
+  --compat-libs "$CONSTRUCTOR_COMPAT_LIBS" \
+  --case default \
+  --output "$CONSTRUCTOR_BUDGET_ROOT/new-default-run" \
+  --budget-root "$CONSTRUCTOR_BUDGET_ROOT"
+```
+
+Cases are `default`, `generate`, `corrupt-byte`, `reverse-generation`,
+`focused-corrected` and `focused-original`. Each output directory is new;
+inputs and outputs belong inside the aggregate 6,144 MiB allocation budget.
+Run cases serially. Use `--check-only` to authenticate inputs/runtime without
+execution, or `--codegen-only` for compilation without proof credit. The main
+cases have a 1,800-second active-time bound; focused cases and code generation
+have 180 seconds. Linux monotonic time excludes laptop suspension. Raw output
+and terminal receipts survive failure.
+
+For finite cleanup reproduction, the two prepared crates are `cleanup-v2` and
+`cleanup-wrong-prefix`. Their exact native/Miri commands, tool digests,
+environments and expected exits are in `frozen/receipts/cleanup-*.json`;
+`frozen/runners/run_cleanup_isolated.py` preserves the corrected bounded
+runner; the initial collector and its completion are also retained. Its paths
+refer to the research workspace and are not a relocatable
+entrypoint. The retained Miri sysroot's complete digest inventory is also
+preserved. Recursive Miri is experimental. Matching output from different
+tools or without that flag is new evidence, not an exact replay of these runs.
+Historical symbolic commands and superseded cleanup commands sanitized inherited
+environment variables but used the existing user Cargo home. The accepted
+replacement cleanup commands instead use isolated Cargo homes and fresh targets.