From 2ff19b8ca2b16987caab45b42ca3c1cce6d33c35 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 27 Sep 2026 00:51:55 +0000 Subject: [PATCH] =?UTF-8?q?feat(applications):=20RapidNJ=20Q-criterion=20b?= =?UTF-8?q?ound,=20generated=20skip=20warrants,=20=E2=84=A4=20instance?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New applications section under src/EpistemicTypes/Applications/, with the per-row RapidNJ branch-and-bound rule as its first worked example. - OrderedGroup: the arithmetic budget (addition, negation, order, the four laws, Nat-indexed scale). - IntegerModel: ℤ as difference pairs, cross-multiplied order, all four laws, the ℤ-group instance, and a decidable order. - SortedRow: rows, the sorted-row and running-maximum invariants, and the prefix/suffix membership decomposition. - QCriterion: qBound = (r-2)·d_next - t_i - t_max and the bound lemma qBound-≤-Q, proved with monotonicity, antitonicity and transitivity only. - RapidNJSkip: Checkable (the exactness seam), the generated skip warrant and its soundness map, skip-known, no-receipt-reflection, and the belief-only reading; FactiveModality.reflect is instantiated by the bound's soundness map. - RapidNJExamples: executable integer check, worked four-taxon scan, the no-always-true refutation, and the runtime status mirror. - Rejection fixture UncheckedSkip (twelve fixtures now); EchoBridge._≤ℕ_ gains an infix declaration at its definition site; check-proofs.sh now recurses, so the Applications tree is gated (seventeen modules). - Docs: docs/applications/rapidnj-q-criterion.adoc plus README, docs index, PROOF-STATUS, CHANGELOG, EXPLAINME, AUDIT, ci-safety and STATE.a2ml. Rational input is a stated obligation, not a claim: the bound consumes no field, multiplication or division law, and the common-denominator rescaling path is documented rather than assumed. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .machine_readable/descriptiles/STATE.a2ml | 20 +- AUDIT.adoc | 8 +- CHANGELOG.adoc | 23 ++ EXPLAINME.adoc | 33 ++ PROOF-STATUS.adoc | 34 +- README.adoc | 39 +++ docs/README.adoc | 18 +- docs/applications/rapidnj-q-criterion.adoc | 274 +++++++++++++++++ docs/ci-safety.adoc | 4 +- docs/continuity-foundations.adoc | 8 +- src/EpistemicTypes/All.agda | 5 + .../Applications/IntegerModel.agda | 239 ++++++++++++++ .../Applications/OrderedGroup.agda | 112 +++++++ .../Applications/QCriterion.agda | 113 +++++++ .../Applications/RapidNJExamples.agda | 166 ++++++++++ .../Applications/RapidNJSkip.agda | 291 ++++++++++++++++++ .../Applications/SortedRow.agda | 82 +++++ src/EpistemicTypes/Base.agda | 7 + src/EpistemicTypes/EchoBridge.agda | 6 + tests/check-proofs.sh | 5 +- tests/check-rejections.sh | 3 +- tests/reject/UncheckedSkip.agda | 44 +++ 22 files changed, 1518 insertions(+), 16 deletions(-) create mode 100644 docs/applications/rapidnj-q-criterion.adoc create mode 100644 src/EpistemicTypes/Applications/IntegerModel.agda create mode 100644 src/EpistemicTypes/Applications/OrderedGroup.agda create mode 100644 src/EpistemicTypes/Applications/QCriterion.agda create mode 100644 src/EpistemicTypes/Applications/RapidNJExamples.agda create mode 100644 src/EpistemicTypes/Applications/RapidNJSkip.agda create mode 100644 src/EpistemicTypes/Applications/SortedRow.agda create mode 100644 tests/reject/UncheckedSkip.agda diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index 87e89e9..b80fa13 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -1,7 +1,7 @@ [metadata] project = "epistemic-types" version = "0.1.0" -last-updated = "2026-06-15" +last-updated = "2026-09-27" status = "prototype" # prototype | active | paused | archived [project-context] @@ -29,6 +29,12 @@ aggregator = "src/EpistemicTypes/All.agda re-exports every module." # Agda modules under src/EpistemicTypes/. list = [ "EpistemicTypes.Access", + "EpistemicTypes.Applications.IntegerModel", + "EpistemicTypes.Applications.OrderedGroup", + "EpistemicTypes.Applications.QCriterion", + "EpistemicTypes.Applications.RapidNJExamples", + "EpistemicTypes.Applications.RapidNJSkip", + "EpistemicTypes.Applications.SortedRow", "EpistemicTypes.All", "EpistemicTypes.Base", "EpistemicTypes.ContinuityExamples", @@ -50,6 +56,12 @@ surreal-bridge = "SurrealAccess carrier + GradedSurrealModality + daySurrealAcce examples = "Worked instances exercising the interfaces." proof-transport = "proofSound derives Meaning holder artifact claim from an accepted sound checker. Receipts alone do not certify; transfer requires the target-holder meaning." proof-transport-example = "Boolean certificate checker with legitimate acceptance and refutations for false claims, changed artifacts and holder-sensitive replay." +applications-ordered-group = "Minimal arithmetic budget for the applications layer: carrier with addition, negation, zero, order, reflexivity, transitivity, joint monotonicity and antitone negation; derived subtraction and Nat-indexed scaling." +applications-integer-model = "The integers as difference pairs over Nat, with the cross-multiplied order, all four OrderedGroup laws, the instance 'ℤ-group', and a decision procedure for the order." +applications-sorted-row = "Rows as entries (index, distance, row sum), the All predicate, membership, the sorted-row and running-maximum invariants, and prefix/suffix composition." +applications-qcriterion = "Q and qBound over any OrderedGroup, the bound lemma qBound-≤-Q, the row lemma qBound-≤-suffix, claim weakening, and prefix/suffix composition." +applications-rapidnj-skip = "Checkable (the exactness seam), scan state, skip evidence, the generated warrant and soundness map, the factive modality, the belief-only reading, and the declared-not-assumed cross-iteration obligation." +applications-rapidnj-examples = "Executable integer check, refutation of an over-eager comparison, a worked four-taxon scan, and the runtime status mirror (Factive / Belief / Collapsed / SansFibre)." [route-to-mvp] milestones = [ @@ -59,6 +71,8 @@ milestones = [ { name = "Concrete Kripke-style semantics", completion = 0 }, { name = "Evidence-state and observation-rule examples", completion = 0 }, { name = "Richer day-bounded surreal fragments as SurrealAccess instances", completion = 0 }, + { name = "Applications layer: RapidNJ Q-criterion bound and skip warrants", completion = 100 }, + { name = "Rational (ℚ) instance and the common-denominator rescaling transport", completion = 0 }, { name = "Lawful instances (only after proving or explicitly assuming laws)", completion = 0 }, ] @@ -69,10 +83,12 @@ items = [ "Add richer day-bounded surreal fragments as instances of the abstract SurrealAccess interface.", "Add lawful instances only after proving or explicitly assuming laws.", "Extend the echo bridge without importing a full graded comonad.", + "Add a rational carrier instance for the applications layer, or prove the common-denominator rescaling transport.", + "Model the row-insertion update that maintains the scan invariants, and cross-iteration bound reuse.", ] [progress-summary] -note = "Prototype. The base interface and all eleven modules typecheck under 'just check' (Agda 2.6.4.3, --safe --without-K, --no-libraries, no postulates). The endofunctor/Modality formers, Warrant, Access transport, EchoBridge residue, SurrealBridge tower, ProofTransport, and its K9-SVC/A2ML attestation example are in place. Remaining work is semantics and lawful instances — see [roadmap]." +note = "Prototype. The base interface and all seventeen modules typecheck under 'just check' (Agda 2.6.4.3, --safe --without-K, --no-libraries, no postulates), against twelve rejection fixtures. The endofunctor/Modality formers, Warrant, Access transport, EchoBridge residue, SurrealBridge tower, ProofTransport, its K9-SVC/A2ML attestation example, and the applications layer (RapidNJ Q-criterion bound, generated skip warrants, discharged integer instance) are in place. Remaining work is semantics, lawful instances, and the rational/rescaling obligation — see [roadmap]." [blockers-and-issues] # No active blockers. diff --git a/AUDIT.adoc b/AUDIT.adoc index 149749c..355eeb9 100644 --- a/AUDIT.adoc +++ b/AUDIT.adoc @@ -18,9 +18,11 @@ The owner authorized proof/security CI and protected-main enforcement on billing incident are superseded. Existing GitHub workflows already run; their current proof coverage is extended by this change. -* The eleven-module core is checked with Agda 2.6.4.3, safe mode, without-K, - internal double checking and warnings as errors. Each source module is checked. -* Eleven deliberate rejection fixtures must fail for their intended type mismatch. +* Every module under `src/EpistemicTypes/` -- seventeen at the time of writing, + including the applications layer -- is checked with Agda 2.6.4.3, safe mode, + without-K, internal double checking and warnings as errors. Each source + module is checked. +* Twelve deliberate rejection fixtures must fail for their intended type mismatch. * Canonical Echo residue correspondence is checked against pinned sibling source. * CodeQL analyzes Actions workflows, and the shared scanner checks secrets. * Main receives changes through PRs with required proof/security checks. Signed diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index abc31dc..ff12341 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -12,6 +12,29 @@ the changelog records what is actually proved, not what is aspired to. === https://github.com/hyperpolymath/epistemic-types/compare/v0.1.0...HEAD[Unreleased] +[[added--2026-09-27]] +==== Added — 2026-09-27 + +* New applications section, `src/EpistemicTypes/Applications/`, with the + RapidNJ per-row Q-criterion bound as its first worked example: + `OrderedGroup` (minimal arithmetic budget), `IntegerModel` (the integers as + difference pairs, with all four laws and a decidable order), `SortedRow` + (rows, invariants, prefix/suffix composition), `QCriterion` (the bound lemma + `qBound-≤-Q` and the row and composition lemmas), `RapidNJSkip` (checkability + seam, generated warrant and soundness, the factive modality, and the belief + reading), and `RapidNJExamples` (the executable integer check, a worked scan, + a refutation of over-eager comparisons, and the runtime status mirror). +* Skipping a matrix quadrant now *generates* a valid warrant whose soundness + map is proved from the bound; no soundness is assumed, and the bound consumes + no ring, multiplication or division laws. Rational input is an explicitly + stated obligation, documented in `docs/applications/rapidnj-q-criterion.adoc`. +* New rejection fixture `UncheckedSkip`: a recorded check the numbers do not + meet is refused, so the rejection manifest is now twelve fixtures. +* `EchoBridge`'s `_≤ℕ_` gained an `infix 4` declaration at its definition site. + A fixity declaration only; no definition changed. +* New documentation: `docs/applications/rapidnj-q-criterion.adoc`, plus README, + documentation-index, proof-status and machine-readable state updates. + [[fixed--2026-09-07]] ==== Fixed — 2026-09-07 diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index c016218..84946b8 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -91,6 +91,29 @@ claims. The theorem remains relative to the specified meaning and checker proof; it does not establish cryptography or physical facts. See link:docs/proof-transport.adoc[]. +=== Skipping a search quadrant generates a warrant, not an assumption + +How this is implemented:: +`src/EpistemicTypes/Applications/` formalizes the per-row bound RapidNJ uses +when searching for the neighbour-joining minimum. `QCriterion.qBound-≤-Q` +proves the bound over an arbitrary `OrderedGroup` using only monotonicity, +antitonicity, transitivity and `Nat`-indexed scaling. `RapidNJSkip` turns a +skip certificate (sorted-row invariant, running-maximum invariant, accepted +exact check) into a `Warrant`, proves its soundness from the bound +(`skip-known`), and instantiates `FactiveModality.reflect` with that soundness +map; held without it, the same run is belief +(`no-receipt-reflection`). + +Caveat:: +The rational case is a *stated obligation*, not a theorem. What is discharged +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 +link:docs/applications/rapidnj-q-criterion.adoc[]. + == Dogfooded Across The Account [cols="1,2,2", options="header"] @@ -112,6 +135,16 @@ link:docs/proof-transport.adoc[]. == Known gaps +[CAUTION] +==== +**The applications layer has no rational instance yet.** The RapidNJ +Q-criterion bound is proved order-generically and discharged for the integers; +a rational carrier (or the common-denominator rescaling transport) is stated as +an obligation in `docs/applications/rapidnj-q-criterion.adoc`, together with the +row-insertion update and cross-iteration bound reuse. +==== + + [CAUTION] ==== **No Kripke semantics.** The prototype defines the syntactic/type-theoretic interfaces for modalities but does not model them against a Kripke frame semantics. This is the largest open theoretical gap. diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 89837ee..e766da1 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -8,6 +8,35 @@ Verification status of the epistemic-types Agda formalisation. The whole library self-contained (`--no-libraries`: it imports only `Agda.Builtin.*` / `Agda.Primitive`). This records a reproduced `agda` run, not a "looks fine" reading. +== Applications layer — 2026-09-27 + +`src/EpistemicTypes/Applications/` adds the first worked application: the +per-row Q-criterion bound used by RapidNJ when searching for the +neighbour-joining minimum. Five modules and one example module pass the same +gate (`--safe --without-K --no-libraries --double-check -W error`, no +postulates): + +* `QCriterion.qBound-≤-Q` proves the row bound over an arbitrary + `OrderedGroup`, using only reflexivity, transitivity, monotone addition, + antitone negation and `Nat`-indexed scaling -- no ring law, no multiplication + or division of carrier elements. +* `RapidNJSkip` generates a warrant from a skip certificate (sorted-row + invariant, running-maximum invariant, accepted exact check) and proves + `skip-known`: the skipped quadrant's entries cannot beat the incumbent. The + soundness map is `FactiveModality.reflect = sound-epi`; without it the same + run is belief (`no-receipt-reflection`). +* `IntegerModel` discharges the arithmetic budget for the integers, and + `RapidNJExamples` turns `dec-≤ℤ` into a `Checkable`, runs a worked four-taxon + scan by computation, and refutes an over-eager comparison + (`no-always-true`). +* One new rejection fixture (`UncheckedSkip`) refuses a recorded check that the + numbers do not meet. + +Not claimed: any rational (ℚ) instance, the rescaling transport from a rational +matrix to its common-denominator integer form, the row-insertion update that +maintains the invariants, and cross-iteration bound reuse. These are stated as +obligations in link:docs/applications/rapidnj-q-criterion.adoc[]. + == Current continuity-foundations correction — 2026-09-07 `ReadView` now entails equality with the indexed store contents. Cached-read @@ -19,8 +48,9 @@ and migration have explicit obligations. The collision theorem refutes every migration requiring a distinction discarded by the retained pair. Resource bounds require measure inequalities; arbitrary grade retagging is removed. -The eleven-module core and eleven deliberate rejection fixtures pass with -Agda 2.6.4.3 under `--safe --without-K --no-libraries`, without warnings. +The eleven-module core and eleven deliberate rejection fixtures (the counts at +that date; `just check` now reports seventeen modules and twelve fixtures) pass +with Agda 2.6.4.3 under `--safe --without-K --no-libraries`, without warnings. The additional canonical Echo integration proves both representation round trips and agreement of lowering; its standard-library dependencies emit Cubical compatibility warnings. See link:docs/continuity-foundations.adoc[] for commands, diff --git a/README.adoc b/README.adoc index 8622ad3..da789a5 100644 --- a/README.adoc +++ b/README.adoc @@ -98,6 +98,36 @@ See link:docs/continuity-foundations.adoc[the breaking API correction and proof boundaries]. An optional integration gate proves correspondence with the actual sibling `EchoResidue.EchoR`; the core remains dependency-free. +== Applications: the RapidNJ Q-criterion + +The `Applications/` tree is where the core interfaces are exercised against +algorithmic claims that arrive with their own arithmetic. Its first example is +the per-row branch-and-bound rule used by RapidNJ (Simonsen, Mailund, Pedersen +2008) when searching for the neighbour-joining minimum: while scanning a row of +distances in increasing order, the row is abandoned as soon as + + qBound = (r - 2) * d(i,next) - t(i) - t_max + +is at least the incumbent `q_min`, because no unexamined entry can beat it. + +The development is order-generic: `Applications.QCriterion.qBound-≤-Q` proves +the bound for any carrier with monotone addition, antitone negation and a +transitive order -- no multiplication or division of carrier elements occurs +anywhere, and the coefficient `(r - 2)` enters only as a `Nat`-indexed repeated +sum. A skip certificate carries the sorted-row invariant, the running-maximum +invariant and an accepted executable check; `Applications.RapidNJSkip` then +*generates* a warrant for the skipped quadrant, and its soundness map is +exactly the `reflect` of a `FactiveModality`: + + run data -> skipWarrant -> skip-sound (the bound lemma) -> reflect -> the claim + +So skipping a quadrant yields knowledge only through a proved bound, never by +assumption, and the same run held without the soundness map is belief. The +integer model is discharged in full (`Applications.IntegerModel`, +`Applications.RapidNJExamples`); the rational case is a *stated* obligation, not +a claim -- see link:docs/applications/rapidnj-q-criterion.adoc[the applications +note] for the rescaling argument and the exact-arithmetic seam. + == Proof transport across trust boundaries `ProofTransport` is parameterised by agents, claim labels, artefacts, @@ -150,6 +180,10 @@ interface is a breaking correction documented in link:docs/proof-transport.adoc[ | Proof transport with explicit semantic soundness | **Novel formalisation** | `EpistemicTypes.ProofTransport` + +| Order-generic RapidNJ Q-criterion bound and skip warrants +| Transcription of a documented algorithm; no novelty theorem +| `EpistemicTypes.Applications.QCriterion` |=== == What remains intentionally unformalized @@ -164,6 +198,10 @@ This is a prototype, not a complete epistemic logic. The following are **intenti * Proof irrelevance or decidability * Global soundness of warrants * Monadic (`bind`) or comonadic (`extract`) structure for `E` +* A rational (ℚ) instance of the applications layer, and the rescaling + transport that would lift the integer certificate to rational input +* Cross-iteration reuse of a skip bound, and the row-insertion update that + maintains the scan invariants (`Applications.RapidNJSkip.WeakeningObligation`) == Build @@ -184,6 +222,7 @@ agda --no-libraries -i src src/EpistemicTypes/All.agda * link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known gaps * link:docs/continuity-foundations.adoc[Continuity foundations] — store coherence, retained information, bounds, and next obligations * link:docs/proof-transport.adoc[Proof transport] — semantic verification across boundaries +* link:docs/applications/rapidnj-q-criterion.adoc[Applications: the RapidNJ Q-criterion] — the bound, the skip warrant, the exact-arithmetic obligation == License diff --git a/docs/README.adoc b/docs/README.adoc index 9d6f89a..e8a5f34 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -23,6 +23,12 @@ authority. endofunctor (map only) and *not* a monad/comonad, and what "epistemically available at standpoint κ" is meant to capture. +| `docs/applications/rapidnj-q-criterion.adoc` +| The applications layer: the RapidNJ per-row Q-criterion bound, the skip + certificate's three invariants, the warrant/soundness chain through + `FactiveModality.reflect`, and the exact-arithmetic (ℚ) obligation stated + rather than assumed. + | `docs/proof-transport.adoc` | Focused walkthrough of `EpistemicTypes.ProofTransport`: how `transmit` downgrades a sender's `Proof` to a receiver's `Receipt`, how `verify` upgrades @@ -64,9 +70,19 @@ The core lives in `src/EpistemicTypes/`. `All.agda` checks `Base`, `Warrant`, publicly re-exported to avoid helper-name collisions. Every core module uses `--safe --without-K` and builtins only. Local checks use Agda 2.6.4.3. +The applications layer lives beside the core in `src/EpistemicTypes/Applications/`: +`OrderedGroup` (the arithmetic budget), `IntegerModel` (the discharged +instance), `SortedRow` (rows and invariants), `QCriterion` (the bound lemma), +`RapidNJSkip` (warrants, soundness, the factive modality), and +`RapidNJExamples` (the worked scan and the runtime status mirror). It is +checked by the same recursive gate as the core, and it is imported -- not +publicly re-exported -- by `All.agda`. See +link:applications/rapidnj-q-criterion.adoc[]. + == Notes * `Echo C y`, `BoundedEcho C measure budget y`, and `E κ A` have separate roles. -* `just check` runs the core proof graph and eleven semantic rejection fixtures. +* `just check` runs the proof graph (seventeen modules, including the + applications layer) and twelve semantic rejection fixtures. * `just check-canonical` separately checks correspondence against actual sibling Echo sources; it requires an explicit standard-library source path. diff --git a/docs/applications/rapidnj-q-criterion.adoc b/docs/applications/rapidnj-q-criterion.adoc new file mode 100644 index 0000000..c253eaf --- /dev/null +++ b/docs/applications/rapidnj-q-criterion.adoc @@ -0,0 +1,274 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Applications: the RapidNJ Q-criterion, formally +Jonathan D.A. Jewell (hyperpolymath) +v0.1.0, 2026-09-27: applications note 1 +:toc: preamble +:toc-title: Contents + +This note is the prose half of `src/EpistemicTypes/Applications/`. It states +what is formalized about RapidNJ's per-row Q-criterion bound, how a skipped +quadrant of the search space generates a *valid* warrant in the sense of +`EpistemicTypes.Warrant`, and exactly which rational-arithmetic obligations +remain stated-but-unproved. The Agda source is the authority; where this note +and a module disagree, the module is right. + +== The algorithm being explained + +Canonical neighbour-joining (Saitou and Nei 1987; Studier and Keppler 1988) +joins, at each of `r` iterations, the pair of clusters minimizing + + q(i,j) = (r - 2) * d(i,j) - t(i) - t(j), t(i) = sum_k d(i,k) + +with `r` the number of remaining clusters and `t` the row sums of the current +distance matrix. A naive implementation scans all `O(r^2)` pairs per +iteration, giving `Theta(r^3)` overall. + +RapidNJ (Simonsen, Mailund, Pedersen 2008) prunes that scan with two +structures beside the matrix `D`: a matrix `S` whose rows are the rows of `D` +sorted by increasing distance, and an index map `I` back into `D`, plus a +maximal row sum `t_max`. For a fixed row `i`, walking `S(i)` from small to +large `d(i,j)` and maintaining the smallest q-value seen so far (`q_min`), +one maintains the lower bound + + qBound(i) = (r - 2) * d(i,next) - t(i) - t_max, + +where `d(i,next)` is the smallest distance not yet examined in the row and +`t_max = max_k t(k)`. Because `r`, `t(i)` and `t_max` are constant during one +row scan and the `d` values are non-decreasing, `qBound` is non-decreasing +along the row. Hence the moment `qBound(i) >= q_min` no unexamined entry of +row `i` can improve on `q_min`, and the rest of the row -- the quadrant +`{ (i,j) : d(i,j) >= d(i,next) }` in the (index, distance) plane -- is skipped. +After the bounded scan of every row, the canonical minimum is guaranteed. +Wheeler's NINJA preprint states the rule in exactly this form and notes it is +"the approach of RapidNJ"; the ERapidNJ paper (2011) records the same +structure, with the improved heuristic replacing `t_max` by a tighter +per-row bound over the remaining rows. + +What is formalized here is that row rule, and only that: the bound, the +skipping, and the epistemic status of the resulting claim. Nothing in this +section is proved about NJ's correctness as a clustering method, about the +tree produced, or about the order in which joins happen. + +== What a skip must carry: three invariants + +The formal development makes the preconditions of the row rule into carried +proof objects rather than comments. A skip certificate is a triple: + +1. *Sorted-row invariant* -- the distance at the stop cursor is a lower bound + for every unexamined entry (`Row.AllDistAtLeast`). Without it, `d(i,next)` + is not a lower bound and the bound says nothing. +2. *Running-maximum invariant* -- every unexamined row sum is at most + `t_max` (`Row.AllRowSumAtMost`). Without it, `-t_max` is not a lower bound + on `-t(j)`. +3. *An accepted check* -- the executable comparison returns `true` for + `q_min <= qBound` (`Skip.CheckStatement`), through a `Checkable` + instance whose verdicts reflect the order (`decide-true`). + +The first two are why skipping is safe; the third is how a *run* knows it is +safe. The implementation maintains 1 and 2 when it inserts the new cluster's +row into `S` after a join; this development does not model that update, only +consumes the invariants. + +== The modules + +[cols="2,3", options="header"] +|=== +| Module | Contents + +| `Applications.OrderedGroup` +| The arithmetic budget: a carrier with `_⊕_`, `neg`, `zeroC`, `_≤_`, and + laws `≤-refl`, `≤-trans`, joint monotonicity `≤-⊕`, antitonicity `≤-neg`. + Derived: `_⊖_`, `scale` (Nat-indexed repeated addition), `scale-mono`. + +| `Applications.IntegerModel` +| The integers as difference pairs over `Nat`: ring-free group operations, + the cross-multiplied order `_≤ℤ_`, all four `OrderedGroup` laws, the group + instance `ℤ-group` (the non-vacuity witness), and `dec-≤ℤ`, a decision + procedure for the order. + +| `Applications.SortedRow` +| Rows as lists of `Entry` (column index, distance, row sum), the `All` + predicate, membership, the two invariants, row concatenation and the + membership decomposition `∈-append` that lets an examined prefix and a + skipped suffix compose. + +| `Applications.QCriterion` +| `Q` and `qBound` over an arbitrary `OrderedGroup`, the bound lemma + `qBound-≤-Q`, the row lemma `qBound-≤-suffix`, claim weakening + (`noBetter-weaken`), and the prefix/suffix composition `noBetter-append`. + +| `Applications.RapidNJSkip` +| The epistemic layer: `Checkable` (the exactness seam), `ScanState`, + `SkipEvidence`, the generated `skipWarrant` and `skipSoundWarrant`, the + factive modality `rapidKnowledge` whose `reflect` *is* `sound-epi`, the + belief-only modality `rapidBelief`, `no-receipt-reflection`, the theorems + `skip-generates-knowledge`, `skip-known`, `whole-row-known`, and the + declared-not-assumed `WeakeningObligation`. + +| `Applications.RapidNJExamples` +| `Checkable` for the integer model built from `dec-≤ℤ`; the refutation + `no-always-true` (an over-eager comparison cannot meet the obligation); a + worked four-taxon scan discharged by computation; and the `Status` mirror + of the runtime vocabulary (`Factive` / `Belief` / `Collapsed` / `SansFibre`). +|=== + +The load-bearing proof is `qBound-≤-Q`: + + qBound-≤-Q : (k : Nat) -> dnext ≤ d -> tj ≤ tmax + -> qBound k ti tmax dnext ≤ Q k ti tj d + +It is proved by adding the same tail to both scaled distances, replacing +`t(j)` by the larger `t_max` under `neg`, and chaining -- that is, using only +`≤-refl`, `≤-trans`, `≤-⊕`, `≤-neg` and `scale-mono` (induction on the +coefficient). No associativity, commutativity, distributivity, inverse or +unit law is used, and no multiplication or division of carrier elements +occurs anywhere in the development. + +== The mapping onto the epistemic core + +The question that motivates the module: how does a `FactiveModality` map onto +the Q-criterion bound, and how does skipping a quadrant *automatically* +generate a valid warrant? The answer is one line long, and it lives in +`RapidNJSkip.Skip`: + + FactiveModality.reflect == sound-epi == skip-sound + +`reflect : E κ A -> A` is instantiated by the soundness map of the generated +skip warrant, whose proof is the bound lemma. So the chain a run follows is + + run data (numbers, cursor, suffix, verdict) + -- skipWarrant ............-> Warrant κ "nothing skipped beats q(min)" + -- skip-sound (bound lemma) -> SoundWarrant κ (same claim) + -- reflect = sound-epi .....-> the claim itself + +and `skip-known` packages the whole chain as one theorem: given the two +invariants and an accepted check for a concrete `ScanState`, the claim holds +for every entry of the skipped suffix, with no soundness assumed anywhere. + +[cols="2,2,2", options="header"] +|=== +| Core notion | In this application | Runtime vocabulary (`EpistemicTypes.jl`) + +| `FactiveModality.reflect` +| `skip-sound`, proved by `qBound-≤-Q` from an accepted `Checkable` verdict +| `epi_status = :Factive` + +| `BeliefModality` (no `reflect`) +| the same run packaged as `Epi` (warrant + token, no soundness map) +| `epi_status = :Belief` + +| `Warrant.Evidence` +| the recorded numbers, cursor, suffix, invariants and verdict +| `Receipt(k, w, y, sig)` plus the raw run fields + +| `no-receipt-reflection` +| a token alone never yields the claim +| why `:Belief` must not be read as `:Factive` + +| evidence but no accepted check +| the gate is not passed, so no `SkipClaimAt` can be produced +| `epi_status = :Collapsed` + +| no warrant at all +| nothing was recorded for the row +| `epi_status = :SansFibre` +|=== + +`RapidNJExamples.Status` names those four statuses and +`skipStatus` reproduces `epi_status`'s decision order (verify the receipt, +then run the gates, then read the rank); `status-of-skip-is-factive` records +that a skip holding an accepted check is `:Factive`. The correspondence is +vocabulary-level on purpose: the runtime is Julia, this development is Agda, +and the shared claim is only that both sides use the same four readings of +evidence. + +== Exact arithmetic: the ℚ obligation, stated + +The user-facing constraint is that skipping must not violate the rational +constraints of the distances it is computed on. The development answers this +in three parts. + +*What the bound needs.* Only the ordered-group budget above. Any carrier with +an exact, monotone `+`, an antitone `-`, and a decidable order that *reflects* +it can run the whole pipeline. In particular no field, no division, and no +multiplication of two carrier elements is used: the coefficient `(r - 2)` is a +`Nat` applied by repeated addition (`scale`). + +*What is discharged.* The integers, in full: `IntegerModel.ℤ-group` proves +the four laws, `RapidNJExamples.ℤ-checkable` turns `dec-≤ℤ` into a +`Checkable`, and the worked scan in the same module is decided by +computation. So the integer case is not merely consistent -- it is running. + +*What is stated and not proved.* A rational instance. Two routes are honest, +and neither is claimed here: + +. *Common-denominator rescaling.* For a finite matrix of rationals choose a + positive integer `f` clearing all denominators. Scaling every distance by + `f` scales every row sum by `f`, hence scales both `Q` and `qBound` by `f`; + the comparison, and therefore every skip decision, is unchanged. The + transport needs scaling laws that the current `OrderedGroup` deliberately + does not assume (`scale f (x ⊕ y) ≡ scale f x ⊕ scale f y`, + `scale f (neg x) ≡ neg (scale f x)`, and the interchange + `scale k (scale f x) ≡ scale f (scale k x)`); each is provable for the + integer model from componentwise arithmetic, and none is derivable from the + record as it stands. Formalizing the rescaling theorem is the natural next + increment. +. *A rational carrier directly.* A numerator/denominator representation with + the cross-multiplied order satisfies the same interface; it owes the same + 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: +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. + +== What is proved, and what is not + +Proved (all machine-checked under `--safe --without-K`, no postulates): + +* `qBound-≤-Q`, `qBound-≤-suffix`, `noBetter-weaken`, `noBetter-append`; +* `skipWarrant` / `skipSoundWarrant` construction and `skip-known`, + `skip-generates-knowledge`, `whole-row-known`; +* `no-receipt-reflection`, so the belief reading is genuinely weaker; +* the integer instance: `ℤ-group`, `ℤ-checkable`, the worked scan, the status + mirror, and the refutation `no-always-true`. + +Not proved, and deliberately so: + +* that neighbour-joining (or RapidNJ) computes a correct tree, or that the + row scan finds the true minimum -- the row rule is conditional on the two + invariants and an accepted check; +* the row-insertion update that maintains the invariants across iterations; +* the rescaling transport, and any rational instance; +* the cross-iteration reuse of bounds (`Skip.WeakeningObligation`: declared, + unused, uninstantiated); +* anything about the tighter ERapidNJ/NINJA bounds, which replace `t_max` by + a per-row bound. + +No novelty is claimed. The formal content is a transcription of the +documented RapidNJ rule into an order-generic setting, plus the observation +that its soundness map is exactly the `reflect` of a `FactiveModality` and +that skipping yields a warrant rather than an assumption. + +== References + +* N. Saitou, M. Nei. The neighbor-joining method. _Mol. Biol. Evol._ 4(4), + 1987. +* J. A. Studier, K. J. Keppler. A note on the neighbor-joining algorithm of + Saitou and Nei. _Mol. Biol. Evol._ 5(6), 1988. +* M. Simonsen, T. Mailund, C. N. S. Pedersen. Rapid Neighbour-Joining. In + _Algorithms in Bioinformatics_ (WABI 2008), LNCS 5251, 113--122. + doi:10.1007/978-3-540-87361-7_10. +* M. Simonsen, T. Mailund, C. N. S. Pedersen. Inference of Large Phylogenies + using Neighbour-Joining (ERapidNJ). 2011. Available from the BIRC software + pages (birc.au.dk/software/rapidnj). +* T. J. Wheeler. Large-scale neighbor-joining with NINJA (preprint), + wheelerlab.org/software/ninja -- source of the quotable statement of the + bound `q_bound = (r - 2) * d_ij - t_i - t_max` and of its stopping rule. +* T. Mailund, C. N. S. Pedersen. QuickJoin -- fast neighbour-joining tree + reconstruction. _Bioinformatics_ 20, 2004. diff --git a/docs/ci-safety.adoc b/docs/ci-safety.adoc index ed51e87..d6e5f2f 100644 --- a/docs/ci-safety.adoc +++ b/docs/ci-safety.adoc @@ -10,8 +10,8 @@ The owner explicitly authorized maintaining these CI and merge safeguards on `Proof core and rejection controls` checks every file under `src/EpistemicTypes/`, including a file accidentally omitted from `All.agda`. It uses Agda 2.6.4.3 with `--safe --without-K --double-check ---ignore-interfaces -W error --no-libraries`. It also runs all eleven enumerated -false-claim controls. The rejection runner requires Agda's type-error exit code +--ignore-interfaces -W error --no-libraries`. It also runs all enumerated +false-claim controls (twelve at the time of writing). The rejection runner requires Agda's type-error exit code and the intended semantic diagnostic; import and environment failures do not pass. `Canonical Echo correspondence` imports the actual `echo-types` source pinned to diff --git a/docs/continuity-foundations.adoc b/docs/continuity-foundations.adoc index 4f6bad7..35a730b 100644 --- a/docs/continuity-foundations.adoc +++ b/docs/continuity-foundations.adoc @@ -146,10 +146,12 @@ agda --no-libraries --safe --without-K --ignore-interfaces -i src src/EpistemicT just check-canonical /path/to/echo-types /path/to/agda-stdlib/src ---- -The core and examples have been checked with Agda 2.6.4.3. `just check` covers -all eleven source modules and eleven semantic rejection fixtures: the four +The core, examples and applications layer have been checked with Agda 2.6.4.3. +`just check` covers every source module under `src/EpistemicTypes/` (seventeen +at the time of writing) and every semantic rejection fixture (twelve): the four proof-transport controls plus `StaleSample`, `FakeFreshness`, `ForkedHistory`, -`ForgedResidue`, `MismatchedSource`, `UnderstatedBound`, and `InventedMigration`. +`ForgedResidue`, `MismatchedSource`, `UnderstatedBound`, `InventedMigration`, and +`UncheckedSkip`. An unrelated import or tool failure fails the rejection gate. The optional canonical integration also checks successfully with the locally diff --git a/src/EpistemicTypes/All.agda b/src/EpistemicTypes/All.agda index 6280350..021ff97 100644 --- a/src/EpistemicTypes/All.agda +++ b/src/EpistemicTypes/All.agda @@ -12,6 +12,11 @@ open import EpistemicTypes.EchoBridge public -- re-exported. The module is still part of the build via this import. import EpistemicTypes.ReadConsistency import EpistemicTypes.ContinuityExamples +-- The applications layer is checked through this import and is deliberately +-- not publicly re-exported: its modules carry application-specific +-- vocabulary (row entries, scan invariants, a checkability record) that has +-- no business in the core namespace. See docs/applications/. +import EpistemicTypes.Applications.RapidNJExamples open import EpistemicTypes.SurrealBridge public open import EpistemicTypes.Examples public open import EpistemicTypes.ProofTransportExample public diff --git a/src/EpistemicTypes/Applications/IntegerModel.agda b/src/EpistemicTypes/Applications/IntegerModel.agda new file mode 100644 index 0000000..e4b14d9 --- /dev/null +++ b/src/EpistemicTypes/Applications/IntegerModel.agda @@ -0,0 +1,239 @@ +{-# OPTIONS --safe --without-K #-} + +-- Applications / IntegerModel +-- +-- A concrete model of `OrderedGroup`: the integers, represented as +-- difference pairs of naturals (mkℤ a b read as a - b). The point of this +-- module is non-vacuity. A specification that assumed an ordered group +-- without exhibiting one would prove nothing about the RapidNJ bound, so +-- the four laws of `OrderedGroup` are proved here for an exact model. +-- +-- Why integers rather than a developed ℚ here. The whole hypothesis budget +-- the Q-criterion proof consumes is order-compatibility of `+` and `neg` +-- (see `EpistemicTypes.Applications.OrderedGroup`); it never divides and +-- never multiplies two carrier elements. Clearing denominators in a +-- rational distance matrix is therefore invisible to the bound argument: +-- for a common positive denominator D, comparing q-values of a ℚ matrix is +-- the same comparison as for its integer rescaling by D, and scaling by the +-- coefficient (r - 2) commutes with that rescaling. The worked matrices in +-- `RapidNJExamples` are integer matrices for exactly this reason. +-- +-- The ℚ instance itself (numerator/denominator pairs with cross-multiplied +-- order) is deliberately NOT claimed here: it needs multiplication +-- monotonicity, which the difference-pair development below does not +-- provide. It is listed as an explicit obligation in +-- link:docs/applications/rapidnj-q-criterion.adoc[], not as a theorem. +-- +-- The order on naturals is reused from `EpistemicTypes.EchoBridge`, so the +-- resource grades there and the arithmetic order here are one relation. + +module EpistemicTypes.Applications.IntegerModel where + +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Nat using (Nat; zero; suc; _+_) + +-- The equality helpers the builtin module does not export. They are +-- defined here (rather than imported) because this development is built +-- with `--no-libraries`; the definitions are the standard ones. +sym : {A : Set} {x y : A} -> x ≡ y -> y ≡ x +sym refl = refl + +trans : {A : Set} {x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z +trans refl q = q + +cong : {A B : Set} (f : A -> B) {x y : A} -> x ≡ y -> f x ≡ f y +cong f refl = refl + +-- A local disjoint sum: a witness, or a proof that there is none. +infixr 1 _⊎_ +data _⊎_ (A B : Set) : Set where + inj₁ : A -> A ⊎ B + inj₂ : B -> A ⊎ B + +open import EpistemicTypes.EchoBridge using + (Impossible; _≤ℕ_; zero≤; suc≤; ≤ℕ-trans; ≤ℕ-plus) +open import EpistemicTypes.Applications.OrderedGroup + +-- ── Naturals ──────────────────────────────────────────────────────────────── + ++0 : (m : Nat) -> m + zero ≡ m ++0 zero = refl ++0 (suc m) = cong suc (+0 m) + ++suc : (m n : Nat) -> m + suc n ≡ suc (m + n) ++suc zero n = refl ++suc (suc m) n = cong suc (+suc m n) + ++-assoc : (a b c : Nat) -> (a + b) + c ≡ a + (b + c) ++-assoc zero b c = refl ++-assoc (suc a) b c = cong suc (+-assoc a b c) + ++-comm : (a b : Nat) -> a + b ≡ b + a ++-comm zero b = sym (+0 b) ++-comm (suc a) b = trans (cong suc (+-comm a b)) (sym (+suc b a)) + +≤ℕ-refl : (m : Nat) -> m ≤ℕ m +≤ℕ-refl zero = zero≤ +≤ℕ-refl (suc m) = suc≤ (≤ℕ-refl m) + +≤ℕ-pred : {m n : Nat} -> suc m ≤ℕ suc n -> m ≤ℕ n +≤ℕ-pred (suc≤ p) = p + +-- Transport an inequality along equalities of its two sides: the statement +-- is unchanged by regrouping its operands. +≤ℕ-cong : {m n m' n' : Nat} -> m ≡ m' -> n ≡ n' -> m ≤ℕ n -> m' ≤ℕ n' +≤ℕ-cong refl refl p = p + +-- Move an inequality right by a common summand. +≤ℕ-shift : {m n : Nat} (k : Nat) -> m ≤ℕ n -> m + k ≤ℕ n + k +≤ℕ-shift {m = zero} {n = n} k zero≤ = ≤ℕ-cong refl (+-comm k n) (≤ℕ-plus k n) +≤ℕ-shift {m = suc m} {n = suc n} k (suc≤ p) = suc≤ (≤ℕ-shift k p) + +-- Move an inequality left by a common summand. +≤ℕ-shift-left : (k : Nat) -> {m n : Nat} -> m ≤ℕ n -> k + m ≤ℕ k + n +≤ℕ-shift-left zero p = p +≤ℕ-shift-left (suc k) p = suc≤ (≤ℕ-shift-left k p) + +-- Inequality is compatible with addition in both arguments. +≤ℕ-add : {a b c d : Nat} -> a ≤ℕ b -> c ≤ℕ d -> a + c ≤ℕ b + d +≤ℕ-add {a} {b} {c} p q = ≤ℕ-trans (≤ℕ-shift c p) (≤ℕ-shift-left b q) + +-- A common right summand can be cancelled. This is the rule that turns +-- "add the same term to both sides" back into the original inequality. +≤ℕ-cancel : {m n : Nat} (k : Nat) -> m + k ≤ℕ n + k -> m ≤ℕ n +≤ℕ-cancel zero p = ≤ℕ-cong (+0 _) (+0 _) p +≤ℕ-cancel {m} {n} (suc k) p = + ≤ℕ-cancel k (≤ℕ-pred (≤ℕ-cong (+suc m k) (+suc n k) p)) + +-- Two four-term regroupings, proved once and reused by the group laws. +-- interleave-AD pairs the outer terms; interleave-AC pairs adjacent terms. +interleave-AC : (a b c d : Nat) -> (a + b) + (c + d) ≡ (a + c) + (b + d) +interleave-AC a b c d = + trans (+-assoc a b (c + d)) + (trans (cong (a +_) (sym (+-assoc b c d))) + (trans (cong (a +_) (cong (_+ d) (+-comm b c))) + (trans (cong (a +_) (+-assoc c b d)) + (sym (+-assoc a c (b + d)))))) + +-- The outer pairing follows from the adjacent one by commuting the middle +-- pair. +interleave-AD : (a b c d : Nat) -> (a + b) + (c + d) ≡ (a + d) + (c + b) +interleave-AD a b c d = + trans (interleave-AC a b c d) + (trans (cong ((a + c) +_) (+-comm b d)) + (interleave-AC a c d b)) + +-- ── Integers as difference pairs ──────────────────────────────────────────── + +record ℤ : Set where + constructor mkℤ + field + plus : Nat + minus : Nat + +-- Field projections, unqualified, so the arithmetic below reads as +-- arithmetic. +open ℤ + +_+ℤ_ : ℤ -> ℤ -> ℤ +mkℤ a b +ℤ mkℤ c d = mkℤ (a + c) (b + d) + +negℤ : ℤ -> ℤ +negℤ (mkℤ a b) = mkℤ b a + +zeroℤ : ℤ +zeroℤ = mkℤ zero zero + +-- a ⊖ b ≤ c ⊖ d iff a + d ≤ c + b, i.e. a - b ≤ c - d. +_≤ℤ_ : ℤ -> ℤ -> Set +x ≤ℤ y = (ℤ.plus x + ℤ.minus y) ≤ℕ (ℤ.plus y + ℤ.minus x) + +-- Congruence for addition, and the two projection laws that let a proof +-- rewrite `plus (x +ℤ y)` into its components. ++-cong : {a a' b b' : Nat} -> a ≡ a' -> b ≡ b' -> a + b ≡ a' + b' ++-cong refl refl = refl + +plus-+ℤ : (x y : ℤ) -> plus (x +ℤ y) ≡ plus x + plus y +plus-+ℤ (mkℤ a b) (mkℤ c d) = refl + +minus-+ℤ : (x y : ℤ) -> minus (x +ℤ y) ≡ minus x + minus y +minus-+ℤ (mkℤ a b) (mkℤ c d) = refl + +plus-negℤ : (x : ℤ) -> plus (negℤ x) ≡ minus x +plus-negℤ (mkℤ a b) = refl + +minus-negℤ : (x : ℤ) -> minus (negℤ x) ≡ plus x +minus-negℤ (mkℤ a b) = refl + +≤ℤ-refl : {x : ℤ} -> x ≤ℤ x +≤ℤ-refl {x} = ≤ℕ-refl (plus x + minus x) + +≤ℤ-trans : {x y z : ℤ} -> x ≤ℤ y -> y ≤ℤ z -> x ≤ℤ z +≤ℤ-trans {x} {y} {z} p q = + ≤ℕ-cancel (plus y + minus y) + (≤ℕ-cong (interleave-AD (plus x) (minus y) (plus y) (minus z)) + (trans (interleave-AD (plus y) (minus x) (plus z) (minus y)) + (+-comm (plus y + minus y) (plus z + minus x))) + (≤ℕ-add p q)) + +≤ℤ-⊕ : {x y u v : ℤ} -> x ≤ℤ y -> u ≤ℤ v -> (x +ℤ u) ≤ℤ (y +ℤ v) +≤ℤ-⊕ {x} {y} {u} {v} p q = + ≤ℕ-cong (sym (+-cong (plus-+ℤ x u) (minus-+ℤ y v))) + (sym (+-cong (plus-+ℤ y v) (minus-+ℤ x u))) + (≤ℕ-cong (interleave-AC (plus x) (minus y) (plus u) (minus v)) + (interleave-AC (plus y) (minus x) (plus v) (minus u)) + (≤ℕ-add p q)) + +≤ℤ-neg : {x y : ℤ} -> x ≤ℤ y -> negℤ y ≤ℤ negℤ x +≤ℤ-neg {x} {y} p = + ≤ℕ-cong + (trans (+-comm (plus x) (minus y)) + (sym (+-cong (plus-negℤ y) (minus-negℤ x)))) + (trans (+-comm (plus y) (minus x)) + (sym (+-cong (plus-negℤ x) (minus-negℤ y)))) + p + +-- The exact model. This is the witness that `OrderedGroup` is inhabited, +-- and therefore that the Q-criterion theorem below is not vacuous. +ℤ-group : OrderedGroup +ℤ-group = record + { Carrier = ℤ + ; _⊕_ = _+ℤ_ + ; neg = negℤ + ; zeroC = zeroℤ + ; _≤_ = _≤ℤ_ + ; ≤-refl = λ {x} -> ≤ℤ-refl {x} + ; ≤-trans = λ {x} {y} {z} -> ≤ℤ-trans {x} {y} {z} + ; ≤-⊕ = λ {x} {y} {u} {v} -> ≤ℤ-⊕ {x} {y} {u} {v} + ; ≤-neg = λ {x} {y} -> ≤ℤ-neg {x} {y} + } + +-- ── Numerals and decidable comparison ─────────────────────────────────────── + +-- Non-negative literals. +mk : Nat -> ℤ +mk n = mkℤ n zero + +-- Negative literals: `negM n` is -n. +negM : Nat -> ℤ +negM n = mkℤ zero n + +mk-+ℤ : (m n : Nat) -> mk m +ℤ mk n ≡ mk (m + n) +mk-+ℤ m n = refl + +mk-negℤ : (n : Nat) -> negℤ (mk n) ≡ negM n +mk-negℤ n = refl + +-- The comparison an implementation actually performs. A total decision +-- procedure is *not* part of `OrderedGroup` (the bound theorem does not +-- need one); it is needed only to turn the bound into a checkable +-- certificate, and its reflection lemma is where exactness is consumed. +dec-≤ℕ : (m n : Nat) -> m ≤ℕ n ⊎ (m ≤ℕ n -> Impossible) +dec-≤ℕ zero n = inj₁ zero≤ +dec-≤ℕ (suc m) zero = inj₂ (λ ()) +dec-≤ℕ (suc m) (suc n) with dec-≤ℕ m n +... | inj₁ p = inj₁ (suc≤ p) +... | inj₂ f = inj₂ (λ { (suc≤ q) -> f q }) + +dec-≤ℤ : (x y : ℤ) -> x ≤ℤ y ⊎ (x ≤ℤ y -> Impossible) +dec-≤ℤ x y = dec-≤ℕ (plus x + minus y) (plus y + minus x) diff --git a/src/EpistemicTypes/Applications/OrderedGroup.agda b/src/EpistemicTypes/Applications/OrderedGroup.agda new file mode 100644 index 0000000..374557b --- /dev/null +++ b/src/EpistemicTypes/Applications/OrderedGroup.agda @@ -0,0 +1,112 @@ +{-# OPTIONS --safe --without-K #-} + +-- Applications / OrderedGroup +-- +-- The exact-arithmetic contract consumed by the RapidNJ Q-criterion proof. +-- +-- RapidNJ (Simonsen, Mailund & Pedersen 2008) prunes its search for the +-- minimum q-value with the row lower bound +-- +-- q_bound = (r - 2) * d(i, next) - t(i) - t(max) +-- +-- where r is the number of remaining clusters, t(i) is the i-th row sum of +-- the distance matrix, t(max) is the largest row sum still under +-- consideration, and d(i, next) is the smallest distance not yet examined +-- in the sorted row S(i). The bound is only a bound if the arithmetic is +-- exact: every inequality manipulation used below must be order-monotone. +-- +-- This record states the *whole* assumption budget of that argument. It is +-- deliberately weaker than "field" or even "ring": the Q-criterion proof +-- never multiplies two carrier elements, never divides, and never needs +-- associativity, commutativity or distributivity, because each step in the +-- proof adds the *syntactically identical* term to both sides. What it does +-- need is that `_+_` and `neg` are monotone for `_≤_`, and that `_≤_` is +-- transitive. Multiplication by the coefficient (r - 2) is definable as +-- repeated addition (`scale` below), so non-negativity of that coefficient +-- is a *typing* fact (it is a Nat), not an extra law. +-- +-- Consequences that matter for the applications section: +-- +-- * 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 +-- 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. +-- +-- `zeroC` is present so that a zero-length scaling exists. No identity law +-- for it is assumed, and none is consumed by any proof in this development. + +module EpistemicTypes.Applications.OrderedGroup where + +open import Agda.Builtin.Nat using (Nat; zero; suc) + +record OrderedGroup : Set₁ where + infixl 6 _⊕_ + infix 4 _≤_ + field + Carrier : Set + + _⊕_ : Carrier -> Carrier -> Carrier + neg : Carrier -> Carrier + zeroC : Carrier + + _≤_ : Carrier -> Carrier -> Set + + -- Reflexivity and transitivity of the order. + ≤-refl : {x : Carrier} -> x ≤ x + ≤-trans : {x y z : Carrier} -> x ≤ y -> y ≤ z -> x ≤ z + + -- Addition is monotone in both arguments simultaneously. The two + -- one-sided rules used by the proof are derived below, so this is the + -- only addition law assumed. + ≤-⊕ : {x y u v : Carrier} -> x ≤ y -> u ≤ v -> x ⊕ u ≤ y ⊕ v + + -- Negation is antitone. This is the only rule that lets the proof + -- replace an upper bound (t(max)) by an entry's own row sum (t(j)). + ≤-neg : {x y : Carrier} -> x ≤ y -> neg y ≤ neg x + +-- Derived rules and the coefficient scaling. Nothing here is assumed. +module Laws (G : OrderedGroup) where + open OrderedGroup G + + -- Addition monotone on the right, used to move a fixed summand across. + ≤-⊕-right : {x y : Carrier} (z : Carrier) -> x ≤ y -> x ⊕ z ≤ y ⊕ z + ≤-⊕-right z p = ≤-⊕ p ≤-refl + + -- Addition monotone on the left, the mirror rule. + ≤-⊕-left : (z : Carrier) {x y : Carrier} -> x ≤ y -> z ⊕ x ≤ z ⊕ y + ≤-⊕-left z p = ≤-⊕ ≤-refl p + + -- x - y, i.e. x + (-y). Subtraction is notation here, not structure: + -- no inverse law is assumed or needed. + _⊖_ : Carrier -> Carrier -> Carrier + x ⊖ y = x ⊕ neg y + + ≤-⊖-right : {x y : Carrier} (z : Carrier) -> x ≤ y -> x ⊖ z ≤ y ⊖ z + ≤-⊖-right z p = ≤-⊕-right (neg z) p + + -- The "slide an upper bound past a subtraction" rule. + ≤-⊖-anti : {x y z : Carrier} -> x ≤ y -> z ⊖ y ≤ z ⊖ x + ≤-⊖-anti {z = z} p = ≤-⊕-left z (≤-neg p) + + -- Repeated addition: the coefficient (r - 2) is applied as a Nat, so it + -- cannot be negative and needs no sign side condition. + scale : Nat -> Carrier -> Carrier + scale zero x = zeroC + scale (suc k) x = scale k x ⊕ x + + -- Non-negative scaling is monotone, by induction on the coefficient. + -- This is the only place where the coefficient enters the bound proof. + scale-mono : {x y : Carrier} (k : Nat) -> x ≤ y -> scale k x ≤ scale k y + scale-mono zero p = ≤-refl + scale-mono (suc k) p = ≤-⊕ (scale-mono k p) p + + -- Combining a certificate with a slack element. A certificate that only + -- establishes `q_bound ⊕ ε ≤ q₀` proves a strictly weaker claim than one + -- establishing `q_bound ≤ q₀`; see `RapidNJSkip.noBetter-weaken`, which + -- makes that weakness explicit instead of hiding it. + ≤-with-slack : {a b c : Carrier} -> a ≤ b -> b ≤ c -> a ≤ c + ≤-with-slack = ≤-trans diff --git a/src/EpistemicTypes/Applications/QCriterion.agda b/src/EpistemicTypes/Applications/QCriterion.agda new file mode 100644 index 0000000..5da05d7 --- /dev/null +++ b/src/EpistemicTypes/Applications/QCriterion.agda @@ -0,0 +1,113 @@ +{-# OPTIONS --safe --without-K #-} + +-- Applications / QCriterion +-- +-- The mathematical core of the RapidNJ quadrant skip, stated over an +-- arbitrary exact `OrderedGroup`: +-- +-- qBound(k, t(i), t(max), d(i,next)) +-- = (r - 2) * d(i,next) - t(i) - t(max) (k = r - 2) +-- Q(k, t(i), t(j), d(i,j)) +-- = (r - 2) * d(i,j) - t(i) - t(j) +-- +-- and the row lemma: if the stop cursor's distance is no greater than any +-- skipped distance, and t(max) bounds every skipped row sum, then the bound +-- at the cursor is below every skipped q-value. That is precisely the +-- statement "the unvisited part of the row cannot improve q(min)". +-- +-- The bound theorem (`qBound-≤-Q`) is the load-bearing part. It uses only +-- monotonicity of addition, antitonicity of negation, and transitivity of +-- the order -- no associativity, commutativity, or distributivity of the +-- carrier. This is why the applications section can work over the +-- difference-pair model of the integers without first developing ℚ: see the +-- header of `EpistemicTypes.Applications.IntegerModel`. + +module EpistemicTypes.Applications.QCriterion where + +open import Agda.Builtin.List using (List) +open import Agda.Builtin.Nat using (Nat) + +open import EpistemicTypes.Applications.OrderedGroup +open import EpistemicTypes.Applications.IntegerModel using (_⊎_; inj₁; inj₂) +import EpistemicTypes.Applications.SortedRow as SortedRow + +-- The criterion, parameterised by the exact arithmetic it reasons about. +module Criterion (G : OrderedGroup) where + open OrderedGroup G + open Laws G + open SortedRow.Row G + + -- The numbers a scan step carries, exactly as a log line would record + -- them. + record Numbers : Set where + constructor numbers + field + coefficient : Nat -- r - 2, as a natural number + row-sum-i : Carrier -- t(i) + row-sum-max : Carrier -- t(max), the running maximum + incumbent : Carrier -- the smallest q-value seen so far + + -- The Neighbour-Joining optimality criterion. + Q : Nat -> Carrier -> Carrier -> Carrier -> Carrier + Q k ti tj d = ((scale k d) ⊕ neg ti) ⊕ neg tj + + -- The RapidNJ row lower bound at the stop cursor. + qBound : Nat -> Carrier -> Carrier -> Carrier -> Carrier + qBound k ti tmax dnext = ((scale k dnext) ⊕ neg ti) ⊕ neg tmax + + -- The bound really is below every q-value of a skipped entry. Note the + -- shape of the proof: add the same term on the right (monotonicity), + -- replace t(j) by the larger t(max) (antitonicity under negation), and + -- chain. No ring identity is used, so no ring axiom is needed. + qBound-≤-Q : (k : Nat) {ti tmax tj dnext d : Carrier} -> + dnext ≤ d -> tj ≤ tmax -> qBound k ti tmax dnext ≤ Q k ti tj d + qBound-≤-Q k {ti} {tmax} {tj} {dnext} {d} dnext≤d tj≤tmax = + ≤-trans inside-≤bound (≤-⊕ ≤-refl (≤-neg tj≤tmax)) + where + -- Compare the two scaled distances with the same tails, then hang + -- t(max) and t(j) off the right in turn. + first : (scale k dnext) ⊕ neg ti ≤ (scale k d) ⊕ neg ti + first = ≤-⊕ (scale-mono k dnext≤d) ≤-refl + + inside-≤bound : ((scale k dnext) ⊕ neg ti) ⊕ neg tmax ≤ + ((scale k d) ⊕ neg ti) ⊕ neg tmax + inside-≤bound = ≤-⊕ first ≤-refl + + -- The claim a skip certifies: nothing in the skipped suffix beats the + -- incumbent. + SkipClaim : (k : Nat) (ti q₀ : Carrier) -> List Entry -> Set + SkipClaim k ti q₀ es = + (e : Entry) -> e ∈E es -> q₀ ≤ Q k ti (Entry.rowSum e) (Entry.dist e) + + -- Row-level soundness: invariants plus an accepted check entail the + -- claim. + qBound-≤-suffix : + {k : Nat} {ti tmax q₀ : Carrier} {cursor : Entry} {suffix : List Entry} -> + AllDistAtLeast (Entry.dist cursor) suffix -> + AllRowSumAtMost tmax suffix -> + q₀ ≤ qBound k ti tmax (Entry.dist cursor) -> + SkipClaim k ti q₀ suffix + qBound-≤-suffix {k = k} {ti = ti} {tmax = tmax} {q₀ = q₀} {cursor = cursor} + ordered maximal accepted e i = + ≤-trans accepted + (qBound-≤-Q k + (∈-All (λ x -> Entry.dist cursor ≤ Entry.dist x) ordered e i) + (∈-All (λ x -> Entry.rowSum x ≤ tmax) maximal e i)) + + -- Lowering the incumbent weakens the claim. This is the lemma that makes + -- an explicit slack visible instead of hiding it. + noBetter-weaken : {k : Nat} {ti q1 q₀ : Carrier} {es : List Entry} -> + q1 ≤ q₀ -> SkipClaim k ti q₀ es -> SkipClaim k ti q1 es + noBetter-weaken {k} {ti} q1≤q₀ claim e i = ≤-trans q1≤q₀ (claim e i) + + -- Examined prefix plus certified suffix covers the whole row. A quadrant + -- skip composes back into a whole-row guarantee through this lemma. + noBetter-append : + {k : Nat} {ti q₀ : Carrier} {pre suf : List Entry} -> + ((e : Entry) -> e ∈E pre -> q₀ ≤ Q k ti (Entry.rowSum e) (Entry.dist e)) -> + SkipClaim k ti q₀ suf -> + (e : Entry) -> e ∈E (pre ++ suf) -> q₀ ≤ Q k ti (Entry.rowSum e) (Entry.dist e) + noBetter-append {pre = pre} {suf = suf} scanned skipped e i + with ∈-append {e = e} {xs = pre} {ys = suf} i + ... | inj₁ p = scanned e p + ... | inj₂ q = skipped e q diff --git a/src/EpistemicTypes/Applications/RapidNJExamples.agda b/src/EpistemicTypes/Applications/RapidNJExamples.agda new file mode 100644 index 0000000..3f93b49 --- /dev/null +++ b/src/EpistemicTypes/Applications/RapidNJExamples.agda @@ -0,0 +1,166 @@ +{-# OPTIONS --safe --without-K #-} + +-- Applications / RapidNJExamples +-- +-- The integer model of the applications layer, made concrete: +-- +-- * a `Checkable` instance for ℤ, built from the decidable order +-- `IntegerModel.dec-≤ℤ`, so the skip pipeline can actually be run; +-- * the refutation that shows why an unsound comparison cannot be +-- installed (the rounding failure mode); +-- * a worked four-taxon scan: numbers, stop cursor, sorted suffix, an +-- accepted check, and the claim that `skip-known` *computes* for it; +-- * the status mirror of the runtime vocabulary used by +-- `EpistemicTypes.jl` (`epi_status ∈ {Factive, Belief, Collapsed, SansFibre}`). +-- +-- Nothing here is assumed: every fact is discharged by computation on +-- literals, which is what makes the integers a non-vacuous witness for the +-- abstract bound theorem. + +module EpistemicTypes.Applications.RapidNJExamples where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Nat using (Nat; zero; suc; _+_) +open import Agda.Builtin.Sigma using (Σ; _,_) + +open import EpistemicTypes.EchoBridge using (Impossible; _≤ℕ_; zero≤; suc≤; ≤ℕ-plus) +open import EpistemicTypes.Applications.OrderedGroup +open import EpistemicTypes.Applications.IntegerModel using + (ℤ; mk; mkℤ; negM; zeroℤ; negℤ; _+ℤ_; _≤ℤ_; _⊎_; inj₁; inj₂; + dec-≤ℤ; ≤ℕ-refl; ℤ-group) +open import EpistemicTypes.Applications.SortedRow +open import EpistemicTypes.Applications.QCriterion +open import EpistemicTypes.Applications.RapidNJSkip + +module Rapid = Skip ℤ-group +module Rowℤ = EpistemicTypes.Applications.SortedRow.Row ℤ-group +module Crℤ = + EpistemicTypes.Applications.QCriterion.Criterion ℤ-group + +open Rapid +open Rowℤ +open Crℤ + +-- ── the executable comparison ────────────────────────────────────────────── + +-- The decision carried together with its witness. Packing both in one +-- `Σ` is what lets the record below be defined without `inspect`: the +-- `false` branch simply has no witness to give. +decide-ℤ : (x y : ℤ) -> Σ Bool (λ b -> b ≡ true -> x ≤ℤ y) +decide-ℤ x y with dec-≤ℤ x y +... | inj₁ p = true , (λ _ -> p) +... | inj₂ f = false , (λ ()) + +ℤ-decide : (x y : ℤ) -> Bool +ℤ-decide x y = Σ.fst (decide-ℤ x y) + +ℤ-decide-true : {x y : ℤ} -> ℤ-decide x y ≡ true -> x ≤ℤ y +ℤ-decide-true {x} {y} = Σ.snd (decide-ℤ x y) + +-- The seam, discharged for the integer model. +ℤ-checkable : Checkable +ℤ-checkable = record + { decide = ℤ-decide + ; decide-true = λ {x} {y} -> ℤ-decide-true {x} {y} + } + +-- ── why an inexact comparison cannot be installed ────────────────────────── + +-- `suc m ≤ℕ zero` has no inhabitant; the coverage checker sees this +-- without any arithmetic. +suc≰zero : (m : Nat) -> suc m ≤ℕ zero -> Impossible +suc≰zero m () + +-- 1 ≤ 0 is refutable in the integer model: the cross-multiplied form +-- normalises to `suc zero ≤ℕ zero`, so the argument is already an +-- impossible pattern. +not-le-ten : mk (suc zero) ≤ℤ mk zero -> Impossible +not-le-ten p = suc≰zero zero p + +-- A comparison that answers `true` too often -- a rounding mode that loses +-- the negative verdict, or a default-accept fast path -- cannot meet the +-- `Checkable` obligation, because its reflection law would prove that +-- every integer is below every other. +no-always-true : ((x y : ℤ) -> x ≤ℤ y) -> Impossible +no-always-true all-le = not-le-ten (all-le (mk (suc zero)) (mk zero)) + +-- ── a worked scan ───────────────────────────────────────────────────────── + +-- Literal inequality proofs. `≤ℤ` on `mk` literals normalises to `≤ℕ` on +-- the corresponding naturals, so these are just successor chains. +≤ℤ-5-7 : mk 5 ≤ℤ mk 7 +≤ℤ-5-7 = ≤ℕ-plus 5 2 + +≤ℤ-5-9 : mk 5 ≤ℤ mk 9 +≤ℤ-5-9 = ≤ℕ-plus 5 4 + +≤ℤ-2-2 : mk 2 ≤ℤ mk 2 +≤ℤ-2-2 = ≤ℕ-refl 2 + +≤ℤ-1-2 : mk 1 ≤ℤ mk 2 +≤ℤ-1-2 = ≤ℕ-plus 1 1 + +-- Four remaining clusters (r = 4, so the coefficient is r - 2 = 2); row +-- sum t(i) = 1; running maximum t(max) = 2; the smallest unexamined +-- distance in row i is 5; the incumbent is q(min) = 0. +-- +-- qBound = (r - 2)·5 - 1 - 2 = 10 - 3 = 7 ≥ 0 = q(min) +-- +-- so the bound cannot be improved by anything further down the row. +example-suffix : List Entry +example-suffix = entry 3 (mk 7) (mk 2) ∷ entry 4 (mk 9) (mk 1) ∷ [] + +example-state : ScanState +example-state = scanning (numbers 2 (mk 1) (mk 2) (mk 0)) + (entry 2 (mk 5) (mk 1)) + example-suffix + +-- The invariants and the accepted check. The check witnesses +-- `7 ≥ 0` by computation (`decide-ℤ` normalises to `true`). +example-evidence : SkipEvidence ℤ-checkable example-state +example-evidence = + allCons ≤ℤ-5-7 (allCons ≤ℤ-5-9 allNil) + , allCons ≤ℤ-2-2 (allCons ≤ℤ-1-2 allNil) + , refl + +-- The claim the run generates, for every entry of the skipped suffix. +example-claim : (e : Entry) -> e ∈E example-suffix -> + mk 0 ≤ℤ Q 2 (mk 1) (Entry.rowSum e) (Entry.dist e) +example-claim = + skip-known Standpoint pruned ℤ-checkable example-state example-evidence + +-- Spot check: the first skipped entry, to which the bound was compared. +-- Its q-value is (2·7 - 1 - 2) = 11, comfortably above the incumbent. +example-spot : mk 0 ≤ℤ Q 2 (mk 1) (mk 2) (mk 7) +example-spot = example-claim (entry 3 (mk 7) (mk 2)) here + +-- ── the status mirror ───────────────────────────────────────────────────── + +-- The runtime's `epi_status` vocabulary, named exactly as +-- `EpistemicTypes.jl` spells it (`src/core/Epistemic.jl`). +data Status : Set where + factive : Status -- a verified receipt whose gates were passed + belief : Status -- a receipt without a soundness map + collapsed : Status -- a verified receipt whose gates were not passed + sans-fibre : Status -- no verified receipt at all + +-- `epi_status`: verify the receipt, then run the gates, then read the rank. +skipStatus : (receiptVerified gatesAccepted : Bool) -> Status +skipStatus false _ = sans-fibre +skipStatus true false = collapsed +skipStatus true true = factive + +-- Holding the evidence *is* verifying the receipt; holding the accepted +-- check *is* passing the gate. Hence: +status-of-skip : {C : Checkable} {s : ScanState} -> SkipEvidence C s -> Status +status-of-skip ev = skipStatus true true + +-- A check that was accepted by an exact comparison is `:Factive`, not +-- `:Belief` -- and `RapidNJSkip.no-receipt-reflection` shows why the +-- evidence alone would have been only `:Belief`: a token does not imply +-- the claim. +status-of-skip-is-factive : {C : Checkable} {s : ScanState} + (ev : SkipEvidence C s) -> status-of-skip {C} {s} ev ≡ factive +status-of-skip-is-factive ev = refl diff --git a/src/EpistemicTypes/Applications/RapidNJSkip.agda b/src/EpistemicTypes/Applications/RapidNJSkip.agda new file mode 100644 index 0000000..17e7921 --- /dev/null +++ b/src/EpistemicTypes/Applications/RapidNJSkip.agda @@ -0,0 +1,291 @@ +{-# OPTIONS --safe --without-K #-} + +-- Applications / RapidNJSkip +-- +-- The epistemic reading of the RapidNJ quadrant skip. This module is the +-- answer to the question "how does a `FactiveModality` map onto the +-- Q-criterion bound, and how does skipping a quadrant generate a *valid* +-- warrant?" +-- +-- The mapping is one line long: `FactiveModality.reflect` for the RapidNJ +-- frame *is* the soundness map of the skip warrant, whose proof is the +-- Q-criterion bound lemma `QCriterion.Criterion.qBound-≤-Q`. Concretely, +-- the chain is +-- +-- run data (numbers, cursor, sorted suffix, accepted check) +-- --(skipWarrant)--> Warrant κ "nothing skipped beats the incumbent" +-- --(skip-sound, the bound lemma)--> SoundWarrant κ (same claim) +-- --(sound-epi = FactiveModality.reflect)--> the claim itself +-- +-- Nothing about soundness is assumed: the warrant is *generated* from the +-- run, the check must be accepted by a `Checkable` instance, and the only +-- 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 +-- link:docs/applications/rapidnj-q-criterion.adoc[]). +-- +-- The same run, held without a soundness map, is belief: `Epi` packages a +-- warrant with a token and `no-receipt-reflection` shows that a token alone +-- is never the claim. +-- +-- Universe note. A warrant is a *type of evidence*, so a record packaging +-- one sits one universe above its claim. The modalities below are +-- therefore instantiated at `lsuc lzero`: claims enter through `Lift₁`, +-- and `lower` takes the reflected claim back down. This is the same +-- universe bookkeeping the core uses for `Warrant` and `Epi`; it is not an +-- extra assumption. + +module EpistemicTypes.Applications.RapidNJSkip where + +open import Agda.Builtin.Bool using (Bool; true) +open import Agda.Builtin.Equality using (_≡_) +open import Agda.Builtin.List using (List) +open import Agda.Builtin.Sigma using (Σ; _,_) +open import Agda.Primitive using (Level; lzero; lsuc) + +open import EpistemicTypes.Base +open import EpistemicTypes.Warrant +open import EpistemicTypes.EchoBridge using (Impossible) +open import EpistemicTypes.Applications.OrderedGroup +import EpistemicTypes.Applications.SortedRow as SortedRow +import EpistemicTypes.Applications.QCriterion as QCriterion + +-- A claim carried one universe up, so that a modality at `lsuc lzero` can +-- take it as an argument. +record Lift₁ (A : Set) : Set₁ where + constructor lift + field + lower : A + +-- The skip layer, parameterised by the exact arithmetic it reasons about. +module Skip (G : OrderedGroup) where + open OrderedGroup G + open Laws G + open SortedRow.Row G + open QCriterion.Criterion G + + -- ── the obligation an executable implementation must meet ──────────────── + + -- 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. + record Checkable : Set₁ where + field + decide : (x y : Carrier) -> Bool + decide-true : {x y : Carrier} -> decide x y ≡ true -> x ≤ y + + -- ── the scan state, as data ───────────────────────────────────────────── + + -- Exactly the line a logger would record for a bounded row scan: the + -- numbers, the stop cursor, and the suffix that was not looked at. + record ScanState : Set where + constructor scanning + field + run : Numbers + cursor : Entry + suffix : List Entry + + -- The check the run performs: the incumbent is at most the bound. In + -- RapidNJ terms: "q(min) ≤ q(bound), so stop scanning this row". + -- + -- Stated as a *type* with a plain body rather than as a pattern-matching + -- function: a matching definition would not unfold on a variable state, + -- and the evidence type below must be syntactically the conclusion of + -- `Checkable.decide-true`. + CheckStatement : (C : Checkable) (s : ScanState) -> Set + CheckStatement C s = + Checkable.decide C (Numbers.incumbent (ScanState.run s)) + (qBound (Numbers.coefficient (ScanState.run s)) + (Numbers.row-sum-i (ScanState.run s)) + (Numbers.row-sum-max (ScanState.run s)) + (Entry.dist (ScanState.cursor s))) ≡ true + + -- The claim a skip carries: no entry of the skipped suffix beats the + -- incumbent, in the same units as the bound. + RowClaim : (s : ScanState) (es : List Entry) -> Set + RowClaim s es = (e : Entry) -> e ∈E es -> + Numbers.incumbent (ScanState.run s) ≤ + Q (Numbers.coefficient (ScanState.run s)) + (Numbers.row-sum-i (ScanState.run s)) + (Entry.rowSum e) (Entry.dist e) + + SkipClaimAt : (s : ScanState) -> Set + SkipClaimAt s = RowClaim s (ScanState.suffix s) + + -- The evidence a skipper holds: the sorted-row invariant, the + -- running-maximum invariant, and an accepted check. Holding this is what + -- it means to have skipped the quadrant. + SkipEvidence : (C : Checkable) (s : ScanState) -> Set + SkipEvidence C s = + Σ (AllDistAtLeast (Entry.dist (ScanState.cursor s)) (ScanState.suffix s)) + (λ _ → Σ (AllRowSumAtMost (Numbers.row-sum-max (ScanState.run s)) + (ScanState.suffix s)) + (λ _ → CheckStatement C s)) + + -- ── warrant generation ────────────────────────────────────────────────── + + -- The warrant is *computed* from the run. Its type of evidence is the + -- skipper's evidence type; no soundness is asserted here. + skipWarrant : (K : Set) (κ : K) (C : Checkable) (s : ScanState) -> + Warrant {wℓ = lzero} K κ (SkipClaimAt s) + Warrant.Evidence (skipWarrant K κ C s) = SkipEvidence C s + + -- Soundness of the generated warrant: the accepted check, routed through + -- the Q-criterion bound lemma, is the claim. + skip-sound : (C : Checkable) (s : ScanState) -> + SkipEvidence C s -> SkipClaimAt s + -- The implicit arguments are supplied explicitly: the coefficient sits + -- under `scale`, which is a defined function, so it cannot be recovered by + -- unification. Naming the numbers is also what a log line does. + skip-sound C s (ordered , maximal , accepted) = + qBound-≤-suffix {k = Numbers.coefficient (ScanState.run s)} + {ti = Numbers.row-sum-i (ScanState.run s)} + {tmax = Numbers.row-sum-max (ScanState.run s)} + {q₀ = Numbers.incumbent (ScanState.run s)} + {cursor = ScanState.cursor s} + ordered maximal (Checkable.decide-true C accepted) + + skipSoundWarrant : (K : Set) (κ : K) (C : Checkable) (s : ScanState) -> + SoundWarrant {wℓ = lzero} K κ (SkipClaimAt s) + SoundWarrant.warrant (skipSoundWarrant K κ C s) = skipWarrant K κ C s + SoundWarrant.sound (skipSoundWarrant K κ C s) = skip-sound C s + + -- ── the factive layer ─────────────────────────────────────────────────── + + -- A warrant whose evidence type is fixed by the caller. This is how the + -- modality below re-uses an existing evidence type under a new claim. + warrantOn : {ℓ : Level} {K : Set} (κ : K) (A : Set ℓ) (E : Set) -> + Warrant {wℓ = lzero} K κ A + Warrant.Evidence (warrantOn κ A E) = E + + -- Knowledge at a standpoint: a sound warrant *and* a token of its + -- evidence. The projection is the soundness map, not the token. + Knowledge : (K : Set) (κ : K) (A : Set₁) -> Set₁ + Knowledge K κ A = Σ (SoundWarrant {ℓ = lsuc lzero} {wℓ = lzero} K κ A) + (λ sw → Warrant.Evidence (SoundWarrant.warrant sw)) + + sound-map : {K : Set} {κ : K} {A B : Set₁} (f : A -> B) -> + SoundWarrant {ℓ = lsuc lzero} {wℓ = lzero} K κ A -> + SoundWarrant {ℓ = lsuc lzero} {wℓ = lzero} K κ B + SoundWarrant.warrant (sound-map {κ = κ} f sw) = + warrantOn κ _ (Warrant.Evidence (SoundWarrant.warrant sw)) + SoundWarrant.sound (sound-map f sw) e = f (SoundWarrant.sound sw e) + + -- The modality: `map` rewrites the soundness map and keeps the evidence. + knowledgeModality : (K : Set) -> Modality K (lsuc lzero) + Modality.E (knowledgeModality K) κ A = Knowledge K κ A + Modality.map (knowledgeModality K) f (sw , e) = (sound-map f sw , e) + + -- The mapping that answers the question: `reflect` *is* the soundness map + -- of the generated skip warrant. + rapidKnowledge : (K : Set) -> FactiveModality K (lsuc lzero) + FactiveModality.modality (rapidKnowledge K) = knowledgeModality K + FactiveModality.reflect (rapidKnowledge K) (sw , e) = sound-epi sw e + + -- ── the theorems ──────────────────────────────────────────────────────── + + -- The same warrant, its soundness map delivering the lifted claim, which + -- is the shape the modality at `lsuc lzero` consumes. + liftedSoundWarrant : (K : Set) (κ : K) (C : Checkable) (s : ScanState) -> + SoundWarrant {ℓ = lsuc lzero} {wℓ = lzero} K κ (Lift₁ (SkipClaimAt s)) + SoundWarrant.warrant (liftedSoundWarrant K κ C s) = + warrantOn κ (Lift₁ (SkipClaimAt s)) (SkipEvidence C s) + SoundWarrant.sound (liftedSoundWarrant K κ C s) e = lift (skip-sound C s e) + + -- Skipping a quadrant, with a run recorded as evidence, yields knowledge + -- of the claim (at the lifted universe). + skip-generates-knowledge : (K : Set) (κ : K) (C : Checkable) + (s : ScanState) -> SkipEvidence C s -> Knowledge K κ (Lift₁ (SkipClaimAt s)) + skip-generates-knowledge K κ C s ev = (liftedSoundWarrant K κ C s , ev) + + -- Reflecting it gives the claim itself. This is the theorem the pipeline + -- consumes: a checked bound, not a trusted one. + skip-known : (K : Set) (κ : K) (C : Checkable) (s : ScanState) -> + SkipEvidence C s -> SkipClaimAt s + skip-known K κ C s ev = + Lift₁.lower (FactiveModality.reflect (rapidKnowledge K) + (skip-generates-knowledge K κ C s ev)) + + -- The examined prefix (checked by the scanner) and the skipped suffix + -- (certified by the generated warrant) cover the whole row: the skip + -- composes back into a whole-row guarantee. + whole-row-known : (K : Set) (κ : K) (C : Checkable) (s : ScanState) + (pre : List Entry) -> + ((e : Entry) -> e ∈E pre -> Numbers.incumbent (ScanState.run s) ≤ + Q (Numbers.coefficient (ScanState.run s)) + (Numbers.row-sum-i (ScanState.run s)) (Entry.rowSum e) (Entry.dist e)) -> + SkipEvidence C s -> + (e : Entry) -> e ∈E (pre ++ ScanState.suffix s) -> + Numbers.incumbent (ScanState.run s) ≤ + Q (Numbers.coefficient (ScanState.run s)) + (Numbers.row-sum-i (ScanState.run s)) (Entry.rowSum e) (Entry.dist e) + whole-row-known K κ C s pre scanned ev = + noBetter-append {k = Numbers.coefficient (ScanState.run s)} + {ti = Numbers.row-sum-i (ScanState.run s)} + {q₀ = Numbers.incumbent (ScanState.run s)} + {pre = pre} {suf = ScanState.suffix s} + scanned (skip-known K κ C s ev) + + -- ── the non-factive layer, for contrast ───────────────────────────────── + + EpiAt : (K : Set) (κ : K) (A : Set₁) -> Set₁ + EpiAt K κ A = Epi {ℓ = lsuc lzero} {wℓ = lzero} K κ A + + receipt-map : {K : Set} {κ : K} {A B : Set₁} (f : A -> B) -> + EpiAt K κ A -> EpiAt K κ B + receipt-map {κ = κ} f (epi w e) = epi (warrantOn κ _ (Warrant.Evidence w)) e + + receipts : (K : Set) -> Modality K (lsuc lzero) + Modality.E (receipts K) κ A = EpiAt K κ A + Modality.map (receipts K) f x = receipt-map f x + + -- Belief: the same run, the same token, no soundness map. + rapidBelief : (K : Set) -> BeliefModality K (lsuc lzero) + BeliefModality.modality (rapidBelief K) = receipts K + + skip-belief-only : (K : Set) (κ : K) (C : Checkable) (s : ScanState) -> + SkipEvidence C s -> EpiAt K κ (Lift₁ (SkipClaimAt s)) + skip-belief-only K κ C s ev = + epi (warrantOn κ (Lift₁ (SkipClaimAt s)) (SkipEvidence C s)) ev + + -- A one-element type, used to exhibit a token whose claim is empty. + data Point : Set where + point : Point + + -- A warrant plus a token is not knowledge: there is no reflection out of + -- `Epi`, for the skip warrants or for any others. + no-receipt-reflection : {K : Set} (κ : K) -> + ((A : Set₁) -> EpiAt K κ A -> A) -> Impossible + no-receipt-reflection {K} κ reflectEpi = + Lift₁.lower (reflectEpi (Lift₁ Impossible) + (epi (warrantOn κ (Lift₁ Impossible) Point) point)) + + -- ── the standpoint frame, for the worked example and the documentation ── + + data Standpoint : Set where + full-scan : Standpoint -- every entry of the row was examined + pruned : Standpoint -- a prefix was examined, the rest is certified + unverified : Standpoint -- the same numbers, no accepted check + + rapidNJKnowledge : FactiveModality Standpoint (lsuc lzero) + rapidNJKnowledge = rapidKnowledge Standpoint + + rapidNJBelief : BeliefModality Standpoint (lsuc lzero) + rapidNJBelief = rapidBelief Standpoint + + -- ── the open obligation, stated and not assumed ───────────────────────── + + -- The "dynamic" RapidNJ variant re-uses a bound across iterations by the + -- argument that q-values only weaken when a cluster is joined. That + -- transport is NOT proved here. The obligation is declared so it can be + -- attacked explicitly, and nothing in this module depends on it: there is + -- no instance and no result that consumes one. + record WeakeningObligation : Set₁ where + field + continues : ScanState -> ScanState -> Set + carries : {s s' : ScanState} -> continues s s' -> + RowClaim s (ScanState.suffix s) -> RowClaim s (ScanState.suffix s') diff --git a/src/EpistemicTypes/Applications/SortedRow.agda b/src/EpistemicTypes/Applications/SortedRow.agda new file mode 100644 index 0000000..d9561f2 --- /dev/null +++ b/src/EpistemicTypes/Applications/SortedRow.agda @@ -0,0 +1,82 @@ +{-# OPTIONS --safe --without-K #-} + +-- Applications / SortedRow +-- +-- The scan state of a RapidNJ row. RapidNJ keeps, beside the distance +-- matrix D, a matrix S whose rows are sorted by increasing distance, and an +-- index map I. For each cluster i it walks S(i) upwards from small to +-- large d(i,j), keeping the smallest q-value seen so far, and stops as soon +-- as the row lower bound cannot improve it. The entries it never looks at +-- are what this module calls the skipped suffix: in the (index, distance) +-- plane they are the quadrant `{ (i,j) : d(i,j) ≥ d(i,next) }`. +-- +-- The two facts the bound argument needs about that quadrant are: +-- +-- * every skipped distance is at least the distance at the stop cursor +-- (`AllDistAtLeast`, the sorted-row invariant), and +-- * every skipped row sum is at most the running maximum +-- (`AllRowSumAtMost`, the running-maximum invariant). +-- +-- Both are carried as *proof objects*, not consumed silently: a certificate +-- that cannot supply them is not a certificate. The implementation +-- maintains them when it inserts the new cluster row after a join. + +module EpistemicTypes.Applications.SortedRow where + +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Nat using (Nat) + +open import EpistemicTypes.Applications.OrderedGroup +open import EpistemicTypes.Applications.IntegerModel using (_⊎_; inj₁; inj₂) + +-- The row layer, parameterised by the exact arithmetic it reasons about. +module Row (G : OrderedGroup) where + open OrderedGroup G + open Laws G + + -- A row entry: the column index j, the distance d(i,j) as seen from the + -- row's cluster i, and the row sum t(j) of the column. + record Entry : Set where + constructor entry + field + index : Nat + dist : Carrier + rowSum : Carrier + + -- P holds of every entry of the list. + data All (P : Entry -> Set) : List Entry -> Set where + allNil : All P [] + allCons : {e : Entry} {es : List Entry} -> P e -> All P es -> All P (e ∷ es) + + -- Membership. + data _∈E_ (e : Entry) : List Entry -> Set where + here : {es : List Entry} -> e ∈E (e ∷ es) + there : {e' : Entry} {es : List Entry} -> e ∈E es -> e ∈E (e' ∷ es) + + ∈-All : (P : Entry -> Set) {es : List Entry} -> + All P es -> (x : Entry) -> x ∈E es -> P x + ∈-All P (allCons p _) x here = p + ∈-All P (allCons p ps) x (there i) = ∈-All P ps x i + + -- The sorted-row invariant, relative to the stop cursor: the cursor's + -- distance is a lower bound for the whole skipped suffix. + AllDistAtLeast : (d : Carrier) -> List Entry -> Set + AllDistAtLeast d = All (λ e -> d ≤ Entry.dist e) + + -- The running-maximum invariant: no skipped row sum exceeds t(max). + AllRowSumAtMost : (b : Carrier) -> List Entry -> Set + AllRowSumAtMost b = All (λ e -> Entry.rowSum e ≤ b) + + -- Concatenation of rows, and the decomposition of membership along it. + -- A whole row is the examined prefix followed by the skipped suffix. + _++_ : List Entry -> List Entry -> List Entry + [] ++ ys = ys + (x ∷ xs) ++ ys = x ∷ (xs ++ ys) + + ∈-append : {e : Entry} {xs ys : List Entry} -> + e ∈E (xs ++ ys) -> e ∈E xs ⊎ e ∈E ys + ∈-append {e} {xs = []} {ys} i = inj₂ i + ∈-append {e} {xs = x ∷ xs} {ys} here = inj₁ here + ∈-append {e} {xs = x ∷ xs} {ys} (there i) with ∈-append {e} {xs = xs} {ys} i + ... | inj₁ p = inj₁ (there p) + ... | inj₂ q = inj₂ q diff --git a/src/EpistemicTypes/Base.agda b/src/EpistemicTypes/Base.agda index a2f3693..afaf445 100644 --- a/src/EpistemicTypes/Base.agda +++ b/src/EpistemicTypes/Base.agda @@ -12,6 +12,13 @@ open import Agda.Builtin.Equality using (_≡_) -- This record intentionally does not include return/η : A -> E κ A. -- Such an introduction rule says that truth is epistemically available at κ, -- which is stronger than a generic modal interface. +-- +-- `FactiveModality.reflect` is where an application plugs in: an algorithm +-- that can prove a claim from the evidence it records instantiates `reflect` +-- with that proof, and the claim is then knowledge rather than assumption. +-- `Applications.RapidNJSkip` does exactly this for a bound-checked skip of a +-- search quadrant (docs/applications/rapidnj-q-criterion.adoc). No +-- application-specific obligation is added to this interface. record Modality {kℓ : Level} (K : Set kℓ) (ℓ : Level) : Set (kℓ ⊔ lsuc ℓ) where field diff --git a/src/EpistemicTypes/EchoBridge.agda b/src/EpistemicTypes/EchoBridge.agda index ec3e3e1..a2b51b2 100644 --- a/src/EpistemicTypes/EchoBridge.agda +++ b/src/EpistemicTypes/EchoBridge.agda @@ -146,6 +146,12 @@ data _≤ℕ_ : Nat -> Nat -> Set where zero≤ : {n : Nat} -> zero ≤ℕ n suc≤ : {m n : Nat} -> m ≤ℕ n -> suc m ≤ℕ suc n +-- Fixity matters for readability: without this declaration the relation +-- would bind tighter than `_+_`, so `m + k ≤ℕ n + k` would parse as +-- `m + (k ≤ℕ n) + k`. Application modules mix the two, so the relation is +-- declared here, where it is defined. +infix 4 _≤ℕ_ + ≤ℕ-trans : {a b c : Nat} -> a ≤ℕ b -> b ≤ℕ c -> a ≤ℕ c ≤ℕ-trans zero≤ _ = zero≤ ≤ℕ-trans (suc≤ p) (suc≤ q) = suc≤ (≤ℕ-trans p q) diff --git a/tests/check-proofs.sh b/tests/check-proofs.sh index bc5f41d..55c3fbe 100644 --- a/tests/check-proofs.sh +++ b/tests/check-proofs.sh @@ -3,8 +3,9 @@ set -euo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." # Check each source module, including any new module omitted from All.agda. -shopt -s nullglob -modules=(src/EpistemicTypes/*.agda) +# The search is recursive so that modules in subdirectories (for example the +# Applications/ tree) are gated even when they are not re-exported by All.agda. +mapfile -t modules < <(find src/EpistemicTypes -name '*.agda' | sort) [[ ${#modules[@]} -gt 0 ]] || { echo 'FAIL: no proof modules'; exit 1; } for module in "${modules[@]}"; do agda --no-libraries --safe --without-K --double-check --ignore-interfaces \ diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh index cc65009..fa77907 100644 --- a/tests/check-rejections.sh +++ b/tests/check-rejections.sh @@ -6,7 +6,7 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." # unrelated parse failures must fail this gate rather than count as rejection. fixtures=(LyingVerifier ForgedAcceptance ReplayedArtifact ReplayedHolder \ StaleSample FakeFreshness ForkedHistory ForgedResidue MismatchedSource \ - UnderstatedBound InventedMigration) + UnderstatedBound InventedMigration UncheckedSkip) expected_files=$(printf 'tests/reject/%s.agda\n' "${fixtures[@]}" | sort) actual_files=$(rg --files tests/reject -g '*.agda' | sort) [[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; } @@ -23,6 +23,7 @@ for fixture in "${fixtures[@]}"; do ReplayedArtifact) expected='true != .*false' ;; ReplayedHolder) expected='Alice != .*Bob' ;; StaleSample|ForkedHistory|ForgedResidue|MismatchedSource) expected='false != .*true' ;; + UncheckedSkip) expected='false != .*true' ;; FakeFreshness) expected='initial .*false !=' ;; UnderstatedBound) expected='1 != 0' ;; InventedMigration) expected='true != .*false' ;; diff --git a/tests/reject/UncheckedSkip.agda b/tests/reject/UncheckedSkip.agda new file mode 100644 index 0000000..53897ae --- /dev/null +++ b/tests/reject/UncheckedSkip.agda @@ -0,0 +1,44 @@ +{-# OPTIONS --safe --without-K #-} +-- Rejection control: a skip whose check was not accepted. +-- +-- The four-taxon scan below is unscannable past its cursor. With r = 4 +-- (coefficient 2), row sum t(i) = 1, running maximum t(max) = 20, cursor +-- distance 5, and incumbent q(min) = 0, +-- +-- qBound = (r - 2)*5 - 1 - 20 = 10 - 21 = -11 < 0 = q(min) +-- +-- so the bound *can* be improved further down the row and an exact +-- comparison answers `false`. Recording that run as evidence would be +-- unsound: it asserts a stop condition the numbers do not meet. The +-- `refl` below is therefore rejected -- the check is the gate, and the +-- Q-criterion bound lemma consumes only accepted checks. +module UncheckedSkip where + +open import Agda.Builtin.Equality using (refl) +open import Agda.Builtin.List using ([]; _∷_) +open import Agda.Builtin.Sigma using (_,_) +open import EpistemicTypes.EchoBridge using (≤ℕ-plus) +open import EpistemicTypes.Applications.IntegerModel using (mk; ≤ℕ-refl; ℤ-group) +open import EpistemicTypes.Applications.RapidNJExamples using (ℤ-checkable; ≤ℤ-5-7) +import EpistemicTypes.Applications.RapidNJSkip +import EpistemicTypes.Applications.SortedRow +import EpistemicTypes.Applications.QCriterion + +module Rapid = EpistemicTypes.Applications.RapidNJSkip.Skip ℤ-group +module Row = EpistemicTypes.Applications.SortedRow.Row ℤ-group +module Cr = + EpistemicTypes.Applications.QCriterion.Criterion ℤ-group + +open Rapid +open Row +open Cr + +state : ScanState +state = scanning (numbers 2 (mk 1) (mk 20) (mk 0)) + (entry 2 (mk 5) (mk 1)) + (entry 3 (mk 7) (mk 2) ∷ []) + +forged : SkipEvidence ℤ-checkable state +forged = allCons ≤ℤ-5-7 allNil + , allCons (≤ℕ-plus 2 18) allNil + , refl