From 13b7c76e188cd94aa116e6303db1dab85013a6b3 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 12 Nov 2026 02:57:00 +0000 Subject: [PATCH] applied: Agda proofs of APP-1 to APP-4 (WO 4.2, 2 of 3) The second of three pull requests for WO 4.2 (owner rulings 2026-11-12). Every new module is gated in the Agda manifest; the gate finds no postulate in any import cone. - Applied/Status.agda: the order of evidence statuses, and `Covers u v`: v is given with a status at least u. zipWith and map pass it to their arguments. - Applied/Missing.agda: APP-1 and APP-4, for any number structure. For each output of a period (members, receipts, payments, closing cash, shortfall, support minutes, both tests) and for each cohort kind: if the output is given with status u, every input that it depends on is given with a status at least u. Once a closing balance is missing, every later one is missing. A "yes" verdict needs every period to be a known "yes"; a known breach decides a verdict; the funding gap needs every shortfall. - Applied/Cash.agda: APP-2 (`cash-identity`: the last closing balance is the opening balance plus, summed over the periods, receipts minus payments; both sides are missing together) and APP-3 (`gap-sound`, `gap-least`), for any ordered abelian group (`Laws`). - Applied/IntLaws.agda: the integer instance of the worked examples satisfies `Laws` (owner ruling 2026-11-12), built on Agda.Builtin only, so APP-2 and APP-3 hold for the model as it runs. - Applied/Cohort.agda: the local helpers of cohortAt are now top-level (`joined`, `renewed`) so that the proofs can name them; the worked examples check unchanged. - PROOF-NEEDS, PROOF-STATUS, EXPLAINME, README, ROADMAP and the applied documents: the Agda leg is proved; the Rocq and Lean legs are open. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- EXPLAINME.adoc | 24 +- README.adoc | 7 +- .../finance/cohort-economics/README.adoc | 3 +- .../finance/cohort-economics/modes.adoc | 3 +- .../methods/types-and-assurance.adoc | 2 +- docs/status/PROOF-NEEDS.adoc | 35 +- docs/status/PROOF-STATUS.adoc | 9 +- docs/status/ROADMAP.adoc | 24 +- verification/proofs/agda/Applied/Cash.agda | 262 +++++++++++++++ verification/proofs/agda/Applied/Cohort.agda | 20 +- verification/proofs/agda/Applied/IntLaws.agda | 246 ++++++++++++++ verification/proofs/agda/Applied/Missing.agda | 229 +++++++++++++ verification/proofs/agda/Applied/Status.agda | 317 ++++++++++++++++++ verification/proofs/agda/MANIFEST | 4 + 14 files changed, 1141 insertions(+), 44 deletions(-) create mode 100644 verification/proofs/agda/Applied/Cash.agda create mode 100644 verification/proofs/agda/Applied/IntLaws.agda create mode 100644 verification/proofs/agda/Applied/Missing.agda create mode 100644 verification/proofs/agda/Applied/Status.agda diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index aff1460..d1023be 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -134,7 +134,8 @@ ____ Methods that apply mathematics to decisions, starting with accounting and finance. A shared input schema keeps missing apart from zero. A cohort model in Agda has three number modes and three synthetic -worked examples, each checked by Agda; its general properties are open. +worked examples, each checked by Agda. Its four general properties are proved +in Agda; the Rocq and Lean re-proofs are next. ____ How this is implemented:: @@ -150,8 +151,8 @@ each, missing ones included, and a control in fails it. Caveat:: -The examples are checked, not the model: its general properties (APP-1 to -APP-4) are open. The examples are synthetic and say nothing about any +Its four general properties (APP-1 to APP-4) are proved in Agda for the +model as it runs; the Rocq and Lean re-proofs are open. The examples are synthetic and say nothing about any organisation. The management-accounting design has no model yet. == Privacy by count @@ -281,14 +282,21 @@ and `_⊔_` as builtins. |Not yet stated in a prover (next on the theory shelf) |APP-1 to APP-4: the cohort model of the applied shelf (missing propagates, -cash identity, the funding gap, status never upgrades) +cash identity, the funding gap, status never upgrades), Agda leg +|proven +|Agda, `--safe --without-K --cubical-compatible` +|`verification/proofs/agda/Applied/Missing.agda`, `Cash.agda`, `IntLaws.agda` +|The model only. APP-2 and APP-3 rest on the laws that `IntLaws.agda` +proves for the integer instance + +|APP-1 to APP-4, Rocq and Lean legs |open |- -|`docs/status/PROOF-NEEDS.adoc`; model `verification/proofs/agda/Applied/Cohort.agda` -|Stated in prose; the worked examples are checked, the properties are not +|- +|Not yet re-proved (WO 4.2, third pull request) |=== -Proofs: 3 proven of 9; 1 argued, 5 open (the token-lattice theorems count as -one). The registry derives `PWG-1` for +Proofs, counted by leg: 7 proven of 17; 1 argued, 9 open (the token-lattice +theorems count as one; APP-1 to APP-4 count one for each prover). The registry derives `PWG-1` for THY-1 from the receipt. The checker versions are those that CI asserts in the Guix shell (CI run 43057783538). diff --git a/README.adoc b/README.adoc index e4d9c7f..477687d 100644 --- a/README.adoc +++ b/README.adoc @@ -35,15 +35,16 @@ describes what is proved, where, and how strongly. * *Applied systems.* Methods that apply mathematics to decisions, starting with accounting and finance. A shared input schema keeps missing apart from zero. A cohort model in Agda has three number modes and three synthetic - worked examples, each checked by Agda; its general properties are open. + worked examples, each checked by Agda. Its four general properties are proved + in Agda; the Rocq and Lean re-proofs are next. * *Privacy by count.* The frame names public repositories only. The number of private repositories in the listing is kept as one number. [NOTE] .Planned ==== -The token-lattice theorems of the theory shelf, proofs of the cohort model -(APP-1 to APP-4), a published atlas, receipts in more home +The token-lattice theorems of the theory shelf, the Rocq and Lean re-proofs +of the cohort model (APP-1 to APP-4), a published atlas, receipts in more home repositories, and a scheduled census. See link:docs/status/ROADMAP.adoc[the roadmap]. ==== diff --git a/applied-systems/finance/cohort-economics/README.adoc b/applied-systems/finance/cohort-economics/README.adoc index 5ef0d02..ef4015b 100644 --- a/applied-systems/finance/cohort-economics/README.adoc +++ b/applied-systems/finance/cohort-economics/README.adoc @@ -41,5 +41,6 @@ link:../../methods/input-schema.adoc[input schema], and its expected outputs. `just applied-build` writes link:generated/examples.adoc[the worked examples] and one Agda module for each example. Agda accepts that module only if the model computes every expected output, missing ones included. The general -properties of the model are open proof obligations APP-1 to APP-4 in +properties of the model, APP-1 to APP-4, are proved in Agda (Rocq and Lean +re-proofs open); see `docs/status/PROOF-NEEDS.adoc`. diff --git a/applied-systems/finance/cohort-economics/modes.adoc b/applied-systems/finance/cohort-economics/modes.adoc index 7723c62..abcd5ef 100644 --- a/applied-systems/finance/cohort-economics/modes.adoc +++ b/applied-systems/finance/cohort-economics/modes.adoc @@ -65,4 +65,5 @@ costs and floors in each mode, so you can compare the results. * Rates do not carry uncertainty. To explore it, write two examples with different rates. * The model checks each worked example exactly. The general properties - (obligations APP-1 to APP-4 in `docs/status/PROOF-NEEDS.adoc`) are open. + (obligations APP-1 to APP-4 in `docs/status/PROOF-NEEDS.adoc`) are proved + in Agda for every mode; the Rocq and Lean re-proofs are open. diff --git a/applied-systems/methods/types-and-assurance.adoc b/applied-systems/methods/types-and-assurance.adoc index a63b623..3a550c0 100644 --- a/applied-systems/methods/types-and-assurance.adoc +++ b/applied-systems/methods/types-and-assurance.adoc @@ -31,5 +31,5 @@ The cohort model (`verification/proofs/agda/Applied/Cohort.agda`) is the first test of these ideas. Each value carries its evidence status, a missing value stays missing, and every worked example is checked by Agda. Its general properties (obligations APP-1 to APP-4 in `docs/status/PROOF-NEEDS.adoc`) are -open. A check of a model on an example is not a proof of the model, and neither +proved in Agda; the Rocq and Lean re-proofs are open. A check of a model on an example is not a proof of the model, and neither establishes the truth of real inputs. diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 33c0292..eef7efc 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -42,40 +42,45 @@ missing input is missing, in every period after it too, and never zero. A verdict is "no" on a known breach and otherwise missing when any value it depends on is missing; it is never "yes" then |Agda, re-checked in Rocq and Lean -|Open: stated here, not yet in Agda (WO 4.2) -|`verification/proofs/agda/Applied/Cohort.agda` +|Agda leg proved; Rocq and Lean legs open (WO 4.2) +|`verification/proofs/agda/Applied/Missing.agda` |APP-2 -|Cash identity: when every input is present, the closing cash of the last -period equals the opening cash plus all receipts minus all payments +|Cash identity: the closing cash of the last period equals the opening cash +plus, summed over the periods, receipts minus payments; when a value is +missing, both sides are missing |Agda, re-checked in Rocq and Lean -|Open: stated here, not yet in Agda (WO 4.2) -|`verification/proofs/agda/Applied/Cohort.agda` +|Agda leg proved; Rocq and Lean legs open (WO 4.2) +|`verification/proofs/agda/Applied/Cash.agda` (`cash-identity`) |APP-3 |The funding gap is sound and least: adding the gap to the opening cash keeps every closing balance at or above its floor, and no smaller non-negative amount does |Agda, re-checked in Rocq and Lean -|Open: stated here, not yet in Agda (WO 4.2) -|`verification/proofs/agda/Applied/Cohort.agda` +|Agda leg proved; Rocq and Lean legs open (WO 4.2) +|`verification/proofs/agda/Applied/Cash.agda` (`gap-sound`, `gap-least`) |APP-4 |Status never upgrades: the evidence status of an output is never stronger than the weakest status of the inputs that it depends on |Agda, re-checked in Rocq and Lean -|Open: stated here, not yet in Agda (WO 4.2) -|`verification/proofs/agda/Applied/Cohort.agda` +|Agda leg proved; Rocq and Lean legs open (WO 4.2) +|`verification/proofs/agda/Applied/Missing.agda` |=== APP-1 to APP-4 are about the cohort model of the applied shelf (re-anchoring plan WO 4.2, owner rulings 2026-11-12). Each statement would be true of any implementation of the model, so each is theory by PROOF-POLICY §1: proved in -Agda and re-checked in Rocq and Lean. The model is written over an abstract -number structure, so APP-2 and APP-3 need only its laws, not the laws of one -number type. They are not theory-shelf admissions: no estate rule depends on -them yet. Each worked example is already checked by Agda; a checked example is -not a proof of the property. +Agda and re-checked in Rocq and Lean. They are not theory-shelf admissions: +no estate rule depends on them yet. + +The Agda leg holds for the model as it runs. APP-1 and APP-4 hold for any +number structure: one statement carries both (`Covers`, in +`Applied/Status.agda`). APP-2 and APP-3 hold for any ordered abelian group +(`Laws`, in `Applied/Cash.agda`), and `Applied/IntLaws.agda` proves that +the integer instance of the worked examples is one. Every module is in the +gated Agda manifest, with no postulate in its import cone. No Mathesis obligation concerns an ABI or an FFI: since WO 3.2 the deed declares neither capability. diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 809a13f..77b702d 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -24,14 +24,15 @@ reader of PROOF-POLICY §8.5.1. |Not yet stated in a prover |APP-1 to APP-4, the cohort model of the applied shelf (WO 4.2) -|Open +|Agda leg proved; Rocq and Lean legs open |- -|Stated in `docs/status/PROOF-NEEDS.adoc`; the model and its three worked -examples check in Agda, but no theorem is stated in Agda yet +|`verification/proofs/agda/Applied/Missing.agda`, `Cash.agda` and +`IntLaws.agda`, gated in CI. No receipt yet: a grade needs all three legs |=== *Overall*: 1 of 6 obligations discharged; 5 open (the token-lattice theorems -count as one). These are counts, not a +count as one). APP-1 to APP-4 have their Agda leg; each stays open until its +Rocq and Lean legs land. These are counts, not a percentage: PROOF-POLICY §8 grades are derived from receipts and are never flattened. The template example proofs were removed in WO 4.1. diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index a11fafe..785a03a 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -176,7 +176,22 @@ One pull request that changes census rows is open at a time (atlas README, that depends on it stays missing. A golden-path control shows that the gate fails when a missing output is read as zero. ** APP-1 to APP-4 are recorded as open in `docs/status/PROOF-NEEDS.adoc`. - Next: the Agda proofs, then the Rocq and Lean re-proofs. + Merged (pull request 81). +* WO 4.2, second pull request: the Agda proofs of APP-1 to APP-4, gated in + CI with no postulate in any import cone. +** `Applied/Status.agda` and `Applied/Missing.agda`: APP-1 and APP-4, for any + number structure. If an output is given with status u, every input that it + depends on is given with a status at least u. Once a closing balance is + missing, every later one is missing; a "yes" verdict needs every period to + be a known "yes"; a known breach decides the verdict. +** `Applied/Cash.agda`: APP-2 (cash identity) and APP-3 (the funding gap is + sound and least), for any ordered abelian group (`Laws`). +** `Applied/IntLaws.agda`: the integer instance of the worked examples is an + ordered abelian group (owner ruling 2026-11-12), so APP-2 and APP-3 hold + for the model as it runs. +** The two local helpers of `cohortAt` became top-level functions, so that + the proofs can name them. The worked examples are unchanged. +** Next: the Rocq and Lean re-proofs (third pull request). * Open item for the owner (ruling 2026-11-12): none of the JSON Lines data files declares a licence; JSON has no comment syntax. The owner will write one `REUSE.toml` rule at the root that covers all of them (doctrine 6: a @@ -222,8 +237,8 @@ anchors `c81cb84` |The three shelves: the theory admission rule and the token-lattice theorems, the applied shelf tied to the evidence spine, the published atlas (needs a ruling) -|In progress: WO 4.1 and the theory ledger merged; WO 4.2 in review (1 of -3 pull requests) +|In progress: WO 4.1, the theory ledger and WO 4.2 (1 of 3) merged; the +Agda proofs of WO 4.2 in review |5 |Scale: receipts in the home repositories, the bridge lock pilot, a @@ -253,4 +268,5 @@ scheduled census, a view of what each repository owes example; the model in Agda, proved; all four invariants recorded; a shared schema; three number modes for different users, with guidance; JSON Lines as the source of generated Agda; proofs in Agda, Rocq and Lean; three pull - requests. + requests; the laws of the integer instance proved in the second pull + request. diff --git a/verification/proofs/agda/Applied/Cash.agda b/verification/proofs/agda/Applied/Cash.agda new file mode 100644 index 0000000..465b3e8 --- /dev/null +++ b/verification/proofs/agda/Applied/Cash.agda @@ -0,0 +1,262 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- APP-2 (cash identity) and APP-3 (the funding gap is sound and least) for +-- the cohort model (Applied.Cohort). +-- +-- Both hold for any number structure that is an ordered abelian group: +-- `Laws` below. The theorems need only these laws, not the laws of one +-- number type. Each is stated on `rowsFrom`, the rows from any period and +-- any previous balance, so it covers `allRows` and every tail of it. +-- Values are in the scaled units of the model (Applied.Cohort, `scaleOf`). + +module Applied.Cash 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) renaming (_-_ to _∸_) +open import Agda.Builtin.Sigma using (Σ; _,_) +open import Applied.Cohort +open import Applied.Status using (T; tt; ⊥; _×_; sym; cong; subst; covers; zipWith-given; ⊓-assoc; ⊓-identityʳ) +open import Applied.Missing using (All) + +trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z +trans refl q = q + +cong₂ : ∀ {A B C : Set} (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v +cong₂ f refl refl = refl + +------------------------------------------------------------------------ +-- Ordered abelian groups + +record Laws (N : Number) : Set where + open Number N + field + neg : R → R + +-assoc : ∀ a b c → (a + b) + c ≡ a + (b + c) + +-comm : ∀ a b → a + b ≡ b + a + +-identityʳ : ∀ a → a + 0# ≡ a + +-inverseʳ : ∀ a → a + neg a ≡ 0# + -‿def : ∀ a b → a - b ≡ a + neg b + ≤-refl : ∀ a → T (a ≤ᵇ a) + ≤-trans : ∀ a b c → T (a ≤ᵇ b) → T (b ≤ᵇ c) → T (a ≤ᵇ c) + ≤-total : ∀ a b → (a ≤ᵇ b) ≡ false → T (b ≤ᵇ a) + ≤-+ : ∀ a b c → T (a ≤ᵇ b) → T ((a + c) ≤ᵇ (b + c)) + +module Proofs (N : Number) (L : Laws N) where + open Number N + open Laws L + open Model N + + ---------------------------------------------------------------------- + -- Group lemmas + + private + -- ((a + r) − q) + x ≡ a + ((r − q) + x) + step-law : ∀ a r q x → ((a + r) - q) + x ≡ a + ((r - q) + x) + step-law a r q x = + trans (cong (λ y → y + x) (-‿def (a + r) q)) + (trans (cong (λ y → y + x) (+-assoc a r (neg q))) + (trans (+-assoc a (r + neg q) x) + (cong (λ y → a + (y + x)) (sym (-‿def r q))))) + + -- ((a + g) + r) − q ≡ ((a + r) − q) + g + shift-law : ∀ a g r q → ((a + g) + r) - q ≡ ((a + r) - q) + g + shift-law a g r q = + trans (-‿def ((a + g) + r) q) + (trans (cong (λ y → y + neg q) (+-assoc a g r)) + (trans (cong (λ y → (a + y) + neg q) (+-comm g r)) + (trans (cong (λ y → y + neg q) (sym (+-assoc a r g))) + (trans (+-assoc (a + r) g (neg q)) + (trans (cong (λ y → (a + r) + y) (+-comm g (neg q))) + (trans (sym (+-assoc (a + r) (neg q) g)) + (cong (λ y → y + g) (sym (-‿def (a + r) q))))))))) + + -- (f − c) + c ≡ f + cancel-right : ∀ f c → (f - c) + c ≡ f + cancel-right f c = + trans (cong (λ y → y + c) (-‿def f c)) + (trans (+-assoc f (neg c) c) + (trans (cong (λ y → f + y) (+-comm (neg c) c)) + (trans (cong (λ y → f + y) (+-inverseʳ c)) + (+-identityʳ f)))) + + -- (c + g) + neg c ≡ g + cancel-left : ∀ c g → (c + g) + neg c ≡ g + cancel-left c g = + trans (cong (λ y → y + neg c) (+-comm c g)) + (trans (+-assoc g c (neg c)) + (trans (cong (λ y → g + y) (+-inverseʳ c)) + (+-identityʳ g))) + + T-subst : ∀ {a b c d} → a ≡ c → b ≡ d → T (a ≤ᵇ b) → T (c ≤ᵇ d) + T-subst refl refl t = t + + T→true : ∀ {b} → T b → b ≡ true + T→true {true} _ = refl + + true→T : ∀ {b} → b ≡ true → T b + true→T refl = tt + + -- f − c ≤ g if and only if f ≤ c + g + below-shift : ∀ f c g → T ((f - c) ≤ᵇ g) → T (f ≤ᵇ (c + g)) + below-shift f c g t = T-subst (cancel-right f c) (+-comm g c) (≤-+ (f - c) g c t) + + shift-below : ∀ f c g → T (f ≤ᵇ (c + g)) → T ((f - c) ≤ᵇ g) + shift-below f c g t = T-subst (sym (-‿def f c)) (cancel-left c g) (≤-+ f (c + g) (neg c) t) + + ---------------------------------------------------------------------- + -- Values that may be missing + + private + valueOr : R → Val R → R + valueOr d missing = d + valueOr _ (given _ x) = x + + truthOr : Val Bool → Bool + truthOr missing = false + truthOr (given _ b) = b + + meet4 : ∀ s t v w → ((s ⊓ t) ⊓ v) ⊓ w ≡ s ⊓ ((t ⊓ v) ⊓ w) + meet4 s t v w = + trans (⊓-assoc (s ⊓ t) v w) + (trans (⊓-assoc s t (v ⊓ w)) + (cong (λ y → s ⊓ y) (sym (⊓-assoc t v w)))) + + -- One period of the cash identity, for values that may be missing. + step-val : ∀ (p r q n : Val R) → + zipWith _+_ (zipWith _-_ (zipWith _+_ p r) q) n ≡ zipWith _+_ p (zipWith _+_ (zipWith _-_ r q) n) + step-val (given s a) (given t b) (given v c) (given w d) = cong₂ given (meet4 s t v w) (step-law a b c d) + step-val missing r q n = refl + step-val (given s a) missing q n = refl + step-val (given s a) (given t b) missing n = refl + step-val (given s a) (given t b) (given v c) missing = refl + + base-val : ∀ (p : Val R) → p ≡ zipWith _+_ p (pure 0#) + base-val missing = refl + base-val (given s a) = sym (cong₂ given (⊓-identityʳ s) (+-identityʳ a)) + + -- Adding g to the previous balance adds g to the closing balance. + shift-val : ∀ (p r q : Val R) g → + zipWith _-_ (zipWith _+_ (map (λ x → x + g) p) r) q ≡ map (λ x → x + g) (zipWith _-_ (zipWith _+_ p r) q) + shift-val (given s a) (given t b) (given v c) g = cong (given ((s ⊓ t) ⊓ v)) (shift-law a g b c) + shift-val missing r q g = refl + shift-val (given s a) missing q g = refl + shift-val (given s a) (given t b) missing g = refl + + -- The floor test after adding g, against the shortfall before. + floor-met : ∀ (F C : Val R) g {s d} → zipWith _-_ F C ≡ given s d → T (d ≤ᵇ g) → + Σ Status (λ s′ → zipWith _≤ᵇ_ F (map (λ x → x + g) C) ≡ given s′ true) + floor-met (given sf f) (given sc c) g eq t = + sf ⊓ sc , cong (given (sf ⊓ sc)) (T→true (below-shift f c g (subst (λ y → T (y ≤ᵇ g)) (sym (cong (valueOr 0#) eq)) t))) + floor-met (given sf f) missing g () + floor-met missing C g () + + floor-needs : ∀ (F C : Val R) g {s d s′} → zipWith _-_ F C ≡ given s d → + zipWith _≤ᵇ_ F (map (λ x → x + g) C) ≡ given s′ true → T (d ≤ᵇ g) + floor-needs (given sf f) (given sc c) g eq ok = + subst (λ y → T (y ≤ᵇ g)) (cong (valueOr 0#) eq) (shift-below f c g (true→T (cong truthOr ok))) + floor-needs (given sf f) missing g () + floor-needs missing C g () + + -- The larger of two values bounds both, and is below any common bound. + max-left : ∀ a b → T (a ≤ᵇ max a b) + max-left a b with a ≤ᵇ b in eq + ... | true = true→T eq + ... | false = ≤-refl a + + max-right : ∀ a b → T (b ≤ᵇ max a b) + max-right a b with a ≤ᵇ b in eq + ... | true = ≤-refl b + ... | false = ≤-total a b eq + + max-least : ∀ a b c → T (a ≤ᵇ c) → T (b ≤ᵇ c) → T (max a b ≤ᵇ c) + max-least a b c ta tb with a ≤ᵇ b + ... | true = tb + ... | false = ta + + module _ (i : Inputs) where + open Inputs i + open Run i + + -- The closing balance after a list of rows, and the sum over the rows + -- of receipts minus payments. + lastClosing : Val R → List Row → Val R + lastClosing p [] = p + lastClosing p (r ∷ rs) = lastClosing (Row.closing r) rs + + netSum : List Row → Val R + netSum [] = pure 0# + netSum (r ∷ rs) = zipWith _+_ (zipWith _-_ (Row.receipts r) (Row.payments r)) (netSum rs) + + -- APP-2. The closing cash of the last period equals the opening cash + -- plus, summed over the periods, receipts minus payments. Both sides + -- are missing together, with the same status when given. + cash-identity : ∀ t n p → lastClosing p (rowsFrom t n p) ≡ zipWith _+_ p (netSum (rowsFrom t n p)) + cash-identity t zero p = base-val p + cash-identity t (suc n) p = + trans (cash-identity (suc t) n (Row.closing (rowAt t p))) + (step-val p (Row.receipts (rowAt t p)) (Row.payments (rowAt t p)) (netSum (rowsFrom (suc t) n (Row.closing (rowAt t p))))) + + -- Adding g to the previous balance adds g to every closing balance: + -- the rows from p + g are the rows from p, shifted. + shifted-closing : ∀ t p g → Row.closing (rowAt t (map (λ x → x + g) p)) ≡ map (λ x → x + g) (Row.closing (rowAt t p)) + shifted-closing t p g = shift-val p (Row.receipts (rowAt t p)) (Row.payments (rowAt t p)) g + + -- A shortfall bounded by g. + Bounded : R → Val R → Set + Bounded g v = Σ Status (λ s → Σ R (λ d → (v ≡ given s d) × T (d ≤ᵇ g))) + + Met : Row → Set + Met r = Σ Status (λ s → Row.cashOk r ≡ given s true) + + -- The worst shortfall bounds every shortfall. + worst-bounds : ∀ rs {u g} → worst rs ≡ given u g → All (λ r → Bounded g (Row.shortfall r)) rs + worst-bounds [] eq = tt + worst-bounds (r ∷ rs) {u} {g} eq with zipWith-given {f = max} {x = Row.shortfall r} {y = worst rs} eq + ... | covers s d eqd _ , covers w m eqm _ = + (s , d , eqd , subst (λ y → T (d ≤ᵇ y)) gval (max-left d m)) , + All-weaken rs (worst-bounds rs eqm) + where + gval : max d m ≡ g + gval = trans (cong (valueOr 0#) (sym (cong₂ (zipWith max) eqd eqm))) (cong (valueOr 0#) eq) + raise : ∀ {v} → Bounded m v → Bounded g v + raise (s′ , d′ , e , t) = s′ , d′ , e , ≤-trans d′ m g t (subst (λ y → T (m ≤ᵇ y)) gval (max-right d m)) + All-weaken : ∀ xs → All (λ x → Bounded m (Row.shortfall x)) xs → All (λ x → Bounded g (Row.shortfall x)) xs + All-weaken [] _ = tt + All-weaken (x ∷ xs) (b , bs) = raise b , All-weaken xs bs + + -- APP-3, sound: when every shortfall is at most g, adding g to the + -- previous balance meets the floor in every period. + meets-floor : ∀ t n p g → All (λ r → Bounded g (Row.shortfall r)) (rowsFrom t n p) → + All Met (rowsFrom t n (map (λ x → x + g) p)) + meets-floor t zero p g _ = tt + meets-floor t (suc n) p g ((s , d , eq , le) , rest) = + subst (λ c → Σ Status (λ s′ → zipWith _≤ᵇ_ (scaled (at (t ∸ 1) floor)) c ≡ given s′ true)) + (sym (shifted-closing t p g)) + (floor-met (scaled (at (t ∸ 1) floor)) (Row.closing (rowAt t p)) g eq le) , + subst (λ q → All Met (rowsFrom (suc t) n q)) (sym (shifted-closing t p g)) (meets-floor (suc t) n (Row.closing (rowAt t p)) g rest) + + gap-sound : ∀ t n p {u g} → worst (rowsFrom t n p) ≡ given u g → + All Met (rowsFrom t n (map (λ x → x + g) p)) + gap-sound t n p eq = meets-floor t n p _ (worst-bounds (rowsFrom t n p) eq) + + -- APP-3, least: no smaller non-negative addition meets every floor. + gap-least : ∀ t n p {u g} g′ → worst (rowsFrom t n p) ≡ given u g → T (0# ≤ᵇ g′) → + All Met (rowsFrom t n (map (λ x → x + g′) p)) → T (g ≤ᵇ g′) + gap-least t zero p g′ eq z _ = subst (λ y → T (y ≤ᵇ g′)) (cong (valueOr 0#) eq) z + gap-least t (suc n) p {u} {g} g′ eq z ((s′ , ok) , rest) + with zipWith-given {f = max} {x = Row.shortfall (rowAt t p)} {y = worst (rowsFrom (suc t) n (Row.closing (rowAt t p)))} eq + ... | covers s d eqd _ , covers w m eqm _ = + subst (λ y → T (y ≤ᵇ g′)) gval (max-least d m g′ head tail) + where + gval : max d m ≡ g + gval = trans (cong (valueOr 0#) (sym (cong₂ (zipWith max) eqd eqm))) (cong (valueOr 0#) eq) + head : T (d ≤ᵇ g′) + head = floor-needs (scaled (at (t ∸ 1) floor)) (Row.closing (rowAt t p)) g′ eqd + (subst (λ c → zipWith _≤ᵇ_ (scaled (at (t ∸ 1) floor)) c ≡ given s′ true) (shifted-closing t p g′) ok) + tail : T (m ≤ᵇ g′) + tail = gap-least (suc t) n (Row.closing (rowAt t p)) g′ eqm z + (subst (λ q → All Met (rowsFrom (suc t) n q)) (shifted-closing t p g′) rest) diff --git a/verification/proofs/agda/Applied/Cohort.agda b/verification/proofs/agda/Applied/Cohort.agda index 87d80bf..7031726 100644 --- a/verification/proofs/agda/Applied/Cohort.agda +++ b/verification/proofs/agda/Applied/Cohort.agda @@ -145,6 +145,17 @@ applyRate : Nat → Nat → Rate → Nat applyRate scale x (perMille m) = (((x div scale) *ℕ m) div 1000) *ℕ scale applyRate scale x (fraction n d) = (x *ℕ n) div d +-- The members who join a modelled cohort, multiplied by the scale. +joined : Nat → Val Nat → Val Rate → Val Nat +joined scale contacts conversion = + zipWith (applyRate scale) (map (λ n → n *ℕ scale) contacts) conversion + +-- The members after k renewals, multiplied by the scale. +renewed : Nat → Val Nat → Val Rate → Nat → Val Nat +renewed scale start retention zero = start +renewed scale start retention (suc k) = + zipWith (applyRate scale) (renewed scale start retention k) retention + -- Active members of one cohort in period t (counted from 1), multiplied by -- the scale. cohortAt : Nat → Nat → Cohort → Val Nat @@ -152,13 +163,8 @@ cohortAt scale t (observed start counts) = if t <ℕ start then pure 0 else map (λ n → n *ℕ scale) (at (t ∸ start) counts) cohortAt scale t (modelled start contacts conversion retention) = - if t <ℕ start then pure 0 else renew (t ∸ start) - where - joined : Val Nat - joined = zipWith (applyRate scale) (map (λ n → n *ℕ scale) contacts) conversion - renew : Nat → Val Nat - renew zero = joined - renew (suc k) = zipWith (applyRate scale) (renew k) retention + if t <ℕ start then pure 0 + else renewed scale (joined scale contacts conversion) retention (t ∸ start) sumAt : Nat → Nat → List Cohort → Val Nat sumAt scale t [] = pure 0 diff --git a/verification/proofs/agda/Applied/IntLaws.agda b/verification/proofs/agda/Applied/IntLaws.agda new file mode 100644 index 0000000..9c581c8 --- /dev/null +++ b/verification/proofs/agda/Applied/IntLaws.agda @@ -0,0 +1,246 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- The integer instance of the cohort model (Applied.IntNumber) is an +-- ordered abelian group: it satisfies `Laws` (Applied.Cash). So APP-2 and +-- APP-3 hold for the model as it runs on the worked examples, and the laws +-- are not vacuous. Built on Agda.Builtin only. +-- +-- Method. Every integer i equals P i ⊖ Q i for two natural numbers. Sums +-- and comparisons then reduce to natural numbers: (a ⊖ b) + (c ⊖ d) is +-- (a + c) ⊖ (b + d), and i ≤ j compares P i + Q j with P j + Q i. + +module Applied.IntLaws where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Int using (Int; pos; negsuc) +open import Agda.Builtin.Nat using (Nat; zero; suc) + renaming (_+_ to _+ℕ_; _-_ to _∸_; _<_ to _<ℕ_) +open import Applied.Cohort using (Number) +open import Applied.IntNumber using (intNumber; _⊖_; neg; _+ℤ_; _≤ℤ_) +open import Applied.Status using (T; tt; sym; cong; subst) +open import Applied.Cash using (Laws; trans; cong₂) + +------------------------------------------------------------------------ +-- Natural numbers + ++0 : ∀ n → n +ℕ 0 ≡ n ++0 zero = refl ++0 (suc n) = cong suc (+0 n) + ++suc : ∀ m n → m +ℕ suc n ≡ suc (m +ℕ n) ++suc zero n = refl ++suc (suc m) n = cong suc (+suc m n) + ++comm : ∀ m n → m +ℕ n ≡ n +ℕ m ++comm zero n = sym (+0 n) ++comm (suc m) n = trans (cong suc (+comm m n)) (sym (+suc n m)) + ++assoc : ∀ m n k → (m +ℕ n) +ℕ k ≡ m +ℕ (n +ℕ k) ++assoc zero n k = refl ++assoc (suc m) n k = cong suc (+assoc m n k) + +-- (w + x) + (y + z) ≡ (w + y) + (x + z) +swap : ∀ w x y z → (w +ℕ x) +ℕ (y +ℕ z) ≡ (w +ℕ y) +ℕ (x +ℕ z) +swap w x y z = + trans (+assoc w x (y +ℕ z)) + (trans (cong (w +ℕ_) (trans (sym (+assoc x y z)) (trans (cong (_+ℕ z) (+comm x y)) (+assoc y x z)))) + (sym (+assoc w y (x +ℕ z)))) + +-- m ≤ n, as the integer order uses it: m < n + 1. +leq : Nat → Nat → Bool +leq m n = m <ℕ suc n + +leq-refl : ∀ n → T (leq n n) +leq-refl zero = tt +leq-refl (suc n) = leq-refl n + +leq-trans : ∀ a b c → T (leq a b) → T (leq b c) → T (leq a c) +leq-trans zero b c _ _ = tt +leq-trans (suc a) zero c () _ +leq-trans (suc a) (suc b) zero _ () +leq-trans (suc a) (suc b) (suc c) p q = leq-trans a b c p q + +leq-total : ∀ a b → leq a b ≡ false → T (leq b a) +leq-total zero b () +leq-total (suc a) zero _ = tt +leq-total (suc a) (suc b) eq = leq-total a b eq + +leq-cancel : ∀ k x y → leq (k +ℕ x) (k +ℕ y) ≡ leq x y +leq-cancel zero x y = refl +leq-cancel (suc k) x y = leq-cancel k x y + +------------------------------------------------------------------------ +-- Integers as differences + +-- (k + a) ⊖ (k + b) ≡ a ⊖ b: one step is definitional. +⊖-cancelˡ : ∀ k a b → (k +ℕ a) ⊖ (k +ℕ b) ≡ a ⊖ b +⊖-cancelˡ zero a b = refl +⊖-cancelˡ (suc k) a b = ⊖-cancelˡ k a b + +⊖-cancelʳ : ∀ k a b → (a +ℕ k) ⊖ (b +ℕ k) ≡ a ⊖ b +⊖-cancelʳ k a b = trans (cong₂ _⊖_ (+comm a k) (+comm b k)) (⊖-cancelˡ k a b) + +-- a ⊖ b depends only on the difference of a and b. +⊖-diff : ∀ a b c d → a +ℕ d ≡ c +ℕ b → a ⊖ b ≡ c ⊖ d +⊖-diff a b c d eq = + trans (sym (⊖-cancelʳ d a b)) + (trans (cong (_⊖ (b +ℕ d)) eq) + (trans (cong ((c +ℕ b) ⊖_) (+comm b d)) + (⊖-cancelʳ b c d))) + +⊖-self : ∀ n → n ⊖ n ≡ pos 0 +⊖-self zero = refl +⊖-self (suc n) = ⊖-self n + +P Q : Int → Nat +P (pos m) = m +P (negsuc n) = 0 +Q (pos m) = 0 +Q (negsuc n) = suc n + +asDiff : ∀ i → i ≡ P i ⊖ Q i +asDiff (pos m) = refl +asDiff (negsuc n) = refl + +-- The parts of a ⊖ b have the difference of a and b. +⊖-parts : ∀ a b → P (a ⊖ b) +ℕ b ≡ a +ℕ Q (a ⊖ b) +⊖-parts zero zero = refl +⊖-parts (suc m) zero = refl +⊖-parts zero (suc n) = refl +⊖-parts (suc m) (suc n) = trans (+suc (P (m ⊖ n)) n) (cong suc (⊖-parts m n)) + +add-parts : ∀ i j → i +ℤ j ≡ (P i +ℕ P j) ⊖ (Q i +ℕ Q j) +add-parts (pos m) (pos n) = refl +add-parts (pos m) (negsuc n) = cong (_⊖ suc n) (sym (+0 m)) +add-parts (negsuc m) (pos n) = cong (λ x → n ⊖ suc x) (sym (+0 m)) +add-parts (negsuc m) (negsuc n) = cong negsuc (sym (+suc m n)) + +-- (a ⊖ b) + (c ⊖ d) ≡ (a + c) ⊖ (b + d) +⊖-+ : ∀ a b c d → (a ⊖ b) +ℤ (c ⊖ d) ≡ (a +ℕ c) ⊖ (b +ℕ d) +⊖-+ a b c d = trans (add-parts (a ⊖ b) (c ⊖ d)) (⊖-diff (p₁ +ℕ p₂) (q₁ +ℕ q₂) (a +ℕ c) (b +ℕ d) arith) + where + p₁ = P (a ⊖ b) ; q₁ = Q (a ⊖ b) ; p₂ = P (c ⊖ d) ; q₂ = Q (c ⊖ d) + arith : (p₁ +ℕ p₂) +ℕ (b +ℕ d) ≡ (a +ℕ c) +ℕ (q₁ +ℕ q₂) + arith = + trans (swap p₁ p₂ b d) + (trans (cong₂ _+ℕ_ (⊖-parts a b) (⊖-parts c d)) + (swap a q₁ c q₂)) + +------------------------------------------------------------------------ +-- The order + +ord : ∀ i j → (i ≤ℤ j) ≡ leq (P i +ℕ Q j) (P j +ℕ Q i) +ord (pos m) (pos n) = sym (cong₂ leq (+0 m) (+0 n)) +ord (pos m) (negsuc n) = sym (cong (λ x → leq x 0) (+suc m n)) +ord (negsuc m) (pos n) = refl +ord (negsuc m) (negsuc n) = refl + +-- Comparing two differences. +ord-⊖ : ∀ a b c d → ((a ⊖ b) ≤ℤ (c ⊖ d)) ≡ leq (a +ℕ d) (c +ℕ b) +ord-⊖ a b c d = + trans (ord (a ⊖ b) (c ⊖ d)) + (trans (sym (leq-cancel (b +ℕ d) _ _)) + (trans (cong₂ leq left right) + (leq-cancel (q₁ +ℕ q₂) (a +ℕ d) (c +ℕ b)))) + where + p₁ = P (a ⊖ b) ; q₁ = Q (a ⊖ b) ; p₂ = P (c ⊖ d) ; q₂ = Q (c ⊖ d) + left : (b +ℕ d) +ℕ (p₁ +ℕ q₂) ≡ (q₁ +ℕ q₂) +ℕ (a +ℕ d) + left = + trans (+comm (b +ℕ d) (p₁ +ℕ q₂)) + (trans (swap p₁ q₂ b d) + (trans (cong (_+ℕ (q₂ +ℕ d)) (⊖-parts a b)) + (trans (swap a q₁ q₂ d) + (trans (cong ((a +ℕ q₂) +ℕ_) (+comm q₁ d)) + (trans (swap a q₂ d q₁) + (trans (+comm (a +ℕ d) (q₂ +ℕ q₁)) + (cong (_+ℕ (a +ℕ d)) (+comm q₂ q₁)))))))) + right : (b +ℕ d) +ℕ (p₂ +ℕ q₁) ≡ (q₁ +ℕ q₂) +ℕ (c +ℕ b) + right = + trans (+comm (b +ℕ d) (p₂ +ℕ q₁)) + (trans (swap p₂ q₁ b d) + (trans (cong ((p₂ +ℕ b) +ℕ_) (+comm q₁ d)) + (trans (swap p₂ b d q₁) + (trans (+comm (p₂ +ℕ d) (b +ℕ q₁)) + (trans (cong ((b +ℕ q₁) +ℕ_) (⊖-parts c d)) + (trans (swap b q₁ c q₂) + (trans (+comm (b +ℕ c) (q₁ +ℕ q₂)) + (cong ((q₁ +ℕ q₂) +ℕ_) (+comm b c))))))))) + +------------------------------------------------------------------------ +-- The laws + +private + open Number intNumber + + +-comm : ∀ i j → i +ℤ j ≡ j +ℤ i + +-comm i j = trans (add-parts i j) (trans (cong₂ _⊖_ (+comm (P i) (P j)) (+comm (Q i) (Q j))) (sym (add-parts j i))) + + +-assoc : ∀ i j k → (i +ℤ j) +ℤ k ≡ i +ℤ (j +ℤ k) + +-assoc i j k = + trans (cong₂ _+ℤ_ (add-parts i j) (asDiff k)) + (trans (⊖-+ (P i +ℕ P j) (Q i +ℕ Q j) (P k) (Q k)) + (trans (cong₂ _⊖_ (+assoc (P i) (P j) (P k)) (+assoc (Q i) (Q j) (Q k))) + (trans (sym (⊖-+ (P i) (Q i) (P j +ℕ P k) (Q j +ℕ Q k))) + (sym (cong₂ _+ℤ_ (asDiff i) (add-parts j k)))))) + + +-identityʳ : ∀ i → i +ℤ pos 0 ≡ i + +-identityʳ (pos m) = cong pos (+0 m) + +-identityʳ (negsuc m) = refl + + +-inverseʳ : ∀ i → i +ℤ neg i ≡ pos 0 + +-inverseʳ (pos zero) = refl + +-inverseʳ (pos (suc n)) = ⊖-self n + +-inverseʳ (negsuc m) = ⊖-self m + + ≤-refl : ∀ i → T (i ≤ℤ i) + ≤-refl (pos m) = leq-refl m + ≤-refl (negsuc m) = leq-refl m + + ≤-trans : ∀ i j k → T (i ≤ℤ j) → T (j ≤ℤ k) → T (i ≤ℤ k) + ≤-trans (pos m) (pos n) (pos k) p q = leq-trans m n k p q + ≤-trans (pos m) (pos n) (negsuc k) p () + ≤-trans (pos m) (negsuc n) k () q + ≤-trans (negsuc m) j (pos k) p q = tt + ≤-trans (negsuc m) (pos n) (negsuc k) p () + ≤-trans (negsuc m) (negsuc n) (negsuc k) p q = leq-trans k n m q p + + ≤-total : ∀ i j → (i ≤ℤ j) ≡ false → T (j ≤ℤ i) + ≤-total (pos m) (pos n) eq = leq-total m n eq + ≤-total (pos m) (negsuc n) eq = tt + ≤-total (negsuc m) (pos n) () + ≤-total (negsuc m) (negsuc n) eq = leq-total n m eq + + -- Adding the same k to both sides leaves the comparison unchanged. + ≤-+-same : ∀ i j k → ((i +ℤ k) ≤ℤ (j +ℤ k)) ≡ (i ≤ℤ j) + ≤-+-same i j k = + trans (cong₂ _≤ℤ_ (add-parts i k) (add-parts j k)) + (trans (ord-⊖ (P i +ℕ P k) (Q i +ℕ Q k) (P j +ℕ P k) (Q j +ℕ Q k)) + (trans (cong₂ leq (rearrange (P i) (P k) (Q j) (Q k)) (rearrange (P j) (P k) (Q i) (Q k))) + (trans (leq-cancel (P k +ℕ Q k) (P i +ℕ Q j) (P j +ℕ Q i)) + (sym (ord i j))))) + where + rearrange : ∀ a k b l → (a +ℕ k) +ℕ (b +ℕ l) ≡ (k +ℕ l) +ℕ (a +ℕ b) + rearrange a k b l = trans (swap a k b l) (+comm (a +ℕ b) (k +ℕ l)) + + ≤-+ : ∀ i j k → T (i ≤ℤ j) → T ((i +ℤ k) ≤ℤ (j +ℤ k)) + ≤-+ i j k t = subst T (sym (≤-+-same i j k)) t + +intLaws : Laws intNumber +intLaws = record + { neg = neg + ; +-assoc = +-assoc + ; +-comm = +-comm + ; +-identityʳ = +-identityʳ + ; +-inverseʳ = +-inverseʳ + ; -‿def = λ a b → refl + ; ≤-refl = ≤-refl + ; ≤-trans = ≤-trans + ; ≤-total = ≤-total + ; ≤-+ = ≤-+ + } + +-- APP-2 and APP-3 for the model as it runs on the worked examples. +module OnIntegers = Applied.Cash.Proofs intNumber intLaws diff --git a/verification/proofs/agda/Applied/Missing.agda b/verification/proofs/agda/Applied/Missing.agda new file mode 100644 index 0000000..969b310 --- /dev/null +++ b/verification/proofs/agda/Applied/Missing.agda @@ -0,0 +1,229 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- APP-1 (missing propagates) and APP-4 (status never upgrades) for the +-- cohort model (Applied.Cohort), for any number structure. +-- +-- One statement carries both. `Covers u v` says that v is given with a +-- status at least u. Each theorem below says: if an output is given with +-- status u, then every input that it depends on is given, with a status at +-- least u. Read one way, an output is missing when an input it depends on +-- is missing (APP-1): it is the constructor `missing`, never a number such +-- as zero. Read the other way, an output is never more certain than an +-- input it depends on (APP-4). + +module Applied.Missing 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) renaming (_-_ to _∸_; _<_ to _<ℕ_) +open import Agda.Builtin.Sigma using (Σ; _,_) +open import Applied.Cohort +open import Applied.Status + +------------------------------------------------------------------------ +-- Lists + +-- Every element satisfies P. A function, not an indexed type, so that no +-- match needs the injectivity of _∷_ (--cubical-compatible). +All : {A : Set} → (A → Set) → List A → Set +All P [] = ⊤ +All P (x ∷ xs) = P x × All P xs + +data _⊎_ (A B : Set) : Set where + inj₁ : A → A ⊎ B + inj₂ : B → A ⊎ B + +-- Some element satisfies P. A function, not an indexed type, so that no +-- match needs the injectivity of _∷_ (--cubical-compatible). +Any : {A : Set} → (A → Set) → List A → Set +Any P [] = ⊥ +Any P (x ∷ xs) = P x ⊎ Any P xs + +All-map : ∀ {A} {P Q : A → Set} → (∀ {x} → P x → Q x) → ∀ xs → All P xs → All Q xs +All-map f [] _ = tt +All-map f (x ∷ xs) (p , ps) = f p , All-map f xs ps + +if-false : ∀ {A : Set} {b : Bool} {x y : A} → b ≡ false → (if b then x else y) ≡ y +if-false refl = refl + +------------------------------------------------------------------------ +-- Cohorts + +joined-needs : ∀ {u scale contacts conversion} → + Covers u (joined scale contacts conversion) → Covers u contacts × Covers u conversion +joined-needs c with zipWith-needs c +... | cl , cc = map-needs cl , cc + +-- The members after any number of renewals need the members who joined; +-- after at least one renewal they need the retention rate too. +renewed-joined : ∀ {u scale start retention} k → + Covers u (renewed scale start retention k) → Covers u start +renewed-joined zero c = c +renewed-joined (suc k) c = renewed-joined k (Σ.fst (zipWith-needs c)) + +renewed-retention : ∀ {u scale start retention} k → + Covers u (renewed scale start retention (suc k)) → Covers u retention +renewed-retention k c = Σ.snd (zipWith-needs c) + +-- A modelled cohort that has started needs its contacts and its +-- conversion rate, and from its first renewal its retention rate. +modelled-needs : ∀ {u scale t start contacts conversion retention} → (t <ℕ start) ≡ false → + Covers u (cohortAt scale t (modelled start contacts conversion retention)) → + Covers u contacts × Covers u conversion +modelled-needs {u} {scale} {t} {start} {contacts} {conversion} {retention} eq c = + joined-needs (renewed-joined {u} {scale} {joined scale contacts conversion} {retention} (t ∸ start) + (subst (Covers u) (if-false eq) c)) + +modelled-renewal-needs : ∀ {u scale t start contacts conversion retention} k → + (t <ℕ start) ≡ false → (t ∸ start) ≡ suc k → + Covers u (cohortAt scale t (modelled start contacts conversion retention)) → + Covers u retention +modelled-renewal-needs {u} {scale} {t} {start} {contacts} {conversion} {retention} k eq gap c = + renewed-retention {u} {scale} {joined scale contacts conversion} {retention} k + (subst (λ n → Covers u (renewed scale (joined scale contacts conversion) retention n)) gap + (subst (Covers u) (if-false eq) c)) + +-- An observed cohort that has started needs its count for the period. +observed-needs : ∀ {u scale t start counts} → (t <ℕ start) ≡ false → + Covers u (cohortAt scale t (observed start counts)) → Covers u (at (t ∸ start) counts) +observed-needs eq c = map-needs (subst (Covers _) (if-false eq) c) + +-- The active members of a period need every cohort's members. +sum-needs : ∀ {u scale t} cs → Covers u (sumAt scale t cs) → All (λ c → Covers u (cohortAt scale t c)) cs +sum-needs [] c = tt +sum-needs (x ∷ cs) c with zipWith-needs c +... | cx , rest = cx , sum-needs cs rest + +------------------------------------------------------------------------ +-- The model + +module Proofs (N : Number) where + open Number N + open Model N + + -- Kleene conjunction: a "yes" needs both sides to be a known "yes". + Yes : Status → Val Bool → Set + Yes u v = Σ Status (λ s → (v ≡ given s true) × (u ≤ˢ s)) + + Yes-weaken : ∀ {u w v} → u ≤ˢ w → Yes w v → Yes u v + Yes-weaken {u} {w} le (s , eq , le′) = s , eq , ≤ˢ-trans u w s le le′ + + private + truth : Val Bool → Bool + truth missing = false + truth (given _ b) = b + + false≢true : false ≡ true → ⊥ + false≢true () + + ⊥-elim : ∀ {A : Set} → ⊥ → A + ⊥-elim () + + ∧-yes : ∀ {x y u} → x ∧ᵏ y ≡ given u true → Yes u x × Yes u y + ∧-yes {given s true} {given t b} eq = + (s , refl , subst (λ w → w ≤ˢ s) (cong statusOr eq) (⊓-≤ˡ s t)) , + (t , cong (given t) (cong truth eq) , subst (λ w → w ≤ˢ t) (cong statusOr eq) (⊓-≤ʳ s t)) + ∧-yes {given s true} {missing} () + ∧-yes {given s false} eq = ⊥-elim (false≢true (cong truth eq)) + ∧-yes {missing} {given t false} eq = ⊥-elim (false≢true (cong truth eq)) + ∧-yes {missing} {given t true} () + ∧-yes {missing} {missing} () + + ∧-false-left : ∀ {x y s} → x ≡ given s false → x ∧ᵏ y ≡ given s false + ∧-false-left refl = refl + + ∧-false-right : ∀ {x y t} → y ≡ given t false → Σ Status (λ u → x ∧ᵏ y ≡ given u false) + ∧-false-right {given s false} refl = s , refl + ∧-false-right {given s true} {t = t} refl = s ⊓ t , refl + ∧-false-right {missing} {t = t} refl = t , refl + + module _ (i : Inputs) where + open Inputs i + open Run i + + -- Each output of a period, and the inputs it needs. `previous` is the + -- closing cash of the period before. + + members-needs : ∀ {u} t previous → Covers u (Row.members (rowAt t previous)) → + Covers u (sumAt scale t cohorts) + members-needs t previous c = map-needs c + + receipts-needs : ∀ {u} t previous → Covers u (Row.receipts (rowAt t previous)) → + Covers u price × Covers u (sumAt scale t cohorts) + receipts-needs t previous c with zipWith-needs c + ... | cp , cm = cp , map-needs cm + + payments-needs : ∀ {u} t previous → Covers u (Row.payments (rowAt t previous)) → + Covers u (at (t ∸ 1) fixed) × Covers u unitCost × Covers u (sumAt scale t cohorts) + payments-needs t previous c with zipWith-needs c + ... | cf , cv with zipWith-needs cv + ... | cu , cm = map-needs cf , cu , map-needs cm + + closing-needs : ∀ {u} t previous → Covers u (Row.closing (rowAt t previous)) → + Covers u previous × Covers u price × Covers u (at (t ∸ 1) fixed) × + Covers u unitCost × Covers u (sumAt scale t cohorts) + closing-needs t previous c with zipWith-needs c + ... | cpr , cpay with zipWith-needs cpr | payments-needs t previous cpay + ... | cprev , crec | cf , cu , cm = cprev , Σ.fst (zipWith-needs crec) , cf , cu , cm + + shortfall-needs : ∀ {u} t previous → Covers u (Row.shortfall (rowAt t previous)) → + Covers u (at (t ∸ 1) floor) × Covers u (Row.closing (rowAt t previous)) + shortfall-needs t previous c with zipWith-needs c + ... | cfl , cc = map-needs cfl , cc + + cashOk-needs : ∀ {u} t previous → Covers u (Row.cashOk (rowAt t previous)) → + Covers u (at (t ∸ 1) floor) × Covers u (Row.closing (rowAt t previous)) + cashOk-needs t previous c with zipWith-needs c + ... | cfl , cc = map-needs cfl , cc + + hours-needs : ∀ {u} t previous → Covers u (Row.hours (rowAt t previous)) → + Covers u minutes × Covers u (sumAt scale t cohorts) + hours-needs t previous c with zipWith-needs c + ... | cmin , cm = cmin , map-needs cm + + capacityOk-needs : ∀ {u} t previous → Covers u (Row.capacityOk (rowAt t previous)) → + Covers u minutes × Covers u (sumAt scale t cohorts) × Covers u (at (t ∸ 1) capacity) + capacityOk-needs t previous c with zipWith-needs c + ... | ch , ccap with hours-needs t previous ch + ... | cmin , cm = cmin , cm , map-needs ccap + + -- The first period starts from the opening cash. + opening-needs : ∀ {u} → Covers u (scaled opening) → Covers u opening + opening-needs = map-needs + + -- Missing in every period after it: once a closing balance is + -- missing, every later closing balance is missing. + closings-missing : ∀ t n → All (λ r → Row.closing r ≡ missing) (rowsFrom t n missing) + closings-missing t zero = tt + closings-missing t (suc n) = refl , closings-missing (suc t) n + + missing-persists : ∀ t n previous → Row.closing (rowAt t previous) ≡ missing → + All (λ r → Row.closing r ≡ missing) (rowsFrom (suc t) n (Row.closing (rowAt t previous))) + missing-persists t n previous eq = + subst (λ p → All (λ r → Row.closing r ≡ missing) (rowsFrom (suc t) n p)) (sym eq) (closings-missing (suc t) n) + + -- A verdict is "yes" only when every period is a known "yes", with a + -- status at least that of the verdict. + verdict-yes : ∀ {u} (f : Row → Val Bool) rs → verdict f rs ≡ given u true → All (λ r → Yes u (f r)) rs + verdict-yes f [] eq = tt + verdict-yes {u} f (r ∷ rs) eq with ∧-yes {f r} {verdict f rs} eq + ... | yr , (s , eq′ , le) = yr , All-map (λ {x} y → Yes-weaken {u} {s} {f x} le y) rs (verdict-yes f rs eq′) + + -- A known breach decides a verdict: it is "no", whatever is missing. + breach-decides : ∀ (f : Row → Val Bool) rs → + Any (λ r → Σ Status (λ s → f r ≡ given s false)) rs → + Σ Status (λ u → verdict f rs ≡ given u false) + breach-decides f [] () + breach-decides f (r ∷ rs) (inj₁ (s , eq)) = s , ∧-false-left {f r} {verdict f rs} eq + breach-decides f (r ∷ rs) (inj₂ p) with breach-decides f rs p + ... | t , eq = ∧-false-right {f r} {verdict f rs} eq + + -- The funding gap is given only when every shortfall is given, with a + -- status at least that of the gap. + gap-needs : ∀ {u} rs → Covers u (worst rs) → All (λ r → Covers u (Row.shortfall r)) rs + gap-needs [] c = tt + gap-needs (r ∷ rs) c with zipWith-needs c + ... | cs , rest = cs , gap-needs rs rest diff --git a/verification/proofs/agda/Applied/Status.agda b/verification/proofs/agda/Applied/Status.agda new file mode 100644 index 0000000..f544575 --- /dev/null +++ b/verification/proofs/agda/Applied/Status.agda @@ -0,0 +1,317 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- The order of evidence statuses, and what a given value tells about the +-- values it was computed from. Used by the proofs of APP-1 and APP-4 +-- (Applied.CohortProofs). + +module Applied.Status where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Nat using (Nat; zero; suc) +open import Agda.Builtin.Sigma using (Σ; _,_) +open import Applied.Cohort + +------------------------------------------------------------------------ +-- Logic + +record ⊤ : Set where + constructor tt + +data ⊥ : Set where + +T : Bool → Set +T true = ⊤ +T false = ⊥ + +infixr 2 _×_ +_×_ : Set → Set → Set +A × B = Σ A (λ _ → B) + +------------------------------------------------------------------------ +-- The order of statuses: illustrative < estimate < reported < verified +-- < definitional. + +rank : Status → Nat +rank illustrative = 0 +rank estimate = 1 +rank reported = 2 +rank verified = 3 +rank definitional = 4 + +_≤ᵇ_ : Nat → Nat → Bool +zero ≤ᵇ _ = true +suc m ≤ᵇ zero = false +suc m ≤ᵇ suc n = m ≤ᵇ n + +≤ᵇ-refl : ∀ n → T (n ≤ᵇ n) +≤ᵇ-refl zero = tt +≤ᵇ-refl (suc n) = ≤ᵇ-refl n + +≤ᵇ-trans : ∀ m n k → T (m ≤ᵇ n) → T (n ≤ᵇ k) → T (m ≤ᵇ k) +≤ᵇ-trans zero _ _ _ _ = tt +≤ᵇ-trans (suc m) zero _ () _ +≤ᵇ-trans (suc m) (suc n) zero _ () +≤ᵇ-trans (suc m) (suc n) (suc k) p q = ≤ᵇ-trans m n k p q + +-- s ≤ˢ t: status s is no stronger than status t. +infix 4 _≤ˢ_ +_≤ˢ_ : Status → Status → Set +s ≤ˢ t = T (rank s ≤ᵇ rank t) + +≤ˢ-refl : ∀ s → s ≤ˢ s +≤ˢ-refl s = ≤ᵇ-refl (rank s) + +≤ˢ-trans : ∀ s t u → s ≤ˢ t → t ≤ˢ u → s ≤ˢ u +≤ˢ-trans s t u = ≤ᵇ-trans (rank s) (rank t) (rank u) + +-- The meet is below each of its arguments. +⊓-≤ˡ : ∀ s t → (s ⊓ t) ≤ˢ s +⊓-≤ˡ illustrative illustrative = tt +⊓-≤ˡ illustrative estimate = tt +⊓-≤ˡ illustrative reported = tt +⊓-≤ˡ illustrative verified = tt +⊓-≤ˡ illustrative definitional = tt +⊓-≤ˡ estimate illustrative = tt +⊓-≤ˡ estimate estimate = tt +⊓-≤ˡ estimate reported = tt +⊓-≤ˡ estimate verified = tt +⊓-≤ˡ estimate definitional = tt +⊓-≤ˡ reported illustrative = tt +⊓-≤ˡ reported estimate = tt +⊓-≤ˡ reported reported = tt +⊓-≤ˡ reported verified = tt +⊓-≤ˡ reported definitional = tt +⊓-≤ˡ verified illustrative = tt +⊓-≤ˡ verified estimate = tt +⊓-≤ˡ verified reported = tt +⊓-≤ˡ verified verified = tt +⊓-≤ˡ verified definitional = tt +⊓-≤ˡ definitional illustrative = tt +⊓-≤ˡ definitional estimate = tt +⊓-≤ˡ definitional reported = tt +⊓-≤ˡ definitional verified = tt +⊓-≤ˡ definitional definitional = tt + +⊓-≤ʳ : ∀ s t → (s ⊓ t) ≤ˢ t +⊓-≤ʳ illustrative illustrative = tt +⊓-≤ʳ illustrative estimate = tt +⊓-≤ʳ illustrative reported = tt +⊓-≤ʳ illustrative verified = tt +⊓-≤ʳ illustrative definitional = tt +⊓-≤ʳ estimate illustrative = tt +⊓-≤ʳ estimate estimate = tt +⊓-≤ʳ estimate reported = tt +⊓-≤ʳ estimate verified = tt +⊓-≤ʳ estimate definitional = tt +⊓-≤ʳ reported illustrative = tt +⊓-≤ʳ reported estimate = tt +⊓-≤ʳ reported reported = tt +⊓-≤ʳ reported verified = tt +⊓-≤ʳ reported definitional = tt +⊓-≤ʳ verified illustrative = tt +⊓-≤ʳ verified estimate = tt +⊓-≤ʳ verified reported = tt +⊓-≤ʳ verified verified = tt +⊓-≤ʳ verified definitional = tt +⊓-≤ʳ definitional illustrative = tt +⊓-≤ʳ definitional estimate = tt +⊓-≤ʳ definitional reported = tt +⊓-≤ʳ definitional verified = tt +⊓-≤ʳ definitional definitional = tt + +------------------------------------------------------------------------ +-- Covers u v: the value v is given, with a status at least u. + +record Covers {A : Set} (u : Status) (v : Val A) : Set where + constructor covers + field + status : Status + value : A + isGiven : v ≡ given status value + atLeast : u ≤ˢ status + +-- A given value covers its own status. +self : ∀ {A} {s : Status} {a : A} → Covers s (given s a) +self {s = s} {a} = covers s a refl (≤ˢ-refl s) + +weaken : ∀ {A} {u w : Status} {v : Val A} → u ≤ˢ w → Covers w v → Covers u v +weaken {u = u} {w} le (covers s a eq le′) = covers s a eq (≤ˢ-trans u w s le le′) + +------------------------------------------------------------------------ +-- Equality, without injectivity of constructors (--cubical-compatible) + +sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x +sym refl = refl + +cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y +cong f refl = refl + +subst : ∀ {A : Set} (P : A → Set) {x y : A} → x ≡ y → P x → P y +subst P refl p = p + +-- The status of a given value; `definitional` for a missing one. +statusOr : ∀ {A} → Val A → Status +statusOr missing = definitional +statusOr (given s _) = s + +-- When zipWith gives a value, both arguments were given, each with a +-- status at least that of the result. +zipWith-given : ∀ {A B C} {f : A → B → C} {x : Val A} {y : Val B} {u : Status} {c : C} → + zipWith f x y ≡ given u c → Covers u x × Covers u y +zipWith-given {x = given s a} {given t b} eq = + covers s a refl (subst (λ w → w ≤ˢ s) (cong statusOr eq) (⊓-≤ˡ s t)) , + covers t b refl (subst (λ w → w ≤ˢ t) (cong statusOr eq) (⊓-≤ʳ s t)) +zipWith-given {x = given s a} {missing} () +zipWith-given {x = missing} () + +zipWith-needs : ∀ {A B C} {f : A → B → C} {x : Val A} {y : Val B} {u : Status} → + Covers u (zipWith f x y) → Covers u x × Covers u y +zipWith-needs (covers s c eq le) with zipWith-given eq +... | cx , cy = weaken le cx , weaken le cy + +map-needs : ∀ {A B} {f : A → B} {x : Val A} {u : Status} → Covers u (map f x) → Covers u x +map-needs {x = given s a} {u} (covers s′ c eq le) = + covers s a refl (subst (λ w → u ≤ˢ w) (cong statusOr (sym eq)) le) +map-needs {x = missing} (covers _ _ () _) + +-- Nothing covers a missing value. +missing-uncovered : ∀ {A} {u : Status} → Covers {A} u missing → ⊥ +missing-uncovered (covers _ _ () _) + +-- The meet is associative, and `definitional` is its unit. +⊓-assoc : ∀ s t u → (s ⊓ t) ⊓ u ≡ s ⊓ (t ⊓ u) +⊓-assoc illustrative illustrative illustrative = refl +⊓-assoc illustrative illustrative estimate = refl +⊓-assoc illustrative illustrative reported = refl +⊓-assoc illustrative illustrative verified = refl +⊓-assoc illustrative illustrative definitional = refl +⊓-assoc illustrative estimate illustrative = refl +⊓-assoc illustrative estimate estimate = refl +⊓-assoc illustrative estimate reported = refl +⊓-assoc illustrative estimate verified = refl +⊓-assoc illustrative estimate definitional = refl +⊓-assoc illustrative reported illustrative = refl +⊓-assoc illustrative reported estimate = refl +⊓-assoc illustrative reported reported = refl +⊓-assoc illustrative reported verified = refl +⊓-assoc illustrative reported definitional = refl +⊓-assoc illustrative verified illustrative = refl +⊓-assoc illustrative verified estimate = refl +⊓-assoc illustrative verified reported = refl +⊓-assoc illustrative verified verified = refl +⊓-assoc illustrative verified definitional = refl +⊓-assoc illustrative definitional illustrative = refl +⊓-assoc illustrative definitional estimate = refl +⊓-assoc illustrative definitional reported = refl +⊓-assoc illustrative definitional verified = refl +⊓-assoc illustrative definitional definitional = refl +⊓-assoc estimate illustrative illustrative = refl +⊓-assoc estimate illustrative estimate = refl +⊓-assoc estimate illustrative reported = refl +⊓-assoc estimate illustrative verified = refl +⊓-assoc estimate illustrative definitional = refl +⊓-assoc estimate estimate illustrative = refl +⊓-assoc estimate estimate estimate = refl +⊓-assoc estimate estimate reported = refl +⊓-assoc estimate estimate verified = refl +⊓-assoc estimate estimate definitional = refl +⊓-assoc estimate reported illustrative = refl +⊓-assoc estimate reported estimate = refl +⊓-assoc estimate reported reported = refl +⊓-assoc estimate reported verified = refl +⊓-assoc estimate reported definitional = refl +⊓-assoc estimate verified illustrative = refl +⊓-assoc estimate verified estimate = refl +⊓-assoc estimate verified reported = refl +⊓-assoc estimate verified verified = refl +⊓-assoc estimate verified definitional = refl +⊓-assoc estimate definitional illustrative = refl +⊓-assoc estimate definitional estimate = refl +⊓-assoc estimate definitional reported = refl +⊓-assoc estimate definitional verified = refl +⊓-assoc estimate definitional definitional = refl +⊓-assoc reported illustrative illustrative = refl +⊓-assoc reported illustrative estimate = refl +⊓-assoc reported illustrative reported = refl +⊓-assoc reported illustrative verified = refl +⊓-assoc reported illustrative definitional = refl +⊓-assoc reported estimate illustrative = refl +⊓-assoc reported estimate estimate = refl +⊓-assoc reported estimate reported = refl +⊓-assoc reported estimate verified = refl +⊓-assoc reported estimate definitional = refl +⊓-assoc reported reported illustrative = refl +⊓-assoc reported reported estimate = refl +⊓-assoc reported reported reported = refl +⊓-assoc reported reported verified = refl +⊓-assoc reported reported definitional = refl +⊓-assoc reported verified illustrative = refl +⊓-assoc reported verified estimate = refl +⊓-assoc reported verified reported = refl +⊓-assoc reported verified verified = refl +⊓-assoc reported verified definitional = refl +⊓-assoc reported definitional illustrative = refl +⊓-assoc reported definitional estimate = refl +⊓-assoc reported definitional reported = refl +⊓-assoc reported definitional verified = refl +⊓-assoc reported definitional definitional = refl +⊓-assoc verified illustrative illustrative = refl +⊓-assoc verified illustrative estimate = refl +⊓-assoc verified illustrative reported = refl +⊓-assoc verified illustrative verified = refl +⊓-assoc verified illustrative definitional = refl +⊓-assoc verified estimate illustrative = refl +⊓-assoc verified estimate estimate = refl +⊓-assoc verified estimate reported = refl +⊓-assoc verified estimate verified = refl +⊓-assoc verified estimate definitional = refl +⊓-assoc verified reported illustrative = refl +⊓-assoc verified reported estimate = refl +⊓-assoc verified reported reported = refl +⊓-assoc verified reported verified = refl +⊓-assoc verified reported definitional = refl +⊓-assoc verified verified illustrative = refl +⊓-assoc verified verified estimate = refl +⊓-assoc verified verified reported = refl +⊓-assoc verified verified verified = refl +⊓-assoc verified verified definitional = refl +⊓-assoc verified definitional illustrative = refl +⊓-assoc verified definitional estimate = refl +⊓-assoc verified definitional reported = refl +⊓-assoc verified definitional verified = refl +⊓-assoc verified definitional definitional = refl +⊓-assoc definitional illustrative illustrative = refl +⊓-assoc definitional illustrative estimate = refl +⊓-assoc definitional illustrative reported = refl +⊓-assoc definitional illustrative verified = refl +⊓-assoc definitional illustrative definitional = refl +⊓-assoc definitional estimate illustrative = refl +⊓-assoc definitional estimate estimate = refl +⊓-assoc definitional estimate reported = refl +⊓-assoc definitional estimate verified = refl +⊓-assoc definitional estimate definitional = refl +⊓-assoc definitional reported illustrative = refl +⊓-assoc definitional reported estimate = refl +⊓-assoc definitional reported reported = refl +⊓-assoc definitional reported verified = refl +⊓-assoc definitional reported definitional = refl +⊓-assoc definitional verified illustrative = refl +⊓-assoc definitional verified estimate = refl +⊓-assoc definitional verified reported = refl +⊓-assoc definitional verified verified = refl +⊓-assoc definitional verified definitional = refl +⊓-assoc definitional definitional illustrative = refl +⊓-assoc definitional definitional estimate = refl +⊓-assoc definitional definitional reported = refl +⊓-assoc definitional definitional verified = refl +⊓-assoc definitional definitional definitional = refl + +⊓-identityʳ : ∀ s → s ⊓ definitional ≡ s +⊓-identityʳ illustrative = refl +⊓-identityʳ estimate = refl +⊓-identityʳ reported = refl +⊓-identityʳ verified = refl +⊓-identityʳ definitional = refl diff --git a/verification/proofs/agda/MANIFEST b/verification/proofs/agda/MANIFEST index b4547cb..2ee9381 100644 --- a/verification/proofs/agda/MANIFEST +++ b/verification/proofs/agda/MANIFEST @@ -7,3 +7,7 @@ verification/proofs/agda|Applied/IntNumber.agda|gated| applied shelf: integer ar verification/proofs/agda|Applied/Example/Approximate.agda|gated| generated: worked example, mode approximate, one input missing verification/proofs/agda|Applied/Example/Exact.agda|gated| generated: worked example, mode exact verification/proofs/agda|Applied/Example/Simple.agda|gated| generated: worked example, mode simple +verification/proofs/agda|Applied/Status.agda|gated| applied shelf: the order of evidence statuses and what a given value needs (APP-1, APP-4) +verification/proofs/agda|Applied/Missing.agda|gated| applied shelf: APP-1 missing propagates, APP-4 status never upgrades (any number structure) +verification/proofs/agda|Applied/Cash.agda|gated| applied shelf: APP-2 cash identity, APP-3 the funding gap is sound and least (ordered abelian groups) +verification/proofs/agda|Applied/IntLaws.agda|gated| applied shelf: the integer instance is an ordered abelian group, so APP-2 and APP-3 apply to the examples