diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index d8d6a1b..0a2c422 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -112,8 +112,11 @@ is the integer model: `IntegerModel` proves every law the bound consumes, and `RapidNJExamples` runs a worked scan by computation. Making rational input first-class needs either a rational carrier instance or the common-denominator rescaling transport; the bound itself never multiplies or divides carrier -elements, so no field law is needed either way. Anything rounded cannot meet -the `Checkable` reflection law, as `no-always-true` shows. See +elements, so no field law is needed either way. Floating point is excluded +because a Float64 carrier is not a model of the four `OrderedGroup` laws +(NaN is not ordered, so `≤-refl` fails) and because the bound would be +about float-computed Q, not exact Q. (`no-always-true` only refutes a +comparison that always answers true; it says nothing about rounding.) See link:docs/applications/rapidnj-q-criterion.adoc[]. == Dogfooded Across The Account diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 0e662ba..864b13e 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -74,6 +74,40 @@ This document uses the estate proof-policy vocabulary: rechecked by this repository; * `OPEN` — not discharged. +[NOTE] +.Design and receipt audit (2026-11-09) +==== +* *Receipts.* The "local receipt 2026-11-07" rows (C-1, C-3, C-4, PR-1, + PR-2, QR-1, OS-1, RS-1) cite logs and hashes kept under `_build/`, which + is gitignored, so those receipts cannot be retrieved from the repository. + Hosted Proof Safety passed on `main` at `dcd4648` (2026-11-07, run + 42395802116). That run is historical evidence for the corpus at that + commit, including the earlier `ReplayedHolder` and `UnderstatedBound` + fixtures; it does not cover the rewritten fixtures, whose receipt is the + pinned-toolchain gate on the commit that carries them. Every + theorem is `ungraded` under PROOF-POLICY §8 (no per-theorem PWG-3 + receipt; no Rocq or Lean leg). +* *Fixtures.* `ReplayedHolder` and `UnderstatedBound` previously failed on an index + mismatch (holder, budget), not on the property they are named for; the + positive `noSilentHolderTransport` and `noUnderstatedBound` carry that + evidence. *Resolved 2026-11-09:* both fixtures now have an + `EXPECTED-REJECTION` boundary with a checked valid prefix. `ReplayedHolder` + fails at the checker's soundness obligation `Bob ≡ Alice` (the + holder-sensitive meaning), and `UnderstatedBound` fails at the `within` + obligation `1 ≤ 0`. +* *Definitional results.* OS-1's equivalence holds for every decoder on + generated inputs (adequacy fixes the answer), and "noninterference" there + is a decoder-relative property, not information-flow noninterference, + which README lists as out of scope. RS-1's "least" holds by definition + (`Migration` and `RelativeReduction` have the same fields). + `status-of-skip-is-factive` is `refl` on a constant. +* *C-2* round-trips with `EchoResidue.EchoR` (a certificate-carrying + residue), not with the canonical `Echo` fibre; the fibre correspondence + is C-4. +* *Floating point.* The earlier argument that rounding is not monotone was + wrong; see `docs/applications/rapidnj-q-criterion.adoc`. +==== + The separate cross-prover labels `AGDA-PENDING`, `AGDA-VERIFIED`, `COQ-CHECKED`, `LEAN-CHECKED`, `BRIDGE-PENDING`, and `RECONCILED` describe verification legs; they do not strengthen the proof-policy status. diff --git a/docs/applications/rapidnj-q-criterion.adoc b/docs/applications/rapidnj-q-criterion.adoc index ea8d17b..f513263 100644 --- a/docs/applications/rapidnj-q-criterion.adoc +++ b/docs/applications/rapidnj-q-criterion.adoc @@ -218,14 +218,22 @@ and neither is claimed here: four group laws, plus the `Checkable` obligation. More proof work, same seam. -*What is excluded.* Floating point. `Checkable.decide-true` is a reflection -law, and rounded arithmetic does not satisfy it in general; the abstract -obstruction is made precise by `RapidNJExamples.no-always-true`, which shows -that a comparison answering `true` for every pair would prove that every -integer is below every other. The practical rule for the runtime is therefore: +*What is excluded.* Floating point. A Float64 carrier is not a model of the +four `OrderedGroup` laws: NaN is unordered, so `≤-refl` fails. (The +record does not ask for associativity, so non-associative float addition is +not itself the obstruction.) +The bound would also be about float-computed Q rather than exact Q. (An +earlier version of this paragraph said rounding is not monotone and cited +`RapidNJExamples.no-always-true`. Round-to-nearest *is* monotone, and +`no-always-true` only shows that a comparison answering `true` for every +pair would prove that every integer is below every other; it says nothing +about rounding. Audit note 2026-11-09.) The practical rule for the runtime +is therefore: the moment a rounding-tolerant `Float64` value participates in a *bound comparison*, the claim cannot be `:Factive`; record it as `:Belief` until an -exact comparison decides it. +exact comparison decides it. "Exact" means recomputed from the exact inputs +(or bounded by a proved error term), not an exact comparison of values that +were already rounded: `2^53 + 1` and `2^53` round to the same Float64. == What is proved, and what is not diff --git a/src/EpistemicTypes/Applications/OrderedGroup.agda b/src/EpistemicTypes/Applications/OrderedGroup.agda index 40f4cd3..b03dde9 100644 --- a/src/EpistemicTypes/Applications/OrderedGroup.agda +++ b/src/EpistemicTypes/Applications/OrderedGroup.agda @@ -29,9 +29,10 @@ -- -- * Any model of these four laws certifies the bound, so the bound does not -- depend on the *representation* of rationals, only on exactness. --- * A Float64 implementation does not satisfy `≤-⊕`: rounding is not --- monotone for every pair of operands, so `x ≤ y` can hold while --- `x + z > y + z` holds under rounding. That is the seam documented in +-- * A Float64 implementation is not a model of these laws: NaN is not +-- ordered, so `≤-refl` fails at NaN (round-to-nearest itself is +-- monotone; corrected 2026-11-09). The bound would also be about +-- float-computed Q, not exact Q. That is the seam documented in -- link:docs/applications/rapidnj-q-criterion.adoc[], and the reason the -- reflection lemma in `RapidNJSkip` is the single non-negotiable -- obligation of an executable implementation. diff --git a/src/EpistemicTypes/Applications/RapidNJSkip.agda b/src/EpistemicTypes/Applications/RapidNJSkip.agda index 1e01e59..ca700d5 100644 --- a/src/EpistemicTypes/Applications/RapidNJSkip.agda +++ b/src/EpistemicTypes/Applications/RapidNJSkip.agda @@ -22,8 +22,9 @@ -- arithmetic fact consumed is the order-monotonicity budget of -- `OrderedGroup` (no ring identities, hence no ℚ-specific law). The -- resulting knowledge is therefore valid in any exact model, and an --- implementation whose arithmetic is not exact fails at exactly one place: --- supplying `Checkable` (see the Float64 seam in +-- implementation whose arithmetic is not exact fails in two places: it is +-- not a model of `OrderedGroup` (IEEE order is not reflexive at NaN), and its +-- comparison is not a sound `Checkable` for exact Q (see the Float64 seam in -- link:docs/applications/rapidnj-q-criterion.adoc[]). -- -- The same run, held without a soundness map, is belief: `Epi` packages a @@ -71,8 +72,8 @@ module Skip (G : OrderedGroup) where -- A decision procedure whose `true` verdicts *reflect* the order. This is -- the single seam between the proof and a running program: an -- implementation with exact arithmetic (integers, or rationals with - -- cross-multiplied comparisons) can supply it; one with rounding cannot, - -- because rounding is not monotone for every pair of operands. + -- cross-multiplied comparisons) can supply it; a Float64 one is excluded + -- because Float64 is not a model of the OrderedGroup laws (2026-11-09). record Checkable : Set₁ where field decide : (x y : Carrier) -> Bool diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh index e05871c..b9ff4b0 100644 --- a/tests/check-rejections.sh +++ b/tests/check-rejections.sh @@ -18,7 +18,7 @@ prefix_dir=$(mktemp -d) trap 'rm -rf "$prefix_dir"' EXIT for fixture in "${fixtures[@]}"; do case "$fixture" in - QueryIgnoresCollision|QuerySuccessInventsSource|ObserverRevealsSecret|OffImageStatusHidden|ForgetfulResidueSufficient) + QueryIgnoresCollision|QuerySuccessInventsSource|ObserverRevealsSecret|OffImageStatusHidden|ForgetfulResidueSufficient|ReplayedHolder|UnderstatedBound) [[ $(rg -c '^-- EXPECTED-REJECTION$' "tests/reject/$fixture.agda") == 1 ]] || { printf 'FAIL: %s must have exactly one rejection boundary\n' "$fixture" exit 1 @@ -51,11 +51,11 @@ for fixture in "${fixtures[@]}"; do case "$fixture" in LyingVerifier|ForgedAcceptance) expected='false != .*true' ;; ReplayedArtifact) expected='true != .*false' ;; - ReplayedHolder) expected='Alice != .*Bob' ;; + ReplayedHolder) expected='Bob != .*Alice' ;; StaleSample|ForkedHistory|ForgedResidue|MismatchedSource) expected='false != .*true' ;; UncheckedSkip) expected='false != .*true' ;; FakeFreshness) expected='initial .*false !=' ;; - UnderstatedBound) expected='1 != 0' ;; + UnderstatedBound) expected='suc _[^ ]* != zero of type Nat' ;; InventedMigration) expected='true != .*false' ;; BeliefIsKnowledge) expected='w₁ != .*w₀' ;; AgentChangesAnchor) expected='0 != 1' ;; diff --git a/tests/reject/ReplayedHolder.agda b/tests/reject/ReplayedHolder.agda index ac63a0a..4ba36d5 100644 --- a/tests/reject/ReplayedHolder.agda +++ b/tests/reject/ReplayedHolder.agda @@ -1,9 +1,18 @@ {-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} module ReplayedHolder where open import Agda.Builtin.Bool using (true) +open import Agda.Builtin.Equality using (refl) open import EpistemicTypes.ProofTransportExample using (Bob; ArtifactIsTrue; module HolderBoundary) -open HolderBoundary using (module Local; aliceLocalProof) +open HolderBoundary using (module Local) --- Holder-sensitive evidence cannot silently acquire a different holder. -replay : Local.View Bob true Local.Proof ArtifactIsTrue -replay = aliceLocalProof +-- Holder-sensitive evidence cannot be re-certified for a different holder. +-- `LocalMeaning holder _ _` is `holder ≡ Alice`. The forgery below +-- replays Alice's accepting checker with Bob as the holder; it fails +-- exactly at the checker's soundness obligation, `Bob ≡ Alice`. Under a +-- holder-independent meaning the same term would type-check, so the +-- rejection is evidence about the meaning, not about the `View` index. +-- (Rewritten 2026-11-09; the earlier fixture failed on the index alone.) + +-- EXPECTED-REJECTION +bobCheck : Local.CertificateCheck Bob true ArtifactIsTrue +bobCheck = Local.certificateCheck (λ _ -> true) (λ _ _ -> refl) diff --git a/tests/reject/UnderstatedBound.agda b/tests/reject/UnderstatedBound.agda index f1cf084..c0c48f1 100644 --- a/tests/reject/UnderstatedBound.agda +++ b/tests/reject/UnderstatedBound.agda @@ -1,9 +1,18 @@ {-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} module UnderstatedBound where -open import Agda.Builtin.Bool open import Agda.Builtin.Nat +open import Agda.Builtin.Bool open import EpistemicTypes.EchoBridge import EpistemicTypes.ContinuityExamples as Examples -open Examples.Residues using (identityRetention; constantCost; boundedTrue) +open Examples.Residues using (identityRetention; constantCost; identityTrue) + +-- A bounded echo must prove its cost is within the budget. The residue +-- costs `finite 1`; the forgery claims budget `finite 0` and supplies the +-- proof that worked for budget `finite 1`. It fails at the `within` +-- obligation, `1 ≤ 0`, not at an index. (Rewritten 2026-11-09; the +-- earlier fixture retyped a finished value and failed on the budget +-- index whatever the cost measure was.) + +-- EXPECTED-REJECTION forged : BoundedEcho identityRetention constantCost (finite zero) true -forged = boundedTrue +forged = bounded identityTrue (finite≤ (suc≤ zero≤))