claims.yaml

# claims.yaml — synth's load-bearing documentation claims, bound to evidence.
#
# Per the pulseengine-claude `claim-verification` skill: a README is a claim
# about the system — the same species as a requirement, pointing the other way.
# CI runs `scripts/claim_check.py claims.yaml`; drift = red.
#
# DESIGN (since the claim-surface extension PR):
#
#   * Numbers live in ONE machine-derived artifact — `artifacts/status.json`,
#     emitted from the `status_fields:` derivations below by
#     `scripts/claim_check.py claims.yaml --emit-status` and STALENESS-GATED
#     (the committed file must equal re-derivation, byte for byte). README
#     badges (shields.io dynamic-JSON) and the GENERATED
#     `docs/status/FEATURE_MATRIX.md` surface them; README/linked-doc prose
#     stays number-free.
#   * Qualitative prose claims ("all i32/i64 ops have T1 proofs", "f64
#     complete", "verified" wording) stay in prose ONLY when pinned here as
#     pattern-claims.
#   * CLAUDE.md and coq/STATUS.md still hand-carry headline numbers (they are
#     working documents, not README-linked marketing surface); their numbers
#     stay count-eq-pinned so a proof landing must update doc + ledger in the
#     same PR.
#   * The README's linked-doc surface is closed: every relative .md link must
#     be claim-covered, generated, or allowlisted with a rationale
#     (`readme_link_coverage:` below).
#   * GitHub repo metadata (description/topics) is pinned under
#     `repo_metadata:` and checked by `scripts/repo_metadata_check.py`
#     (CI step in the claim-check job; API failure = loud SKIP, never a
#     false red).
#
# When a proof lands / a rule lands / a roadmap status changes: regenerate the
# derived artifacts (`--emit-status`), and update CLAUDE.md/coq/STATUS.md AND
# this ledger in the same PR. Never "fix" a red gate by loosening the ledger
# while leaving a prose overclaim in place.
#
# Not bound here (deliberately — runtime-derived, gated elsewhere): the
# 141/141 ordeal-vs-Z3 agreement and 139/139 validator counts (re-derived by
# the CI `verify` job that actually runs them), the wasm spec-suite compile
# rate (CI-tracked), and cycle/size numbers (gale silicon + differential
# jobs).

# -----------------------------------------------------------------------------
# status_fields — the derivations behind artifacts/status.json (the single
# machine-derived numbers artifact). Each field is re-computed from source on
# every claim_check run; the committed status.json and the generated
# docs/status/FEATURE_MATRIX.md must match exactly.
# -----------------------------------------------------------------------------
status_fields:
  version:
    kind: capture
    file: Cargo.toml
    pattern: '^version = "([^"]+)"'   # [workspace.package].version (pin-swept)
  rocq_qed:
    kind: count
    pattern: 'Qed\.'
    glob: ['coq/Synth/**/*.v']
  rocq_admitted:
    kind: count
    pattern: 'Admitted\.'
    glob: ['coq/Synth/**/*.v']
  rocq_admit_tactics:
    kind: count
    pattern: '^\s*admit\.'
    glob: ['coq/Synth/**/*.v']
  rocq_axioms:
    kind: count
    pattern: '^\s*(?:Axiom|Parameter) '
    glob: ['coq/Synth/**/*.v']
  sel_dsl_rules:
    kind: count
    pattern: '^rule_'
    glob: ['coq/vcr_sel_rules.manifest']
  sel_dsl_rule_qed:
    kind: count
    pattern: '^(?:Theorem|Lemma) rule_\w+_correct'
    glob: ['coq/Synth/Synth/VcrSelRules.v']
  sel_dsl_pilot_qed:
    kind: count
    pattern: 'Qed\.'
    glob: ['coq/Synth/Synth/VcrSelPilot.v']
  sail_bridge_qed:
    kind: count
    pattern: 'Qed\.'
    glob: ['coq/Synth/ARM/SailArmBridge.v']
  # -- ISA-model basis (#867): the #682-class trusted base, made countable.
  # STATIC textual classification (a heuristic, labelled as one): a rule
  # theorem is "stated against the simplified model" iff its conclusion runs
  # the flat ArmSemantics.v executor on the rule's sequence — the literal
  # `exec_program (rule_` text in VcrSelRules.v. What this can miss: a theorem
  # phrased through an alias of exec_program, or a future Sail-basis theorem
  # that ALSO mentions exec_program; today neither exists, and the companion
  # invariants in SYNTH-ISA-MODEL-BASIS (rule-theorem count == simplified-basis
  # conclusion count, zero SailArmBridge imports) pin that.
  sel_rules_simplified_basis:
    kind: count
    pattern: 'exec_program \(rule_'
    glob: ['coq/Synth/Synth/VcrSelRules.v']
  # ArmRefinement.v's ASSUMED simplified->Sail connection, itemized:
  # `Admitted.` + `admit.` tactics + the opaque `Axiom sail_exec_instr`.
  # The number that should only shrink (toward real Sail-generated semantics).
  arm_refinement_assumed_connection:
    kind: count
    pattern: '(?:Admitted\.)|(?:^\s*admit\.)|(?:^\s*(?:Axiom|Parameter) )'
    glob: ['coq/Synth/ARM/ArmRefinement.v']
  # The simplified model's OWN axiomatic surface: float/conversion bit-level
  # operations taken on faith inside the very model the proofs execute.
  arm_semantics_axioms:
    kind: count
    pattern: '^\s*(?:Axiom|Parameter) '
    glob: ['coq/Synth/ARM/ArmSemantics.v']
  # -- #867 phase 2: model-coverage tier counts, read from the COMMITTED
  # artifacts/model-coverage.json (whose freshness vs re-derivation is gated
  # by `scripts/model_coverage_audit.py --check` in the claim-check CI job —
  # so these counts cannot go stale OR be hand-edited without a red build).
  # Tier names are unique to the arm_instr universe in that artifact.
  isa_model_bridge_validated:
    kind: count
    pattern: '"tier": "bridge-validated"'
    glob: ['artifacts/model-coverage.json']
  isa_model_simplified_only:
    kind: count
    pattern: '"tier": "simplified-only"'
    glob: ['artifacts/model-coverage.json']
  # THE COMPLEMENT (the #867 headline): modelled ISA behaviours NO proof
  # exercises — the candidate list for the next silent miscompile.
  isa_model_uncovered:
    kind: count
    pattern: '"tier": "uncovered"'
    glob: ['artifacts/model-coverage.json']
  wasmcert_bridge_qed:
    kind: count
    pattern: 'Qed\.'
    glob: ['coq/Synth/WASM/WasmCertBridge.v']
  kani_harnesses:
    kind: count
    pattern: '#\[kani::proof\]'
    glob: ['crates/**/*.rs']
  verus_spec_fns:
    kind: count
    pattern: '^pub open spec fn '
    glob: ['crates/synth-synthesis/src/contracts.rs']
  # Distinct WasmOp variants the AArch64 selector implementation references
  # (truncated before its test module — decline-list mentions live in tests).
  # This is the mechanical "ops handled" figure for the host-native backend.
  aarch64_selector_ops:
    kind: distinct-tokens
    file: crates/synth-backend-aarch64/src/selector.rs
    pattern: 'WasmOp::([A-Za-z0-9]+)'
    before: 'mod tests'
  # Names, not numbers — const is allowed here, but the supporting crates must
  # exist on disk or the derivation fails.
  backends:
    kind: const
    value:
      - arm-thumb2-cortex-m
      - arm-a32-cortex-r5
      - riscv32-rv32imac
      - aarch64-a64
    require:
      - crates/synth-backend
      - crates/synth-backend-riscv
      - crates/synth-backend-aarch64

# -----------------------------------------------------------------------------
# readme_link_coverage — the README-linked .md surface is CLOSED. A linked doc
# must be claim-covered (some claim's `doc:`), listed as generated, or
# allowlisted here WITH a rationale. New links fail CI until classified.
# -----------------------------------------------------------------------------
readme_link_coverage:
  generated:
    - docs/status/FEATURE_MATRIX.md         # rendered by --emit-status; staleness-gated
  unpinned_ok:
    - path: CHANGELOG.md
      rationale: append-only release narrative; historical record, no live current-state claims
    - path: CONTRIBUTING.md
      rationale: process document; carries no capability or verification claims
    - path: docs/spectre-policy.md
      rationale: normative policy statement reviewed per lowering-rule PR; qualitative, no derived counts
    - path: docs/architecture/SYNTH_LOOM_RELATIONSHIP.md
      rationale: qualitative two-tier (loom optimizes / synth compiles) design note; no derived counts
    - path: docs/requirements/REQUIREMENTS.md
      rationale: forward-looking requirements draft (marked Draft in the doc); aspirational by nature, not a current-state claim surface
    - path: scripts/repro/vcr_ver_001_gate.md
      rationale: frozen repro evidence transcript for VCR-VER-001; existence pinned by SYNTH-VCR-VER-001-DEMONSTRATED

# -----------------------------------------------------------------------------
# repo_metadata — the GitHub About surface (description + topics), pinned
# verbatim. `scripts/repo_metadata_check.py` fetches the live values and fails
# on mismatch (API/network failure = loud SKIP so a flake can't block merges).
# -----------------------------------------------------------------------------
repo_metadata:
  repo: pulseengine/synth
  description: "Synth — WebAssembly-to-native compiler for ARM Cortex-M/R (Thumb-2/A32), RISC-V RV32, and AArch64, with mechanized Rocq correctness proofs, per-compilation translation validation, and sound WCET bounds. Part of the PulseEngine toolchain."
  topics:
    - aarch64
    - arm
    - compiler
    - embedded
    - formal-verification
    - pulseengine
    - riscv
    - rust
    - wcet
    - webassembly

claims:
  # ---------------------------------------------------------------------------
  # README badges — the number surface. The README carries NO hand-typed proof
  # counts; it carries shields.io dynamic-JSON badges whose JSONPath queries
  # must point at fields status.json actually derives. History: was
  # "298 Qed / 8 Admitted" prose while the tree held 470; prose numbers are
  # now banned from the README entirely.
  # ---------------------------------------------------------------------------
  - id: SYNTH-README-STATUS-BADGES
    doc: README.md
    text: "artifacts/status.json"
    evidence:
      - kind: verbatim                       # badge query → derived field, 1:1
        text: "query=%24.rocq_qed"
      - kind: status-field
        name: rocq_qed
      - kind: verbatim
        text: "query=%24.rocq_admitted"
      - kind: status-field
        name: rocq_admitted
      - kind: verbatim
        text: "query=%24.sel_dsl_rules"
      - kind: status-field
        name: sel_dsl_rules

  # ---------------------------------------------------------------------------
  # Headline Rocq proof counts — CLAUDE.md and coq/STATUS.md still hand-carry
  # them (working docs); count-eq keeps doc + ledger moving together.
  # ---------------------------------------------------------------------------
  - id: SYNTH-PROOF-COUNT-CLAUDE-MD
    doc: CLAUDE.md
    text: "591 Qed / 3 Admitted"
    evidence:
      - kind: count-eq
        pattern: 'Qed\.'
        glob: ['coq/Synth/**/*.v']
        expect: 591
      - kind: count-eq
        pattern: 'Admitted\.'
        glob: ['coq/Synth/**/*.v']
        expect: 3

  - id: SYNTH-PROOF-COUNT-STATUS-MD
    doc: coq/STATUS.md
    text: "591 Qed / 3 Admitted"
    evidence:
      - kind: count-eq                       # headline + Total line must both agree
        pattern: '591 Qed / 3 Admitted'
        glob: ['coq/STATUS.md']
        expect: 2
      - kind: count-eq
        pattern: 'Qed\.'
        glob: ['coq/Synth/**/*.v']
        expect: 591
      - kind: count-eq
        pattern: 'Admitted\.'
        glob: ['coq/Synth/**/*.v']
        expect: 3
      - kind: count-eq                       # the "+2 admit. tactics" disclosure
        pattern: '^\s*admit\.'
        glob: ['coq/Synth/**/*.v']
        expect: 2

  # ---------------------------------------------------------------------------
  # The admit breakdown the README discloses — per-file, so a new admit
  # anywhere (or a silent move between files) is visible, not just the total.
  # The prose statement is qualitative ("0 division admits"); the per-file
  # numbers live HERE, not in prose.
  # ---------------------------------------------------------------------------
  - id: SYNTH-ADMIT-BREAKDOWN
    doc: README.md
    text: "0 division admits"
    evidence:
      - kind: count-eq
        pattern: 'Admitted\.'
        glob: ['coq/Synth/Synth/CorrectnessI32.v']
        expect: 0
      - kind: count-eq
        pattern: 'Admitted\.'
        glob: ['coq/Synth/Synth/Compilation.v']
        expect: 0
      - kind: count-eq
        pattern: 'Admitted\.'
        glob: ['coq/Synth/Synth/CorrectnessSimple.v']
        expect: 1
      - kind: count-eq
        pattern: 'Admitted\.'
        glob: ['coq/Synth/ARM/ArmRefinement.v']
        expect: 2
      - kind: no-new                         # both admit. tactics live here
        pattern: '^\s*admit\.'
        glob: ['coq/Synth/ARM/ArmRefinement.v']
        recorded: 2

  # "0 i64 admits" (README + CLAUDE.md) — i64 T1 parity must not regress.
  - id: SYNTH-I64-ZERO-ADMITS
    doc: README.md
    text: "0 i64 admits"
    evidence:
      - kind: count-max
        pattern: 'Admitted\.'
        glob: ['coq/Synth/Synth/CorrectnessI64*.v']
        max: 0

  # The intro's scope claim: T1 for i32+i64 selection, T2-only for float/SIMD.
  - id: SYNTH-T1-SCOPE
    doc: README.md
    text: "cover the i32 and i64 instruction selection with result-correspondence (T1) proofs"
    evidence:
      - kind: file-exists
        path: coq/Synth/Synth/CorrectnessI32.v
      - kind: file-exists
        path: coq/Synth/Synth/CorrectnessI64.v
      - kind: verbatim                       # the honest scoping must stay next to it
        text: "float/SIMD selection has existence-only (T2) proofs"

  # ---------------------------------------------------------------------------
  # f32/f64 capability — the README stated "rejected loudly" three releases
  # after real VFP lowering shipped (v0.41 f32, v0.43 f64, #369 closed). The
  # claim binds the prose to selector anchors AND keeps the honest residual
  # (#782: trunc_sat undecoded + a pressure-dependent f32 class) next to it.
  # ---------------------------------------------------------------------------
  - id: SYNTH-F32-F64-VFP
    doc: README.md
    text: "scalar f32/f64 via VFP on FPU targets"
    evidence:
      - kind: count-eq                       # a real f64 arithmetic lowering arm
        pattern: 'F64Add \| F64Sub \| F64Mul \| F64Div => \{'
        glob: ['crates/synth-synthesis/src/instruction_selector.rs']
        expect: 1
      - kind: verbatim                       # the honest residual stays adjacent
        # THIRD occupant of this pin, and the churn is the lesson. It was "#782"
        # until the v0.53 #880 audit (that issue closed across v0.49–v0.52 while
        # the README still called it open), then "#881" — which v0.53's OWN L1
        # lane closed 14 h AFTER the doc-honesty lane had already landed, so the
        # release very nearly shipped citing three issues it had just fixed.
        #
        # Root cause: a pin naming an ISSUE NUMBER goes stale the instant that
        # issue is fixed, and since claim_check only asserts the phrase is
        # PRESENT, it then GREEN-CONFIRMS a false residual — the ledger defends
        # the defect instead of catching it. Pin the CAPABILITY GAP instead of
        # its tracker: this phrase becomes false exactly when the gap closes,
        # which is the property a residual pin was always supposed to have.
        text: "single-precision FPUs"

  # call_indirect: self-contained dispatch shipped v0.47 (#275 closed) with a
  # red-first execution differential; the README must not regress to either the
  # old loud-decline wording or an unevidenced blanket claim.
  - id: SYNTH-CALL-INDIRECT-SELFCONTAINED
    doc: README.md
    text: "self-contained `--cortex-m` dispatch via a PC-relative flash funcref table since v0.47 (#275)"
    evidence:
      - kind: file-exists
        path: scripts/repro/call_indirect_275_selfcontained_execution_differential.py
      - kind: file-exists
        path: scripts/repro/call_indirect_275_selfcontained_execution.wat

  # ---------------------------------------------------------------------------
  # ARCHITECTURE.md — validity-checked in the claim-surface extension PR
  # (April-era single-backend + benchmark-relic content removed). The pins
  # below hold the load-bearing structural statements to the tree.
  # ---------------------------------------------------------------------------
  - id: SYNTH-ARCH-BACKENDS
    doc: ARCHITECTURE.md
    text: "four backends"
    evidence:
      - kind: file-exists
        path: crates/synth-backend
      - kind: file-exists
        path: crates/synth-backend-riscv
      - kind: file-exists
        path: crates/synth-backend-aarch64
      - kind: verbatim
        text: "| AArch64 (host-native) | `synth-backend-aarch64` | A64 |"

  # The register-allocation description was WRONG for months ("R0-R12 for
  # temporaries" — R12 is encoder scratch, R9/R10/R11 are reserved bases; the
  # #212/#215 corruption class). Bind the prose to the actual pool constant.
  - id: SYNTH-ARCH-REGISTER-POOL
    doc: ARCHITECTURE.md
    text: "Allocatable pool: R0–R8"
    evidence:
      - kind: count-eq
        pattern: 'const ALLOCATABLE_REGS: \[Reg; 9\] = \['
        glob: ['crates/synth-synthesis/src/instruction_selector.rs']
        expect: 1
      - kind: verbatim
        text: "R12 (encoder scratch — never allocated)"

  # The honesty rule the whole doc leans on: undecodable ops loud-skip.
  - id: SYNTH-ARCH-LOUD-DECLINE
    doc: ARCHITECTURE.md
    text: "declines loudly"
    evidence:
      - kind: count-eq                       # the deliberate-ignore predicate
        pattern: 'fn is_intentionally_ignored'
        glob: ['crates/synth-core/src/wasm_decoder.rs']
        expect: 1

  # ---------------------------------------------------------------------------
  # "verified"/"implemented" wording — bound to the roadmap yaml's status
  # field, never free-floating prose. rivet's status lifecycle is the source.
  # ---------------------------------------------------------------------------
  - id: SYNTH-VCR-RA-001-VERIFIED
    doc: README.md
    text: "allocator with liveness-based Belady spilling: `verified`"
    evidence:
      - kind: yaml-field
        path: artifacts/verified-codegen-roadmap.yaml
        id: VCR-RA-001
        field: status
        equals: verified

  - id: SYNTH-VCR-RA-001-VERIFIED-CLAUDE-MD
    doc: CLAUDE.md
    text: "`VCR-RA-001` allocator with Belady spilling — **verified,"
    evidence:
      - kind: yaml-field
        path: artifacts/verified-codegen-roadmap.yaml
        id: VCR-RA-001
        field: status
        equals: verified

  - id: SYNTH-VCR-VER-001-DEMONSTRATED
    doc: README.md
    text: "**demonstrated** (implemented; [evidence](scripts/repro/vcr_ver_001_gate.md))"
    evidence:
      - kind: yaml-field
        path: artifacts/verified-codegen-roadmap.yaml
        id: VCR-VER-001
        field: status
        equals: implemented
      - kind: file-exists
        path: scripts/repro/vcr_ver_001_gate.md

  # VCR-VER-002 (#166): trap-preservation gate over ordeal 0.9's trap module.
  # in-progress, not implemented. LIVE (derived-ARM-trap-term) classes now:
  # i32 div/rem, i64 div/rem (#756, field-derived), unreachable, i32
  # load/store (all widths), call_indirect, i32.trunc_f32_s/u, i32.trunc_f64_s/u
  # (#756, D-register guard). i64.trunc_f32/f64 SHIP a guarded lowering since
  # #869, but their symbolic ARM-side wiring (F64 compare/decompose chain) is
  # the named residual — classifier unit-gated + EXECUTION-gated (the #869
  # differential runs every trap row under unicorn), not yet derived-term VC.
  # Phase B (ordeal 0.9.1, ordeal#59/TR-020): float→int trunc trap class
  # covered — trunc_op/trap_trunc wrapper + #709 boundary-table eval gate.
  - id: SYNTH-VCR-VER-002-STATUS
    doc: artifacts/verified-codegen-roadmap.yaml
    text: "Trap-preservation VC catches dropped WASM traps (i32+i64 div/rem, memory OOB, call_indirect, unreachable, float→int trunc); live-validator wiring in progress"
    evidence:
      - kind: yaml-field
        path: artifacts/verified-codegen-roadmap.yaml
        id: VCR-VER-002
        field: status
        equals: proposed
      - kind: file-exists
        path: crates/synth-verify/src/trap.rs
      - kind: file-exists
        path: crates/synth-verify/tests/trap_preservation.rs

  # VCR-VER-003 (#777 / #757): per-compilation static-data addressing validator.
  # Concrete byte-equality (NOT SMT): every static-data reloc resolves to the
  # runtime-correct byte (active segments applied in declaration order,
  # later-wins). In synth-core so it runs on EVERY compilation (default
  # `--features riscv`, not `verify`). Non-vacuous red-first gate: same validator
  # Mismatch on .position() (the #757 bug) / Consistent on .rposition().
  #
  # Phase 2 (#777 follow-ups, v0.47): (a) SPANNED reloc check — the mixed split
  # validates every runtime-covered byte of a conservatively-widened access
  # (MAX_ACCESS_BYTES) against the SHIPPED packed init blob (the
  # staggered-overlap straddle phase 1 silently miscompiled is now refused);
  # (b) the self-contained #758 ROM image is packed by the shared
  # declaration-order packer and validated unconditionally against the
  # reconstructed runtime image; (c) RV32 active segments SHIP since v0.48
  # (#798): packed as .wasm_data records (declaration order, startup copies
  # to __linear_memory_base + off at reset), the emitted blob READ BACK via
  # served_image_from_records and hard-error-validated against the runtime
  # image (the v0.47 drop-warning is gone; de-vacuated control_step
  # differential + full-boot unicorn oracle gate the runtime side);
  # (d) AArch64 N/A for THIS validator: it has linear-memory load/store since
  # #851 but no active DATA SEGMENTS / packed init blob, so there is nothing for
  # the static-data addressing VC to validate (the follow-on that adds data-seg
  # init is where this becomes applicable). The
  # count-eq pins below hold the wiring UNCONDITIONAL: exactly one
  # spanned-validator call on the mixed split, exactly one ROM-image and one
  # RV32 served-image (read-back) call.
  - id: SYNTH-VCR-VER-003-STATUS
    doc: artifacts/verified-codegen-roadmap.yaml
    text: "Static-data addressing VC catches the overlapping-segment wrong-segment miscompile (#757) at compile time on every module"
    evidence:
      - kind: yaml-field
        path: artifacts/verified-codegen-roadmap.yaml
        id: VCR-VER-003
        field: status
        equals: implemented
      - kind: file-exists
        path: crates/synth-core/src/static_data_addr.rs
      - kind: file-exists
        path: crates/synth-cli/tests/vcr_ver_003_addr_777.rs
      - kind: count-eq                       # phase 2: spanned check wired on the mixed split
        pattern: 'validate_reloc_resolutions_spanned\('
        glob: crates/synth-cli/src/main.rs
        expect: 1
      - kind: count-eq                       # phase 2: #758 ROM image + #798 RV32 read-back checks
        pattern: 'validate_served_image\('
        glob: crates/synth-cli/src/main.rs
        expect: 2
      - kind: count-eq                       # #798: the RV32 served image is the EMITTED blob read back
        pattern: 'served_image_from_records\('
        glob: crates/synth-cli/src/main.rs
        expect: 1

  - id: SYNTH-VCR-SEL-001-STATUS
    doc: README.md
    text: "increments 1–4 shipped default-on (`SYNTH_SEL_DSL`, opt-out `SYNTH_NO_SEL_DSL=1`)"
    evidence:
      - kind: yaml-field
        path: artifacts/verified-codegen-roadmap.yaml
        id: VCR-SEL-001
        field: status
        equals: implemented

  - id: SYNTH-VCR-ISA-001-STATUS
    doc: README.md
    text: "approved — Sail/ASL bridge spike landed"
    evidence:
      - kind: yaml-field
        path: artifacts/verified-codegen-roadmap.yaml
        id: VCR-ISA-001
        field: status
        equals: approved
      - kind: file-exists                    # lemma count flows via status.json
        path: coq/Synth/ARM/SailArmBridge.v

  # ---------------------------------------------------------------------------
  # ISA-model basis (#867) — the #682 class made an explicit, counted,
  # CI-pinned trusted-base entry. #682's shape: a green Qed against the
  # SIMPLIFIED hand-written semantics (ArmSemantics.v modelled LSL_reg with
  # Wasm's mod-32 masking, not ARMv7-M's Rm[7:0]) while shipped code silently
  # miscompiled — the proof was fine, the MODEL was unfaithful. These pins
  # count how much of the proof surface still rests on the simplified model
  # rather than the Sail-derived one, and how much of the simplified->Sail
  # connection is assumed. count-eq (not count-max) on purpose: movement in
  # EITHER direction must update coq/STATUS.md and this ledger together — a
  # new simplified-basis rule theorem is a VISIBLE debt bump, never silent.
  # Classification is STATIC and textual (documented at the
  # sel_rules_simplified_basis status field above): it counts theorem
  # conclusions of the literal form `exec_program (rule_...)`.
  # ---------------------------------------------------------------------------
  - id: SYNTH-ISA-MODEL-BASIS
    doc: coq/STATUS.md
    text: '"is my semantics model faithful?" has no formal solution'
    evidence:
      - kind: verbatim                       # "covered" != "faithful" must stay in the doc
        text: '**"covered" ≠ "faithful"**'
      - kind: count-eq                       # all 50 rule theorems conclude via the simplified executor
        pattern: 'exec_program \(rule_'
        glob: ['coq/Synth/Synth/VcrSelRules.v']
        expect: 50
      - kind: count-same                     # rule theorems == simplified-basis conclusions,
        legs:                                # 1:1 — a future Sail-basis rule theorem breaks
          - name: rule-correct-theorems      # this pair and forces reclassification HERE
            pattern: '^(?:Theorem|Lemma) rule_\w+_correct'
            glob: ['coq/Synth/Synth/VcrSelRules.v']
          - name: simplified-basis-conclusions
            pattern: 'exec_program \(rule_'
            glob: ['coq/Synth/Synth/VcrSelRules.v']
      - kind: count-eq                       # VcrSelRules imports NOTHING Sail-derived
        pattern: 'Require Import Synth\.ARM\.SailArmBridge'
        glob: ['coq/Synth/Synth/VcrSelRules.v']
        expect: 0
      - kind: count-eq                       # expansion-tier re-proofs are ALSO simplified-basis
        pattern: '^(?:Theorem|Lemma) rule_\w+_expansion_correct'
        glob: ['coq/Synth/Synth/VcrSelExpansion.v']
        expect: 10
      - kind: count-eq                       # the assumed simplified->Sail connection:
        pattern: '(?:Admitted\.)|(?:^\s*admit\.)|(?:^\s*(?:Axiom|Parameter) )'
        glob: ['coq/Synth/ARM/ArmRefinement.v']  # 2 Admitted + 2 admit. + 1 opaque Axiom
        expect: 5
      - kind: count-eq                       # the simplified model's own axiom surface
        pattern: '^\s*(?:Axiom|Parameter) '
        glob: ['coq/Synth/ARM/ArmSemantics.v']
        expect: 72
      - kind: status-field                   # the numbers flow to status.json
        name: sel_rules_simplified_basis
      - kind: status-field
        name: arm_refinement_assumed_connection
      - kind: status-field
        name: arm_semantics_axioms
      - kind: file-exists                    # phase 2: the coverage artifact +
        path: artifacts/model-coverage.json  # its loud complement report
      - kind: file-exists
        path: scripts/model_coverage_audit.py
      - kind: status-field
        name: isa_model_uncovered
      - kind: status-field
        name: isa_model_simplified_only
      - kind: status-field
        name: isa_model_bridge_validated

  # VCR-WASM-001 (Track B): WASM source semantics anchored on WasmCert-Coq.
  # Phase 1 (v0.45): i32.add. Phase 2 (v0.47): the i32 integer fragment batch
  # (arithmetic/bitwise/shifts/eqz/comparisons) in WasmCertBridge.v (op-level +
  # executor-level per op, + encoding/bit-level helpers). The reference rules
  # are hand transcriptions of the PINNED coq9.0-wasm-2.2.0 sources with
  # line-level provenance (WasmCertReference.v); the real external dep is
  # nix-FEASIBLE but bazel-deferred on three named blockers (see the roadmap
  # entry). Phase 3 (v0.48, #242): the extra-coq-package bazel/nix HOOK is
  # LANDED (patches/rules_rocq_rust_extra_coq_pkg.patch) — blocker (1) closed —
  # but the REAL dep stays PENDING and the transcription stays UNCHANGED,
  # because nixpkgs pin 88d3861a ships wasmcert 2.2.0 propagating the UNFREE
  # compcert 3.16 (blockers (2)+(3)); wasmcert >= 2.2.1 (drops CompCert) not
  # yet in the pin. So the transcription status here is INTENTIONALLY
  # unchanged. The WASM-side analogue of SailArmBridge.v (ISA-001). Lemma count
  # flows via status.json (wasmcert_bridge_qed).
  - id: SYNTH-VCR-WASM-001-STATUS
    doc: artifacts/verified-codegen-roadmap.yaml
    text: "PHASE 2 (v0.47): real-dependency FEASIBILITY SPIKE result"
    evidence:
      - kind: yaml-field
        path: artifacts/verified-codegen-roadmap.yaml
        id: VCR-WASM-001
        field: status
        equals: implemented
      - kind: file-exists
        path: coq/Synth/WASM/WasmCertBridge.v
      - kind: file-exists
        path: coq/Synth/WASM/WasmCertReference.v

  # ---------------------------------------------------------------------------
  # Verified selector DSL coverage — the rule table, its manifest, and the
  # Qed theorems must stay 1:1. The VALUE is not pinned in prose (it flows to
  # status.json / the badge); the INVARIANT — every manifest rule has exactly
  # one correctness theorem and the table carries no admits — is.
  # ---------------------------------------------------------------------------
  - id: SYNTH-SEL-DSL-RULES
    doc: README.md
    text: "every manifest rule has a 1:1 Qed correctness theorem"
    evidence:
      - kind: count-same
        legs:
          - name: manifest-rules
            pattern: '^rule_'
            glob: ['coq/vcr_sel_rules.manifest']
          - name: rule-correct-theorems
            pattern: '^(?:Theorem|Lemma) rule_\w+_correct'
            glob: ['coq/Synth/Synth/VcrSelRules.v']
      - kind: count-max                      # the rule table carries no admits
        pattern: 'Admitted\.'
        glob: ['coq/Synth/Synth/VcrSelRules.v']
        max: 0
      - kind: status-field                   # the value the badge surfaces
        name: sel_dsl_rules

  - id: SYNTH-SEL-DSL-COVERAGE-STATUS-MD
    doc: coq/STATUS.md
    text: "**50 (32%)**"                     # DSL-served column total, per-op-family table (#667)
    evidence:
      - kind: count-eq
        pattern: '^rule_'
        glob: ['coq/vcr_sel_rules.manifest']
        expect: 50
      - kind: verbatim
        text: "**50 Qed / 0 Admitted**"

  # ---------------------------------------------------------------------------
  # Trusted base — the axioms the Rocq suite rests on, re-counted, never
  # hand-maintained (STATUS.md said "41 axioms" while the tree held 93).
  # ---------------------------------------------------------------------------
  - id: SYNTH-AXIOM-BASE
    doc: coq/STATUS.md
    text: "**Total: 93 Axiom/Parameter declarations**"
    evidence:
      - kind: count-eq
        pattern: '^\s*(?:Axiom|Parameter) '
        glob: ['coq/Synth/**/*.v']
        expect: 93

  # ---------------------------------------------------------------------------
  # Other verification tracks stated in the README — wording pinned, counts
  # via status.json.
  # ---------------------------------------------------------------------------
  - id: SYNTH-KANI-HARNESSES
    doc: README.md
    text: "Bounded model checking harnesses for the ARM encoder"
    evidence:
      - kind: count-min                      # the track must not silently empty out
        pattern: '#\[kani::proof\]'
        glob: ['crates/**/*.rs']
        min: 1
      - kind: status-field
        name: kani_harnesses

  - id: SYNTH-VERUS-SPECS
    doc: README.md
    text: "Spec functions in `synth-synthesis/src/contracts.rs`"
    evidence:
      - kind: file-exists
        path: crates/synth-synthesis/src/contracts.rs
      - kind: status-field
        name: verus_spec_fns

  # ---------------------------------------------------------------------------
  # #778 WCET — the SOUND-critical per-op cycle model constants. These numbers
  # are load-bearing: a bound that undercounts real cycles is disqualifying, and
  # the summation gate (wcet_bound_gate.rs) re-derives from THIS same table so it
  # cannot flag a wrong number. Pinning the constants here is the honest
  # substitute for the cycle-accurate oracle that does not exist in-env: any edit
  # to a sound-critical entry reddens the claim-check and forces a conscious
  # re-derivation against the Cortex-M3/M4 TRM (max over {M3, M4}). The doc text
  # lives in CLAUDE.md's Track D.
  # ---------------------------------------------------------------------------
  - id: SYNTH-WCET-CYCLE-MODEL
    doc: CLAUDE.md
    text: "`STRAIGHTLINE_CEIL_PER_HALFWORD = 5`"
    evidence:
      # The straight-line-expansion ceiling — bumped 4→5 after auditing a 3-reg
      # 16-bit PUSH/POP in I64Popcnt (1+3=4 cyc/halfword had zero margin).
      - kind: count-eq
        pattern: 'const STRAIGHTLINE_CEIL_PER_HALFWORD: u64 = 5;'
        glob: ['crates/synth-backend/src/wcet.rs']
        expect: 1
      # UMULL = M3-worst 5 (reachable via reciprocal-multiply div-by-const, #322).
      - kind: count-eq
        pattern: 'Umull \{ \.\. \} => Cycles\(5\),'
        glob: ['crates/synth-backend/src/wcet.rs']
        expect: 1
      # MLA/MLS = M3-worst 2 (1 on M4).
      - kind: count-eq
        pattern: 'Mls \{ \.\. \} \| Mla \{ \.\. \} => Cycles\(2\),'
        glob: ['crates/synth-backend/src/wcet.rs']
        expect: 1
      # Hardware divide = data-dependent MAX 12.
      - kind: count-eq
        pattern: 'Sdiv \{ \.\. \} \| Udiv \{ \.\. \} => Cycles\(12\),'
        glob: ['crates/synth-backend/src/wcet.rs']
        expect: 1
      # The four i64 SOFTWARE div/rem = LoopedExpansion decline (internal 64-iter
      # runtime loop; a straight sum would undercount).
      - kind: count-eq
        pattern: 'I64DivU \{ \.\. \} \| I64DivS \{ \.\. \} \| I64RemU \{ \.\. \} \| I64RemS \{ \.\. \} => LoopedExpansion,'
        glob: ['crates/synth-backend/src/wcet.rs']
        expect: 1
      # BL/BLX direct-call branch overhead = 4 (#778 phase 3 inter-procedural
      # composition). MAX over {M3, M4}: both TRMs time BL/BLX as `1 + P` where P
      # is the pipeline-refill penalty (1..3 by target alignment/width/speculation),
      # so the worst case is 1 + 3 = 4 — the SAME branch-with-refill class the table
      # already prices for taken Bx/BOffset/BCondOffset. The callee body + its
      # return are counted separately (in the callee's own bound), so no return
      # penalty is added here. Editing this reddens the claim and forces a conscious
      # re-derivation against the TRM.
      - kind: count-eq
        pattern: 'const BL_BLX_CALL_OVERHEAD_CYCLES: u64 = 4;'
        glob: ['crates/synth-backend/src/wcet.rs']
        expect: 1
      # #778 phase 4 (#49) — the SOUND-critical self-recursion FRAME COUNT. A
      # certified single-self-call chain of derived depth `d` runs `d+1` frames
      # (the `+1` is the BASE frame, which executes own_cycles but no self-call);
      # the composer folds `(max_depth+1) × frame_cost`. Omitting the +1 would
      # undercount the base frame by one → unsound. Pinning the fold guards
      # against a silent off-by-one regression.
      - kind: count-eq
        pattern: 'let frames = \(cert\.max_depth as u128\)\.saturating_add\(1\);'
        glob: ['crates/synth-backend/src/wcet_compose.rs']
        expect: 1
      # #778 phase 5 — the SOUND-critical masked-ceiling BOTH-ENDPOINTS MAX. For a
      # data-dependent masked loop bound `x & K ∈ [0, K]`, the worst-case trip is
      # at the `rhs = K` endpoint for a count-UP loop and the `rhs = 0` endpoint
      # for a count-DOWN loop. Seeding only ONE endpoint emits a bound BELOW a real
      # count-down execution (the fatal class). synth evaluates BOTH endpoints,
      # requires BOTH to terminate (the `?` operators), and takes the MAX. Pinning
      # this guards against a silent single-endpoint regression that would undercount.
      - kind: count-eq
        pattern: 'let \(hi, lo\) = \(at\(ceiling\)\?, at\(0\)\?\);'
        glob: ['crates/synth-backend/src/wcet_loops.rs']
        expect: 1

  # ---------------------------------------------------------------------------
  # #880 — FEATURE_MATRIX template prose pins. The staleness gate only proves
  # committed doc == render(template); it cannot see WRONG TEMPLATE PROSE
  # (v0.51 called shipped aarch64 div/rem/popcnt/calls "not yet"/"declined";
  # v0.52 called the shipped-and-DEFAULT #865 OOB-trap a "follow-on" — both
  # caught only by a human cold read at tag time). These claims pin the
  # template's load-bearing capability phrases VERBATIM and bind each to
  # independent evidence: the oracle that EXECUTES the capability exists AND
  # is CI-WIRED (the #879 lesson — an unwired oracle gates nothing), plus a
  # code anchor where a stable one exists. LIMIT (stated honestly): a
  # verbatim pin catches DRIFT of a pinned phrase — weakening/rewording a
  # shipped capability reddens CI and forces a deliberate ledger bump next to
  # the evidence — but it cannot catch a brand-NEW false claim typed into the
  # template; that residual stays on review, and on extending this list
  # whenever a new load-bearing phrase lands.
  # ---------------------------------------------------------------------------
  - id: SYNTH-MATRIX-AARCH64-BOUNDS-DEFAULT
    doc: scripts/templates/feature_matrix.md.tmpl
    text: "**BOUNDS-CHECKED by default** — an out-of-bounds access traps (`brk`) exactly where wasmtime traps"
    evidence:
      - kind: file-exists
        path: scripts/repro/aarch64_bounds_865_differential.py
      - kind: count-min                      # the oracle is CI-wired, not shelfware
        pattern: 'aarch64_bounds_865_differential\.py'
        glob: ['.github/workflows/ci.yml']
        min: 1
      - kind: count-min                      # the enforcing default's code anchor
        pattern: 'MemBounds::Software'
        glob: ['crates/synth-backend-aarch64/src/selector.rs']
        min: 1

  # #851 lane L3 — the load-bearing HONESTY claim of this lane. v0.52's cold
  # review caught a doc that described a shipped feature as "not yet"; v0.53
  # made the `x28` precondition explicit so the NEXT feature could not quietly
  # add a second one. This pin holds that line: if globals or the funcref table
  # ever become an ambient input the embedder must supply, the sentence claiming
  # they are EMITTED must change with it, and the gate reddens until it does.
  - id: SYNTH-MATRIX-AARCH64-EMITTED-NOT-PRECONDITION
    doc: scripts/templates/feature_matrix.md.tmpl
    text: "The globals region and the funcref table are explicitly **NOT** preconditions: synth EMITS both into the object with their contents"
    evidence:
      # The single producer of both regions — if this file goes, the claim goes.
      - kind: file-exists
        path: crates/synth-backend-aarch64/src/substrate.rs
      # The regions are placed in the object, not assumed: a `.data` blob and a
      # `.text`-resident table, reached PC-relatively (no base register).
      - kind: count-min
        pattern: 'DataBlob'
        glob: ['crates/synth-backend-aarch64/src/elf.rs']
        min: 1
      - kind: count-min
        pattern: 'AArch64AdrPrelPgHi21'
        glob: ['crates/synth-backend-aarch64/src/selector.rs']
        min: 1

  # #851 lane L3 — all THREE §4.4.8 traps are EMITTED, not inherited from `blr`
  # (which is total). Pinned to both oracles being CI-wired, so the claim cannot
  # outlive its evidence.
  - id: SYNTH-MATRIX-AARCH64-CALL-INDIRECT-TRAPS
    doc: scripts/templates/feature_matrix.md.tmpl
    text: "all THREE WASM §4.4.8 trap guards emitted inline: out-of-range index (UNSIGNED bounds compare), null slot, and signature mismatch"
    evidence:
      - kind: file-exists
        path: scripts/repro/aarch64_call_indirect_851_differential.py
      - kind: count-min
        pattern: 'aarch64_call_indirect_851_differential\.py'
        glob: ['.github/workflows/ci.yml']
        min: 1
      - kind: count-min
        pattern: 'aarch64_globals_851_differential\.py'
        glob: ['.github/workflows/ci.yml']
        min: 1

  - id: SYNTH-MATRIX-AARCH64-DIVREM-POPCNT
    doc: scripts/templates/feature_matrix.md.tmpl
    # v0.53: the op list this sentence heads grew (select/CSEL, drop/nop, wrap,
    # extends), so the trailing " and `popcnt` (#851)" no longer reads verbatim.
    # Re-pinned to the capability-bearing span — the trap-guard parenthetical is
    # the load-bearing soundness claim and stays inside the pin, so a silent
    # removal of the ÷0 / INT_MIN÷−1 guards still reddens this gate.
    text: "`div_s/div_u/rem_s/rem_u` (with the ÷0 + INT_MIN/−1 WASM trap guards), `popcnt`"
    evidence:
      - kind: file-exists
        path: scripts/repro/aarch64_divrem_851_differential.py
      - kind: count-min
        pattern: 'aarch64_divrem_851_differential\.py'
        glob: ['.github/workflows/ci.yml']
        min: 1

  - id: SYNTH-MATRIX-CALL-INDIRECT-FLASH-TABLE
    doc: scripts/templates/feature_matrix.md.tmpl
    text: "self-contained dispatch is PC-relative via a flash funcref table (v0.47)"
    evidence:
      - kind: file-exists
        path: scripts/repro/call_indirect_275_selfcontained_execution_differential.py
      - kind: count-min
        pattern: 'call_indirect_275_selfcontained_execution_differential\.py'
        glob: ['.github/workflows/ci.yml']
        min: 1

  - id: SYNTH-MATRIX-TRUNC-SAT
    doc: scripts/templates/feature_matrix.md.tmpl
    text: "Decoded and lowered as bare saturating VCVT (§4.3.2: NaN→0, out-of-range saturates, never traps)"
    evidence:
      - kind: file-exists
        path: scripts/repro/trunc_sat_782_differential.py
      - kind: count-min
        pattern: 'trunc_sat_782_differential\.py'
        glob: ['.github/workflows/ci.yml']
        min: 1

  # The v0.51/v0.52-CLASS defect this lane FIXED in the same PR: the template
  # still said "RV32 warns loudly on dropped initializer bytes" four releases
  # after #798 (v0.48) shipped the segments and replaced the warning with a
  # hard error. The corrected phrase is pinned to the hard-error call site in
  # the RV32 backend and to the full-boot oracle.
  - id: SYNTH-MATRIX-RV32-DATA-SHIP
    doc: scripts/templates/feature_matrix.md.tmpl
    text: "RV32 ships active data segments as `.wasm_data` records — the emitted blob is read back and any served/runtime disagreement hard-errors the compile (#798, v0.48)"
    evidence:
      - kind: count-eq                       # the read-back hard-error in the backend
        pattern: 'validate_served_image'
        glob: ['crates/synth-backend-riscv/src/backend.rs']
        expect: 1
      - kind: file-exists
        path: scripts/repro/rv32_data_798_boot_differential.py
      - kind: count-min                      # #879-class: the boot oracle must be CI-wired
        pattern: 'rv32_data_798_boot_differential\.py'
        glob: ['.github/workflows/ci.yml']
        min: 1

  # Multi-memory: the matrix said "D — module-level loud decline" while the
  # #406 per-memory lowering (N distinct native base regions, execution
  # differential CI-wired) had been shipping — the v0.51 understatement class.
  - id: SYNTH-MATRIX-MULTI-MEMORY
    doc: scripts/templates/feature_matrix.md.tmpl
    text: "N memories lower to N distinct native base regions on ARM `--relocatable`"
    evidence:
      - kind: file-exists
        path: crates/synth-cli/tests/multi_memory_406.rs
      - kind: file-exists
        path: scripts/repro/multi_memory_406_differential.py
      - kind: count-min
        pattern: 'multi_memory_406_differential\.py'
        glob: ['.github/workflows/ci.yml']
        min: 1

  # Same class, second find of this audit: the WCET decline row still listed
  # "calls" as a blanket D two releases after phase-3 inter-procedural
  # composition (v0.48) bounded direct local calls.
  - id: SYNTH-MATRIX-WCET-COMPOSITION
    doc: scripts/templates/feature_matrix.md.tmpl
    text: "`total = own + Σ site-multiplier × callee-total` over direct `BL` calls to local bounded callees (v0.48, phase 3); a declined callee propagates its decline UP"
    evidence:
      - kind: file-exists
        path: crates/synth-backend/src/wcet_compose.rs
      - kind: file-exists
        path: crates/synth-backend/src/wcet_recursion.rs
      - kind: file-exists
        path: crates/synth-backend/src/wcet_loops.rs
      - kind: file-exists
        path: crates/synth-cli/tests/wcet_bound_gate.rs
      - kind: verbatim                       # the honest residual row stays adjacent
        text: "Unhinted data-dependent loops, indirect/external calls, tree/mutual recursion, i64 software div/rem, non-M3/M4 cores | D"

  # ---------------------------------------------------------------------------
  # #879 — the gpio-thin oracle's CI wiring, pinned so it cannot be silently
  # UN-wired again (it sat un-wired for two releases while its size claim
  # headlined v0.50.1 and v0.52.0). Pins the script + the pinned real-driver
  # fixture, capstone in the job's dep install (the mask census disassembles
  # .text), and the CI-side NON-ZERO check-count assertion (exit 0 alone is
  # not trusted — the "0 ops accepted PASS" lesson).
  # ---------------------------------------------------------------------------
  - id: SYNTH-GPIO-846-ORACLE-CI-WIRED
    doc: .github/workflows/ci.yml
    text: "scripts/repro/gpio_thin_846_differential.py"
    evidence:
      - kind: file-exists
        path: scripts/repro/gpio_thin_846_differential.py
      - kind: file-exists
        path: scripts/repro/gpio_thin_846.loom.wasm
      - kind: verbatim
        text: "pip install wasmtime unicorn pyelftools capstone"
      - kind: verbatim
        text: 'grep -q "^#846 CHECKS=75/75" gpio846.out'

  # ---------------------------------------------------------------------------
  # VCR-MEM-004 / #901 — the SoftwareBoundsChecker cost claim.
  #
  # `synth-memory/src/bounds.rs` carried "~25-40% overhead" as a bare assertion
  # for its whole life, and #901's whole premise is that verification pays for
  # itself against exactly that number. So the doc now states a MEASURED cost,
  # and this entry pins the doc's numbers to the constants the byte gate
  # asserts against real compiled bytes. Change the lowering and the gate's
  # constants move; move them without updating the doc and this reddens.
  #
  # What is pinned is the CAPABILITY (a measured guard tax and a measured
  # recovery on a named fixture), never an issue number — a closed issue would
  # let the ledger green-confirm a false residual (the v0.53 lesson).
  # ---------------------------------------------------------------------------
  - id: SYNTH-PROVEN-SAFE-901-MEASURED
    doc: crates/synth-memory/src/bounds.rs
    text: "138 B (+147 %) and 40 instructions"
    evidence:
      - kind: verbatim
        text: "recovers 80 B (58 % of the tax)"
      - kind: file-exists
        path: crates/synth-cli/tests/proven_safe_bounds_901.rs
      - kind: file-exists
        path: scripts/repro/proven_safe_bounds_901_differential.py
      - kind: file-exists
        path: scripts/repro/proven_safe_bounds_901.wat
      # The doc's 138 B tax and 80 B recovery ARE the gate's constants.
      - kind: count-eq
        pattern: "const TAX_ALL_8: usize = 138;"
        glob: "crates/synth-cli/tests/proven_safe_bounds_901.rs"
        expect: 1
      - kind: count-eq
        pattern: "const SAVED_PROVEN_5: usize = 80;"
        glob: "crates/synth-cli/tests/proven_safe_bounds_901.rs"
        expect: 1
      # Fail-closed is the deliverable: the refusal must stay in the ingestion.
      - kind: count-eq
        pattern: "REFUSED — module_sha256 mismatch"
        glob: "crates/synth-core/src/proven_safe.rs"
        expect: 1

  # ---------------------------------------------------------------------------
  # #890 — the ORACLE-WIRING surface, generalized. SYNTH-GPIO-846-ORACLE-CI-WIRED
  # above pins ONE script's CI wiring by hand; that is the instance-at-a-time
  # shape this entry replaces. `scripts/repro/*.py` are synth's execution
  # oracles, and 69 of 150 were referenced by NO workflow while nothing in the
  # tree told a forgotten gate from an intentionally-manual one. Every script now
  # carries a `# ci-status:` declaration and `scripts/oracle_wiring_check.py`
  # (claim-check CI job) PROVES every `wired` one is actually wired — that check
  # is mechanical and needs no ledger. What a header CANNOT express is the
  # ratchet on the totals, which is what this entry is:
  #
  #   * wired   >= 145 — a FLOOR. The oracle surface must not be emptied by
  #                      deleting harnesses instead of fixing them.
  #   * manual  <=   7 — a CEILING on the legitimate escape hatch (4 measurement,
  #                      2 scratch, 1 external-input; itemized in the doc). An
  #                      eighth needs a conversation, not a commit.
  #   * unwired <=   0 — a CEILING OF ZERO on known debt. A new oracle that is
  #                      not wired is a RED BUILD, not a backlog entry.
  #
  # Lower the manual ceiling when one is wired; never raise it to green a build.
  # ---------------------------------------------------------------------------
  - id: SYNTH-ORACLE-WIRING-890
    doc: scripts/repro/ORACLE_WIRING.md
    text: "**145 wired**"
    evidence:
      - kind: file-exists
        path: scripts/oracle_wiring_check.py
      - kind: count-min                      # the surface must not be emptied
        pattern: '^# ci-status: wired'
        glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
        min: 145
      - kind: count-max                      # the legitimate escape hatch
        pattern: '^# ci-status: manual'
        glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
        max: 7
      - kind: count-max                      # known debt: zero, and it stays zero
        pattern: '^# ci-status: unwired'
        glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
        max: 0
      - kind: verbatim                       # the doc must carry the manual budget
        text: "**7 manual**"
      - kind: verbatim
        text: "**0 unwired**"

  # ---------------------------------------------------------------------------
  # #910 — what a wired oracle ATTESTS. SYNTH-ORACLE-WIRING-890 above pins that
  # a step RUNS each oracle; it says nothing about what that step checks, and
  # measured on the #890 result, 152 of 160 oracle steps asserted only the
  # process exit code. Exit 0 cannot tell "emulated 240 vectors" from "the loop
  # never ran", so every `wired` oracle now declares a `# ci-checks:` floor that
  # scripts/oracle_run.py enforces per run.
  #
  # The CAPABILITY pinned here (deliberately not an issue number — a ledger
  # pinned to a closed issue green-confirms a false residual, the v0.53 burn):
  #
  #   * every wired oracle carries a floor      — count-min 150 declarations
  #   * the execution population does not shrink — count-min 133 `emulations`
  #                                                declarations, and the summed
  #                                                floor is ratcheted in CI by
  #                                                --min-emulation-floor
  #   * the `none` escape hatch stays at ONE     — count-max 1. A second oracle
  #                                                that can bind to nothing needs
  #                                                a conversation, not a commit.
  #
  # Floors are `>=`, so adding a fixture cannot redden a step; the ratchet
  # direction is UP. Lower the recorded minimum only when the evidence genuinely
  # weakened — never to green a build.
  # ---------------------------------------------------------------------------
  - id: SYNTH-ORACLE-CHECK-FLOORS-910
    doc: scripts/repro/ORACLE_WIRING.md
    text: "**295,621 emulator entries**"
    evidence:
      - kind: file-exists
        path: scripts/oracle_run.py
      - kind: file-exists
        path: scripts/oracle_evidence.py
      - kind: count-min                      # every wired oracle declares a floor
        pattern: '^# ci-checks: '
        glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
        min: 150
      - kind: count-min                      # the EXECUTION population, per script
        pattern: '^# ci-checks: emulations >= '
        glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
        min: 137
      - kind: count-max                      # the "nothing can be bound" hatch
        pattern: '^# ci-checks: none'
        glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
        max: 1
      - kind: verbatim                       # the doc carries the per-mode split
        text: "**137 oracles**"
      - kind: verbatim
        text: "Reported per mode and never summed across modes."
      - kind: verbatim                       # the itemized weak-floor list stays
        text: "## The oracles whose floor is weak, itemized"

  # ---------------------------------------------------------------------------
  # #910 — the THIRD surface carrying this number: the FEATURE_MATRIX template.
  #
  # Found while adding the #916 and #901 oracles: ORACLE_WIRING.md and ci.yml
  # were pinned, the generated matrix was NOT, so the ledger reported 42/42 HOLD
  # while the matrix still read "133 oracles assert 294,914". A number quotable
  # in a shipped doc and bound to no gate is the #880 defect exactly — the gate
  # checked the matrix against its RENDER, never its CONTENT.
  #
  # Pinned on the TEMPLATE, not the rendered file: the render is generated
  # (`--emit-status`), so pinning the output would be satisfiable by a
  # regeneration that faithfully reproduces wrong prose.
  # ---------------------------------------------------------------------------
  - id: SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX
    doc: scripts/templates/feature_matrix.md.tmpl
    text: "**137 oracles assert 295,621 emulator"
    evidence:
      - kind: file-exists
        path: scripts/oracle_run.py
      - kind: count-min                      # same population the other two pin
        pattern: '^# ci-checks: emulations >= '
        glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
        min: 137

  # ---------------------------------------------------------------------------
  # #910 — the CI side of the same claim, pinned so the doc's number and the
  # number the gate actually enforces cannot drift apart, and so the routing
  # cannot be quietly undone (unrouting a step would restore exit-status-only
  # assertion while every other surface still claimed a floor).
  # ---------------------------------------------------------------------------
  - id: SYNTH-ORACLE-CHECK-FLOORS-910-CI
    doc: .github/workflows/ci.yml
    text: "--min-emulation-floor 295684"
    evidence:
      - kind: count-min                      # oracle steps routed through the driver
        pattern: 'oracle_run\.py scripts/repro/'
        glob: ['.github/workflows/*.yml']
        min: 159
      - kind: count-min                      # per-job measured-evidence ledgers
        pattern: 'oracle_evidence\.py'
        glob: ['.github/workflows/*.yml']
        min: 37
      - kind: verbatim
        text: "ORACLE_EVIDENCE_JSONL: oracle-evidence.jsonl"

  # ---------------------------------------------------------------------------
  # #910 — the coverage instrument says its SCOPE. The job was `Code Coverage`,
  # a name implying whole-system coverage for a measurement of the Rust test
  # suite alone; the differentials spawn an UNINSTRUMENTED subprocess from other
  # jobs and are structurally invisible to it. Pinned so the scope caveat cannot
  # be dropped while the number stays quotable — a green-but-meaningless number
  # is worse than a red one.
  # ---------------------------------------------------------------------------
  - id: SYNTH-COVERAGE-SCOPE-910
    doc: .github/workflows/ci.yml
    text: "name: Rust-test Line Coverage (unit + integration only)"
    evidence:
      - kind: verbatim                       # the caveat travels WITH the number
        text: "**Do not add them together.**"
      - kind: verbatim
        text: "UNINSTRUMENTED process"

  - id: SYNTH-COVERAGE-SCOPE-910-README
    doc: README.md
    text: "<b>Rust-test line coverage only</b>"
    evidence:
      - kind: verbatim                       # the badge alt-text matches the scope
        text: "[![Rust-test line coverage]"
      - kind: verbatim
        text: "It understates the testing that exists and is not a completeness measure"