chore(v0.56): codecov config (#923) + three logged deferrals to v0.57

artifacts/release-v0.56.yaml

@@ -150,7 +150,11 @@ artifacts:
       and the gpio differential gate it — a smaller wrong answer is a
       regression, not a win. Carries a before/after number or it is not done.
     status: proposed
-    release: v0.56
+    release: v0.57
+    # DEFERRED from v0.56 (scope decision, logged not silent):
+    #   #846 changes SHIPPING BYTES for a 4-byte win; it needs the frozen
+    #   anchors + the gpio differential re-pinned in its own gated lane, not a
+    #   release-tail squeeze.
     tags: [optimization, gale, code-size]
     links:
       - type: derives-from
@@ -179,7 +183,10 @@ artifacts:
       Gate: the cross-backend parity ledger flips in the SAME commit that makes
       them lower, and the ledger's stale-entry check keeps the count honest.
     status: proposed
-    release: v0.56
+    release: v0.57
+    # DEFERRED from v0.56 (scope decision, logged not silent):
+    #   #851 aarch64 param homing is capability work needing its own execution
+    #   differential across the 4 named divergences.
     tags: [aarch64, capability-gap, epic-851]
     links:
       - type: derives-from
@@ -386,3 +393,43 @@ artifacts:
       priority: must
       verification-track: execution-differential
       issue: "#931, #930"
+
+  - id: RQ-57-I32CONST
+    type: system-req
+    title: "i32.const is covered by NEITHER half of the verification story"
+    description: >
+      #933, reported by a consumer discharging a downstream object-code
+      obligation. `synth verify` DECLINES Const/Local ops as register
+      operations, deferring them to the per-rule Rocq theorems — a reasonable
+      split. Three of the four deferred-to theorems are Qed
+      (`local_get/set/tee_correct`, `i64_const_correct`). `i32_const_correct`
+      is Admitted, so for `i32.const` the SMT half skips it AND the proof half
+      is open. Nothing covers the single most common op in any module.
+      This is NOT missing mathematics: `movw_movt_reconstruct_Z` and
+      `i32_const_large_reconstruct` are both Qed. The theorem is FALSE AS
+      STATED — it quantifies over un-normalized `Z` representatives, and a
+      counterexample exists (n = 2^32 + 0x10000). Closing it is a CONTRACT
+      change, one of: (a) normalize `I32Const` at the WASM model boundary
+      (push `VI32 (I32.repr n)`), which is what a real wasm i32.const means and
+      lets `i32_const_large_reconstruct` discharge it directly; or (b) add the
+      `I32.valid_unsigned n` hypothesis, the contract the #73 div_s proof
+      adopted. (a) is the principled one and touches 9 `.v` files.
+      DEFERRED from v0.56 (scope decision, logged not silent): this is a
+      contract change under the repo's own #166 gate — "never weaken a theorem
+      to force a Qed" — so it needs deliberate review rather than a
+      release-tail squeeze, and the hermetic Rocq rebuild is a long verify
+      loop. The gap is disclosed in the source, not hidden; what makes it
+      urgent is that it turned out to be load-bearing for someone downstream.
+    status: proposed
+    release: v0.57
+    tags: [verification, rocq, coverage-gap, consumer-reported]
+    links:
+      - type: derives-from
+        target: BR-001
+      - type: refines
+        target: NFR-002
+    fields:
+      req-type: functional
+      priority: should
+      verification-track: proof
+      issue: "#933"

codecov.yml

@@ -0,0 +1,71 @@
+# Codecov configuration — #923.
+#
+# Before this file there was NO codecov config anywhere in the repo, so
+# `codecov/patch` ran on codecov's defaults (patch target `auto`: changed lines
+# must meet the project average). Nobody chose that. It failed on essentially
+# every PR and was treated as advisory for dozens of merges.
+#
+# That habit is not free. It is the same reflex that once let a red **Clippy**
+# through as "just codecov" (#683, main went red). A check everyone is trained
+# to ignore is worse than no check, so the choice here is to state the intent in
+# config rather than leave it inferred from merge habits.
+#
+# ---------------------------------------------------------------------------
+# WHAT WAS MEASURED FIRST (#923 step 1), and how it changed the plan
+# ---------------------------------------------------------------------------
+# `cargo llvm-cov --workspace` (CI's exclusion set), classified per file by
+# whether an out-of-process EXECUTION oracle asserts it:
+#
+#     class          lines    instrumented-covered
+#     differential   50238    86.2 %
+#     unit-only      47754    83.4 %
+#     TOTAL          97992    84.8 %
+#
+# The hypothesis in #923 was that differential-covered files are dragged down
+# because `cargo llvm-cov` instruments the Rust suite IN-PROCESS while the
+# differentials spawn `synth` as a separate, uninstrumented process. **At the
+# aggregate that is not what the data shows** — differential-asserted files read
+# slightly HIGHER (86.2 %) than unit-only ones (83.4 %). The effect is real
+# per-file (`synth-backend-aarch64/src/backend.rs`: 267 lines, 44.2 %, exercised
+# end-to-end constantly) but it does not dominate, and 6945 uncovered lines sit
+# in differential-asserted files.
+#
+# The measurement also named the real target, which is NOT what was expected:
+# `synth-verify/src/arm_semantics.rs` — 2481 lines at 47.4 %, unit-only, the
+# largest single genuine gap in the workspace. Tests there would add evidence;
+# tests written to lift the aarch64 backend's number would not.
+#
+# ---------------------------------------------------------------------------
+# THE THRESHOLDS, and why these numbers
+# ---------------------------------------------------------------------------
+coverage:
+  status:
+    project:
+      default:
+        # Measured 84.8 % at v0.56. 80 % is a floor chosen to be met today with
+        # real headroom, so a red `project` means coverage genuinely FELL rather
+        # than "a PR touched an awkward file". Raise it when the arm_semantics.rs
+        # gap closes; the ratchet direction is up.
+        target: 80%
+        threshold: 1%
+        informational: false
+
+    patch:
+      default:
+        # EXPLICITLY informational, not de-facto.
+        #
+        # This is the honest encoding of how it is already used, and it is not a
+        # surrender: a patch status cannot distinguish "these changed lines are
+        # untested" from "these changed lines are asserted by an execution
+        # differential the instrument cannot see". Until the differentials emit
+        # profile data (VG-009), a blocking patch gate reports a number it has
+        # no way to make true.
+        #
+        # It still POSTS, so the signal stays visible on the PR — it just does
+        # not pretend to be a gate. `project` above is the one that blocks.
+        informational: true
+
+comment:
+  layout: "reach, diff, flags, files"
+  behavior: default
+  require_changes: false