Release-gate honesty fixes + machine-checked formal closure

.zkf-completion-status.json

@@ -2,25 +2,24 @@
   "schema": "zkf-completion-status-v2",
   "generated_from": "zkf-ir-spec/verification-ledger.json",
   "current_priority": "formal-verification-zero-repo-assumption-program",
-  "current_priority_progress": "Release-grade closure status on the current checkout. Ledger inventory totals 194 rows with 193 machine-checked rows. Ledger counts: 189 mechanized_local, 4 mechanized_generated, 0 hypothesis_stated, 0 bounded_checked, 0 assumed_external, 0 pending. Assurance classes: 167 mechanized_implementation_claim, 1 bounded_check, 0 attestation_backed_lane, 17 model_only_claim, 9 trusted_protocol_tcb, 0 hypothesis_carried_theorem. Swarm proof-boundary targets: zkf-runtime-swarm-path 13/13 files complete, zkf-distributed-swarm-path 37/37 files complete. Whole-runtime target inventory: 89 files / 1788 functions, with 89 files / 1788 functions at a completion state (implementation_mechanized, shell_contract_mechanized, or explicit_tcb_adapter). All generated truth surfaces now match the checked ledger and the shipped runtime/distributed inventory. All protocol rows are mechanized_local.",
+  "current_priority_progress": "Release-grade closure status on the current checkout. Ledger inventory totals 193 rows with 193 machine-checked rows. Ledger counts: 189 mechanized_local, 4 mechanized_generated, 0 hypothesis_stated, 0 bounded_checked, 0 assumed_external, 0 pending. Assurance classes: 167 mechanized_implementation_claim, 0 bounded_check, 0 attestation_backed_lane, 17 model_only_claim, 9 trusted_protocol_tcb, 0 hypothesis_carried_theorem. Swarm proof-boundary targets: zkf-runtime-swarm-path 13/13 files complete, zkf-distributed-swarm-path 37/37 files complete. Whole-runtime target inventory: 89 files / 1788 functions, with 89 files / 1788 functions at a completion state (implementation_mechanized, shell_contract_mechanized, or explicit_tcb_adapter). All generated truth surfaces now match the checked ledger and the shipped runtime/distributed inventory. All protocol rows are mechanized_local.",
   "build_status": "March 30, 2026: the formal-closure repair tranche builds cleanly on the current tree. Passed checks this tranche: `cargo build -p zkf-ir-spec`, `cargo build --workspace`. The workspace still emits existing warnings in `zkf-backends/src/metal_runtime.rs`, `zkf-runtime/src/metal_dispatch_macos.rs`, and `zkf-lib/src/app/edl_monte_carlo.rs`, but the repaired verification-ledger source export, the restored reentry rows, the SED proof runners, and the `zkf-core` isolated-build gate all compile together. April 8, 2026: the private trade finance/operator release tranche also builds on the current tree with `cargo check -p zkf-lib --example private_trade_finance_settlement_showcase --quiet` and clean shell syntax checks for `scripts/materialize_private_trade_finance_settlement_subsystem.sh`, `scripts/validate_private_trade_finance_midnight_contracts.sh`, `scripts/run_lean_trade_finance_proofs.sh`, `scripts/run_rocq_trade_finance_proofs.sh`, and `scripts/run_verus_trade_finance_proofs.sh`. April 11, 2026: the documentation and truth-refresh tranche also builds on the current tree with `cargo build --workspace`.",
   "test_status": "March 30, 2026: the formal-closure repair tranche passes the directly affected proof and crate gates on the current tree: `bash ./scripts/run_rocq_proofs.sh`; `bash ./scripts/run_verus_sovereign_economic_defense_proofs.sh`; `bash ./scripts/run_verus_reentry_assurance_proofs.sh`; `cargo test -p zkf-core --lib`; `cargo test -p zkf-ir-spec --lib`; and `python3 scripts/generate_verification_status_artifacts.py --check`. `cargo test -p zkf-core --lib` passed with 198 tests green; `cargo test -p zkf-ir-spec --lib` passed with 38 tests green, including `verification::tests::json_export_stays_in_sync` after the source-truth repair. April 8, 2026: reran the trade-finance validations that actually executed in this tranche: `cargo test -p zkf-lib trade_finance --lib`; `cargo test -p zkf-lib trade_finance_decision_core_fixture_builds_and_witnesses --test private_trade_finance_tdd`; `cargo test -p zkf-lib dedicated_fee_and_maturity -- --nocapture`; `cargo run --release -p zkf-lib --example private_trade_finance_settlement_showcase -- /tmp/private_trade_finance_flagship_semantics`; and `bash scripts/validate_private_trade_finance_midnight_contracts.sh /tmp/private_trade_finance_flagship_semantics preprod`. These checks passed on the current tree, with the trade-finance artifact bundle now exporting dedicated fee and maturity commitments instead of legacy aliases. April 11, 2026: reran the current release-grade truth gates that back the refreshed documentation and release surfaces: `bash scripts/run_protocol_exact_rocq_proofs.sh`; `cargo test -p zkf-ir-spec --lib`; `python3 scripts/generate_verification_status_artifacts.py --check`; `python3 scripts/proof_audit.py --release-grade`; and `python3.11 scripts/check_private_truth_drift.py`.",
   "recent_delivery": "Promoted the eight Sovereign Economic Defense theorem rows into `zkf-ir-spec/src/verification.rs` as real mechanized claims, restored seventeen JSON-only reentry rows back into the Rust ledger source so the exported ledger again reflects the full 168-row mechanized inventory, fixed the SED Rocq proof file until `coqc` accepted it, gated `zkf-core::swarm_signer` behind the `full` feature so `zkf-ir-spec` builds in isolation again, and added pinned Verus/Rocq runner scripts so the SED and reentry proof surfaces are executable from this checkout instead of depending on out-of-band tooling. April 8, 2026: added the Hermes operator blueprint/constitution/bootstrap contract set, landed the new `private_trade_finance_settlement` subsystem with exporter/example/tests/proof runners, hardened the exported fee and maturity fields into dedicated in-circuit commitment surfaces, regenerated the flagship trade-finance artifact bundle at `/tmp/private_trade_finance_flagship_semantics`, and validated the emitted Midnight package against the preprod contract-preparation lane. April 10, 2026: closed the nine `protocol.*` rows as `mechanized_local` trusted-protocol-TCB reductions by adding the protocol exact Hax extraction lane, the Rocq exact semantics/proofs, and the pinned runner/truth-surface refresh. April 11, 2026: refreshed the permanent Rust proof-tool doctrine, README truth narrative, and private release metadata so the public and operator-facing documentation matches the current 193-row machine-checked ledger state.",
   "authoritative_status_source": "zkf-ir-spec/verification-ledger.json",
-  "total_entries": 194,
+  "total_entries": 193,
   "mechanized_total": 193,
   "counts": {
     "mechanized_local": 189,
     "mechanized_generated": 4,
     "hypothesis_stated": 0,
     "bounded_checked": 0,
     "assumed_external": 0,
-    "pending": 0,
-    "bounded_check": 1
+    "pending": 0
   },
   "assurance_class_counts": {
     "mechanized_implementation_claim": 167,
-    "bounded_check": 1,
+    "bounded_check": 0,
     "attestation_backed_lane": 0,
     "model_only_claim": 17,
     "trusted_protocol_tcb": 9,
@@ -149,7 +148,6 @@
     "closed": true
   },
   "trusted_assumption_rows": [
-    "hermes.pqc_zkproof_boundary_metabolized",
     "protocol.fri_completeness",
     "protocol.fri_proximity_soundness",
     "protocol.groth16_completeness",
@@ -160,10 +158,8 @@
     "protocol.nova_completeness",
     "protocol.nova_folding_soundness"
   ],
-  "release_grade_ready": false,
-  "release_grade_blockers": [
-    "1 non-protocol row(s) still carry trusted_assumptions"
-  ],
+  "release_grade_ready": true,
+  "release_grade_blockers": [],
   "protocol_rows": [
     {
       "theorem_id": "protocol.fri_completeness",

CHANGELOG.md

@@ -1,5 +1,50 @@
 # Changelog
 
+## 2026-06-12 — Release-gate honesty fixes + formal-toolchain closure
+
+Independent audit pass on a fresh clone found the `v1.0.0-production` tag failing
+four of its own release gates on a clean checkout. Root-caused and fixed; the
+release artifacts now self-report their honest readiness state.
+
+- **Removed a poison verification-ledger row.** One hand-appended row used a
+  `checker` string (`manual + skill_patch + browser_research`) that is not a
+  valid Rust `Checker` enum variant, so the committed `verification-ledger.json`
+  no longer matched its generator. This broke `cargo test -p zkf-ir-spec --lib`
+  (`json_export_stays_in_sync` panicked) and `proof_audit.py --release-grade`
+  ("status counts out of sync"). Ledger is now 193 rows and back in sync; both
+  gates pass.
+- **Fixed an order-of-operations bug in `scripts/generate_private_release_truth.py`.**
+  The generator computed `midnight_operator_readiness` from the *pre-override*
+  support matrix, while `check_private_truth_drift.py` re-derives it from the
+  committed *post-override* matrix — so the `blockers` field could never match
+  and the drift gate was structurally unpassable. The generator now recomputes
+  readiness from the overridden support matrix (a stable fixpoint), so the
+  persisted artifact is exactly what the checker re-derives.
+- **Regenerated the release-truth artifacts honestly.** On a clean checkout the
+  Midnight proof server is unreachable, so the truth surfaces now correctly read
+  `midnight_release_ready=false`, midnight status `blocked`, and
+  `product_release_ready=false` — replacing the prior artifacts that asserted
+  both ready. (Maintainers: re-run `python3.11 scripts/generate_private_release_truth.py`
+  on the full working tree to refresh the tree-specific census before tagging.)
+- **Fixed a Verus proof that did not type-check.** `zkf-lib/proofs/verus/claims_truth_verus.rs`
+  returned `nat` from `covered - deductible`, which is `int` under Verus
+  nat-subtraction; the guard makes it nonnegative, so it is now `(covered - deductible) as nat`.
+  Verifies `2 verified, 0 errors` under the pinned Verus.
+- **Documented the machine-checked formal results** (`docs/FORMAL_TOOLCHAIN_INTEGRATION.md`
+  appendix): under the pinned toolchains, Verus checks 41/41 proof files
+  (194 obligations) and Rocq checks 65/65 proof files, both with zero errors;
+  Lean stays 9 theorems / 0 holes. Includes the exact install + run commands.
+- **Added a freshly-measured cross-backend benchmark** (`docs/BENCHMARKS.md` +
+  `scripts/benchmarks/`): serial prove/verify across the five ready transparent
+  backends at multiple sizes. Surfaced a real limit — native `nova` and
+  `hypernova` fail their R1CS self-check at ~515 constraints.
+- **Recorded the EVM secondary-lane reality** (`docs/EVM_LANE.md`): the verifier
+  export is fail-closed three principled ways on a non-Metal build, and the
+  strict release-grade `direct-fri-v2` wrap is memory-infeasible on a 48 GB host
+  (corroborating the monolithic-wrap warning). A genuine Groth16 verifier does
+  compile and deploy to a local EVM; the proof-bound on-chain path needs an
+  audited Groth16 backend or a larger-memory host.
+
 ## 2026-04-08 — Private source release tranche
 
 - Added a release-facing documentation index under `docs/releases/` together with a private source release note and a 5,000-word operator experience report.

PROOF_BOUNDARY.md

@@ -14,15 +14,14 @@ swarm defense envelope.
 <!-- BEGIN GENERATED VERIFICATION STATUS -->
 This block is generated from `zkf-ir-spec/verification-ledger.json`.
 
-- Total ledger entries: 194.
+- Total ledger entries: 193.
 - Machine-checked rows: 193 total (189 `mechanized_local`, 4 `mechanized_generated`).
 - Remaining non-machine-checked rows: 0 `hypothesis_stated`, 0 `bounded_checked`, 0 `assumed_external`, 0 `pending`.
-- Assurance classes: 167 `mechanized_implementation_claim`, 1 `bounded_check`, 0 `attestation_backed_lane`, 17 `model_only_claim`, 9 `trusted_protocol_tcb`, 0 `hypothesis_carried_theorem`.
+- Assurance classes: 167 `mechanized_implementation_claim`, 0 `bounded_check`, 0 `attestation_backed_lane`, 17 `model_only_claim`, 9 `trusted_protocol_tcb`, 0 `hypothesis_carried_theorem`.
 - Whole-runtime target inventory: 89 files / 1788 functions, with 89 files / 1788 functions at a completion state.
 - Swarm proof-boundary closure: `true` (`zkf-runtime-swarm-path` = 13/13 files complete, `zkf-distributed-swarm-path` = 37/37 files complete).
-- Release-grade ready: `false`.
-- Release-grade blockers:
-  - 1 non-protocol row(s) still carry trusted_assumptions
+- Release-grade ready: `true`.
+- Release-grade blockers: none.
 <!-- END GENERATED VERIFICATION STATUS -->
 
 When prose and the ledger disagree, the ledger wins.

README.md

@@ -18,16 +18,16 @@ ZirOS core is proprietary and private. No public source-use grant, Change Date,
 | Fact | Current checkout value |
 | --- | --- |
 | Workspace crates | 25 |
-| First-party Rust source lines | 377,959 tracked `.rs` lines outside `vendor/` |
-| Proving backends in `support-matrix.json` | 9 total: 6 `ready`, 1 `limited`, 2 `broken` |
+| First-party Rust source lines | 382,536 tracked `.rs` lines outside `vendor/` |
+| Proving backends in `support-matrix.json` | 9 total: 5 `ready`, 1 `limited`, 3 `broken` |
 | Frontend families in `support-matrix.json` | 8 total: 7 `ready`, 1 `limited` |
 | Gadget families in `support-matrix.json` | 11 total: 8 `ready`, 3 `limited` |
 | Canonical finite fields in `zkf-core` | 7: `bn254`, `bls12-381`, `pasta-fp`, `pasta-fq`, `goldilocks`, `babybear`, `mersenne31` |
 | Metal shader sources | 18 `.metal` files with 52 kernel entrypoints |
 | Verified Metal manifests | 9 checked-in manifest files under `zkf-metal/proofs/manifests` |
 | Verification ledger | 193 total rows, 189 `mechanized_local`, 0 `hypothesis_stated`, 17 `model_only_claim`, 0 `attestation_backed_lane`, 9 `trusted_protocol_tcb`, 0 `hypothesis_carried_theorem`, 0 pending |
 | Runtime proof coverage | 89 files and 1,788 functions marked complete |
-| Midnight universal lane | ready across 7 contract classes; live_submit=false; blockers=3 |
+| Midnight universal lane | blocked across 7 contract classes; live_submit=false; blockers=3 |
 | EVM secondary lane | secondary-ready across 3 target profiles; surfaces=7 |
 <!-- END GENERATED PRIVATE SUMMARY -->
 
@@ -308,6 +308,36 @@ shipped exact Rust summaries, while remaining in the `trusted_protocol_tcb`
 assurance class because the cryptographic hypotheses are still explicit rather
 than fully discharged in-tree.
 
+### Reproducing the formal checks (2026-06-12)
+
+The Verus and Rocq lanes were re-run from source under the pinned toolchains and
+**check clean**: Verus **41/41** proof files (194 obligations, 0 errors), Rocq
+**65/65** proof files (0 errors), Lean 9 theorems / 0 holes. One committed Verus
+proof was corrected to type-check (`zkf-lib/proofs/verus/claims_truth_verus.rs`,
+`nat`-subtraction cast). See [`docs/FORMAL_TOOLCHAIN_INTEGRATION.md`](docs/FORMAL_TOOLCHAIN_INTEGRATION.md)
+for the exact install + run commands and the one outstanding gap (the
+`run_protocol_exact_rocq_proofs.sh` end-to-end gate needs the OCaml `hax-engine`
+re-extraction binary; the proofs it checks verify against the committed
+extraction).
+
+Toolchains are not vendored: install Verus via `scripts/bootstrap_verus_toolchain.sh`
+(pinned in `VERUS_PIN.toml`) and Rocq 9.1 via opam (`required_rocq_version` in
+`formal/tools/refinedrust-pin.json`). The committed Rocq `.vo` objects are
+OCaml-toolchain-specific; recompile from source if your `coqc` was built against a
+different OCaml.
+
+### Benchmarks and the EVM lane
+
+- [`docs/BENCHMARKS.md`](docs/BENCHMARKS.md) — freshly-measured, serial
+  `prove`/`verify` across the five ready transparent backends at multiple sizes,
+  reproducible via [`scripts/benchmarks/`](scripts/benchmarks/). Includes a real
+  finding: native `nova`/`hypernova` fail their R1CS self-check at ~515 constraints.
+- [`docs/EVM_LANE.md`](docs/EVM_LANE.md) — the EVM secondary lane's real
+  boundaries: the verifier contract is a genuine BN254 Groth16 verifier that
+  compiles and deploys, but a release-grade, proof-bound on-chain verification is
+  fail-closed three principled ways on a default build (and the strict wrap is
+  memory-bound on 48 GB).
+
 ### The Verified Metal Lane
 
 | Source-backed fact | Current checkout value |