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..7296e48 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -74,6 +74,34 @@ 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), which + covers the current corpus; record that run here as the receipt. Every + theorem is `ungraded` under PROOF-POLICY §8 (no per-theorem PWG-3 + receipt; no Rocq or Lean leg). +* *Fixtures.* `ReplayedHolder` and `UnderstatedBound` fail on an index + mismatch (holder, budget), not on the property they are named for; the + positive `noSilentHolderTransport` and `noUnderstatedBound` carry that + evidence. C-1's "semantic type mismatch" holds for the error text, not + for every property named. +* *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..541acce 100644 --- a/docs/applications/rapidnj-q-criterion.adoc +++ b/docs/applications/rapidnj-q-criterion.adoc @@ -218,11 +218,17 @@ 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. 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..167de6a 100644 --- a/src/EpistemicTypes/Applications/RapidNJSkip.agda +++ b/src/EpistemicTypes/Applications/RapidNJSkip.agda @@ -71,8 +71,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/reject/ReplayedHolder.agda b/tests/reject/ReplayedHolder.agda index ac63a0a..972408b 100644 --- a/tests/reject/ReplayedHolder.agda +++ b/tests/reject/ReplayedHolder.agda @@ -5,5 +5,8 @@ open import EpistemicTypes.ProofTransportExample using (Bob; ArtifactIsTrue; mod open HolderBoundary using (module Local; aliceLocalProof) -- Holder-sensitive evidence cannot silently acquire a different holder. +-- Audit 2026-11-09: this is rejected because `View` is indexed by holder, +-- which would also reject it under a holder-independent `Meaning`; the +-- holder-sensitivity evidence is the positive `noSilentHolderTransport`. replay : Local.View Bob true Local.Proof ArtifactIsTrue replay = aliceLocalProof diff --git a/tests/reject/UnderstatedBound.agda b/tests/reject/UnderstatedBound.agda index f1cf084..d21c53f 100644 --- a/tests/reject/UnderstatedBound.agda +++ b/tests/reject/UnderstatedBound.agda @@ -1,5 +1,8 @@ {-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-} module UnderstatedBound where +-- Audit 2026-11-09: this retypes `boundedTrue` (budget `finite 1`) at budget +-- `finite 0`, so it fails on the budget index whatever the cost measure is. +-- The bound check itself is shown by the positive `noUnderstatedBound`. open import Agda.Builtin.Bool open import Agda.Builtin.Nat open import EpistemicTypes.EchoBridge