Repository navigation
feat(findings): every finding names its support; findings.ncl enforced in CI (HYP-01, PR B) - #922
Merged
Merged
Conversation
…ed level (HYP-01)
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 once, after suppression, so no module can emit a
finding without:
support - %{kind: "pattern"} for every rule match today (Elixir
rules carry the tag, not a proof);
evidence - one token: rule, rule version, span, observations;
level - derived by Verdict.level/2, never set by a rule (a
forged level is overwritten): sound only for a mechanical
re-check that confirms, epi with evidence, belief without.
Verdict.attach_recheck/3 is the only path to "sound". It refuses a
re-check of another file, or one whose target digest does not match
the bytes on disk; a refuting re-check derives "epi".
The bash fallback emits the same fields, with the level derived by a
jq def that mirrors Verdict.level/2. GitHub-annotation and text output
render "[level: support]" from the record; SARIF carries
hypatia.level / hypatia.support in the result property bag, outside
the fingerprint. The level counts go on their own stderr line, so the
existing summary line keeps its shape.
Fields are additive. gitbot-fleet's consumers (run-fleet.sh,
fleet-coordinator.sh, submit-finding.sh, apply-baseline.sh) and
.hypatia-baseline.json matching all read findings by key.
test/verdict_test.exs (14 tests) reads the level names out of
Verdict.idr and the sound re-check out of the positive control
tests/accept/LeanHoleRecheckSound.idr, so the two sides cannot drift.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
…ed in CI (HYP-01) schema/ is canonical for findings (ruling 2026-10-14). The old findings.ncl did not evaluate under Nickel 1.11 (its export block was not valid syntax), and generate-findings.ncl called std.env, which no Nickel release has. Nothing referenced either file, so nothing had ever been validated. generate-findings.ncl is removed. The new findings.ncl describes what the producers actually emit: the escript's array (Findings) and the bash fallback's report (BashReport). Both carry support / evidence / level, and the LevelDerived contract re-derives the level and refuses a disagreeing record, so a pattern match can never be reported "sound". The rules.a2ml observation thresholds are labelled as belief formation. Records are open, so the change is additive for consumers. scripts/check-findings-schema.sh --self-test must accept 3 good fixtures and refuse 7 bad ones, each with the message its .expect file names (pattern/observed/refuted claiming sound, belief with evidence, missing support, malformed digest, unknown level). escript-soundness.yml runs that self-test, then validates the repo's own consumer-shaped scan (Nickel 1.11.0, SHA-256 pinned). Locally the self-scan validates: 42 findings, all epi. The first draft of the schema refused real output: cicd_rules, git_state and workflow_hardening emit `"line": null`, so `line` accepts null. 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: 28
✨ 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:42
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 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,evidenceand a derivedlevel.lib/hypatia/verdict.ex(Hypatia.Verdict) is the JSON mirror ofsrc/Hypatia/ABI/Verdict.idr.CLI.collect_findings/2funnels every rule-module finding throughVerdict.annotate/1exactly once, after suppression.support: {kind: "pattern"}, one evidence token (rule, rule version, span, observations), andlevel: "epi". Elixir rules carry the tag only; none is proved sound.levelis derived byVerdict.level/2, and a level a rule tries to set is overwritten.Verdict.attach_recheck/3is 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. Arefutesresult derives"epi". No scan path attaches a re-check yet.hypatia-cli-bash.sh): same fields. The level comes from a jqdefmirroringVerdict.level/2.[level: support]from it. SARIF putshypatia.levelandhypatia.supportin the result property bag, outsidepartialFingerprints, 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.nclrewritten.generate-findings.nclcalledstd.env, which no Nickel release has. Nothing referenced either file, so the generator is removed.Findings(escript array) andBashReport(bash fallback).LevelDerivedcontract re-deriveslevelfromsupport+evidenceand refuses a record that disagrees.Falsifiers
scripts/check-findings-schema.sh --self-test(CI:escript-soundness.yml)PASS: findings schema self-test, 3 accepted, 7 refused.expectnames: pattern / observed / refuted claiming sound, belief with evidence, missing support, malformed digest, unknown levelscripts/check-findings-schema.sh consumer.json(CI: same job, after the consumer-shaped scan)PASS: … satisfies Findings (42 findings; by level: {"epi":42})"line": nullfrom cicd_rules, git_state and workflow_hardening);linenow accepts nullmix test1810 tests, 0 failures, 242 excluded(baseline 1796 / 0 / 242)level/2to call any mechanical support sound → 2 failurestest/verdict_test.exsVerdict.idr; the sound re-check is read from PR A's positive control, so the two sides can't driftrun-escript-soundness.sh14/14 rules fired at expected severityhypatia-cli-bash.shhas the same 74-line report before and afterBackward 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.jsonmatching 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_EXSoverride.phoenix_template1.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 AuditandRust License & Ban Check(the Security workflow) were already red onmainat4be38c8(scheduled runs 2902–2904, before HYP-01).Security Statusfails because it reads.github/workflows/security-policy.ymlwithout a checkout step. This PR touches neither Rust nor that workflow.Anomalies noticed, not touched
mix format --check-formattedflagslib/rules/workflow_audit.ex. That predates this PR, and no workflow gates formatting.🤖 Generated with Claude Code
https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
Generated by Claude Code