diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 62980ffc..dda873e5 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -177,6 +177,7 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa | `RuleEngine.idr` | Rule-evaluation types | | `Verdict.idr` | Verdict records (HYP-01): support = Pattern / Observed n / Mechanical re-check; `Sound` only from a confirming re-check. Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) | | `Retraction.idr` | Quarantine as retraction (HYP-01): a token survives iff its support thins into what remains; a finding survives through one of its tokens. Transcribed from residual-evidence-types `Revision.agda` @ 97244f5 | +| `RsrProfile.idr` | RSR capability-profile resolution (engineering model of `lib/rules/rsr_conformance.ex`): deed precedence, fail-closed duplicate/list-less clauses, a2ml fallback, and when criterion 3.2.2 agrees with the scorecard's `profile_present` (and the one case it does not). Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) | **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager). The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml index eea9c8e2..694af5be 100644 --- a/.github/workflows/verify-proofs.yml +++ b/.github/workflows/verify-proofs.yml @@ -213,7 +213,9 @@ jobs: # from a confirming prover re-check. The typechecker is the falsifier: # tests/accept/ must be accepted, and every tests/reject/ module must be # refused at `invalid` with the diagnostic its `-- EXPECT:` line names. - - name: Verdict accept/reject fixtures (HYP-01) + # The same fixtures gate RsrProfile.idr, the model of the RSR + # capability-profile resolution (lib/rules/rsr_conformance.ex). + - name: Verdict + RSR-profile accept/reject fixtures (HYP-01) run: bash scripts/check-verdicts.sh - name: Summary diff --git a/scripts/check-verdicts.sh b/scripts/check-verdicts.sh index ba896bcd..37ad0b18 100755 --- a/scripts/check-verdicts.sh +++ b/scripts/check-verdicts.sh @@ -10,7 +10,8 @@ # # 1. the ABI package builds (the positive set, first: a broken toolchain or # a missing import must never turn into a "successful" rejection); -# 2. Verdict.idr and Retraction.idr contain no escape-hatch marker at all; +# 2. Verdict.idr, Retraction.idr and RsrProfile.idr contain no +# escape-hatch marker at all; # 3. every module under tests/accept/ is ACCEPTED (positive controls); # 4. every module under tests/reject/ is REFUSED, and refused only at its # declaration `invalid`, with the diagnostic its `-- EXPECT:` line @@ -18,6 +19,11 @@ # slip is also "refused at invalid"), or a refusal for a missing name, # import or parse, is a broken fixture, not a pass. # +# The same accept/reject discipline gates src/Hypatia/ABI/RsrProfile.idr, the +# model of the RSR capability-profile resolution in +# lib/rules/rsr_conformance.ex (tests/accept/RsrProfileResolution.idr and the +# RSR-profile modules under tests/reject/). +# # An empty tests/accept/ or tests/reject/ is a broken checkout, not a pass. # The Lean half of the positive control (re-running the prover and comparing # digests) is scripts/recheck-lean-hole.sh. @@ -35,12 +41,13 @@ mkdir -p "$logs" "$idris2" --version -# 1. Positive set: the ABI package, Verdict included. +# 1. Positive set: the ABI package, Verdict, Retraction and RsrProfile included. "$idris2" --build src/abi/hypatia-abi.ipkg export IDRIS2_PATH="$PWD/build/abi/ttc${IDRIS2_PATH:+:$IDRIS2_PATH}" # 2. No escape hatch in the modules the rejections are about. -for module in src/Hypatia/ABI/Verdict.idr src/Hypatia/ABI/Retraction.idr; do +for module in src/Hypatia/ABI/Verdict.idr src/Hypatia/ABI/Retraction.idr \ + src/Hypatia/ABI/RsrProfile.idr; do if grep -nE 'believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry|admit|native_decide|Admitted|unsafeCoerce|Obj\.magic' \ "$module"; then echo "ERROR: escape-hatch marker in $module" >&2 diff --git a/src/Hypatia/ABI/RsrProfile.idr b/src/Hypatia/ABI/RsrProfile.idr new file mode 100644 index 00000000..00b271cb --- /dev/null +++ b/src/Hypatia/ABI/RsrProfile.idr @@ -0,0 +1,457 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Hypatia ABI — RSR capability-profile resolution (engineering property) +-- +-- A repository declares its RSR capability profile in one of two carriers: +-- a top-level `(rsr-profile …)` clause of its chora deed, or the legacy +-- `/rsr-profile.a2ml`. This module is a model of how +-- lib/rules/rsr_conformance.ex resolves the two, and of the two places that +-- read the result: the scorecard's `profile_present` field and the detector +-- for criterion 3.2.2 (profile present). +-- +-- Mirrored Elixir (Hypatia.Rules.RsrConformance, on main after bffd76a): +-- `declared_capabilities/1` ~ `declaredCapabilities` +-- `deed_profile_capabilities/1` ~ `resolve` (with `profileBodies`, +-- `readBodies`) +-- `clause_capabilities/1` ~ `readClause` (with `capLists`, +-- `keepCaps`) +-- `a2ml_capabilities/1` ~ `a2mlCapabilities` +-- `profile_present/0` (3.2.2) ~ `criterion322` +-- `present_mr("rsr-profile.a2ml")` ~ `a2mlFileVerdict` +-- `deed_clause?/2` ~ not used by 3.2.2 since bffd76a; before +-- it, 3.2.2 passed on any clause, which is +-- the defect `deedDecidedAgrees` excludes +-- `Scorecard.profile_present` ~ `scorecardProfilePresent` +-- (`caps != :none`) +-- +-- What the model abstracts: a deed that is missing, unreadable or does not +-- parse as a `repo-deed` is `Nothing` (all give `:absent`); a parsed deed +-- is its list of top-level items, so a clause nested inside another one is an +-- `OtherClause` and is never read; a field key is only "capabilities or +-- not"; an a2ml carrier is missing, present but declaring no list (does not +-- parse, has no `[rsr-profile]`/`[profile]` section, or has no +-- `capabilities` list), or present with its string list. +-- +-- What is proved here (Idris2, %default total, no proof-bypass primitives): +-- * deed precedence: exactly one well-formed clause decides, whatever the +-- a2ml says (`deedPrecedence`, `a2mlIgnoredUnlessAbsent`); +-- * fail-closed: two or more clauses, or one clause without a +-- capabilities list, declare nothing and fail 3.2.2, whatever the a2ml +-- says (`duplicateDeclaresNothing`, `listlessDeclaresNothing`, +-- `duplicateFailsCriterion`, `listlessFailsCriterion`); +-- * fallback: with no clause the result is the a2ml reading +-- (`fallbackNoDeed`, `fallbackNoClause`, `fallbackCriterionNoClause`); +-- * consistency: 3.2.2 passes iff the scorecard says `profile_present` +-- whenever the deed decides (`deedDecidedAgrees`, the bffd76a fix) and +-- whenever the a2ml is not "present but declaring nothing" +-- (`a2mlDecidedAgrees`); they disagree in exactly that one case +-- (`disagreementIsExactly`), and it is inhabited (`residualDivergence`): +-- with no deed clause, 3.2.2 checks only that rsr-profile.a2ml exists, +-- while the scorecard needs it to yield a capabilities list. +-- +-- What is NOT proved here: that the Elixir behaves as this model. The +-- Elixir is not extracted from this module; the correspondence is by review +-- and by the ExUnit cases in test/rules/rsr_conformance_test.exs. The +-- theorems are properties of the model, not verified code. + +module Hypatia.ABI.RsrProfile + +%default total +%unbound_implicits off + +------------------------------------------------------------------------ +-- Section 1: The two carriers +------------------------------------------------------------------------ + +||| A capability name. The deed reader keeps strings and symbols alike by +||| their text, so both become a `Capability`. +public export +Capability : Type +Capability = String + +||| An element of a deed list value: a string, a symbol, or anything else +||| (number, boolean, uuid, nested list), which the reader drops. +public export +data Atom = StrAtom String | SymAtom String | OtherAtom + +||| A field value: a list, or anything that is not a list. +public export +data Value = ListValue (List Atom) | ScalarValue + +||| A field key, as far as the reader distinguishes keys. +public export +data Key = KCapabilities | KOther + +||| An item in the body of an `(rsr-profile …)` clause. +public export +data BodyItem = BodyField Key Value | BodyClause + +||| A top-level item of a parsed repo deed. An `(rsr-profile …)` clause +||| nested inside another clause is part of that `OtherClause`. +public export +data TopItem = ProfileClause (List BodyItem) | OtherClause | OtherTopField + +||| The legacy `rsr-profile.a2ml`, as the two Elixir readers of it see it. +public export +data A2mlState = A2mlMissing | A2mlDeclaresNothing | A2mlDeclares (List Capability) + +||| What a repository offers: its deed (`Nothing` when there is no +||| parseable repo deed) and its legacy a2ml. +public export +record ProfileSource where + constructor MkProfileSource + deed : Maybe (List TopItem) + a2ml : A2mlState + +------------------------------------------------------------------------ +-- Section 2: Reading the deed (`deed_profile_capabilities/1`) +------------------------------------------------------------------------ + +||| What the deed says about the profile. +public export +data Resolution = Absent | Declared (List Capability) | DeclaresNothing + +||| The text of the strings and symbols in a list; everything else dropped. +public export +keepCaps : List Atom -> List Capability +keepCaps [] = [] +keepCaps (StrAtom s :: vs) = s :: keepCaps vs +keepCaps (SymAtom s :: vs) = s :: keepCaps vs +keepCaps (OtherAtom :: vs) = keepCaps vs + +||| Every `:capabilities` field of a clause body whose value is a list, in +||| order. +public export +capLists : List BodyItem -> List (List Atom) +capLists [] = [] +capLists (BodyField KCapabilities (ListValue vs) :: rest) = vs :: capLists rest +capLists (_ :: rest) = capLists rest + +||| The first capabilities list, or nothing. +public export +firstList : List (List Atom) -> Resolution +firstList [] = DeclaresNothing +firstList (vs :: _) = Declared (keepCaps vs) + +||| `clause_capabilities/1`. +public export +readClause : List BodyItem -> Resolution +readClause body = firstList (capLists body) + +||| The bodies of the top-level `(rsr-profile …)` clauses, in order. +public export +profileBodies : List TopItem -> List (List BodyItem) +profileBodies [] = [] +profileBodies (ProfileClause b :: rest) = b :: profileBodies rest +profileBodies (_ :: rest) = profileBodies rest + +||| None: absent. One: that clause. Two or more: declares nothing. +public export +readBodies : List (List BodyItem) -> Resolution +readBodies [] = Absent +readBodies [b] = readClause b +readBodies (_ :: _ :: _) = DeclaresNothing + +||| `deed_profile_capabilities/1`. +public export +resolve : Maybe (List TopItem) -> Resolution +resolve Nothing = Absent +resolve (Just items) = readBodies (profileBodies items) + +------------------------------------------------------------------------ +-- Section 3: The final capability set and its two readers +------------------------------------------------------------------------ + +||| The Elixir `caps`: `:none` or a list. +public export +data Caps = CapsNone | CapsList (List Capability) + +||| `a2ml_capabilities/1`. +public export +a2mlCapabilities : A2mlState -> Caps +a2mlCapabilities A2mlMissing = CapsNone +a2mlCapabilities A2mlDeclaresNothing = CapsNone +a2mlCapabilities (A2mlDeclares cs) = CapsList cs + +||| The `case` of `declared_capabilities/1`. +public export +fromResolution : Resolution -> A2mlState -> Caps +fromResolution Absent a = a2mlCapabilities a +fromResolution (Declared cs) _ = CapsList cs +fromResolution DeclaresNothing _ = CapsNone + +||| `declared_capabilities/1`. +public export +declaredCapabilities : ProfileSource -> Caps +declaredCapabilities src = fromResolution (resolve (deed src)) (a2ml src) + +||| The scorecard field: `profile_present: caps != :none`. +public export +scorecardProfilePresent : Caps -> Bool +scorecardProfilePresent CapsNone = False +scorecardProfilePresent (CapsList _) = True + +||| A criterion verdict, as far as 3.2.2 produces one. +public export +data CriterionVerdict = Pass | Fail + +||| Whether a verdict passes. +public export +passes : CriterionVerdict -> Bool +passes Pass = True +passes Fail = False + +||| `present_mr("rsr-profile.a2ml")`: the file exists. +public export +a2mlFileVerdict : A2mlState -> CriterionVerdict +a2mlFileVerdict A2mlMissing = Fail +a2mlFileVerdict A2mlDeclaresNothing = Pass +a2mlFileVerdict (A2mlDeclares _) = Pass + +||| The `case` of `profile_present/0`. +public export +check322 : Resolution -> A2mlState -> CriterionVerdict +check322 Absent a = a2mlFileVerdict a +check322 DeclaresNothing _ = Fail +check322 (Declared _) _ = Pass + +||| Criterion 3.2.2, `profile_present/0`. +public export +criterion322 : ProfileSource -> CriterionVerdict +criterion322 src = check322 (resolve (deed src)) (a2ml src) + +------------------------------------------------------------------------ +-- Section 4: Lemmas on the reading steps +------------------------------------------------------------------------ + +public export +fromDeclared : (a : A2mlState) -> (r : Resolution) -> {cs : List Capability} + -> r = Declared cs -> fromResolution r a = CapsList cs +fromDeclared _ _ Refl = Refl + +public export +fromNothing : (a : A2mlState) -> (r : Resolution) + -> r = DeclaresNothing -> fromResolution r a = CapsNone +fromNothing _ _ Refl = Refl + +public export +fromAbsent : (a : A2mlState) -> (r : Resolution) + -> r = Absent -> fromResolution r a = a2mlCapabilities a +fromAbsent _ _ Refl = Refl + +public export +checkNothing : (a : A2mlState) -> (r : Resolution) + -> r = DeclaresNothing -> check322 r a = Fail +checkNothing _ _ Refl = Refl + +public export +checkAbsent : (a : A2mlState) -> (r : Resolution) + -> r = Absent -> check322 r a = a2mlFileVerdict a +checkAbsent _ _ Refl = Refl + +||| One clause: the reading is that clause's. +public export +oneClause : (bs : List (List BodyItem)) -> (body : List BodyItem) + -> bs = [body] -> readBodies bs = readClause body +oneClause _ _ Refl = Refl + +||| Two or more clauses: the deed declares nothing. +public export +twoClauses : (bs : List (List BodyItem)) + -> {b1, b2 : List BodyItem} -> {rest : List (List BodyItem)} + -> bs = b1 :: b2 :: rest -> readBodies bs = DeclaresNothing +twoClauses _ Refl = Refl + +||| No clause: the deed is absent. +public export +noClause : (bs : List (List BodyItem)) -> bs = [] -> readBodies bs = Absent +noClause _ Refl = Refl + +||| A non-empty list of lists reads as its first list. +public export +firstCons : (vs : List Atom) -> (more : List (List Atom)) -> (ls : List (List Atom)) + -> ls = vs :: more -> firstList ls = Declared (keepCaps vs) +firstCons _ _ _ Refl = Refl + +||| An empty list of lists declares nothing. +public export +firstNil : (ls : List (List Atom)) -> ls = [] -> firstList ls = DeclaresNothing +firstNil _ Refl = Refl + +||| A clause with a capabilities list declares its first list. +public export +listedClause : (body : List BodyItem) -> (vs : List Atom) -> (more : List (List Atom)) + -> capLists body = vs :: more -> readClause body = Declared (keepCaps vs) +listedClause body vs more prf = firstCons vs more (capLists body) prf + +||| A clause without a capabilities list declares nothing. +public export +listlessClause : (body : List BodyItem) -> capLists body = [] + -> readClause body = DeclaresNothing +listlessClause body prf = firstNil (capLists body) prf + +------------------------------------------------------------------------ +-- Section 5: Deed precedence +------------------------------------------------------------------------ + +||| Exactly one top-level clause with a capabilities list: the deed's list +||| is the profile, for every a2ml state. +public export +deedPrecedence : (items : List TopItem) -> (a : A2mlState) + -> (body : List BodyItem) -> profileBodies items = [body] + -> (vs : List Atom) -> (more : List (List Atom)) + -> capLists body = vs :: more + -> declaredCapabilities (MkProfileSource (Just items) a) + = CapsList (keepCaps vs) +deedPrecedence items a body one vs more listed = + fromDeclared a (readBodies (profileBodies items)) + (trans (oneClause (profileBodies items) body one) + (listedClause body vs more listed)) + +||| Whenever the deed decides (anything but `Absent`), the a2ml is not read. +public export +a2mlIgnoredUnlessAbsent : (r : Resolution) -> Not (r = Absent) + -> (a, b : A2mlState) + -> fromResolution r a = fromResolution r b +a2mlIgnoredUnlessAbsent Absent notAbsent _ _ = void (notAbsent Refl) +a2mlIgnoredUnlessAbsent (Declared _) _ _ _ = Refl +a2mlIgnoredUnlessAbsent DeclaresNothing _ _ _ = Refl + +------------------------------------------------------------------------ +-- Section 6: Fail-closed +------------------------------------------------------------------------ + +||| Two or more top-level clauses declare nothing, for every a2ml state. +public export +duplicateDeclaresNothing : (items : List TopItem) -> (a : A2mlState) + -> {b1, b2 : List BodyItem} -> {rest : List (List BodyItem)} + -> profileBodies items = b1 :: b2 :: rest + -> declaredCapabilities (MkProfileSource (Just items) a) = CapsNone +duplicateDeclaresNothing items a dup = + fromNothing a (readBodies (profileBodies items)) + (twoClauses (profileBodies items) dup) + +||| One clause without a capabilities list declares nothing, for every a2ml +||| state. +public export +listlessDeclaresNothing : (items : List TopItem) -> (a : A2mlState) + -> (body : List BodyItem) -> profileBodies items = [body] + -> capLists body = [] + -> declaredCapabilities (MkProfileSource (Just items) a) = CapsNone +listlessDeclaresNothing items a body one listless = + fromNothing a (readBodies (profileBodies items)) + (trans (oneClause (profileBodies items) body one) + (listlessClause body listless)) + +||| Two or more top-level clauses fail 3.2.2, for every a2ml state. +public export +duplicateFailsCriterion : (items : List TopItem) -> (a : A2mlState) + -> {b1, b2 : List BodyItem} -> {rest : List (List BodyItem)} + -> profileBodies items = b1 :: b2 :: rest + -> criterion322 (MkProfileSource (Just items) a) = Fail +duplicateFailsCriterion items a dup = + checkNothing a (readBodies (profileBodies items)) + (twoClauses (profileBodies items) dup) + +||| One clause without a capabilities list fails 3.2.2, for every a2ml +||| state. +public export +listlessFailsCriterion : (items : List TopItem) -> (a : A2mlState) + -> (body : List BodyItem) -> profileBodies items = [body] + -> capLists body = [] + -> criterion322 (MkProfileSource (Just items) a) = Fail +listlessFailsCriterion items a body one listless = + checkNothing a (readBodies (profileBodies items)) + (trans (oneClause (profileBodies items) body one) + (listlessClause body listless)) + +------------------------------------------------------------------------ +-- Section 7: Fallback to the a2ml +------------------------------------------------------------------------ + +||| No parseable deed: the profile is the a2ml reading. +public export +fallbackNoDeed : (a : A2mlState) + -> declaredCapabilities (MkProfileSource Nothing a) = a2mlCapabilities a +fallbackNoDeed _ = Refl + +||| A deed without a top-level clause: the profile is the a2ml reading. +public export +fallbackNoClause : (items : List TopItem) -> (a : A2mlState) + -> profileBodies items = [] + -> declaredCapabilities (MkProfileSource (Just items) a) = a2mlCapabilities a +fallbackNoClause items a none = + fromAbsent a (readBodies (profileBodies items)) (noClause (profileBodies items) none) + +||| A deed without a top-level clause: 3.2.2 is the a2ml file check. +public export +fallbackCriterionNoClause : (items : List TopItem) -> (a : A2mlState) + -> profileBodies items = [] + -> criterion322 (MkProfileSource (Just items) a) = a2mlFileVerdict a +fallbackCriterionNoClause items a none = + checkAbsent a (readBodies (profileBodies items)) (noClause (profileBodies items) none) + +------------------------------------------------------------------------ +-- Section 8: 3.2.2 and the scorecard agree +------------------------------------------------------------------------ + +public export +agreeWhenDecided : (r : Resolution) -> (a : A2mlState) -> Not (r = Absent) + -> passes (check322 r a) = scorecardProfilePresent (fromResolution r a) +agreeWhenDecided Absent _ notAbsent = void (notAbsent Refl) +agreeWhenDecided (Declared _) _ _ = Refl +agreeWhenDecided DeclaresNothing _ _ = Refl + +public export +agreeUnlessEmptyA2ml : (r : Resolution) -> (a : A2mlState) + -> Not (a = A2mlDeclaresNothing) + -> passes (check322 r a) = scorecardProfilePresent (fromResolution r a) +agreeUnlessEmptyA2ml Absent A2mlMissing _ = Refl +agreeUnlessEmptyA2ml Absent A2mlDeclaresNothing notEmpty = void (notEmpty Refl) +agreeUnlessEmptyA2ml Absent (A2mlDeclares _) _ = Refl +agreeUnlessEmptyA2ml (Declared _) _ _ = Refl +agreeUnlessEmptyA2ml DeclaresNothing _ _ = Refl + +public export +disagreeReading : (r : Resolution) -> (a : A2mlState) + -> Not (passes (check322 r a) = scorecardProfilePresent (fromResolution r a)) + -> (r = Absent, a = A2mlDeclaresNothing) +disagreeReading Absent A2mlMissing differ = void (differ Refl) +disagreeReading Absent A2mlDeclaresNothing _ = (Refl, Refl) +disagreeReading Absent (A2mlDeclares _) differ = void (differ Refl) +disagreeReading (Declared _) _ differ = void (differ Refl) +disagreeReading DeclaresNothing _ differ = void (differ Refl) + +||| When the deed decides, 3.2.2 passes iff the scorecard says the profile +||| is present. This is the property bffd76a restored: a duplicated or +||| list-less clause neither passes 3.2.2 nor counts as a profile. +public export +deedDecidedAgrees : (src : ProfileSource) -> Not (resolve (deed src) = Absent) + -> passes (criterion322 src) = scorecardProfilePresent (declaredCapabilities src) +deedDecidedAgrees src notAbsent = agreeWhenDecided (resolve (deed src)) (a2ml src) notAbsent + +||| Unless the a2ml is present but declares no capabilities list, 3.2.2 +||| passes iff the scorecard says the profile is present. +public export +a2mlDecidedAgrees : (src : ProfileSource) -> Not (a2ml src = A2mlDeclaresNothing) + -> passes (criterion322 src) = scorecardProfilePresent (declaredCapabilities src) +a2mlDecidedAgrees src notEmpty = agreeUnlessEmptyA2ml (resolve (deed src)) (a2ml src) notEmpty + +||| The two readers disagree only when there is no deed clause and the a2ml +||| is present but declares no capabilities list. +public export +disagreementIsExactly : (src : ProfileSource) + -> Not (passes (criterion322 src) = scorecardProfilePresent (declaredCapabilities src)) + -> (resolve (deed src) = Absent, a2ml src = A2mlDeclaresNothing) +disagreementIsExactly src differ = disagreeReading (resolve (deed src)) (a2ml src) differ + +||| And that case occurs: no deed, and an rsr-profile.a2ml that exists but +||| yields no capabilities list, passes 3.2.2 while the scorecard reports no +||| profile. +public export +residualDivergence : ( criterion322 (MkProfileSource Nothing A2mlDeclaresNothing) = Pass + , scorecardProfilePresent + (declaredCapabilities (MkProfileSource Nothing A2mlDeclaresNothing)) + = False ) +residualDivergence = (Refl, Refl) diff --git a/src/abi/README.adoc b/src/abi/README.adoc index 46a642da..b056474b 100644 --- a/src/abi/README.adoc +++ b/src/abi/README.adoc @@ -36,6 +36,7 @@ been undetectable, so the dead copy was deleted (issue #815, DEBT-REGISTER C-4). |`src/Hypatia/ABI/RuleEngine.idr` |Rule engine type definitions and proof obligations |`src/Hypatia/ABI/Verdict.idr` |Verdict records (HYP-01): every verdict names its support; `Sound` only from a confirming prover re-check. Gate: `just check-verdicts` |`src/Hypatia/ABI/Retraction.idr` |Quarantine as retraction (HYP-01): a finding survives a quarantine only through a token whose support is kept. Gate: `just check-verdicts` +|`src/Hypatia/ABI/RsrProfile.idr` |RSR capability-profile resolution: a model of `lib/rules/rsr_conformance.ex` (deed precedence, fail-closed clauses, a2ml fallback, 3.2.2 vs `profile_present`). Gate: `just check-verdicts` |`src/Hypatia/ABI/Gen.idr` |The generator: evaluates the ABI and emits the generated mirrors |=== diff --git a/src/abi/hypatia-abi.ipkg b/src/abi/hypatia-abi.ipkg index 7a8964a9..9523d1db 100644 --- a/src/abi/hypatia-abi.ipkg +++ b/src/abi/hypatia-abi.ipkg @@ -24,6 +24,7 @@ modules = Hypatia.ABI.Types , Hypatia.ABI.RuleEngine , Hypatia.ABI.Verdict , Hypatia.ABI.Retraction + , Hypatia.ABI.RsrProfile builddir = "../../build/abi" diff --git a/tests/accept/RsrProfileResolution.idr b/tests/accept/RsrProfileResolution.idr new file mode 100644 index 00000000..71641bb5 --- /dev/null +++ b/tests/accept/RsrProfileResolution.idr @@ -0,0 +1,123 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- POSITIVE CONTROL (RSR capability-profile resolution). The cases of +-- test/rules/rsr_conformance_test.exs that exercise the profile reader, +-- stated against the model in src/Hypatia/ABI/RsrProfile.idr and accepted +-- by evaluation, plus the module's theorems applied to them. +-- scripts/check-verdicts.sh requires Idris2 to ACCEPT this module; the +-- RSR-profile cases in tests/reject/ are the other half. + +module RsrProfileResolution + +import Hypatia.ABI.RsrProfile + +%default total +%unbound_implicits off + +-- `(rsr-profile :version "1.0.0" :capabilities ("container" rust))`, after the +-- deed's own top-level fields. +deedEra : List TopItem +deedEra = + [ OtherTopField, OtherTopField + , ProfileClause [ BodyField KOther ScalarValue + , BodyField KCapabilities (ListValue [StrAtom "container", SymAtom "rust"]) ] + ] + +-- Strings and symbols alike, in order. +deedEraDeclares : declaredCapabilities (MkProfileSource (Just RsrProfileResolution.deedEra) A2mlMissing) + = CapsList ["container", "rust"] +deedEraDeclares = Refl + +bashBody : List BodyItem +bashBody = [BodyField KOther ScalarValue, BodyField KCapabilities (ListValue [StrAtom "bash"])] + +bashDeed : List TopItem +bashDeed = [OtherTopField, ProfileClause RsrProfileResolution.bashBody] + +-- The deed wins over a legacy .a2ml beside it. +deedWins : declaredCapabilities (MkProfileSource (Just RsrProfileResolution.bashDeed) (A2mlDeclares ["container"])) + = CapsList ["bash"] +deedWins = deedPrecedence bashDeed (A2mlDeclares ["container"]) bashBody Refl [StrAtom "bash"] [] Refl + +-- Two clauses declare nothing, and the .a2ml is not consulted. +dupDeed : List TopItem +dupDeed = + [ ProfileClause [BodyField KCapabilities (ListValue [StrAtom "bash"])] + , ProfileClause [BodyField KCapabilities (ListValue [StrAtom "rust"])] + ] + +dupDeclaresNothing : declaredCapabilities (MkProfileSource (Just RsrProfileResolution.dupDeed) (A2mlDeclares ["bash"])) + = CapsNone +dupDeclaresNothing = duplicateDeclaresNothing dupDeed (A2mlDeclares ["bash"]) Refl + +dupFails : criterion322 (MkProfileSource (Just RsrProfileResolution.dupDeed) (A2mlDeclares ["bash"])) = Fail +dupFails = duplicateFailsCriterion dupDeed (A2mlDeclares ["bash"]) Refl + +-- `(rsr-profile :version "1.0.0")`: one clause, no list. +listlessBody : List BodyItem +listlessBody = [BodyField KOther ScalarValue] + +listlessDeed : List TopItem +listlessDeed = [ProfileClause RsrProfileResolution.listlessBody] + +listlessNothing : declaredCapabilities (MkProfileSource (Just RsrProfileResolution.listlessDeed) (A2mlDeclares ["bash"])) + = CapsNone +listlessNothing = listlessDeclaresNothing listlessDeed (A2mlDeclares ["bash"]) listlessBody Refl Refl + +listlessFails : criterion322 (MkProfileSource (Just RsrProfileResolution.listlessDeed) (A2mlDeclares ["bash"])) = Fail +listlessFails = listlessFailsCriterion listlessDeed (A2mlDeclares ["bash"]) listlessBody Refl Refl + +-- A capabilities field that is not a list is skipped; a later list is read. +scalarThenList : declaredCapabilities + (MkProfileSource + (Just [ProfileClause [ BodyField KCapabilities ScalarValue + , BodyField KCapabilities (ListValue [StrAtom "a"]) ]]) + A2mlMissing) + = CapsList ["a"] +scalarThenList = Refl + +-- An empty list is a declared (empty) profile, not `:none`. +emptyListDeclared : scorecardProfilePresent + (declaredCapabilities + (MkProfileSource (Just [ProfileClause [BodyField KCapabilities (ListValue [])]]) + A2mlMissing)) + = True +emptyListDeclared = Refl + +-- `(notes (rsr-profile :capabilities ("container")))`: a nested clause is not +-- the profile, so the reader falls back to the (missing) .a2ml. +nestedDeed : List TopItem +nestedDeed = [OtherTopField, OtherClause] + +nestedFallsBack : declaredCapabilities (MkProfileSource (Just RsrProfileResolution.nestedDeed) A2mlMissing) + = CapsNone +nestedFallsBack = fallbackNoClause nestedDeed A2mlMissing Refl + +-- The legacy carrier on its own. +a2mlOnly : declaredCapabilities (MkProfileSource Nothing (A2mlDeclares ["container", "rust"])) + = CapsList ["container", "rust"] +a2mlOnly = fallbackNoDeed (A2mlDeclares ["container", "rust"]) + +-- Empty repo: no deed, no .a2ml; 3.2.2 fails and no profile is present. +emptyRepoFails : criterion322 (MkProfileSource Nothing A2mlMissing) = Fail +emptyRepoFails = Refl + +-- 3.2.2 agrees with the scorecard on the cases bffd76a fixed. +nothingIsNotAbsent : Not (DeclaresNothing = Absent) +nothingIsNotAbsent Refl impossible + +dupAgrees : passes (criterion322 (MkProfileSource (Just RsrProfileResolution.dupDeed) (A2mlDeclares ["bash"]))) + = scorecardProfilePresent + (declaredCapabilities (MkProfileSource (Just RsrProfileResolution.dupDeed) (A2mlDeclares ["bash"]))) +dupAgrees = deedDecidedAgrees (MkProfileSource (Just dupDeed) (A2mlDeclares ["bash"])) nothingIsNotAbsent + +-- The residual case: no deed clause and an .a2ml that exists but yields no +-- capabilities list. 3.2.2 passes on the file's presence; the scorecard +-- reports no profile. +residualPasses : criterion322 (MkProfileSource Nothing A2mlDeclaresNothing) = Pass +residualPasses = fst residualDivergence + +residualNotPresent : scorecardProfilePresent (declaredCapabilities (MkProfileSource Nothing A2mlDeclaresNothing)) + = False +residualNotPresent = snd residualDivergence diff --git a/tests/reject/A2mlOverridesDeed.idr b/tests/reject/A2mlOverridesDeed.idr new file mode 100644 index 00000000..4ad73ccd --- /dev/null +++ b/tests/reject/A2mlOverridesDeed.idr @@ -0,0 +1,29 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- EXPECTED REJECTION (RSR capability-profile resolution). +-- scripts/check-verdicts.sh passes only if Idris2 refuses this module, and +-- only at the declaration `invalid`. Every other declaration must +-- typecheck, so that the refusal is for the stated reason and not for a +-- missing import or a typo. +-- +-- Must fail: when the deed carries exactly one well-formed (rsr-profile …) +-- clause, its list is the profile; the legacy .a2ml beside it is not read. +-- +-- EXPECT: Mismatch between: "container" and "bash". + +module A2mlOverridesDeed + +import Hypatia.ABI.RsrProfile + +%default total +%unbound_implicits off + +bashDeed : List TopItem +bashDeed = [ProfileClause [BodyField KCapabilities (ListValue [StrAtom "bash"])]] + +source : ProfileSource +source = MkProfileSource (Just A2mlOverridesDeed.bashDeed) (A2mlDeclares ["container"]) + +invalid : declaredCapabilities A2mlOverridesDeed.source = CapsList ["container"] +invalid = Refl diff --git a/tests/reject/DuplicatedClauseIsAProfile.idr b/tests/reject/DuplicatedClauseIsAProfile.idr new file mode 100644 index 00000000..34e9bb6e --- /dev/null +++ b/tests/reject/DuplicatedClauseIsAProfile.idr @@ -0,0 +1,33 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- EXPECTED REJECTION (RSR capability-profile resolution). +-- scripts/check-verdicts.sh passes only if Idris2 refuses this module, and +-- only at the declaration `invalid`. Every other declaration must +-- typecheck, so that the refusal is for the stated reason and not for a +-- missing import or a typo. +-- +-- Must fail: a deed carrying two top-level (rsr-profile …) clauses declares +-- nothing, so the scorecard cannot report a profile as present, even with an +-- rsr-profile.a2ml beside it that declares one. +-- +-- EXPECT: Mismatch between: True and False. + +module DuplicatedClauseIsAProfile + +import Hypatia.ABI.RsrProfile + +%default total +%unbound_implicits off + +dupDeed : List TopItem +dupDeed = + [ ProfileClause [BodyField KCapabilities (ListValue [StrAtom "bash"])] + , ProfileClause [BodyField KCapabilities (ListValue [StrAtom "rust"])] + ] + +source : ProfileSource +source = MkProfileSource (Just DuplicatedClauseIsAProfile.dupDeed) (A2mlDeclares ["bash"]) + +invalid : scorecardProfilePresent (declaredCapabilities DuplicatedClauseIsAProfile.source) = True +invalid = Refl diff --git a/tests/reject/DuplicatedClausePassesProfileCriterion.idr b/tests/reject/DuplicatedClausePassesProfileCriterion.idr new file mode 100644 index 00000000..492e268a --- /dev/null +++ b/tests/reject/DuplicatedClausePassesProfileCriterion.idr @@ -0,0 +1,33 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- EXPECTED REJECTION (RSR capability-profile resolution). +-- scripts/check-verdicts.sh passes only if Idris2 refuses this module, and +-- only at the declaration `invalid`. Every other declaration must +-- typecheck, so that the refusal is for the stated reason and not for a +-- missing import or a typo. +-- +-- Must fail: criterion 3.2.2 on a deed carrying two top-level +-- (rsr-profile …) clauses. Before bffd76a the detector passed on any clause +-- while the capability reader declared nothing; the model fails it. +-- +-- EXPECT: Mismatch between: Pass and Fail. + +module DuplicatedClausePassesProfileCriterion + +import Hypatia.ABI.RsrProfile + +%default total +%unbound_implicits off + +dupDeed : List TopItem +dupDeed = + [ ProfileClause [BodyField KCapabilities (ListValue [StrAtom "bash"])] + , ProfileClause [BodyField KCapabilities (ListValue [StrAtom "rust"])] + ] + +source : ProfileSource +source = MkProfileSource (Just DuplicatedClausePassesProfileCriterion.dupDeed) (A2mlDeclares ["bash"]) + +invalid : criterion322 DuplicatedClausePassesProfileCriterion.source = Pass +invalid = Refl diff --git a/tests/reject/ListlessClauseFallsBack.idr b/tests/reject/ListlessClauseFallsBack.idr new file mode 100644 index 00000000..c5fa5389 --- /dev/null +++ b/tests/reject/ListlessClauseFallsBack.idr @@ -0,0 +1,29 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- EXPECTED REJECTION (RSR capability-profile resolution). +-- scripts/check-verdicts.sh passes only if Idris2 refuses this module, and +-- only at the declaration `invalid`. Every other declaration must +-- typecheck, so that the refusal is for the stated reason and not for a +-- missing import or a typo. +-- +-- Must fail: a single (rsr-profile …) clause without a :capabilities list +-- declares nothing. It does not fall back to the rsr-profile.a2ml beside it. +-- +-- EXPECT: Mismatch between: CapsList ["bash"] and CapsNone. + +module ListlessClauseFallsBack + +import Hypatia.ABI.RsrProfile + +%default total +%unbound_implicits off + +listlessDeed : List TopItem +listlessDeed = [ProfileClause [BodyField KOther ScalarValue]] + +source : ProfileSource +source = MkProfileSource (Just ListlessClauseFallsBack.listlessDeed) (A2mlDeclares ["bash"]) + +invalid : declaredCapabilities ListlessClauseFallsBack.source = CapsList ["bash"] +invalid = Refl diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 40dc00d2..fb5b5421 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -317,6 +317,77 @@ Checked against PROOF-POLICY as pinned by `+metadatastician/standards 3-practice |=== // END GENERATED: proof ledger +==== RSR capability-profile resolution (2026-11-09) + +An *engineering* property (estate PROOF-POLICY §1: Idris2), so it is not +graded on the Proof Witness Grade ladder (§8.1) and uses the §5 tokens only. +`+src/Hypatia/ABI/RsrProfile.idr+` models how +`+lib/rules/rsr_conformance.ex+` resolves a repository's capability profile: +`+declared_capabilities/1+`, `+deed_profile_capabilities/1+`, +`+clause_capabilities/1+` and `+a2ml_capabilities/1+` feed the scorecard's +`+profile_present+`; `+profile_present/0+` is the criterion 3.2.2 detector. +The Elixir is not extracted from the model. The theorems are properties of +the model; the correspondence is by review and by ExUnit cases, and is +recorded separately below. `+scripts/check-verdicts.sh+` (CI: `idris2 --check` job) is the gate. + +[width="100%",cols="28%,14%,42%,16%",options="header",] +|=== +|File |Language |Claim |Status +|`+src/Hypatia/ABI/RsrProfile.idr+` |Idris2 |Model theorems. Deed +precedence: exactly one top-level clause with a capabilities list decides, +for every a2ml state (`+deedPrecedence+`, `+a2mlIgnoredUnlessAbsent+`). +Fail-closed: two or more clauses, or one without a list, declare nothing +and fail 3.2.2, for every a2ml state (`+duplicateDeclaresNothing+`, +`+listlessDeclaresNothing+`, `+duplicateFailsCriterion+`, +`+listlessFailsCriterion+`). Fallback: no clause, the a2ml reading +(`+fallbackNoDeed+`, `+fallbackNoClause+`, +`+fallbackCriterionNoClause+`). Consistency: 3.2.2 passes iff +`+scorecardProfilePresent+` whenever the deed decides +(`+deedDecidedAgrees+`, the bffd76a fix) or the a2ml is not present-but- +declaring-nothing (`+a2mlDecidedAgrees+`); they disagree in exactly that +case (`+disagreementIsExactly+`) |PROVEN — Verify Proofs run 42634000625, idris2 --check job 129217248108, at commit 34c7bc7cff0cf54b1b5707a497d9f8abf826e844 (Idris2 v0.7.0, ABI package build) + +|`+tests/accept/RsrProfileResolution.idr+` |Idris2 |Positive control: +the profile-reader cases of test/rules/rsr_conformance_test.exs stated +against the model and accepted by evaluation (`+deedEraDeclares+`, +`+deedWins+`, `+dupDeclaresNothing+`, `+dupFails+`, +`+listlessNothing+`, `+listlessFails+`, `+nestedFallsBack+`, +`+a2mlOnly+`, `+dupAgrees+`) |TESTED — accepted in the same job + +|`+tests/reject/DuplicatedClauseIsAProfile.idr+` |Idris2 |Expected +rejection: a duplicated clause counted as a present profile is refused at +`+invalid+` |TESTED — refused at `invalid` in the same job + +|`+tests/reject/DuplicatedClausePassesProfileCriterion.idr+` |Idris2 +|Expected rejection: a duplicated clause passing 3.2.2 is refused at +`+invalid+` |TESTED — refused at `invalid` in the same job + +|`+tests/reject/ListlessClauseFallsBack.idr+` |Idris2 |Expected +rejection: a list-less clause falling back to the a2ml is refused at +`+invalid+` |TESTED — refused at `invalid` in the same job + +|`+tests/reject/A2mlOverridesDeed.idr+` |Idris2 |Expected rejection: the +a2ml overriding a well-formed deed clause is refused at `+invalid+` |TESTED +— refused at `invalid` in the same job + +|Correspondence, lib/rules/rsr_conformance.ex |Elixir |The model's +functions behave as the Elixir functions their header names. Argued by +review; no kernel checked it, and the Elixir is not extracted from the +model |ASSUMED + +|Runtime behaviour, lib/rules/rsr_conformance.ex |Elixir |Deed era, +deed beside a2ml, duplicated, list-less and nested clauses, and 3.2.2 on a +duplicated or list-less clause: test/rules/rsr_conformance_test.exs +(sampled cases) |TESTED + +|`+src/Hypatia/ABI/RsrProfile.idr+` |Idris2 |3.2.2 and the scorecard's +profile_present can never disagree. False of the code as it stands: with +no deed clause, 3.2.2 checks only that rsr-profile.a2ml exists, while the +scorecard needs it to yield a capabilities list, so an a2ml that does not +parse or carries no list passes 3.2.2 with no profile present +(`+residualDivergence+`) |OPEN +|=== + === Properties Proven ==== 1. Confidence Bounds (`+ConfidenceBounds.idr+`) @@ -427,6 +498,21 @@ Lean legs are still owed (PROOF-POLICY §8.4). `+preventionBranchSource+`, `+preventionBranchTarget+`, `+preventionCodeReviewSource+`, `+preventionCodeReviewTarget+` +==== 9. RSR capability-profile resolution (`+RsrProfile.idr+`) + +Engineering property; §5 tokens only, no PWG grade. Status: as in the +inventory row above. These are properties of the model, not of the Elixir. + +* *P9.1* Deed precedence: `+deedPrecedence+`, `+a2mlIgnoredUnlessAbsent+` +* *P9.2* Fail-closed: `+duplicateDeclaresNothing+`, + `+listlessDeclaresNothing+`, `+duplicateFailsCriterion+`, + `+listlessFailsCriterion+` +* *P9.3* Fallback: `+fallbackNoDeed+`, `+fallbackNoClause+`, + `+fallbackCriterionNoClause+` +* *P9.4* Consistency of 3.2.2 with the scorecard: `+deedDecidedAgrees+`, + `+a2mlDecidedAgrees+`; the exact residual: `+disagreementIsExactly+`, + `+residualDivergence+` + === Dangerous Pattern Audit [cols=",,",options="header",] @@ -443,10 +529,34 @@ Lean legs are still owed (PROOF-POLICY §8.4). === Coverage -Coverage is the Proof Ledger above. A row covers its own model; whether the -Elixir runtime follows a model is a separate row (`+models-runtime-refinement+`, -and the rows that name a runtime test). The earlier hand-written coverage map -marked models "Full" without that evidence and has been retired. +|API type safety |`+Types.idr+`, `+GraphQL.idr+`, `+REST.idr+`, +`+GRPC.idr+`, `+FFI.idr+` |Full + +|Quarantine logic |`+Quarantine.idr+` |Full + +|Batch rollback |`+BatchRollback.idr+` |Full + +|VeriSimDB connector |`+VerisimdbConnector.idr+` |Full (model; statement +superseded 2026-11-01) + +|Logtalk → Elixir alert-table correspondence +|`+LogtalkMigration.agda+` |Finite model only — Grade 3 / +AGDA-VERIFIED (receipt above); fix text and runtime refinement excluded + +|Neural ensemble aggregation |`+NeuralConsensus.idr+` |Full (bounds + +min-lower-bound) + +|RSR capability-profile resolution |`+RsrProfile.idr+` |Model only; +correspondence to the Elixir ASSUMED + +|VCL parser totality |`+ParserTotality.lean+` |Full (FROM-clause subset) + +|VCL query correctness |- |Partial + +|Neural network convergence |`+PageRankInvariants.lean+`, +`+ESNSpectralScaling.lean+` |Preconditions proven; full +convergence/stability in progress (Lean + Mathlib) +|=== === File Locations