Repository navigation
feat(abi): verdict record names its support; Sound only from a prover re-check (HYP-01, PR A) - #920
Merged
Merged
Conversation
check-proof-status.sh splits each PROOF-STATUS row on the opening `+ delimiter, which leaves exactly one identifier per piece, then stepped the loop by 2. Every second identifier was never checked: on main the gate reported 7 identifiers checked out of 16 named. Step by 1. Measured on main's PROOF-STATUS.adoc with the fix: files named 27, identifiers checked 16, mismatches 0, so nothing stale was hiding in the unchecked half. Mutant: renaming a lemma that sat in an odd slot (decSound in the HYP-01 row that follows) was green before the fix and is red after it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
… re-check (HYP-01) A gate verdict is an Epi: a claim, the evidence tokens it was issued on (rule id + version, matched span, fleet observation count), and the support they give. src/Hypatia/ABI/Verdict.idr (%default total, no proof-bypass primitives) transcribes that shape to the ABI layer: Support = Pattern | Observed Nat | Mechanical ProverRecheck `Sound` has one constructor, indexed by `Mechanical`, demanding a re-check whose result `Confirms`; a `Sound` witness names the SHA-256 of its re-check artefact. `level` (sound / epi / belief) is derived from the record, and is "sound" only when a witness exists. Falsifiers, both run in verify-proofs.yml: - scripts/check-verdicts.sh: ABI builds; tests/accept/ accepted; each tests/reject/ module refused at `invalid` with the diagnostic its `-- EXPECT:` line names (PatternIsNotSound, ObservedIsNotSound, RefutedRecheckIsNotSound, MalformedDigest). - scripts/recheck-lean-hole.sh: re-runs Lean 4.30.0 on the code_safety proof-hole fixture and requires both digests in the positive control (tests/accept/LeanHoleRecheckSound.idr) to match, with two negative controls. Sibling consumed by pin, not re-declared: scripts/fetch-siblings.sh fetches epistemic-types @ 6a68de3 and scripts/check-sibling-citations.sh (new CI job) fails if a cited definition is absent there. The correspondence itself stays ASSUMED and is recorded as such in verification/PROOF-STATUS.adoc. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
Contributor
|
Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configuration
📒 Files selected for processing: 18
✨ Finishing Touches
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
hyperpolymath
marked this pull request as ready for review
October 14, 2026 01:21
hyperpolymath
enabled auto-merge (squash)
October 14, 2026 01:21
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
…d in CI (HYP-01, PR B) (#922) HYP-01, PR B of 3. It follows #920 (PR A, merged as `ce5fc63`). PR C (quarantine retraction) comes next. Ruling applied: `schema/` is canonical for findings. `schemas/` holds no findings schema, and merging the two directories stays out of scope, as the issue says. ## What changes **Every finding in CI output carries `support`, `evidence` and a derived `level`.** - `lib/hypatia/verdict.ex` (`Hypatia.Verdict`) is the JSON mirror of `src/Hypatia/ABI/Verdict.idr`. - `CLI.collect_findings/2` funnels every rule-module finding through `Verdict.annotate/1` exactly once, after suppression. - Today every rule finding is `support: {kind: "pattern"}`, one evidence token (rule, rule version, span, observations), and `level: "epi"`. Elixir rules carry the tag only; none is proved sound. - `level` is derived by `Verdict.level/2`, and a level a rule tries to set is overwritten. - `Verdict.attach_recheck/3` is the only path to `"sound"`. It refuses a re-check of another file, or one whose target digest doesn't match the bytes on disk. A `refutes` result derives `"epi"`. No scan path attaches a re-check yet. - **Bash fallback** (`hypatia-cli-bash.sh`): same fields. The level comes from a jq `def` mirroring `Verdict.level/2`. - **Pass/fail text is derived from the record.** GitHub annotations and text output render `[level: support]` from it. SARIF puts `hypatia.level` and `hypatia.support` in the result property bag, outside `partialFingerprints`, so already-triaged alerts don't re-open. The level counts go on their own stderr line, leaving the existing summary line's shape unchanged. **`schema/findings.ncl` rewritten.** - The old file never evaluated: its export block isn't valid Nickel syntax. `generate-findings.ncl` called `std.env`, which no Nickel release has. Nothing referenced either file, so the generator is removed. - The new schema describes what the producers actually emit: `Findings` (escript array) and `BashReport` (bash fallback). - The `LevelDerived` contract re-derives `level` from `support` + `evidence` and refuses a record that disagrees. - The rules.a2ml thresholds (5 to propose; 10 + 3 fixes to auto-approve) are labelled as belief formation. ## Falsifiers | Gate | Result locally | Negative control | |---|---|---| | `scripts/check-findings-schema.sh --self-test` (CI: `escript-soundness.yml`) | `PASS: findings schema self-test, 3 accepted, 7 refused` | 7 bad fixtures, each refused with the message its `.expect` names: pattern / observed / refuted claiming sound, belief with evidence, missing support, malformed digest, unknown level | | `scripts/check-findings-schema.sh consumer.json` (CI: same job, after the consumer-shaped scan) | `PASS: … satisfies Findings (42 findings; by level: {"epi":42})` | The first schema draft refused real output (`"line": null` from cicd_rules, git_state and workflow_hardening); `line` now accepts null | | `mix test` | `1810 tests, 0 failures, 242 excluded` (baseline 1796 / 0 / 242) | Mutating `level/2` to call any mechanical support sound → 2 failures | | `test/verdict_test.exs` | 14 tests | Level names are read from `Verdict.idr`; the sound re-check is read from PR A's positive control, so the two sides can't drift | | `run-escript-soundness.sh` | `14/14 rules fired at expected severity` | — | | ShellCheck | New scripts clean; `hypatia-cli-bash.sh` has the same 74-line report before and after | — | ## Backward compatibility The fields are additive and every record is open. gitbot-fleet's consumers (`run-fleet.sh`, `fleet-coordinator.sh`, `submit-finding.sh`, `apply-baseline.sh`) and `.hypatia-baseline.json` matching all read by key. The escript still prints a bare JSON array, and severities are unchanged. ## Notes on local verification hex.pm is blocked by this session's network policy. Locally, the 14 locked deps were built from their upstream GitHub tags through an uncommitted `MIX_EXS` override. `phoenix_template` 1.1.0 isn't tagged on GitHub, so 1.0.4 was used; it satisfies phoenix's `~> 1.0`. CI uses the real lock. ## Known red checks that aren't this PR's `Security Status`, `Rust Dependency Audit` and `Rust License & Ban Check` (the Security workflow) were already red on `main` at `4be38c8` (scheduled runs 2902–2904, before HYP-01). `Security Status` fails because it reads `.github/workflows/security-policy.yml` without a checkout step. This PR touches neither Rust nor that workflow. ## Anomalies noticed, not touched `mix format --check-formatted` flags `lib/rules/workflow_audit.ex`. That predates this PR, and no workflow gates formatting. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --- _Generated by [Claude Code](https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
…name their facts (HYP-01, PR C) (#923) HYP-01, PR C of 3. It follows #920 (PR A) and #922 (PR B), both merged. There are three feature commits, each reviewable on its own, plus one review-fix commit. ## 1. `build(siblings)`: pin residual-evidence-types at `97244f5` This is a separate commit, one per pin. `Revision.agda` and `Context.agda` at that pin are the specification for quarantine-as-retraction (RE-1). ## 2. `feat(safety)`: quarantine is retraction Quarantining a bot, a rule (`rule:<module>/<id>`) or a prover (`prover:<name>`) retracts an assumption. Each evidence token rests on its rule, and on its bot when it names one; a confirming re-check rests on its prover. The rule is RE-1's `survives-retraction` / `survives-dependent`: - A token survives iff its support thins into what remains. - A finding survives through any surviving token, or through a confirming re-check whose prover isn't retracted. A sound finding therefore survives the quarantine of the rule that flagged it, but not the quarantine of its prover. A refuting re-check supports nothing, so its prover is never named. - A survivor keeps only its surviving tokens, and its level is re-derived from them. - A finding with nothing left moves to the retracted list, keeping its original evidence and naming what it rested on in `retracted_by` (JSON-safe wire names). **`src/Hypatia/ABI/Retraction.idr`** (`%default total`) transcribes the shape: - `Thin` (Context.agda `_⊆_`), `Retraction`, `retractThin` (`retract-⊆`); - `Dependent`, without `Holds`, which hypatia can't state as a type; - `survivesDependent`, `retractedSupportDies`, `survivor`. It is gated by `scripts/check-verdicts.sh`: - `tests/reject/RetractedSupportSurvives.idr` (the FalseRetraction pattern, transcribed) is refused at `invalid` with `Mismatch between: [?x] and [].` - `tests/accept/IndependentTokenSurvives.idr` is accepted. **Runtime:** `Hypatia.Verdict.Retraction`, plus `Quarantine.retracted_assumptions/0` and `Quarantine.retract_dependents/1`. A soft quarantine retracts too, since a high false-positive rate is exactly a reason to stop trusting the findings. ## 3. `feat(dispatch)`: every manifest step names its facts; factless steps are refused You ruled that Signalbox's thesis applies to hypatia's own derived workflow, since no Signalbox repository exists. The dispatch manifest is the workflow hypatia derives for `dispatch-runner.sh`. - Every step now carries `facts`: the pattern it acts on, its support (`observed` with the fleet occurrence count, or `pattern`), its evidence, and the derived level. - `DispatchManifest.compile/1` refuses the **whole** manifest if any step names no fact, and `write/2` then writes nothing. - `PatternAnalyzer.dispatch_and_write/2` compiles the manifest **before** anything reaches the fleet. The routed actions are dispatched, and the manifest written, only when every step names its fact. A refusal dispatches nothing and is reported as path nil, zero counts and the steps named, rather than crashing on `{:ok, _, _} =`. - A step's Bayesian `confidence` stays in its own field and is never a fact. - `facts` is additive for `dispatch-runner.sh`, which reads entries by key. ## Review round (CodeRabbit), commit `49c9653` | Finding | Result | |---|---| | 🟠 Major: factless actions reached the fleet before the manifest was refused | Fixed: `dispatch_and_write/2` compiles first. New test plus negative control; the dispatch-before-compile mutant fails it | | 🟡 Minor: a refuting re-check's prover was named in `retracted_by` | Fixed: only a confirming re-check is retracted support. New test; the old rule fails it | | 🔵 Trivial: `dependent-holds` citation row vs header | Fixed: the row is marked "named as deliberately not transcribed" | ## Gate output (local; verify-proofs runs on this PR since it targets main) ``` PASS: accepted positive control IndependentTokenSurvives PASS: accepted positive control LeanHoleRecheckSound PASS: rejected MalformedDigest at invalid: Can't find an implementation for So False. PASS: rejected ObservedIsNotSound at invalid: Mismatch between: Mechanical recheck and Observed 5. PASS: rejected PatternIsNotSound at invalid: Mismatch between: Mechanical recheck and Pattern. PASS: rejected RefutedRecheckIsNotSound at invalid: Mismatch between: Confirms and Refutes. PASS: rejected RetractedSupportSurvives at invalid: Mismatch between: [?x] and []. PASS: ABI package, 2 positive control(s), 5 expected rejection(s) sibling citations: checked 14, stale 0 PROOF-STATUS currency: files named 39, identifiers checked 57, mismatches 0 trusted-base markers: fixture=19 allowed=3 comment=1 debt=0 1825 tests, 0 failures, 242 excluded (main: 1810 / 0 / 242) PASS: … satisfies Findings (41 findings; by level: {"epi":41}) PASS: findings schema self-test, 3 accepted, 7 refused ``` **Mutants, all red:** - Survival premise checked against Γ instead of Δ: the ABI doesn't build. - A token survives if *any* of its assumptions remains: 1 test fails. - `compile/1` never refuses: 1 test fails. - Dispatch before compile: 1 test fails. - Any mechanical prover counts as retracted support: 1 test fails. **Negative controls:** - A finding not resting on the quarantined rule is untouched. - After release, nothing is retracted. - A fact-complete manifest dispatches every action. ## Status rows (PROOF-STATUS "Verdict support") | Row | Status | Artefact | |---|---|---| | `Retraction.idr` lemmas | PROVEN | `retractThin`, `survivesDependent`, `retractedSupportDies`, `survivor`, `noTokensNoSurvival` | | RetractedSupportSurvives refused / IndependentTokenSurvives accepted | TESTED | `check-verdicts.sh` lines above | | Correspondence to Revision.agda | ASSUMED | pin + 9 names checked | | Runtime: quarantine retracts dependents | TESTED | `test/retraction_test.exs` (10 tests, including quarantine → retract → release through the live GenServer) | | Runtime wiring: called by a scan or dispatch path | **OPEN** | it isn't, like the rest of the safety systems (CLAUDE.md Known Gap 2) | | Derived steps name their facts; factless refused before dispatch | TESTED | `test/dispatch_manifest_test.exs` (5 new) | | Signalbox-derived workflow | **OPEN** | no Signalbox repository exists | ## Known red checks that aren't this PR's `Security Status`, `Rust Dependency Audit` and `Rust License & Ban Check` were already red on `main` before HYP-01 (scheduled runs 2902–2904 at `4be38c8`). Root causes and proposed patches are in [this comment](#923 (comment)). This PR touches no Rust and not that workflow. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
HYP-01, PR A of 3 (stacked: B = findings schema
support/level, C = quarantine retraction + a factful Signalbox workflow).What this adds
src/Hypatia/ABI/Verdict.idr(%default total, no proof-bypass primitives) is the Epi shape transcribed to the ABI layer:Verdict { claim, evidence : List EvidenceToken, support : Support }. AnEvidenceTokenis rule module + id + version, a span, and a fleet observation count.Support = Pattern | Observed Nat | Mechanical ProverRecheck.Sound : Support -> Typehas one constructor,Rechecked. It is indexed byMechanicaland demandsresult recheck = Confirms. AProverRecheckcarries the SHA-256 of the target and of the prover's output, andsoundArtefactreturns the latter.level(sound/epi/belief) is derived from the record and never stored beside it.Proved in Idris2 0.7.0:
patternNotSound,observedNotSound,refutedNotSound;decSound;soundLevelHasWitness,patternNeverSoundLevel,observedNeverSoundLevel,soundVerdictLevel;Sha256literal of the wrong shape does not typecheck.Falsifiers (all wired into
verify-proofs.yml)scripts/check-verdicts.sh(idris2 job)tests/accept/LeanHoleRecheckSound.idris accepted. Eachtests/reject/*.idris refused atinvalidwith exactly the diagnostic its-- EXPECT:line namesinvalidfor the wrong reason) → redscripts/recheck-lean-hole.sh(lake job)test/soundness/fixtures/code_safety/sorry.lean. Both digests in the positive control must match the fresh run, and Lean's own "declaration uses" diagnostic must appear at the span linescripts/check-sibling-citations.sh(newsibling-citationsjob)scripts/fetch-siblings.shfetches epistemic-types @6a68de3. Every definitionVerdict.idrcites (Warrant, Epi, SoundWarrant, sound-epi, no-receipt-reflection) must be declared at the pin, and the header must name that pinAlso in this PR
fix(proof-status), a separate commit.scripts/check-proof-status.shstepped its span loop by 2 and so checked only every second identifier: 7 of the 16 named on main. With it fixed, main's document still shows 0 mismatches, so nothing stale was hiding. The rows this PR adds are now all gated: 44 identifiers, 0 mismatches.verification/PROOF-STATUS.adocgains a "Verdict support" table. Verdict.idr is PROVEN, the four rejects and the control are TESTED, the Epi/SoundWarrant correspondence is ASSUMED, and Elixir rules carrying proofs stays OPEN.just check-verdicts,just recheck-lean-holeandjust check-siblings. The CLAUDE.md recipe count was re-measured withjust --summary | wc -wand is now 43 (it said 39; it was already 40 before this PR).test/soundness/README.adocnotes thatsorry.leanis now digest-pinned.Status rows
Verdict.idr:patternNotSound,observedNotSound,refutedNotSound,soundLevelHasWitnesscheck-verdicts.sh:PASS: rejected PatternIsNotSound at invalid: Mismatch between: Mechanical recheck and Pattern.(+3)recheck-lean-hole.sh:PASS: positive control agrees with a fresh Lean 4.30.0 re-checkNot done here
🤖 Generated with Claude Code
https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
Generated by Claude Code