From d1569ae4cebb9a507a053e90780f59d58d55831e Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 12 Nov 2026 01:28:25 +0000 Subject: [PATCH 1/4] applied: input schema, cohort model in Agda, three worked examples (WO 4.2, 1 of 3) The first of three pull requests for WO 4.2 of the re-anchoring plan (owner rulings 2026-11-12). - Input schema (applied-systems/methods/input-schema.adoc, enforced by scripts/applied/inputs.mjs): the fields of the evidence rules, with access separate from evidence status. A missing input has the value null; the validator refuses 0 or "" for it. - Cohort model, verification/proofs/agda/Applied/Cohort.agda, over an abstract number structure. Every value is missing or given with an evidence status; an output that depends on a missing input stays missing; verdicts use Kleene conjunction. Three number modes: simple (observed counts), approximate (rates per 1000, rounded down) and exact (fractions). Mode exact multiplies every quantity by one common denominator, so all three modes run on one integer instance (Applied/IntNumber.agda). Guidance: cohort-economics/modes.adoc. - Three synthetic worked examples in JSON Lines. `just applied-build` writes one Agda module for each and the view generated/examples.adoc. Agda accepts a module only if the model computes every expected output, missing ones included. In the approximate example the retention of cohort B is missing; every value of P4 and the cash verdict stay missing. - `just applied-check` joins check-views. A golden-path control shows that the Agda gate fails when a missing output is read as zero. - APP-1 to APP-4 (missing propagates, cash identity, funding gap, status never upgrades) are recorded as open in PROOF-NEEDS. The Agda proofs and the Rocq and Lean re-proofs are the next two pull requests. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- EXPLAINME.adoc | 28 +- Justfile | 16 +- README.adoc | 8 +- applied-systems/README.adoc | 1 + .../finance/cohort-economics/README.adoc | 16 + .../examples/approximate.jsonl | 60 ++ .../cohort-economics/examples/exact.jsonl | 60 ++ .../cohort-economics/examples/simple.jsonl | 60 ++ .../cohort-economics/generated/examples.adoc | 605 ++++++++++++++++++ .../finance/cohort-economics/modes.adoc | 68 ++ applied-systems/methods/input-schema.adoc | 96 +++ .../methods/types-and-assurance.adoc | 9 +- docs/status/PROOF-NEEDS.adoc | 44 +- docs/status/PROOF-STATUS.adoc | 8 +- docs/status/ROADMAP.adoc | 34 +- mathesis_chora.deed | 3 +- scripts/applied/cohort.mjs | 333 ++++++++++ scripts/applied/inputs.mjs | 43 ++ tests/applied/applied.test.mjs | 63 ++ tests/golden/check_controls_test.sh | 15 +- verification/proofs/agda/Applied/Cohort.agda | 277 ++++++++ .../agda/Applied/Example/Approximate.agda | 112 ++++ .../proofs/agda/Applied/Example/Exact.agda | 112 ++++ .../proofs/agda/Applied/Example/Simple.agda | 112 ++++ .../proofs/agda/Applied/IntNumber.agda | 147 +++++ verification/proofs/agda/MANIFEST | 5 + 26 files changed, 2311 insertions(+), 24 deletions(-) create mode 100644 applied-systems/finance/cohort-economics/examples/approximate.jsonl create mode 100644 applied-systems/finance/cohort-economics/examples/exact.jsonl create mode 100644 applied-systems/finance/cohort-economics/examples/simple.jsonl create mode 100644 applied-systems/finance/cohort-economics/generated/examples.adoc create mode 100644 applied-systems/finance/cohort-economics/modes.adoc create mode 100644 applied-systems/methods/input-schema.adoc create mode 100644 scripts/applied/cohort.mjs create mode 100644 scripts/applied/inputs.mjs create mode 100644 tests/applied/applied.test.mjs create mode 100644 verification/proofs/agda/Applied/Cohort.agda create mode 100644 verification/proofs/agda/Applied/Example/Approximate.agda create mode 100644 verification/proofs/agda/Applied/Example/Exact.agda create mode 100644 verification/proofs/agda/Applied/Example/Simple.agda create mode 100644 verification/proofs/agda/Applied/IntNumber.agda diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index f9911f0..aff1460 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -132,15 +132,27 @@ resolution is argued, not proved. [quote, README.adoc] ____ Methods that apply mathematics to decisions, starting -with accounting and finance. Design documents only so far. +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. ____ How this is implemented:: `link:applied-systems/README.adoc[]` and its subdirectories: a management -accounting design, a decision record, an event map and evidence guidance. +accounting design, a decision record, an event map and evidence guidance. The +input schema (`link:applied-systems/methods/input-schema.adoc[]`, enforced by +`scripts/applied/inputs.mjs`) gives each input an evidence status and keeps +missing apart from zero. The cohort model +(`verification/proofs/agda/Applied/Cohort.agda`) has three number modes and +three synthetic worked examples; the Agda gate checks every expected output of +each, missing ones included, and a control in +`tests/golden/check_controls_test.sh` shows that a missing value read as zero +fails it. Caveat:: -No executable model, data schema or worked example exists yet (WO 4.2). +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 +organisation. The management-accounting design has no model yet. == Privacy by count @@ -267,8 +279,16 @@ and `_⊔_` as builtins. |- |`docs/proposals/mathesis-research-programme.adoc` |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) +|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 |=== -Proofs: 3 proven of 5; 1 argued, 1 open. The registry derives `PWG-1` for +Proofs: 3 proven of 9; 1 argued, 5 open (the token-lattice theorems count as +one). 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/Justfile b/Justfile index e41d84f..68f23be 100644 --- a/Justfile +++ b/Justfile @@ -710,8 +710,9 @@ uncloak: check: check-views check-proofs # Needs bun, network for the receipts, and MATHESIS_STANDARDS (see `registry`). -# Views current: catalogue, census tests, atlas, claims registry and bridges -check-views: catalogue-check census-test atlas-check registry-check +# Views current: catalogue, census tests, atlas, claims registry, bridges and +# the worked cohort examples +check-views: catalogue-check census-test atlas-check registry-check applied-check # Needs agda, coqc and lean, e.g. in the pinned Guix: # guix time-machine -C build/channels.scm -- shell -m build/manifest.scm -- just check-proofs @@ -776,3 +777,14 @@ registry-check: # story: just theory-ledger "THY-2 admitted after its Lean leg landed" theory-ledger note="": bun scripts/registry/claims-registry.mjs ledger {{ if note == "" { "" } else { "--note " + quote(note) } }} + +# Regenerate the Agda checks and the view of the worked cohort examples +# (applied shelf, re-anchoring plan WO 4.2) from their JSON Lines +applied-build: + bun scripts/applied/cohort.mjs build + +# Fail if a generated file of the cohort examples is stale; test the input +# schema and the example validator. Agda checks the examples in check-proofs. +applied-check: + bun scripts/applied/cohort.mjs check + bun test tests/applied/ diff --git a/README.adoc b/README.adoc index a3949a3..e4d9c7f 100644 --- a/README.adoc +++ b/README.adoc @@ -33,15 +33,17 @@ describes what is proved, where, and how strongly. pinned Guix shell. A theorem enters the theory shelf only under a stated admission rule, and a generated index lists each one with its dependant. * *Applied systems.* Methods that apply mathematics to decisions, starting - with accounting and finance. Design documents only so far. + 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. * *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, the applied -shelf tied to the evidence rules, a published atlas, receipts in more home +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 repositories, and a scheduled census. See link:docs/status/ROADMAP.adoc[the roadmap]. ==== diff --git a/applied-systems/README.adoc b/applied-systems/README.adoc index 710af40..6c36bda 100644 --- a/applied-systems/README.adoc +++ b/applied-systems/README.adoc @@ -23,6 +23,7 @@ Do not copy a private case here merely by changing its name. |link:decision-science/README.adoc[Decision science] |Event chains, uncertainty and the value of additional information. |link:organisational-design/README.adoc[Organisational design] |Capacity, role design, service safeguards and implementation constraints. |link:methods/evidence-and-assumptions.adoc[Evidence and assumptions] |Shared conventions for status, provenance, units and uncertainty. +|link:methods/input-schema.adoc[Input schema] |One record for each model input, with its evidence status; missing is never zero. |link:methods/types-and-assurance.adoc[Types and assurance] |Research questions connecting types to reliable applied models. |=== diff --git a/applied-systems/finance/cohort-economics/README.adoc b/applied-systems/finance/cohort-economics/README.adoc index e95e9ba..5ef0d02 100644 --- a/applied-systems/finance/cohort-economics/README.adoc +++ b/applied-systems/finance/cohort-economics/README.adoc @@ -27,3 +27,19 @@ Sensitivity analysis should report conversion, renewal retention and workload together with minimum cash, the period of cumulative payback (if reached), full-cost result and capacity excess. Do not call an infeasible workload case viable merely because its financial column is positive. + +== Model and worked examples + +The cohort model is `verification/proofs/agda/Applied/Cohort.agda`: active +members, receipts, payments, closing cash, the shortfall below the cash floor, +support minutes, the floor and capacity verdicts, and the funding gap. Every +value can be missing and carries an evidence status. The model has three number +modes; link:modes.adoc[Number modes] says which one to use. + +Each file in `examples/` is one synthetic worked example: its inputs, in the +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 +`docs/status/PROOF-NEEDS.adoc`. diff --git a/applied-systems/finance/cohort-economics/examples/approximate.jsonl b/applied-systems/finance/cohort-economics/examples/approximate.jsonl new file mode 100644 index 0000000..dd16d3f --- /dev/null +++ b/applied-systems/finance/cohort-economics/examples/approximate.jsonl @@ -0,0 +1,60 @@ +{"description":"Rates are whole numbers per 1000. Each step counts whole members and rounds down. The retention rate of cohort B is missing. Cohort B in P3 needs no retention, so it is known. Every value in P4 that depends on it stays missing, and so does the cash verdict. The capacity verdict is known: P3 is above capacity.","kind":"example","mode":"approximate","name":"approximate","period_length":"one month; each month end is a renewal date","periods":["P1","P2","P3","P4"],"synthetic":true,"title":"Rates per 1000, one input missing (mode approximate)"} +{"description":"The first recruitment campaign.","id":"A","kind":"cohort","start":"P1"} +{"description":"A second, smaller campaign two months later.","id":"B","kind":"cohort","start":"P3"} +{"access":"public","depends_on":[],"description":"Cash at the start of P1","evidence_status":"illustrative","id":"opening_cash","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence","value":600000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Cash received from each active member in each period","evidence_status":"illustrative","id":"price","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence per member per period","value":1500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Avoidable cost of each active member in each period","evidence_status":"illustrative","id":"unit_cost","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence per member per period","value":400,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time that each active member needs in each period","evidence_status":"illustrative","id":"support_minutes","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"minutes per member per period","value":30,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"People that the campaign of cohort A reaches","evidence_status":"illustrative","id":"A.contacts","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"people","value":2000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Contacts of cohort A who join","evidence_status":"illustrative","id":"A.conversion","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"per 1000","value":100,"verified_on":null} +{"access":"public","depends_on":[],"description":"Members of cohort A who renew at each renewal date","evidence_status":"illustrative","id":"A.retention","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"per 1000","value":850,"verified_on":null} +{"access":"public","depends_on":[],"description":"People that the campaign of cohort B reaches","evidence_status":"illustrative","id":"B.contacts","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"people","value":1500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Contacts of cohort B who join","evidence_status":"illustrative","id":"B.conversion","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"per 1000","value":80,"verified_on":null} +{"access":"public","depends_on":[],"description":"Members of cohort B who renew at each renewal date","evidence_status":"missing","id":"B.retention","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"per 1000","value":null,"verified_on":null} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P1","value":200} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P1","value":300000} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P1","value":430000} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P1","value":470000} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P1","value":-270000} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P1","value":6000} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P1","value":true} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P1","value":true} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P2","value":170} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P2","value":255000} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P2","value":418000} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P2","value":307000} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P2","value":-107000} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P2","value":5100} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P2","value":true} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P2","value":true} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P3","value":264} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P3","value":396000} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P3","value":455600} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P3","value":247400} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P3","value":-47400} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P3","value":7920} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P3","value":true} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P3","value":false} +{"evidence_status":"missing","id":"members","kind":"expected","period":"P4","value":null} +{"evidence_status":"missing","id":"receipts","kind":"expected","period":"P4","value":null} +{"evidence_status":"missing","id":"payments","kind":"expected","period":"P4","value":null} +{"evidence_status":"missing","id":"closing","kind":"expected","period":"P4","value":null} +{"evidence_status":"missing","id":"shortfall","kind":"expected","period":"P4","value":null} +{"evidence_status":"missing","id":"hours","kind":"expected","period":"P4","value":null} +{"evidence_status":"missing","id":"cash_ok","kind":"expected","period":"P4","value":null} +{"evidence_status":"missing","id":"capacity_ok","kind":"expected","period":"P4","value":null} +{"evidence_status":"missing","id":"cash_verdict","kind":"expected","period":null,"value":null} +{"evidence_status":"illustrative","id":"capacity_verdict","kind":"expected","period":null,"value":false} +{"evidence_status":"missing","id":"gap","kind":"expected","period":null,"value":null} diff --git a/applied-systems/finance/cohort-economics/examples/exact.jsonl b/applied-systems/finance/cohort-economics/examples/exact.jsonl new file mode 100644 index 0000000..c24618c --- /dev/null +++ b/applied-systems/finance/cohort-economics/examples/exact.jsonl @@ -0,0 +1,60 @@ +{"description":"Rates are exact fractions. A member count can be a fraction: it is an expected value, not a head count. Nothing is rounded, so the funding gap is exact to a fraction of a penny.","kind":"example","mode":"exact","name":"exact","period_length":"one month; each month end is a renewal date","periods":["P1","P2","P3","P4"],"synthetic":true,"title":"Exact fractions (mode exact)"} +{"description":"The first recruitment campaign.","id":"A","kind":"cohort","start":"P1"} +{"description":"A second, smaller campaign two months later.","id":"B","kind":"cohort","start":"P3"} +{"access":"public","depends_on":[],"description":"Cash at the start of P1","evidence_status":"illustrative","id":"opening_cash","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence","value":600000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Cash received from each active member in each period","evidence_status":"illustrative","id":"price","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence per member per period","value":1500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Avoidable cost of each active member in each period","evidence_status":"illustrative","id":"unit_cost","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence per member per period","value":400,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time that each active member needs in each period","evidence_status":"illustrative","id":"support_minutes","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"minutes per member per period","value":30,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"People that the campaign of cohort A reaches","evidence_status":"illustrative","id":"A.contacts","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"people","value":2000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Contacts of cohort A who join","evidence_status":"illustrative","id":"A.conversion","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"fraction","value":"1/10","verified_on":null} +{"access":"public","depends_on":[],"description":"Members of cohort A who renew at each renewal date","evidence_status":"illustrative","id":"A.retention","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"fraction","value":"17/20","verified_on":null} +{"access":"public","depends_on":[],"description":"People that the campaign of cohort B reaches","evidence_status":"illustrative","id":"B.contacts","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"people","value":1500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Contacts of cohort B who join","evidence_status":"illustrative","id":"B.conversion","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"fraction","value":"2/25","verified_on":null} +{"access":"public","depends_on":[],"description":"Members of cohort B who renew at each renewal date","evidence_status":"illustrative","id":"B.retention","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"fraction","value":"4/5","verified_on":null} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P1","value":200} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P1","value":300000} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P1","value":430000} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P1","value":470000} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P1","value":-270000} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P1","value":6000} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P1","value":true} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P1","value":true} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P2","value":170} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P2","value":255000} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P2","value":418000} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P2","value":307000} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P2","value":-107000} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P2","value":5100} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P2","value":true} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P2","value":true} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P3","value":"264.5"} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P3","value":396750} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P3","value":455800} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P3","value":247950} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P3","value":-47950} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P3","value":7935} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P3","value":true} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P3","value":false} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P4","value":"218.825"} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P4","value":"328237.5"} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P4","value":437530} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P4","value":"138657.5"} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P4","value":"61342.5"} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P4","value":"6564.75"} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P4","value":false} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P4","value":true} +{"evidence_status":"illustrative","id":"cash_verdict","kind":"expected","period":null,"value":false} +{"evidence_status":"illustrative","id":"capacity_verdict","kind":"expected","period":null,"value":false} +{"evidence_status":"illustrative","id":"gap","kind":"expected","period":null,"value":"61342.5"} diff --git a/applied-systems/finance/cohort-economics/examples/simple.jsonl b/applied-systems/finance/cohort-economics/examples/simple.jsonl new file mode 100644 index 0000000..cbd1bd4 --- /dev/null +++ b/applied-systems/finance/cohort-economics/examples/simple.jsonl @@ -0,0 +1,60 @@ +{"description":"You enter the active members that you count in each period. The model applies no rate and rounds nothing. Cash meets the floor until P4. Support time is above capacity in P3.","kind":"example","mode":"simple","name":"simple","period_length":"one month; each month end is a renewal date","periods":["P1","P2","P3","P4"],"synthetic":true,"title":"Observed counts (mode simple)"} +{"description":"The first recruitment campaign.","id":"A","kind":"cohort","start":"P1"} +{"description":"A second, smaller campaign two months later.","id":"B","kind":"cohort","start":"P3"} +{"access":"public","depends_on":[],"description":"Cash at the start of P1","evidence_status":"illustrative","id":"opening_cash","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence","value":600000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Cash received from each active member in each period","evidence_status":"illustrative","id":"price","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence per member per period","value":1500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Avoidable cost of each active member in each period","evidence_status":"illustrative","id":"unit_cost","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"pence per member per period","value":400,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time that each active member needs in each period","evidence_status":"illustrative","id":"support_minutes","kind":"input","owner":"mathesis","period":null,"source":"synthetic","unit":"minutes per member per period","value":30,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Fixed payments in the period","evidence_status":"illustrative","id":"fixed_cost","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"pence","value":350000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Agreed minimum cash at the end of the period","evidence_status":"illustrative","id":"cash_floor","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"pence","value":200000,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Support time available in the period","evidence_status":"illustrative","id":"capacity_minutes","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"minutes","value":7500,"verified_on":null} +{"access":"public","depends_on":[],"description":"Active members of cohort A","evidence_status":"illustrative","id":"A.active","kind":"input","owner":"mathesis","period":"P1","source":"synthetic","unit":"members","value":200,"verified_on":null} +{"access":"public","depends_on":[],"description":"Active members of cohort A","evidence_status":"illustrative","id":"A.active","kind":"input","owner":"mathesis","period":"P2","source":"synthetic","unit":"members","value":170,"verified_on":null} +{"access":"public","depends_on":[],"description":"Active members of cohort A","evidence_status":"illustrative","id":"A.active","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"members","value":150,"verified_on":null} +{"access":"public","depends_on":[],"description":"Active members of cohort A","evidence_status":"illustrative","id":"A.active","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"members","value":140,"verified_on":null} +{"access":"public","depends_on":[],"description":"Active members of cohort B","evidence_status":"illustrative","id":"B.active","kind":"input","owner":"mathesis","period":"P3","source":"synthetic","unit":"members","value":120,"verified_on":null} +{"access":"public","depends_on":[],"description":"Active members of cohort B","evidence_status":"illustrative","id":"B.active","kind":"input","owner":"mathesis","period":"P4","source":"synthetic","unit":"members","value":100,"verified_on":null} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P1","value":200} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P1","value":300000} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P1","value":430000} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P1","value":470000} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P1","value":-270000} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P1","value":6000} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P1","value":true} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P1","value":true} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P2","value":170} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P2","value":255000} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P2","value":418000} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P2","value":307000} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P2","value":-107000} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P2","value":5100} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P2","value":true} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P2","value":true} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P3","value":270} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P3","value":405000} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P3","value":458000} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P3","value":254000} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P3","value":-54000} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P3","value":8100} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P3","value":true} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P3","value":false} +{"evidence_status":"illustrative","id":"members","kind":"expected","period":"P4","value":240} +{"evidence_status":"illustrative","id":"receipts","kind":"expected","period":"P4","value":360000} +{"evidence_status":"illustrative","id":"payments","kind":"expected","period":"P4","value":446000} +{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P4","value":168000} +{"evidence_status":"illustrative","id":"shortfall","kind":"expected","period":"P4","value":32000} +{"evidence_status":"illustrative","id":"hours","kind":"expected","period":"P4","value":7200} +{"evidence_status":"illustrative","id":"cash_ok","kind":"expected","period":"P4","value":false} +{"evidence_status":"illustrative","id":"capacity_ok","kind":"expected","period":"P4","value":true} +{"evidence_status":"illustrative","id":"cash_verdict","kind":"expected","period":null,"value":false} +{"evidence_status":"illustrative","id":"capacity_verdict","kind":"expected","period":null,"value":false} +{"evidence_status":"illustrative","id":"gap","kind":"expected","period":null,"value":32000} diff --git a/applied-systems/finance/cohort-economics/generated/examples.adoc b/applied-systems/finance/cohort-economics/generated/examples.adoc new file mode 100644 index 0000000..fad075c --- /dev/null +++ b/applied-systems/finance/cohort-economics/generated/examples.adoc @@ -0,0 +1,605 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Generated by scripts/applied/cohort.mjs from the files in examples/. Do not edit. += Cohort model: worked examples + +Each example is synthetic and illustrative. Agda checks every output below +against the model (`verification/proofs/agda/Applied/Cohort.agda`); a missing +value stays missing. Money is in pence. link:../modes.adoc[The number modes] +say which mode to use. + +== Rates per 1000, one input missing (mode approximate) + +Mode: `approximate`. Periods: P1, P2, P3, P4 (one month; each month end is a renewal date). + +Rates are whole numbers per 1000. Each step counts whole members and rounds down. The retention rate of cohort B is missing. Cohort B in P3 needs no retention, so it is known. Every value in P4 that depends on it stays missing, and so does the cash verdict. The capacity verdict is known: P3 is above capacity. + +Cohorts: + +* A, from P1: The first recruitment campaign. +* B, from P3: A second, smaller campaign two months later. + +.Inputs +[cols="2,1,2,1,1",options="header"] +|=== +|Input |Period |Unit |Value |Status + +|Cash at the start of P1 (`opening_cash`) +|all +|pence +|600000 +|illustrative + +|Cash received from each active member in each period (`price`) +|all +|pence per member per period +|1500 +|illustrative + +|Avoidable cost of each active member in each period (`unit_cost`) +|all +|pence per member per period +|400 +|illustrative + +|Support time that each active member needs in each period (`support_minutes`) +|all +|minutes per member per period +|30 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P1 +|pence +|350000 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P2 +|pence +|350000 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P3 +|pence +|350000 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P4 +|pence +|350000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P1 +|pence +|200000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P2 +|pence +|200000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P3 +|pence +|200000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P4 +|pence +|200000 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P1 +|minutes +|7500 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P2 +|minutes +|7500 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P3 +|minutes +|7500 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P4 +|minutes +|7500 +|illustrative + +|People that the campaign of cohort A reaches (`A.contacts`) +|all +|people +|2000 +|illustrative + +|Contacts of cohort A who join (`A.conversion`) +|all +|per 1000 +|100 +|illustrative + +|Members of cohort A who renew at each renewal date (`A.retention`) +|all +|per 1000 +|850 +|illustrative + +|People that the campaign of cohort B reaches (`B.contacts`) +|all +|people +|1500 +|illustrative + +|Contacts of cohort B who join (`B.conversion`) +|all +|per 1000 +|80 +|illustrative + +|Members of cohort B who renew at each renewal date (`B.retention`) +|all +|per 1000 +|_missing_ +|missing + +|=== + +.Outputs +[cols="1,1,1,1,1,1,1,1,1",options="header"] +|=== +|Period |Members |Receipts |Payments |Closing cash |Shortfall below floor |Support minutes |Floor met |Capacity met + +|P1 +|200 +|300000 +|430000 +|470000 +|-270000 +|6000 +|yes +|yes + +|P2 +|170 +|255000 +|418000 +|307000 +|-107000 +|5100 +|yes +|yes + +|P3 +|264 +|396000 +|455600 +|247400 +|-47400 +|7920 +|yes +|no + +|P4 +|_missing_ +|_missing_ +|_missing_ +|_missing_ +|_missing_ +|_missing_ +|_missing_ +|_missing_ + +|=== + +Floor met in every period: _missing_. Capacity met in every period: no. Funding gap (the least addition to the opening cash that meets every floor): _missing_. + +== Exact fractions (mode exact) + +Mode: `exact`. Periods: P1, P2, P3, P4 (one month; each month end is a renewal date). + +Rates are exact fractions. A member count can be a fraction: it is an expected value, not a head count. Nothing is rounded, so the funding gap is exact to a fraction of a penny. + +Cohorts: + +* A, from P1: The first recruitment campaign. +* B, from P3: A second, smaller campaign two months later. + +.Inputs +[cols="2,1,2,1,1",options="header"] +|=== +|Input |Period |Unit |Value |Status + +|Cash at the start of P1 (`opening_cash`) +|all +|pence +|600000 +|illustrative + +|Cash received from each active member in each period (`price`) +|all +|pence per member per period +|1500 +|illustrative + +|Avoidable cost of each active member in each period (`unit_cost`) +|all +|pence per member per period +|400 +|illustrative + +|Support time that each active member needs in each period (`support_minutes`) +|all +|minutes per member per period +|30 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P1 +|pence +|350000 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P2 +|pence +|350000 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P3 +|pence +|350000 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P4 +|pence +|350000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P1 +|pence +|200000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P2 +|pence +|200000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P3 +|pence +|200000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P4 +|pence +|200000 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P1 +|minutes +|7500 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P2 +|minutes +|7500 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P3 +|minutes +|7500 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P4 +|minutes +|7500 +|illustrative + +|People that the campaign of cohort A reaches (`A.contacts`) +|all +|people +|2000 +|illustrative + +|Contacts of cohort A who join (`A.conversion`) +|all +|fraction +|1/10 +|illustrative + +|Members of cohort A who renew at each renewal date (`A.retention`) +|all +|fraction +|17/20 +|illustrative + +|People that the campaign of cohort B reaches (`B.contacts`) +|all +|people +|1500 +|illustrative + +|Contacts of cohort B who join (`B.conversion`) +|all +|fraction +|2/25 +|illustrative + +|Members of cohort B who renew at each renewal date (`B.retention`) +|all +|fraction +|4/5 +|illustrative + +|=== + +.Outputs +[cols="1,1,1,1,1,1,1,1,1",options="header"] +|=== +|Period |Members |Receipts |Payments |Closing cash |Shortfall below floor |Support minutes |Floor met |Capacity met + +|P1 +|200 +|300000 +|430000 +|470000 +|-270000 +|6000 +|yes +|yes + +|P2 +|170 +|255000 +|418000 +|307000 +|-107000 +|5100 +|yes +|yes + +|P3 +|264.5 +|396750 +|455800 +|247950 +|-47950 +|7935 +|yes +|no + +|P4 +|218.825 +|328237.5 +|437530 +|138657.5 +|61342.5 +|6564.75 +|no +|yes + +|=== + +Floor met in every period: no. Capacity met in every period: no. Funding gap (the least addition to the opening cash that meets every floor): 61342.5. + +== Observed counts (mode simple) + +Mode: `simple`. Periods: P1, P2, P3, P4 (one month; each month end is a renewal date). + +You enter the active members that you count in each period. The model applies no rate and rounds nothing. Cash meets the floor until P4. Support time is above capacity in P3. + +Cohorts: + +* A, from P1: The first recruitment campaign. +* B, from P3: A second, smaller campaign two months later. + +.Inputs +[cols="2,1,2,1,1",options="header"] +|=== +|Input |Period |Unit |Value |Status + +|Cash at the start of P1 (`opening_cash`) +|all +|pence +|600000 +|illustrative + +|Cash received from each active member in each period (`price`) +|all +|pence per member per period +|1500 +|illustrative + +|Avoidable cost of each active member in each period (`unit_cost`) +|all +|pence per member per period +|400 +|illustrative + +|Support time that each active member needs in each period (`support_minutes`) +|all +|minutes per member per period +|30 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P1 +|pence +|350000 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P2 +|pence +|350000 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P3 +|pence +|350000 +|illustrative + +|Fixed payments in the period (`fixed_cost`) +|P4 +|pence +|350000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P1 +|pence +|200000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P2 +|pence +|200000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P3 +|pence +|200000 +|illustrative + +|Agreed minimum cash at the end of the period (`cash_floor`) +|P4 +|pence +|200000 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P1 +|minutes +|7500 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P2 +|minutes +|7500 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P3 +|minutes +|7500 +|illustrative + +|Support time available in the period (`capacity_minutes`) +|P4 +|minutes +|7500 +|illustrative + +|Active members of cohort A (`A.active`) +|P1 +|members +|200 +|illustrative + +|Active members of cohort A (`A.active`) +|P2 +|members +|170 +|illustrative + +|Active members of cohort A (`A.active`) +|P3 +|members +|150 +|illustrative + +|Active members of cohort A (`A.active`) +|P4 +|members +|140 +|illustrative + +|Active members of cohort B (`B.active`) +|P3 +|members +|120 +|illustrative + +|Active members of cohort B (`B.active`) +|P4 +|members +|100 +|illustrative + +|=== + +.Outputs +[cols="1,1,1,1,1,1,1,1,1",options="header"] +|=== +|Period |Members |Receipts |Payments |Closing cash |Shortfall below floor |Support minutes |Floor met |Capacity met + +|P1 +|200 +|300000 +|430000 +|470000 +|-270000 +|6000 +|yes +|yes + +|P2 +|170 +|255000 +|418000 +|307000 +|-107000 +|5100 +|yes +|yes + +|P3 +|270 +|405000 +|458000 +|254000 +|-54000 +|8100 +|yes +|no + +|P4 +|240 +|360000 +|446000 +|168000 +|32000 +|7200 +|no +|yes + +|=== + +Floor met in every period: no. Capacity met in every period: no. Funding gap (the least addition to the opening cash that meets every floor): 32000. diff --git a/applied-systems/finance/cohort-economics/modes.adoc b/applied-systems/finance/cohort-economics/modes.adoc new file mode 100644 index 0000000..7723c62 --- /dev/null +++ b/applied-systems/finance/cohort-economics/modes.adoc @@ -0,0 +1,68 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Number modes of the cohort model + +The cohort model has three number modes. Each example names one mode. The +model is the same in each mode: only the way that it gets the active members +changes. Choose the mode from what you know and what you need. + +[cols="1,2,2,2",options="header"] +|=== +|Mode |You enter |The model does |Use it when + +|`simple` +|The active members that you count (or plan) in each period +|No rates and no rounding: it uses your counts as they are +|You want the plainest correct answer, or you are not sure which mode to use. +Start here. + +|`approximate` +|Contacts, and a conversion and a retention rate as whole numbers per 1000 +|Counts whole members: at each step it rounds down +|An estimate is enough, and you think in rates, for example "about 85 in 100 +renew". + +|`exact` +|Contacts, and the rates as exact fractions, for example `17/20` +|Keeps every value exact. A member count can be a fraction: it is an expected +value, not a head count +|You compare scenarios closely, or the rounding of the approximate mode +changes a decision. +|=== + +== The same model in every mode + +* Every value can be missing. An output that depends on a missing input stays + missing; it does not become zero. +* Each value has an evidence status. An output is never more certain than the + inputs that it depends on. +* A verdict ("the cash floor holds in every period") is yes, no or missing. A + known breach makes it "no", even when a later period is missing. +* Money is in pence. The funding gap is the least amount that, added to the + opening cash, keeps the cash at or above the floor at the end of every + period. + +== How the modes differ + +In mode `approximate`, a cohort with 2000 contacts and a conversion of 100 per +1000 has 200 members. With a retention of 850 per 1000, it has 170 members +after the first renewal and 144 after the second (144.5 rounded down). + +In mode `exact`, the same cohort has 170 members after the first renewal and +144.5 after the second. The half member is part of an expected value. The +model reaches this result without fractions: it multiplies every quantity by +one common denominator, works in whole numbers, and divides at the end. So +nothing is rounded at any step. + +The examples in link:generated/examples.adoc[the worked examples] use the same +costs and floors in each mode, so you can compare the results. + +== Limits + +* The period and the renewal date are the same: each period ends with a + renewal. State the period length in the example. +* A rate stays the same at each renewal. A rate that changes is not yet + modelled. +* 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. diff --git a/applied-systems/methods/input-schema.adoc b/applied-systems/methods/input-schema.adoc new file mode 100644 index 0000000..70093a8 --- /dev/null +++ b/applied-systems/methods/input-schema.adoc @@ -0,0 +1,96 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Input schema + +One record for each input of an applied model. The fields are the ones that +link:evidence-and-assumptions.adoc[Evidence and assumptions] asks for. +`scripts/applied/inputs.mjs` enforces the schema; the worked cohort examples +are its first users. Store records as JSON Lines, one record on each line, in +I-JSON serialised by JCS. + +[cols="1,1,3",options="header"] +|=== +|Field |Type |Meaning + +|`kind` +|`"input"` +|The record type. + +|`id` +|dotted name +|What the input is, for example `opening_cash` or `A.retention`. One id can +have one record for each period. + +|`description` +|text +|What the value means, in words. + +|`unit` +|text +|The unit, for example `pence` or `minutes per member per period`. + +|`period` +|text or null +|The period that the value applies to. Null when it applies to every period. + +|`source` +|text +|Where the value comes from. Every input in this repository is `synthetic`. + +|`owner` +|text +|Who answers for the value. + +|`evidence_status` +|one of the five below +|How well the value is established. + +|`verified_on` +|date or null +|The last verification date. A `verified` input must have one. + +|`depends_on` +|list of ids +|The inputs that this value is derived from. + +|`access` +|`public` or `restricted` +|Who may see the value. This is independent of the evidence status: public +does not mean verified, and restricted does not mean true. Mathesis holds +public inputs only. + +|`value` +|number, text or null +|The value. The model that reads the input says which form it takes. +|=== + +== Evidence status + +[cols="1,3",options="header"] +|=== +|Status |Meaning + +|`verified` |Checked against an identified source for a stated date and definition. +|`reported` |Attributed to a person or document; not independently established. +|`estimate` |Derived by a stated method, with uncertainty and limitations. +|`illustrative` |Invented to explore behaviour; not evidence about an organisation. +|`missing` |The value is not known. +|=== + +== Missing is not zero + +A missing input has the status `missing` and the value `null`. The validator +refuses a missing input with the value `0` or `""`, and a `null` value with any +other status. A required input that has no record at all is an error too: +write the record and mark it missing. + +An output that depends on a missing input is missing. It does not become zero. +The cohort model keeps this rule in every number mode. The rule is stated as +obligation APP-1 in link:../../docs/status/PROOF-NEEDS.adoc[the proof needs]. + +== Synthetic examples + +A public example is synthetic by construction. Its inputs are `illustrative` +(or `missing`), because invented values are not evidence about an +organisation. Its outputs are therefore `illustrative` or `missing` too: an +output is never more certain than the inputs that it depends on (obligation +APP-4). diff --git a/applied-systems/methods/types-and-assurance.adoc b/applied-systems/methods/types-and-assurance.adoc index 50a05b9..a63b623 100644 --- a/applied-systems/methods/types-and-assurance.adoc +++ b/applied-systems/methods/types-and-assurance.adoc @@ -25,4 +25,11 @@ of a causal model. Keep proof obligations and receipts separate from empirical validation. Follow the estate's canonical proof policy for any implementation; for first-party Rust, explicitly allocate Creusot/Pearlite implementation contracts and complementary Verus obligations, recording inapplicable or pending -work. This initial contribution contains no executable implementation or proof. +work. + +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 +establishes the truth of real inputs. diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 9a2213f..33c0292 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -36,13 +36,47 @@ home in Mathesis. |Open (next on the theory shelf) |Statements: `docs/proposals/mathesis-research-programme.adoc` -|To be allocated -|The invariants of the applied shelf that merit a proof -|Not chosen -|Open: not yet stated (WO 4.2) -|`applied-systems/` +|APP-1 +|Missing propagates: in the cohort model, an output that depends on a +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` + +|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 +|Agda, re-checked in Rocq and Lean +|Open: stated here, not yet in Agda (WO 4.2) +|`verification/proofs/agda/Applied/Cohort.agda` + +|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` + +|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` |=== +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. + 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 5ef49f5..809a13f 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -23,13 +23,15 @@ reader of PROOF-POLICY §8.5.1. |- |Not yet stated in a prover -|The applied invariants (WO 4.2) +|APP-1 to APP-4, the cohort model of the applied shelf (WO 4.2) |Open |- -|Not yet stated +|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 |=== -*Overall*: 1 of 3 obligations discharged; 2 open. These are counts, not a +*Overall*: 1 of 6 obligations discharged; 5 open (the token-lattice theorems +count as one). 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 0159fa8..76545b8 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -18,8 +18,8 @@ under <>. decision record, event map and shared evidence/type-assurance guidance. * No private case data, executable model, empirical validation or formal proof is claimed by this documentation contribution. -* Next: define a minimal data schema and a synthetic worked implementation; - allocate and record proof obligations when executable work begins. +* Next (2026-11-12, WO 4.2): the input schema, the cohort model in Agda and + three synthetic worked examples are in review; see the stage 4 entry. === First theory theorem (2026-11-09) @@ -158,6 +158,25 @@ One pull request that changes census rows is open at a time (atlas README, append-only, written only by `just theory-ledger`. `just registry-check` fails when the ledger is behind or a past entry changed; the `must` clause `theory-ledger-current` states the invariant (approved by the owner). + Merged (pull request 80). +* WO 4.2, the applied shelf, in three pull requests (owner rulings + 2026-11-12). This is the first: +** The input schema (`applied-systems/methods/input-schema.adoc`, enforced by + `scripts/applied/inputs.mjs`): the fields of the evidence rules, with + missing kept apart from zero. +** The cohort model, `verification/proofs/agda/Applied/Cohort.agda`, over an + abstract number structure. Three number modes (simple, approximate, + exact), with guidance in + `applied-systems/finance/cohort-economics/modes.adoc`. Mode exact works in + whole numbers over one common denominator, so all three modes run on one + integer instance. +** Three synthetic worked examples in JSON Lines. `just applied-build` + generates one Agda module for each, and the Agda gate checks every expected + output. In the approximate example one input is missing, and every output + 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. * The IANA registration drafts of DEED, K9 and k9-coordination are corrected in a separate session on the standards repository; filing is the owner's act. @@ -199,7 +218,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 merged; the theory ledger in review +|In progress: WO 4.1 and the theory ledger merged; WO 4.2 in review (1 of +3 pull requests) |5 |Scale: receipts in the home repositories, the bridge lock pilot, a @@ -222,3 +242,11 @@ scheduled census, a view of what each repository owes WO 3.3; the contract text, `must` severity `critical`, probes with "probe-deferred" accepted, amber band accepted; WO 3.4: true proof obligations only, EXPLAINME at the root, CI runs may be cited when labelled. +* Stage 4 (2026-11-11 and 2026-11-12), through the selector: all template + proofs and theory stubs removed; admissions with an append-only ledger, + written by a recipe; the ledger `must` clause; stage 4 pull requests may be + merged when every check is green. WO 4.2: cohort economics as the worked + 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. diff --git a/mathesis_chora.deed b/mathesis_chora.deed index 147b5ba..a0bf5ac 100644 --- a/mathesis_chora.deed +++ b/mathesis_chora.deed @@ -1022,7 +1022,8 @@ "verification/proofs/coq/FeatureReachability.v" "verification/proofs/lean4/FeatureReachability.lean" "EXPLAINME.adoc" - "docs/theory/admissions.jsonl" "docs/theory/ledger.jsonl" "docs/theory/generated/") + "docs/theory/admissions.jsonl" "docs/theory/ledger.jsonl" "docs/theory/generated/" + "scripts/applied/" "tests/applied/" "verification/proofs/agda/Applied/") :removed ("archetypes/" "build/docs-seed/" "build/templates/" "rsr-template-repo_chora.deed" "src/interface/" "benches/" "build/container/Containerfile" "tests/ffi_strings_test.sh" diff --git a/scripts/applied/cohort.mjs b/scripts/applied/cohort.mjs new file mode 100644 index 0000000..1eec03f --- /dev/null +++ b/scripts/applied/cohort.mjs @@ -0,0 +1,333 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// +// The worked examples of the cohort model (re-anchoring plan WO 4.2). +// +// Each file in applied-systems/finance/cohort-economics/examples/ is one +// synthetic worked example: an example record, its cohorts, its inputs (in +// the shared input schema, inputs.mjs) and the expected outputs. This script +// validates each example and writes two views of it: +// +// verification/proofs/agda/Applied/Example/.agda +// the inputs as Agda terms, and one check for each expected output. Agda +// runs the model (Applied.Cohort) and accepts the module only if every +// expected output, missing ones included, is what the model computes. +// applied-systems/finance/cohort-economics/generated/examples.adoc +// the inputs and the expected outputs as tables. +// +// usage: bun scripts/applied/cohort.mjs build | check + +import {readFile, writeFile, readdir, mkdir} from 'node:fs/promises'; +import {fileURLToPath} from 'node:url'; +import path from 'node:path'; +import {parseJsonl} from '../atlas/census-atlas.mjs'; +import {validateInput} from './inputs.mjs'; + +const root = path.resolve(path.dirname(fileURLToPath(import.meta.url)), '../..'); +export const EXAMPLES = 'applied-systems/finance/cohort-economics/examples'; +export const VIEW = 'applied-systems/finance/cohort-economics/generated/examples.adoc'; +export const AGDA_DIR = 'verification/proofs/agda/Applied/Example'; + +export const MODES = ['simple', 'approximate', 'exact']; +const COMMON = { + opening_cash: 'pence', price: 'pence per member per period', unit_cost: 'pence per member per period', + support_minutes: 'minutes per member per period', +}; +const PER_PERIOD = {fixed_cost: 'pence', cash_floor: 'pence', capacity_minutes: 'minutes'}; +const ROW_OUTPUTS = ['members', 'receipts', 'payments', 'closing', 'shortfall', 'hours', 'cash_ok', 'capacity_ok']; +const SUMMARY_OUTPUTS = ['cash_verdict', 'capacity_verdict', 'gap']; +const TRUTHS = new Set(['cash_ok', 'capacity_ok', 'cash_verdict', 'capacity_verdict']); +const SYNTHETIC = ['illustrative', 'missing']; +const EXAMPLE_FIELDS = ['description', 'kind', 'mode', 'name', 'period_length', 'periods', 'synthetic', 'title']; +const COHORT_FIELDS = ['description', 'id', 'kind', 'start']; +const EXPECTED_FIELDS = ['evidence_status', 'id', 'kind', 'period', 'value']; + +const need = (ok, message) => { + if (!ok) throw new Error(message); +}; +const text = v => typeof v === 'string' && v.trim() !== ''; +const closed = (r, fields, where) => { + for (const k of Object.keys(r)) need(fields.includes(k), `${where}: unknown field ${k}`); + for (const k of fields) need(k in r, `${where}: missing field ${k}`); +}; +const natural = v => Number.isSafeInteger(v) && v >= 0; + +// A number as an exact fraction {n, d} of BigInts, d > 0: an integer, a +// decimal string or a fraction string "n/d". +export function parseNumber(v, where) { + if (Number.isSafeInteger(v)) return {n: BigInt(v), d: 1n}; + need(typeof v === 'string', `${where}: a number is an integer, a decimal string or "n/d"`); + let m = /^(-?)(\d+)\.(\d+)$/.exec(v); + if (m) return {n: BigInt(m[1] + m[2] + m[3]), d: 10n ** BigInt(m[3].length)}; + m = /^(-?\d+)\/([1-9]\d*)$/.exec(v); + need(m, `${where}: ${JSON.stringify(v)} is not an integer, a decimal string or "n/d"`); + return {n: BigInt(m[1]), d: BigInt(m[2])}; +} + +function validateHeader(ex, name) { + need(ex?.kind === 'example', `${name}: the first record is the example record`); + closed(ex, EXAMPLE_FIELDS, `${name}: example`); + need(ex.name === name, `${name}: the example name matches the file name`); + need(MODES.includes(ex.mode), `${name}: mode is one of ${MODES.join(', ')}`); + need(ex.synthetic === true, `${name}: a public example is synthetic by construction`); + for (const k of ['title', 'description', 'period_length']) need(text(ex[k]), `${name}: ${k} is text`); + need(Array.isArray(ex.periods) && ex.periods.length > 0 && ex.periods.every(text), `${name}: periods lists period labels`); + need(new Set(ex.periods).size === ex.periods.length, `${name}: period labels are unique`); +} + +function addCohort(acc, r, where) { + closed(r, COHORT_FIELDS, where); + need(/^[A-Z][A-Za-z0-9]*$/.test(r.id), `${where}: a cohort id is a capitalised name`); + need(acc.periodIndex.has(r.start), `${where}: start is a period label`); + need(text(r.description), `${where}: description is text`); + need(!acc.cohorts.some(c => c.id === r.id), `${where}: duplicate cohort ${r.id}`); + acc.cohorts.push(r); +} + +function addInput(acc, r, where) { + validateInput(r, where); + need(r.access === 'public', `${where} (${r.id}): Mathesis holds public inputs only`); + need(SYNTHETIC.includes(r.evidence_status), + `${where} (${r.id}): a synthetic input is illustrative (or missing); it is not evidence about an organisation`); + const key = `${r.id}@${r.period}`; + need(!acc.inputs.has(key), `${where}: duplicate input ${key}`); + acc.inputs.set(key, r); +} + +function addExpected(acc, r, where) { + closed(r, EXPECTED_FIELDS, where); + const isRow = ROW_OUTPUTS.includes(r.id); + need(isRow || SUMMARY_OUTPUTS.includes(r.id), `${where}: unknown output ${r.id}`); + const periodOk = isRow ? acc.periodIndex.has(r.period) : r.period === null; + need(periodOk, `${where} (${r.id}): period is ${isRow ? 'a period label' : 'null'}`); + need(SYNTHETIC.includes(r.evidence_status), `${where} (${r.id}): an output of synthetic inputs is illustrative or missing`); + need((r.evidence_status === 'missing') === (r.value === null), `${where} (${r.id}): a missing output has the value null, and only a missing one`); + if (r.value !== null && TRUTHS.has(r.id)) need(typeof r.value === 'boolean', `${where} (${r.id}): the value is true or false`); + if (r.value !== null && !TRUTHS.has(r.id)) parseNumber(r.value, `${where} (${r.id})`); + const key = `${r.id}@${r.period}`; + need(!acc.expected.has(key), `${where}: duplicate expected output ${key}`); + acc.expected.set(key, r); +} + +const ADD = {cohort: addCohort, input: addInput, expected: addExpected}; + +// The inputs that a mode reads, each with its unit and the form of its value. +function wantedInputs(ex, cohorts, periodIndex) { + const wanted = new Map(); + for (const [id, unit] of Object.entries(COMMON)) wanted.set(`${id}@null`, {unit, form: 'integer'}); + for (const [id, unit] of Object.entries(PER_PERIOD)) for (const p of ex.periods) wanted.set(`${id}@${p}`, {unit, form: 'integer'}); + const rate = ex.mode === 'approximate' ? {unit: 'per 1000', form: 'permille'} : {unit: 'fraction', form: 'fraction'}; + for (const c of cohorts) { + if (ex.mode === 'simple') { + for (const p of ex.periods.slice(periodIndex.get(c.start) - 1)) wanted.set(`${c.id}.active@${p}`, {unit: 'members', form: 'natural'}); + } else { + wanted.set(`${c.id}.contacts@null`, {unit: 'people', form: 'natural'}); + wanted.set(`${c.id}.conversion@null`, rate); + wanted.set(`${c.id}.retention@null`, rate); + } + } + return wanted; +} + +const fractionUpToOne = v => { + const m = typeof v === 'string' && /^(\d+)\/([1-9]\d*)$/.exec(v); + return Boolean(m) && BigInt(m[1]) <= BigInt(m[2]); +}; +const FORMS = { + integer: [Number.isSafeInteger, 'an integer'], + natural: [natural, 'a whole number'], + permille: [v => natural(v) && v <= 1000, 'a whole number from 0 to 1000'], + fraction: [fractionUpToOne, 'a fraction "n/d" from 0 to 1'], +}; + +// Throw unless the records form one valid worked example; return it. +export function validateExample(records, name) { + const ex = records[0]; + validateHeader(ex, name); + const acc = {periodIndex: new Map(ex.periods.map((p, i) => [p, i + 1])), cohorts: [], inputs: new Map(), expected: new Map()}; + for (const [i, r] of records.slice(1).entries()) { + const where = `${name}: record ${i + 2}`; + need(Object.hasOwn(ADD, r.kind), `${where}: kind is cohort, input or expected`); + ADD[r.kind](acc, r, where); + } + need(acc.cohorts.length > 0, `${name}: at least one cohort`); + const wanted = wantedInputs(ex, acc.cohorts, acc.periodIndex); + for (const key of acc.inputs.keys()) need(wanted.has(key), `${name}: input ${key} is not read in mode ${ex.mode}`); + for (const [key, w] of wanted) { + const r = acc.inputs.get(key); + need(r, `${name}: input ${key} is absent; a missing input is a record with the value null`); + need(r.unit === w.unit, `${name}: input ${key} has the unit "${w.unit}"`); + const [ok, form] = FORMS[w.form]; + need(r.value === null || ok(r.value), `${name}: input ${key} is ${form}`); + } + for (const p of ex.periods) for (const id of ROW_OUTPUTS) need(acc.expected.has(`${id}@${p}`), `${name}: no expected ${id} for ${p}`); + for (const id of SUMMARY_OUTPUTS) need(acc.expected.has(`${id}@null`), `${name}: no expected ${id}`); + return {ex, ...acc}; +} + +// ---------------------------------------------------------------- Agda view + +const agdaInt = n => (n >= 0n ? `pos ${n}` : `negsuc ${-n - 1n}`); +const status = r => (r.evidence_status === 'missing' ? null : r.evidence_status); +const val = (r, term) => (r.value === null ? 'missing' : `given ${status(r)} ${term(r.value)}`); +const paren = s => (s.includes(' ') ? `(${s})` : s); +const list = items => (items.length ? `${items.map(paren).join(' ∷ ')} ∷ []` : '[]'); +const rate = (mode, v) => (mode === 'approximate' ? `(perMille ${v})` : `(fraction ${v.split('/').join(' ')})`); +const AGDA_FIELD = { + members: 'members', receipts: 'receipts', payments: 'payments', closing: 'closing', shortfall: 'shortfall', + hours: 'hours', cash_ok: 'cashOk', capacity_ok: 'capacityOk', cash_verdict: 'cashVerdict', + capacity_verdict: 'capacityVerdict', gap: 'gap', +}; + +function expect(r) { + if (r.value === null) return 'absent'; + if (typeof r.value === 'boolean') return `(truth ${r.evidence_status} ${r.value})`; + const {n, d} = parseNumber(r.value, r.id); + return `(number ${r.evidence_status} (${agdaInt(n)}) ${d})`; +} + +export const moduleName = name => name[0].toUpperCase() + name.slice(1); + +export function renderAgda(v, source) { + const {ex, cohorts, inputs, expected, periodIndex} = v; + const get = key => inputs.get(key); + const money = key => val(get(key), x => `(${agdaInt(BigInt(x))})`); + const perPeriod = id => list(ex.periods.map(p => money(`${id}@${p}`))); + const cohortTerm = c => { + const start = periodIndex.get(c.start); + if (ex.mode === 'simple') { + const counts = ex.periods.slice(start - 1).map(p => val(get(`${c.id}.active@${p}`), x => String(x))); + return `observed ${start} (${list(counts)})`; + } + const contacts = val(get(`${c.id}.contacts@null`), x => String(x)); + const r = key => val(get(key), x => rate(ex.mode, x)); + return `modelled ${start} ${paren(contacts)} ${paren(r(`${c.id}.conversion@null`))} ${paren(r(`${c.id}.retention@null`))}`; + }; + const out = [ + '{-# OPTIONS --safe --without-K --cubical-compatible #-}', + '-- SPDX-License-Identifier: MPL-2.0', + `-- Generated by scripts/applied/cohort.mjs from ${source}.`, + '-- Do not edit: change the example and run `just applied-build`.', + '--', + `-- ${ex.title} (mode ${ex.mode}). Agda accepts this module only if the`, + '-- model computes every expected output below, missing ones included.', + '', + `module Applied.Example.${moduleName(ex.name)} where`, + '', + 'open import Agda.Builtin.Bool using (Bool; true; false)', + 'open import Agda.Builtin.Equality using (_≡_; refl)', + 'open import Agda.Builtin.Int using (pos; negsuc)', + 'open import Agda.Builtin.List using (_∷_; [])', + 'open import Applied.Cohort', + 'open import Applied.IntNumber', + '', + 'inputs : Inputs', + 'inputs = record', + ` { periods = ${ex.periods.length}`, + ` ; opening = ${money('opening_cash@null')}`, + ` ; price = ${money('price@null')}`, + ` ; unitCost = ${money('unit_cost@null')}`, + ` ; minutes = ${money('support_minutes@null')}`, + ` ; fixed = ${perPeriod('fixed_cost')}`, + ` ; floor = ${perPeriod('cash_floor')}`, + ` ; capacity = ${perPeriod('capacity_minutes')}`, + ` ; cohorts = ${list(cohorts.map(cohortTerm))}`, + ' }', + '', + 'result : Result', + 'result = run inputs', + ]; + for (const p of ex.periods) { + out.push('', `-- Period ${p}`); + for (const id of ROW_OUTPUTS) { + out.push(`_ : check result ${periodIndex.get(p)} ${AGDA_FIELD[id]} ${expect(expected.get(`${id}@${p}`))} ≡ true`, '_ = refl'); + } + } + out.push('', '-- Over all periods'); + for (const id of SUMMARY_OUTPUTS) { + out.push(`_ : checkSummary result ${AGDA_FIELD[id]} ${expect(expected.get(`${id}@null`))} ≡ true`, '_ = refl'); + } + return out.join('\n') + '\n'; +} + +// --------------------------------------------------------------- AsciiDoc view + +const cell = s => String(s).replaceAll('|', String.raw`\|`).replaceAll('\n', ' '); +const shown = r => (r.value === null ? '_missing_' : typeof r.value === 'boolean' ? (r.value ? 'yes' : 'no') : String(r.value)); + +export function renderView(examples) { + const out = [ + '// SPDX-License-Identifier: CC-BY-SA-4.0', + '// Generated by scripts/applied/cohort.mjs from the files in examples/. Do not edit.', + '= Cohort model: worked examples', + '', + 'Each example is synthetic and illustrative. Agda checks every output below', + 'against the model (`verification/proofs/agda/Applied/Cohort.agda`); a missing', + 'value stays missing. Money is in pence. link:../modes.adoc[The number modes]', + 'say which mode to use.', + ]; + for (const {ex, cohorts, inputs, expected} of examples) { + out.push('', `== ${ex.title}`, '', `Mode: \`${ex.mode}\`. Periods: ${ex.periods.join(', ')} (${ex.period_length}).`, '', ex.description, ''); + out.push('Cohorts:', ''); + for (const c of cohorts) out.push(`* ${c.id}, from ${c.start}: ${c.description}`); + out.push('', '.Inputs', '[cols="2,1,2,1,1",options="header"]', '|===', '|Input |Period |Unit |Value |Status', ''); + for (const r of inputs.values()) { + out.push(`|${cell(r.description)} (\`${r.id}\`)`, `|${r.period ?? 'all'}`, `|${cell(r.unit)}`, `|${cell(shown(r))}`, `|${r.evidence_status}`, ''); + } + out.push('|===', '', '.Outputs', '[cols="1,1,1,1,1,1,1,1,1",options="header"]', '|===', + '|Period |Members |Receipts |Payments |Closing cash |Shortfall below floor |Support minutes |Floor met |Capacity met', ''); + for (const p of ex.periods) { + out.push(`|${p}`, ...ROW_OUTPUTS.map(id => `|${cell(shown(expected.get(`${id}@${p}`)))}`), ''); + } + out.push('|===', ''); + const s = id => shown(expected.get(`${id}@null`)); + out.push(`Floor met in every period: ${s('cash_verdict')}. Capacity met in every period: ${s('capacity_verdict')}. ` + + `Funding gap (the least addition to the opening cash that meets every floor): ${s('gap')}.`); + } + return out.join('\n') + '\n'; +} + +// ---------------------------------------------------------------------- CLI + +export async function loadExamples() { + const files = (await readdir(path.join(root, EXAMPLES))).filter(f => f.endsWith('.jsonl')).sort(); + need(files.length > 0, `${EXAMPLES}: no examples`); + const out = []; + for (const f of files) { + const rel = `${EXAMPLES}/${f}`; + const records = parseJsonl(await readFile(path.join(root, rel), 'utf8'), rel); + out.push({rel, v: validateExample(records, path.basename(f, '.jsonl'))}); + } + return out; +} + +export async function views() { + const examples = await loadExamples(); + const files = new Map(examples.map(({rel, v}) => [`${AGDA_DIR}/${moduleName(v.ex.name)}.agda`, renderAgda(v, rel)])); + files.set(VIEW, renderView(examples.map(e => e.v))); + return files; +} + +if (process.argv[1] && path.resolve(process.argv[1]) === fileURLToPath(import.meta.url)) { + const [cmd] = process.argv.slice(2); + try { + need(cmd === 'build' || cmd === 'check', 'usage: cohort.mjs build | check'); + const files = await views(); + const onDisk = (await readdir(path.join(root, AGDA_DIR)).catch(() => [])).map(f => `${AGDA_DIR}/${f}`).filter(f => f.endsWith('.agda')); + for (const f of onDisk) need(files.has(f), `${f} has no example; remove it or add the example`); + for (const [rel, body] of files) { + const file = path.join(root, rel); + if (cmd === 'build') { + await mkdir(path.dirname(file), {recursive: true}); + await writeFile(file, body); + } else { + const now = await readFile(file, 'utf8').catch(() => null); + need(now === body, `${rel} is stale; run: just applied-build`); + } + } + console.log(cmd === 'build' ? `wrote ${files.size} files` : `PASS: the ${files.size} generated files of the cohort examples are current`); + } catch (e) { + console.error('ERROR: ' + e.message); + process.exitCode = 1; + } +} diff --git a/scripts/applied/inputs.mjs b/scripts/applied/inputs.mjs new file mode 100644 index 0000000..bb5689c --- /dev/null +++ b/scripts/applied/inputs.mjs @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// +// The shared input schema of the applied shelf (re-anchoring plan WO 4.2). +// +// applied-systems/methods/input-schema.adoc states the schema; this module +// enforces it. One input record holds the fields that +// applied-systems/methods/evidence-and-assumptions.adoc asks for: a +// description, unit, period, source, owner, evidence status, last +// verification date and dependencies, with access as a separate field. A +// missing input has the value null: never zero. + +export const STATUSES = ['verified', 'reported', 'estimate', 'illustrative', 'missing']; +export const ACCESS = ['public', 'restricted']; +const FIELDS = ['access', 'depends_on', 'description', 'evidence_status', 'id', 'kind', 'owner', 'period', 'source', 'unit', 'value', 'verified_on']; + +const text = v => typeof v === 'string' && v.trim() !== ''; +const isDate = v => typeof v === 'string' && /^\d{4}-\d{2}-\d{2}$/.test(v); +const need = (ok, message) => { + if (!ok) throw new Error(message); +}; + +// Throw unless `r` is a well-formed input record. `where` names it in errors. +export function validateInput(r, where = 'input') { + need(r !== null && typeof r === 'object' && !Array.isArray(r), `${where}: an input is an object`); + for (const k of Object.keys(r)) need(FIELDS.includes(k), `${where}: unknown field ${k}`); + for (const k of FIELDS) need(k in r, `${where}: missing field ${k}`); + need(r.kind === 'input', `${where}: kind is "input"`); + need(typeof r.id === 'string' && /^[A-Za-z][A-Za-z0-9_]*(\.[A-Za-z][A-Za-z0-9_]*)*$/.test(r.id), `${where}: id is a dotted name`); + for (const k of ['description', 'unit', 'source', 'owner']) need(text(r[k]), `${where} (${r.id}): ${k} is text`); + need(r.period === null || text(r.period), `${where} (${r.id}): period is text or null`); + need(STATUSES.includes(r.evidence_status), `${where} (${r.id}): evidence_status is one of ${STATUSES.join(', ')}`); + need(r.verified_on === null || isDate(r.verified_on), `${where} (${r.id}): verified_on is a date or null`); + need(r.evidence_status !== 'verified' || r.verified_on !== null, `${where} (${r.id}): a verified input has a verified_on date`); + need(Array.isArray(r.depends_on) && r.depends_on.every(text), `${where} (${r.id}): depends_on lists input ids`); + need(ACCESS.includes(r.access), `${where} (${r.id}): access is one of ${ACCESS.join(', ')}`); + if (r.evidence_status === 'missing') { + need(r.value === null, `${where} (${r.id}): a missing input has the value null, not zero or text`); + } else { + need(r.value !== null && r.value !== undefined, `${where} (${r.id}): only a missing input has the value null`); + } + return r; +} diff --git a/tests/applied/applied.test.mjs b/tests/applied/applied.test.mjs new file mode 100644 index 0000000..ffb7443 --- /dev/null +++ b/tests/applied/applied.test.mjs @@ -0,0 +1,63 @@ +// SPDX-License-Identifier: MPL-2.0 +// The shared input schema and the worked cohort examples (re-anchoring plan +// WO 4.2): a missing input is null, never zero; each example is complete and +// synthetic; the generated files follow from the examples alone. +import {test, expect} from 'bun:test'; +import {readFileSync} from 'node:fs'; +import {validateInput} from '../../scripts/applied/inputs.mjs'; +import {validateExample, parseNumber, views, EXAMPLES} from '../../scripts/applied/cohort.mjs'; +import {parseJsonl} from '../../scripts/atlas/census-atlas.mjs'; + +const load = name => parseJsonl(readFileSync(new URL(`../../${EXAMPLES}/${name}.jsonl`, import.meta.url), 'utf8')); +const input = { + access: 'public', depends_on: [], description: 'Cash at the start', evidence_status: 'illustrative', id: 'opening_cash', + kind: 'input', owner: 'mathesis', period: null, source: 'synthetic', unit: 'pence', value: 1, verified_on: null, +}; + +test('the input schema accepts a well-formed input and a missing one', () => { + expect(validateInput(input)).toBe(input); + expect(validateInput({...input, evidence_status: 'missing', value: null}).value).toBeNull(); + expect(validateInput({...input, evidence_status: 'verified', verified_on: '2026-11-12'}).evidence_status).toBe('verified'); +}); + +test('the input schema keeps missing apart from zero', () => { + const bad = (r, msg) => expect(() => validateInput(r)).toThrow(msg); + bad({...input, evidence_status: 'missing', value: 0}, /value null, not zero/); + bad({...input, evidence_status: 'missing', value: ''}, /value null, not zero/); + bad({...input, value: null}, /only a missing input/); + bad({...input, evidence_status: 'verified'}, /verified_on/); + bad({...input, evidence_status: 'guessed'}, /evidence_status/); + bad({...input, access: 'secret'}, /access/); + bad({...input, extra: 1}, /unknown field/); + const {unit, ...noUnit} = input; + bad(noUnit, /missing field unit/); +}); + +test('each committed example is valid and its generated files are current', async () => { + for (const name of ['simple', 'approximate', 'exact']) expect(validateExample(load(name), name).ex.mode).toBe(name); + const files = await views(); + for (const [rel, body] of files) expect(readFileSync(new URL(`../../${rel}`, import.meta.url), 'utf8')).toBe(body); +}); + +test('the example validator fails closed', () => { + const recs = load('approximate'); + const bad = (list, msg) => expect(() => validateExample(list, 'approximate')).toThrow(msg); + const without = id => recs.filter(r => !(r.kind === 'input' && r.id === id)); + const swap = (id, change) => recs.map(r => (r.kind === 'input' && r.id === id ? {...r, ...change} : r)); + bad(without('B.retention'), /B.retention@null is absent; a missing input is a record with the value null/); + bad(swap('A.retention', {value: 1001}), /from 0 to 1000/); + bad(swap('A.retention', {evidence_status: 'reported'}), /not evidence about an organisation/); + bad(swap('A.retention', {access: 'restricted'}), /public inputs only/); + bad([{...recs[0], synthetic: false}, ...recs.slice(1)], /synthetic by construction/); + bad([{...recs[0], mode: 'exact'}, ...recs.slice(1)], /fraction/); + bad(recs.filter(r => !(r.kind === 'expected' && r.id === 'closing' && r.period === 'P4')), /no expected closing for P4/); + bad(recs.map(r => (r.kind === 'expected' && r.id === 'closing' && r.period === 'P4' ? {...r, value: 0} : r)), /a missing output has the value null/); +}); + +test('numbers parse exactly', () => { + expect(parseNumber(-3, 'x')).toEqual({n: -3n, d: 1n}); + expect(parseNumber('138657.5', 'x')).toEqual({n: 1386575n, d: 10n}); + expect(parseNumber('-17/20', 'x')).toEqual({n: -17n, d: 20n}); + expect(() => parseNumber('1/0', 'x')).toThrow(/not an integer/); + expect(() => parseNumber(1.5, 'x')).toThrow(/decimal string/); +}); diff --git a/tests/golden/check_controls_test.sh b/tests/golden/check_controls_test.sh index b1443fa..9c6daf5 100644 --- a/tests/golden/check_controls_test.sh +++ b/tests/golden/check_controls_test.sh @@ -1,8 +1,9 @@ #!/usr/bin/env bash # SPDX-License-Identifier: MPL-2.0 # Controls for the golden path (re-anchoring plan WO 2.5): `just test` fails on -# a stale view, and `just check-proofs` (a dependency of `just check`, which -# `just test` runs first) fails on a proof that does not check. +# a stale view; `just check-proofs` (a dependency of `just check`, which +# `just test` runs first) fails on a proof that does not check; and it fails +# when a worked cohort example reads a missing value as zero (WO 4.2). # # Each control runs in a copy of the working tree, so the repository is never # changed. The proof control needs agda on PATH (CI runs it in the pinned Guix). @@ -39,4 +40,14 @@ d=$(copy proof) printf '\nbroken : Set\nbroken = Set\n' >> "$d/verification/proofs/agda/FeatureReachability.agda" expect_fail "failing proof" "$d" check-proofs "FeatureReachability.agda" +# A missing value read as zero (re-anchoring plan WO 4.2): the worked example +# says that the closing cash of P4, which depends on a missing input, is 0. +# The generated Agda check then fails, because the model keeps it missing. +d=$(copy missing) +f="$d/applied-systems/finance/cohort-economics/examples/approximate.jsonl" +grep -qF '{"evidence_status":"missing","id":"closing","kind":"expected","period":"P4","value":null}' "$f" +sed -i 's/{"evidence_status":"missing","id":"closing","kind":"expected","period":"P4","value":null}/{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P4","value":0}/' "$f" +(cd "$d" && just --quiet applied-build >/dev/null) +expect_fail "missing read as zero" "$d" check-proofs "Approximate.agda" + exit "$fail" diff --git a/verification/proofs/agda/Applied/Cohort.agda b/verification/proofs/agda/Applied/Cohort.agda new file mode 100644 index 0000000..87d80bf --- /dev/null +++ b/verification/proofs/agda/Applied/Cohort.agda @@ -0,0 +1,277 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- A cohort model for the applied shelf (re-anchoring plan WO 4.2). +-- +-- What it computes. Recruitment cohorts join and renew once in each +-- period. Their active members bring receipts and cost support time. The +-- model computes, for each period: active members, receipts, payments, +-- the closing cash balance, the shortfall below the cash floor, support +-- minutes, and whether the floor and the support capacity hold. Over all +-- periods it computes a verdict for each, and the funding gap: the least +-- amount that, added to the opening cash, keeps every closing balance at +-- or above its floor. The method is +-- applied-systems/finance/cohort-economics/README.adoc. +-- +-- Missing values. Every input is `missing` or `given` with an evidence +-- status. An output is `missing` when any input that it depends on is +-- missing; it never becomes zero. Its status is never stronger than the +-- weakest input it depends on. A verdict is three-valued: a known breach +-- decides it even when other periods are missing (Kleene conjunction). +-- +-- Number modes. The arithmetic is any `Number`. A cohort is `observed` +-- (counts per period: mode simple) or `modelled` from contacts, a +-- conversion rate and a retention rate. A rate is `perMille` (mode +-- approximate: whole members, rounded down at each step) or a `fraction` +-- (mode exact). In mode exact the model multiplies every quantity by one +-- common denominator, `scaleOf`, so that each value is a whole number and +-- nothing is rounded. Each output is then that number divided by the +-- scale. +-- +-- The obligations APP-1 to APP-4 (docs/status/PROOF-NEEDS.adoc) are about +-- this module. They are open; this module states the model only. +-- +-- The import cone is this file and Agda's built-in modules. + +module Applied.Cohort where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Nat using (Nat; zero; suc; div-helper) + renaming (_+_ to _+ℕ_; _*_ to _*ℕ_; _-_ to _∸_; _<_ to _<ℕ_) + +if_then_else_ : {A : Set} → Bool → A → A → A +if true then x else y = x +if false then x else y = y + +------------------------------------------------------------------------ +-- Evidence status (applied-systems/methods/evidence-and-assumptions.adoc) + +-- From weakest to strongest. `missing` is not a status: a missing value +-- is the constructor `missing` of `Val`. `definitional` marks a value that +-- the model fixes itself (a cohort before its start, an empty sum); no +-- input carries it. +data Status : Set where + illustrative estimate reported verified definitional : Status + +-- The weaker of two statuses. +infixr 7 _⊓_ +_⊓_ : Status → Status → Status +illustrative ⊓ _ = illustrative +_ ⊓ illustrative = illustrative +estimate ⊓ _ = estimate +_ ⊓ estimate = estimate +reported ⊓ _ = reported +_ ⊓ reported = reported +verified ⊓ _ = verified +_ ⊓ verified = verified +definitional ⊓ definitional = definitional + +------------------------------------------------------------------------ +-- Values that may be missing + +data Val (A : Set) : Set where + missing : Val A + given : Status → A → Val A + +pure : {A : Set} → A → Val A +pure = given definitional + +map : {A B : Set} → (A → B) → Val A → Val B +map f missing = missing +map f (given s a) = given s (f a) + +zipWith : {A B C : Set} → (A → B → C) → Val A → Val B → Val C +zipWith f (given s a) (given t b) = given (s ⊓ t) (f a b) +zipWith f _ _ = missing + +-- Kleene conjunction: a known `false` decides the result. +infixr 6 _∧ᵏ_ +_∧ᵏ_ : Val Bool → Val Bool → Val Bool +given s false ∧ᵏ _ = given s false +given s true ∧ᵏ given t b = given (s ⊓ t) b +given s true ∧ᵏ missing = missing +missing ∧ᵏ given t false = given t false +missing ∧ᵏ _ = missing + +-- The element at a position, counted from zero; `missing` past the end. +at : {A : Set} → Nat → List (Val A) → Val A +at _ [] = missing +at zero (x ∷ _) = x +at (suc n) (_ ∷ xs) = at n xs + +------------------------------------------------------------------------ +-- Natural-number helpers + +_div_ : Nat → Nat → Nat +n div zero = zero +n div (suc m) = div-helper 0 m n m + +_^_ : Nat → Nat → Nat +b ^ zero = 1 +b ^ suc e = b *ℕ (b ^ e) + +------------------------------------------------------------------------ +-- Cohorts and rates + +data Rate : Set where + perMille : Nat → Rate -- n per 1000; whole members, rounded down + fraction : Nat → Nat → Rate -- numerator and denominator; exact + +data Cohort : Set where + -- Mode simple: the first period, and the active members in that period + -- and each one after it. + observed : Nat → List (Val Nat) → Cohort + -- Modes approximate and exact: the first period, the contacts, the + -- conversion rate and the retention rate at each renewal. + modelled : Nat → Val Nat → Val Rate → Val Rate → Cohort + +denominator : Val Rate → Nat +denominator (given _ (fraction _ d)) = d +denominator _ = 1 + +-- The common denominator of a run of `periods` periods: for each exact +-- cohort, the conversion denominator times the retention denominator to +-- the power `periods`. It is 1 when no rate is a fraction. +scaleOf : Nat → List Cohort → Nat +scaleOf periods [] = 1 +scaleOf periods (observed _ _ ∷ cs) = scaleOf periods cs +scaleOf periods (modelled _ _ c r ∷ cs) = + denominator c *ℕ (denominator r ^ periods) *ℕ scaleOf periods cs + +-- Apply a rate to a count multiplied by the scale. +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 + +-- Active members of one cohort in period t (counted from 1), multiplied by +-- the scale. +cohortAt : Nat → Nat → Cohort → Val Nat +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 + +sumAt : Nat → Nat → List Cohort → Val Nat +sumAt scale t [] = pure 0 +sumAt scale t (c ∷ cs) = zipWith _+ℕ_ (cohortAt scale t c) (sumAt scale t cs) + +------------------------------------------------------------------------ +-- The arithmetic of money, minutes and members + +record Number : Set₁ where + field + R : Set + 0# : R + _+_ : R → R → R + _-_ : R → R → R + _*_ : R → R → R + _≤ᵇ_ : R → R → Bool + fromNat : Nat → R + +------------------------------------------------------------------------ +-- The model + +module Model (N : Number) where + open Number N + + max : R → R → R + max a b = if a ≤ᵇ b then b else a + + record Inputs : Set where + field + periods : Nat + opening : Val R -- cash at the start, in pence + price : Val R -- receipts per active member per period, pence + unitCost : Val R -- avoidable cost per active member per period, pence + minutes : Val R -- support minutes per active member per period + fixed : List (Val R) -- fixed payments in each period, pence + floor : List (Val R) -- agreed cash floor at the end of each period, pence + capacity : List (Val R) -- support minutes available in each period + cohorts : List Cohort + + -- Every money, minute and member value below is multiplied by the scale. + record Row : Set where + field + members : Val R + receipts : Val R + payments : Val R + closing : Val R + shortfall : Val R -- floor minus closing; positive is a breach + hours : Val R -- support minutes needed + cashOk : Val Bool -- closing at or above the floor + capacityOk : Val Bool -- support minutes within capacity + + record Result : Set where + field + scale : Nat + rows : List Row + cashVerdict : Val Bool + capacityVerdict : Val Bool + gap : Val R -- least addition to the opening cash that meets every floor + + module Run (i : Inputs) where + open Inputs i + + scale : Nat + scale = scaleOf periods cohorts + + scaled : Val R → Val R + scaled = map (λ x → x * fromNat scale) + + -- The row of period t, after a closing balance of `previous`. + rowAt : Nat → Val R → Row + rowAt t previous = record + { members = m + ; receipts = rec + ; payments = pay + ; closing = clo + ; shortfall = zipWith _-_ flo clo + ; hours = hrs + ; cashOk = zipWith _≤ᵇ_ flo clo + ; capacityOk = zipWith _≤ᵇ_ hrs (scaled (at (t ∸ 1) capacity)) + } + where + m = map fromNat (sumAt scale t cohorts) + rec = zipWith _*_ price m + pay = zipWith _+_ (scaled (at (t ∸ 1) fixed)) (zipWith _*_ unitCost m) + clo = zipWith _-_ (zipWith _+_ previous rec) pay + hrs = zipWith _*_ minutes m + flo = scaled (at (t ∸ 1) floor) + + -- Rows from period t onwards, `left` of them. + rowsFrom : Nat → Nat → Val R → List Row + rowsFrom t zero previous = [] + rowsFrom t (suc n) previous = r ∷ rowsFrom (suc t) n (Row.closing r) + where r = rowAt t previous + + allRows : List Row + allRows = rowsFrom 1 periods (scaled opening) + + verdict : (Row → Val Bool) → List Row → Val Bool + verdict f [] = pure true + verdict f (r ∷ rs) = f r ∧ᵏ verdict f rs + + worst : List Row → Val R + worst [] = pure 0# + worst (r ∷ rs) = zipWith max (Row.shortfall r) (worst rs) + + result : Result + result = record + { scale = scale + ; rows = allRows + ; cashVerdict = verdict Row.cashOk allRows + ; capacityVerdict = verdict Row.capacityOk allRows + ; gap = worst allRows + } + + run : Inputs → Result + run i = Run.result i diff --git a/verification/proofs/agda/Applied/Example/Approximate.agda b/verification/proofs/agda/Applied/Example/Approximate.agda new file mode 100644 index 0000000..53b272c --- /dev/null +++ b/verification/proofs/agda/Applied/Example/Approximate.agda @@ -0,0 +1,112 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Generated by scripts/applied/cohort.mjs from applied-systems/finance/cohort-economics/examples/approximate.jsonl. +-- Do not edit: change the example and run `just applied-build`. +-- +-- Rates per 1000, one input missing (mode approximate) (mode approximate). Agda accepts this module only if the +-- model computes every expected output below, missing ones included. + +module Applied.Example.Approximate where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Int using (pos; negsuc) +open import Agda.Builtin.List using (_∷_; []) +open import Applied.Cohort +open import Applied.IntNumber + +inputs : Inputs +inputs = record + { periods = 4 + ; opening = given illustrative (pos 600000) + ; price = given illustrative (pos 1500) + ; unitCost = given illustrative (pos 400) + ; minutes = given illustrative (pos 30) + ; fixed = (given illustrative (pos 350000)) ∷ (given illustrative (pos 350000)) ∷ (given illustrative (pos 350000)) ∷ (given illustrative (pos 350000)) ∷ [] + ; floor = (given illustrative (pos 200000)) ∷ (given illustrative (pos 200000)) ∷ (given illustrative (pos 200000)) ∷ (given illustrative (pos 200000)) ∷ [] + ; capacity = (given illustrative (pos 7500)) ∷ (given illustrative (pos 7500)) ∷ (given illustrative (pos 7500)) ∷ (given illustrative (pos 7500)) ∷ [] + ; cohorts = (modelled 1 (given illustrative 2000) (given illustrative (perMille 100)) (given illustrative (perMille 850))) ∷ (modelled 3 (given illustrative 1500) (given illustrative (perMille 80)) missing) ∷ [] + } + +result : Result +result = run inputs + +-- Period P1 +_ : check result 1 members (number illustrative (pos 200) 1) ≡ true +_ = refl +_ : check result 1 receipts (number illustrative (pos 300000) 1) ≡ true +_ = refl +_ : check result 1 payments (number illustrative (pos 430000) 1) ≡ true +_ = refl +_ : check result 1 closing (number illustrative (pos 470000) 1) ≡ true +_ = refl +_ : check result 1 shortfall (number illustrative (negsuc 269999) 1) ≡ true +_ = refl +_ : check result 1 hours (number illustrative (pos 6000) 1) ≡ true +_ = refl +_ : check result 1 cashOk (truth illustrative true) ≡ true +_ = refl +_ : check result 1 capacityOk (truth illustrative true) ≡ true +_ = refl + +-- Period P2 +_ : check result 2 members (number illustrative (pos 170) 1) ≡ true +_ = refl +_ : check result 2 receipts (number illustrative (pos 255000) 1) ≡ true +_ = refl +_ : check result 2 payments (number illustrative (pos 418000) 1) ≡ true +_ = refl +_ : check result 2 closing (number illustrative (pos 307000) 1) ≡ true +_ = refl +_ : check result 2 shortfall (number illustrative (negsuc 106999) 1) ≡ true +_ = refl +_ : check result 2 hours (number illustrative (pos 5100) 1) ≡ true +_ = refl +_ : check result 2 cashOk (truth illustrative true) ≡ true +_ = refl +_ : check result 2 capacityOk (truth illustrative true) ≡ true +_ = refl + +-- Period P3 +_ : check result 3 members (number illustrative (pos 264) 1) ≡ true +_ = refl +_ : check result 3 receipts (number illustrative (pos 396000) 1) ≡ true +_ = refl +_ : check result 3 payments (number illustrative (pos 455600) 1) ≡ true +_ = refl +_ : check result 3 closing (number illustrative (pos 247400) 1) ≡ true +_ = refl +_ : check result 3 shortfall (number illustrative (negsuc 47399) 1) ≡ true +_ = refl +_ : check result 3 hours (number illustrative (pos 7920) 1) ≡ true +_ = refl +_ : check result 3 cashOk (truth illustrative true) ≡ true +_ = refl +_ : check result 3 capacityOk (truth illustrative false) ≡ true +_ = refl + +-- Period P4 +_ : check result 4 members absent ≡ true +_ = refl +_ : check result 4 receipts absent ≡ true +_ = refl +_ : check result 4 payments absent ≡ true +_ = refl +_ : check result 4 closing absent ≡ true +_ = refl +_ : check result 4 shortfall absent ≡ true +_ = refl +_ : check result 4 hours absent ≡ true +_ = refl +_ : check result 4 cashOk absent ≡ true +_ = refl +_ : check result 4 capacityOk absent ≡ true +_ = refl + +-- Over all periods +_ : checkSummary result cashVerdict absent ≡ true +_ = refl +_ : checkSummary result capacityVerdict (truth illustrative false) ≡ true +_ = refl +_ : checkSummary result gap absent ≡ true +_ = refl diff --git a/verification/proofs/agda/Applied/Example/Exact.agda b/verification/proofs/agda/Applied/Example/Exact.agda new file mode 100644 index 0000000..fa1695a --- /dev/null +++ b/verification/proofs/agda/Applied/Example/Exact.agda @@ -0,0 +1,112 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Generated by scripts/applied/cohort.mjs from applied-systems/finance/cohort-economics/examples/exact.jsonl. +-- Do not edit: change the example and run `just applied-build`. +-- +-- Exact fractions (mode exact) (mode exact). Agda accepts this module only if the +-- model computes every expected output below, missing ones included. + +module Applied.Example.Exact where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Int using (pos; negsuc) +open import Agda.Builtin.List using (_∷_; []) +open import Applied.Cohort +open import Applied.IntNumber + +inputs : Inputs +inputs = record + { periods = 4 + ; opening = given illustrative (pos 600000) + ; price = given illustrative (pos 1500) + ; unitCost = given illustrative (pos 400) + ; minutes = given illustrative (pos 30) + ; fixed = (given illustrative (pos 350000)) ∷ (given illustrative (pos 350000)) ∷ (given illustrative (pos 350000)) ∷ (given illustrative (pos 350000)) ∷ [] + ; floor = (given illustrative (pos 200000)) ∷ (given illustrative (pos 200000)) ∷ (given illustrative (pos 200000)) ∷ (given illustrative (pos 200000)) ∷ [] + ; capacity = (given illustrative (pos 7500)) ∷ (given illustrative (pos 7500)) ∷ (given illustrative (pos 7500)) ∷ (given illustrative (pos 7500)) ∷ [] + ; cohorts = (modelled 1 (given illustrative 2000) (given illustrative (fraction 1 10)) (given illustrative (fraction 17 20))) ∷ (modelled 3 (given illustrative 1500) (given illustrative (fraction 2 25)) (given illustrative (fraction 4 5))) ∷ [] + } + +result : Result +result = run inputs + +-- Period P1 +_ : check result 1 members (number illustrative (pos 200) 1) ≡ true +_ = refl +_ : check result 1 receipts (number illustrative (pos 300000) 1) ≡ true +_ = refl +_ : check result 1 payments (number illustrative (pos 430000) 1) ≡ true +_ = refl +_ : check result 1 closing (number illustrative (pos 470000) 1) ≡ true +_ = refl +_ : check result 1 shortfall (number illustrative (negsuc 269999) 1) ≡ true +_ = refl +_ : check result 1 hours (number illustrative (pos 6000) 1) ≡ true +_ = refl +_ : check result 1 cashOk (truth illustrative true) ≡ true +_ = refl +_ : check result 1 capacityOk (truth illustrative true) ≡ true +_ = refl + +-- Period P2 +_ : check result 2 members (number illustrative (pos 170) 1) ≡ true +_ = refl +_ : check result 2 receipts (number illustrative (pos 255000) 1) ≡ true +_ = refl +_ : check result 2 payments (number illustrative (pos 418000) 1) ≡ true +_ = refl +_ : check result 2 closing (number illustrative (pos 307000) 1) ≡ true +_ = refl +_ : check result 2 shortfall (number illustrative (negsuc 106999) 1) ≡ true +_ = refl +_ : check result 2 hours (number illustrative (pos 5100) 1) ≡ true +_ = refl +_ : check result 2 cashOk (truth illustrative true) ≡ true +_ = refl +_ : check result 2 capacityOk (truth illustrative true) ≡ true +_ = refl + +-- Period P3 +_ : check result 3 members (number illustrative (pos 2645) 10) ≡ true +_ = refl +_ : check result 3 receipts (number illustrative (pos 396750) 1) ≡ true +_ = refl +_ : check result 3 payments (number illustrative (pos 455800) 1) ≡ true +_ = refl +_ : check result 3 closing (number illustrative (pos 247950) 1) ≡ true +_ = refl +_ : check result 3 shortfall (number illustrative (negsuc 47949) 1) ≡ true +_ = refl +_ : check result 3 hours (number illustrative (pos 7935) 1) ≡ true +_ = refl +_ : check result 3 cashOk (truth illustrative true) ≡ true +_ = refl +_ : check result 3 capacityOk (truth illustrative false) ≡ true +_ = refl + +-- Period P4 +_ : check result 4 members (number illustrative (pos 218825) 1000) ≡ true +_ = refl +_ : check result 4 receipts (number illustrative (pos 3282375) 10) ≡ true +_ = refl +_ : check result 4 payments (number illustrative (pos 437530) 1) ≡ true +_ = refl +_ : check result 4 closing (number illustrative (pos 1386575) 10) ≡ true +_ = refl +_ : check result 4 shortfall (number illustrative (pos 613425) 10) ≡ true +_ = refl +_ : check result 4 hours (number illustrative (pos 656475) 100) ≡ true +_ = refl +_ : check result 4 cashOk (truth illustrative false) ≡ true +_ = refl +_ : check result 4 capacityOk (truth illustrative true) ≡ true +_ = refl + +-- Over all periods +_ : checkSummary result cashVerdict (truth illustrative false) ≡ true +_ = refl +_ : checkSummary result capacityVerdict (truth illustrative false) ≡ true +_ = refl +_ : checkSummary result gap (number illustrative (pos 613425) 10) ≡ true +_ = refl diff --git a/verification/proofs/agda/Applied/Example/Simple.agda b/verification/proofs/agda/Applied/Example/Simple.agda new file mode 100644 index 0000000..a19ab22 --- /dev/null +++ b/verification/proofs/agda/Applied/Example/Simple.agda @@ -0,0 +1,112 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Generated by scripts/applied/cohort.mjs from applied-systems/finance/cohort-economics/examples/simple.jsonl. +-- Do not edit: change the example and run `just applied-build`. +-- +-- Observed counts (mode simple) (mode simple). Agda accepts this module only if the +-- model computes every expected output below, missing ones included. + +module Applied.Example.Simple where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.Int using (pos; negsuc) +open import Agda.Builtin.List using (_∷_; []) +open import Applied.Cohort +open import Applied.IntNumber + +inputs : Inputs +inputs = record + { periods = 4 + ; opening = given illustrative (pos 600000) + ; price = given illustrative (pos 1500) + ; unitCost = given illustrative (pos 400) + ; minutes = given illustrative (pos 30) + ; fixed = (given illustrative (pos 350000)) ∷ (given illustrative (pos 350000)) ∷ (given illustrative (pos 350000)) ∷ (given illustrative (pos 350000)) ∷ [] + ; floor = (given illustrative (pos 200000)) ∷ (given illustrative (pos 200000)) ∷ (given illustrative (pos 200000)) ∷ (given illustrative (pos 200000)) ∷ [] + ; capacity = (given illustrative (pos 7500)) ∷ (given illustrative (pos 7500)) ∷ (given illustrative (pos 7500)) ∷ (given illustrative (pos 7500)) ∷ [] + ; cohorts = (observed 1 ((given illustrative 200) ∷ (given illustrative 170) ∷ (given illustrative 150) ∷ (given illustrative 140) ∷ [])) ∷ (observed 3 ((given illustrative 120) ∷ (given illustrative 100) ∷ [])) ∷ [] + } + +result : Result +result = run inputs + +-- Period P1 +_ : check result 1 members (number illustrative (pos 200) 1) ≡ true +_ = refl +_ : check result 1 receipts (number illustrative (pos 300000) 1) ≡ true +_ = refl +_ : check result 1 payments (number illustrative (pos 430000) 1) ≡ true +_ = refl +_ : check result 1 closing (number illustrative (pos 470000) 1) ≡ true +_ = refl +_ : check result 1 shortfall (number illustrative (negsuc 269999) 1) ≡ true +_ = refl +_ : check result 1 hours (number illustrative (pos 6000) 1) ≡ true +_ = refl +_ : check result 1 cashOk (truth illustrative true) ≡ true +_ = refl +_ : check result 1 capacityOk (truth illustrative true) ≡ true +_ = refl + +-- Period P2 +_ : check result 2 members (number illustrative (pos 170) 1) ≡ true +_ = refl +_ : check result 2 receipts (number illustrative (pos 255000) 1) ≡ true +_ = refl +_ : check result 2 payments (number illustrative (pos 418000) 1) ≡ true +_ = refl +_ : check result 2 closing (number illustrative (pos 307000) 1) ≡ true +_ = refl +_ : check result 2 shortfall (number illustrative (negsuc 106999) 1) ≡ true +_ = refl +_ : check result 2 hours (number illustrative (pos 5100) 1) ≡ true +_ = refl +_ : check result 2 cashOk (truth illustrative true) ≡ true +_ = refl +_ : check result 2 capacityOk (truth illustrative true) ≡ true +_ = refl + +-- Period P3 +_ : check result 3 members (number illustrative (pos 270) 1) ≡ true +_ = refl +_ : check result 3 receipts (number illustrative (pos 405000) 1) ≡ true +_ = refl +_ : check result 3 payments (number illustrative (pos 458000) 1) ≡ true +_ = refl +_ : check result 3 closing (number illustrative (pos 254000) 1) ≡ true +_ = refl +_ : check result 3 shortfall (number illustrative (negsuc 53999) 1) ≡ true +_ = refl +_ : check result 3 hours (number illustrative (pos 8100) 1) ≡ true +_ = refl +_ : check result 3 cashOk (truth illustrative true) ≡ true +_ = refl +_ : check result 3 capacityOk (truth illustrative false) ≡ true +_ = refl + +-- Period P4 +_ : check result 4 members (number illustrative (pos 240) 1) ≡ true +_ = refl +_ : check result 4 receipts (number illustrative (pos 360000) 1) ≡ true +_ = refl +_ : check result 4 payments (number illustrative (pos 446000) 1) ≡ true +_ = refl +_ : check result 4 closing (number illustrative (pos 168000) 1) ≡ true +_ = refl +_ : check result 4 shortfall (number illustrative (pos 32000) 1) ≡ true +_ = refl +_ : check result 4 hours (number illustrative (pos 7200) 1) ≡ true +_ = refl +_ : check result 4 cashOk (truth illustrative false) ≡ true +_ = refl +_ : check result 4 capacityOk (truth illustrative true) ≡ true +_ = refl + +-- Over all periods +_ : checkSummary result cashVerdict (truth illustrative false) ≡ true +_ = refl +_ : checkSummary result capacityVerdict (truth illustrative false) ≡ true +_ = refl +_ : checkSummary result gap (number illustrative (pos 32000) 1) ≡ true +_ = refl diff --git a/verification/proofs/agda/Applied/IntNumber.agda b/verification/proofs/agda/Applied/IntNumber.agda new file mode 100644 index 0000000..c358e8a --- /dev/null +++ b/verification/proofs/agda/Applied/IntNumber.agda @@ -0,0 +1,147 @@ +{-# OPTIONS --safe --without-K --cubical-compatible #-} +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Integer arithmetic for the cohort model (Applied.Cohort), and the +-- checks that the generated worked examples use. All three number modes +-- run on these integers: mode exact multiplies every value by a common +-- denominator first. Each operation uses Agda's built-in natural-number +-- primitives, so large values check quickly. + +module Applied.IntNumber where + +open import Agda.Builtin.Bool using (Bool; true; false) +open import Agda.Builtin.Int using (Int; pos; negsuc) +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Nat using (Nat; zero; suc) + renaming (_+_ to _+ℕ_; _*_ to _*ℕ_; _-_ to _∸_; _<_ to _<ℕ_; _==_ to _==ℕ_) +open import Applied.Cohort + +------------------------------------------------------------------------ +-- Integers + +_⊖_ : Nat → Nat → Int +m ⊖ n = if m <ℕ n then negsuc ((n ∸ m) ∸ 1) else pos (m ∸ n) + +neg : Int → Int +neg (pos zero) = pos zero +neg (pos (suc n)) = negsuc n +neg (negsuc n) = pos (suc n) + +_+ℤ_ : Int → Int → Int +pos m +ℤ pos n = pos (m +ℕ n) +pos m +ℤ negsuc n = m ⊖ suc n +negsuc m +ℤ pos n = n ⊖ suc m +negsuc m +ℤ negsuc n = negsuc (suc (m +ℕ n)) + +_-ℤ_ : Int → Int → Int +a -ℤ b = a +ℤ neg b + +_*ℤ_ : Int → Int → Int +pos m *ℤ pos n = pos (m *ℕ n) +pos m *ℤ negsuc n = neg (pos (m *ℕ suc n)) +negsuc m *ℤ pos n = neg (pos (suc m *ℕ n)) +negsuc m *ℤ negsuc n = pos (suc m *ℕ suc n) + +_≤ℤ_ : Int → Int → Bool +pos m ≤ℤ pos n = m <ℕ suc n +pos m ≤ℤ negsuc n = false +negsuc m ≤ℤ pos n = true +negsuc m ≤ℤ negsuc n = n <ℕ suc m + +_==ℤ_ : Int → Int → Bool +pos m ==ℤ pos n = m ==ℕ n +negsuc m ==ℤ negsuc n = m ==ℕ n +_ ==ℤ _ = false + +intNumber : Number +intNumber = record + { R = Int + ; 0# = pos 0 + ; _+_ = _+ℤ_ + ; _-_ = _-ℤ_ + ; _*_ = _*ℤ_ + ; _≤ᵇ_ = _≤ℤ_ + ; fromNat = pos + } + +open Model intNumber public + +------------------------------------------------------------------------ +-- Checks for the worked examples + +_&&_ : Bool → Bool → Bool +true && b = b +false && _ = false + +sameStatus : Status → Status → Bool +sameStatus illustrative illustrative = true +sameStatus estimate estimate = true +sameStatus reported reported = true +sameStatus verified verified = true +sameStatus definitional definitional = true +sameStatus _ _ = false + +sameBool : Bool → Bool → Bool +sameBool true true = true +sameBool false false = true +sameBool _ _ = false + +-- An expected output of a worked example: absent (missing), a number +-- n / d with its status, or a truth value with its status. +data Expect : Set where + absent : Expect + number : Status → Int → Nat → Expect + truth : Status → Bool → Expect + +-- A computed value, multiplied by `scale`, agrees with an expectation. +agrees : Nat → Val Int → Expect → Bool +agrees scale missing absent = true +agrees scale (given s x) (number t n d) = + sameStatus s t && ((x *ℤ pos d) ==ℤ (n *ℤ pos scale)) +agrees _ _ _ = false + +agreesB : Val Bool → Expect → Bool +agreesB missing absent = true +agreesB (given s b) (truth t c) = sameStatus s t && sameBool b c +agreesB _ _ = false + +data Field : Set where + members receipts payments closing shortfall hours : Field + cashOk capacityOk : Field + +-- The value of one field in period t (counted from 1) agrees with an +-- expectation; false when the period does not exist. +check : Result → Nat → Field → Expect → Bool +check res t f e = inRange t (Result.rows res) && field' f (pick t (Result.rows res)) + where + inRange : Nat → List Row → Bool + inRange zero _ = false + inRange (suc zero) (_ ∷ _) = true + inRange (suc (suc n)) (_ ∷ rs) = inRange (suc n) rs + inRange _ [] = false + pick : Nat → List Row → Row + pick _ [] = record + { members = missing ; receipts = missing ; payments = missing + ; closing = missing ; shortfall = missing ; hours = missing + ; cashOk = missing ; capacityOk = missing } + pick (suc zero) (r ∷ _) = r + pick (suc n) (_ ∷ rs) = pick n rs + pick zero (r ∷ _) = r + field' : Field → Row → Bool + field' members r = agrees (Result.scale res) (Row.members r) e + field' receipts r = agrees (Result.scale res) (Row.receipts r) e + field' payments r = agrees (Result.scale res) (Row.payments r) e + field' closing r = agrees (Result.scale res) (Row.closing r) e + field' shortfall r = agrees (Result.scale res) (Row.shortfall r) e + field' hours r = agrees (Result.scale res) (Row.hours r) e + field' cashOk r = agreesB (Row.cashOk r) e + field' capacityOk r = agreesB (Row.capacityOk r) e + +data Summary : Set where + cashVerdict capacityVerdict gap : Summary + +checkSummary : Result → Summary → Expect → Bool +checkSummary res cashVerdict e = agreesB (Result.cashVerdict res) e +checkSummary res capacityVerdict e = agreesB (Result.capacityVerdict res) e +checkSummary res gap e = agrees (Result.scale res) (Result.gap res) e diff --git a/verification/proofs/agda/MANIFEST b/verification/proofs/agda/MANIFEST index 16863db..b4547cb 100644 --- a/verification/proofs/agda/MANIFEST +++ b/verification/proofs/agda/MANIFEST @@ -2,3 +2,8 @@ # Format: ||gated|quarantine| # Prior check (2026-07-17): agda --safe only; full 2026-11 policy pending CI. verification/proofs/agda|FeatureReachability.agda|gated| additive features: reachability monotone in the requested set (no library imports) +verification/proofs/agda|Applied/Cohort.agda|gated| applied shelf: the cohort model, missing values and evidence status (WO 4.2; Agda.Builtin only) +verification/proofs/agda|Applied/IntNumber.agda|gated| applied shelf: integer arithmetic of the cohort model and the checks of its worked examples +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 From cfce30d287baec61c6332b7920b4693728e268cb Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 12 Nov 2026 01:30:27 +0000 Subject: [PATCH 2/4] applied: answer the SonarCloud style findings on the generator The 20 findings on PR 81 were style only (the quality gate passed): Sets for membership tests, no nested template literals or nested ternaries, String in place of x => String(x), replaceAll, one push call, \w in the id pattern, and Promise.all in place of await in a loop. The generated files are byte-for-byte the same. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- scripts/applied/cohort.mjs | 69 +++++++++++++++++++++----------------- scripts/applied/inputs.mjs | 6 ++-- 2 files changed, 42 insertions(+), 33 deletions(-) diff --git a/scripts/applied/cohort.mjs b/scripts/applied/cohort.mjs index 1eec03f..a7598b6 100644 --- a/scripts/applied/cohort.mjs +++ b/scripts/applied/cohort.mjs @@ -35,13 +35,14 @@ const COMMON = { }; const PER_PERIOD = {fixed_cost: 'pence', cash_floor: 'pence', capacity_minutes: 'minutes'}; const ROW_OUTPUTS = ['members', 'receipts', 'payments', 'closing', 'shortfall', 'hours', 'cash_ok', 'capacity_ok']; -const SUMMARY_OUTPUTS = ['cash_verdict', 'capacity_verdict', 'gap']; +const SUMMARY_OUTPUTS = new Set(['cash_verdict', 'capacity_verdict', 'gap']); const TRUTHS = new Set(['cash_ok', 'capacity_ok', 'cash_verdict', 'capacity_verdict']); -const SYNTHETIC = ['illustrative', 'missing']; +const SYNTHETIC = new Set(['illustrative', 'missing']); const EXAMPLE_FIELDS = ['description', 'kind', 'mode', 'name', 'period_length', 'periods', 'synthetic', 'title']; const COHORT_FIELDS = ['description', 'id', 'kind', 'start']; const EXPECTED_FIELDS = ['evidence_status', 'id', 'kind', 'period', 'value']; +const keyOf = (id, period) => `${id}@${period}`; const need = (ok, message) => { if (!ok) throw new Error(message); }; @@ -87,7 +88,7 @@ function addCohort(acc, r, where) { function addInput(acc, r, where) { validateInput(r, where); need(r.access === 'public', `${where} (${r.id}): Mathesis holds public inputs only`); - need(SYNTHETIC.includes(r.evidence_status), + need(SYNTHETIC.has(r.evidence_status), `${where} (${r.id}): a synthetic input is illustrative (or missing); it is not evidence about an organisation`); const key = `${r.id}@${r.period}`; need(!acc.inputs.has(key), `${where}: duplicate input ${key}`); @@ -97,10 +98,10 @@ function addInput(acc, r, where) { function addExpected(acc, r, where) { closed(r, EXPECTED_FIELDS, where); const isRow = ROW_OUTPUTS.includes(r.id); - need(isRow || SUMMARY_OUTPUTS.includes(r.id), `${where}: unknown output ${r.id}`); + need(isRow || SUMMARY_OUTPUTS.has(r.id), `${where}: unknown output ${r.id}`); const periodOk = isRow ? acc.periodIndex.has(r.period) : r.period === null; need(periodOk, `${where} (${r.id}): period is ${isRow ? 'a period label' : 'null'}`); - need(SYNTHETIC.includes(r.evidence_status), `${where} (${r.id}): an output of synthetic inputs is illustrative or missing`); + need(SYNTHETIC.has(r.evidence_status), `${where} (${r.id}): an output of synthetic inputs is illustrative or missing`); need((r.evidence_status === 'missing') === (r.value === null), `${where} (${r.id}): a missing output has the value null, and only a missing one`); if (r.value !== null && TRUTHS.has(r.id)) need(typeof r.value === 'boolean', `${where} (${r.id}): the value is true or false`); if (r.value !== null && !TRUTHS.has(r.id)) parseNumber(r.value, `${where} (${r.id})`); @@ -172,7 +173,7 @@ const status = r => (r.evidence_status === 'missing' ? null : r.evidence_status) const val = (r, term) => (r.value === null ? 'missing' : `given ${status(r)} ${term(r.value)}`); const paren = s => (s.includes(' ') ? `(${s})` : s); const list = items => (items.length ? `${items.map(paren).join(' ∷ ')} ∷ []` : '[]'); -const rate = (mode, v) => (mode === 'approximate' ? `(perMille ${v})` : `(fraction ${v.split('/').join(' ')})`); +const rate = (mode, v) => (mode === 'approximate' ? `(perMille ${v})` : `(fraction ${v.replaceAll('/', ' ')})`); const AGDA_FIELD = { members: 'members', receipts: 'receipts', payments: 'payments', closing: 'closing', shortfall: 'shortfall', hours: 'hours', cash_ok: 'cashOk', capacity_ok: 'capacityOk', cash_verdict: 'cashVerdict', @@ -196,12 +197,14 @@ export function renderAgda(v, source) { const cohortTerm = c => { const start = periodIndex.get(c.start); if (ex.mode === 'simple') { - const counts = ex.periods.slice(start - 1).map(p => val(get(`${c.id}.active@${p}`), x => String(x))); + const counts = ex.periods.slice(start - 1).map(p => val(get(keyOf(`${c.id}.active`, p)), String)); return `observed ${start} (${list(counts)})`; } - const contacts = val(get(`${c.id}.contacts@null`), x => String(x)); + const contacts = val(get(keyOf(`${c.id}.contacts`, null)), String); const r = key => val(get(key), x => rate(ex.mode, x)); - return `modelled ${start} ${paren(contacts)} ${paren(r(`${c.id}.conversion@null`))} ${paren(r(`${c.id}.retention@null`))}`; + const conversion = paren(r(keyOf(`${c.id}.conversion`, null))); + const retention = paren(r(keyOf(`${c.id}.retention`, null))); + return `modelled ${start} ${paren(contacts)} ${conversion} ${retention}`; }; const out = [ '{-# OPTIONS --safe --without-K --cubical-compatible #-}', @@ -240,12 +243,14 @@ export function renderAgda(v, source) { for (const p of ex.periods) { out.push('', `-- Period ${p}`); for (const id of ROW_OUTPUTS) { - out.push(`_ : check result ${periodIndex.get(p)} ${AGDA_FIELD[id]} ${expect(expected.get(`${id}@${p}`))} ≡ true`, '_ = refl'); + const e = expect(expected.get(keyOf(id, p))); + out.push(`_ : check result ${periodIndex.get(p)} ${AGDA_FIELD[id]} ${e} ≡ true`, '_ = refl'); } } out.push('', '-- Over all periods'); for (const id of SUMMARY_OUTPUTS) { - out.push(`_ : checkSummary result ${AGDA_FIELD[id]} ${expect(expected.get(`${id}@null`))} ≡ true`, '_ = refl'); + const e = expect(expected.get(keyOf(id, null))); + out.push(`_ : checkSummary result ${AGDA_FIELD[id]} ${e} ≡ true`, '_ = refl'); } return out.join('\n') + '\n'; } @@ -253,7 +258,12 @@ export function renderAgda(v, source) { // --------------------------------------------------------------- AsciiDoc view const cell = s => String(s).replaceAll('|', String.raw`\|`).replaceAll('\n', ' '); -const shown = r => (r.value === null ? '_missing_' : typeof r.value === 'boolean' ? (r.value ? 'yes' : 'no') : String(r.value)); +const shown = r => { + if (r.value === null) return '_missing_'; + if (r.value === true) return 'yes'; + if (r.value === false) return 'no'; + return String(r.value); +}; export function renderView(examples) { const out = [ @@ -268,8 +278,7 @@ export function renderView(examples) { ]; for (const {ex, cohorts, inputs, expected} of examples) { out.push('', `== ${ex.title}`, '', `Mode: \`${ex.mode}\`. Periods: ${ex.periods.join(', ')} (${ex.period_length}).`, '', ex.description, ''); - out.push('Cohorts:', ''); - for (const c of cohorts) out.push(`* ${c.id}, from ${c.start}: ${c.description}`); + out.push('Cohorts:', '', ...cohorts.map(c => `* ${c.id}, from ${c.start}: ${c.description}`)); out.push('', '.Inputs', '[cols="2,1,2,1,1",options="header"]', '|===', '|Input |Period |Unit |Value |Status', ''); for (const r of inputs.values()) { out.push(`|${cell(r.description)} (\`${r.id}\`)`, `|${r.period ?? 'all'}`, `|${cell(r.unit)}`, `|${cell(shown(r))}`, `|${r.evidence_status}`, ''); @@ -277,7 +286,7 @@ export function renderView(examples) { out.push('|===', '', '.Outputs', '[cols="1,1,1,1,1,1,1,1,1",options="header"]', '|===', '|Period |Members |Receipts |Payments |Closing cash |Shortfall below floor |Support minutes |Floor met |Capacity met', ''); for (const p of ex.periods) { - out.push(`|${p}`, ...ROW_OUTPUTS.map(id => `|${cell(shown(expected.get(`${id}@${p}`)))}`), ''); + out.push(`|${p}`, ...ROW_OUTPUTS.map(id => `|${cell(shown(expected.get(keyOf(id, p))))}`), ''); } out.push('|===', ''); const s = id => shown(expected.get(`${id}@null`)); @@ -292,13 +301,11 @@ export function renderView(examples) { export async function loadExamples() { const files = (await readdir(path.join(root, EXAMPLES))).filter(f => f.endsWith('.jsonl')).sort(); need(files.length > 0, `${EXAMPLES}: no examples`); - const out = []; - for (const f of files) { + return Promise.all(files.map(async f => { const rel = `${EXAMPLES}/${f}`; const records = parseJsonl(await readFile(path.join(root, rel), 'utf8'), rel); - out.push({rel, v: validateExample(records, path.basename(f, '.jsonl'))}); - } - return out; + return {rel, v: validateExample(records, path.basename(f, '.jsonl'))}; + })); } export async function views() { @@ -308,6 +315,17 @@ export async function views() { return files; } +async function write(rel, body) { + const file = path.join(root, rel); + await mkdir(path.dirname(file), {recursive: true}); + await writeFile(file, body); +} + +async function current(rel, body) { + const now = await readFile(path.join(root, rel), 'utf8').catch(() => null); + need(now === body, `${rel} is stale; run: just applied-build`); +} + if (process.argv[1] && path.resolve(process.argv[1]) === fileURLToPath(import.meta.url)) { const [cmd] = process.argv.slice(2); try { @@ -315,16 +333,7 @@ if (process.argv[1] && path.resolve(process.argv[1]) === fileURLToPath(import.me const files = await views(); const onDisk = (await readdir(path.join(root, AGDA_DIR)).catch(() => [])).map(f => `${AGDA_DIR}/${f}`).filter(f => f.endsWith('.agda')); for (const f of onDisk) need(files.has(f), `${f} has no example; remove it or add the example`); - for (const [rel, body] of files) { - const file = path.join(root, rel); - if (cmd === 'build') { - await mkdir(path.dirname(file), {recursive: true}); - await writeFile(file, body); - } else { - const now = await readFile(file, 'utf8').catch(() => null); - need(now === body, `${rel} is stale; run: just applied-build`); - } - } + await Promise.all([...files].map(([rel, body]) => (cmd === 'build' ? write(rel, body) : current(rel, body)))); console.log(cmd === 'build' ? `wrote ${files.size} files` : `PASS: the ${files.size} generated files of the cohort examples are current`); } catch (e) { console.error('ERROR: ' + e.message); diff --git a/scripts/applied/inputs.mjs b/scripts/applied/inputs.mjs index bb5689c..f4e5be3 100644 --- a/scripts/applied/inputs.mjs +++ b/scripts/applied/inputs.mjs @@ -12,7 +12,7 @@ export const STATUSES = ['verified', 'reported', 'estimate', 'illustrative', 'missing']; export const ACCESS = ['public', 'restricted']; -const FIELDS = ['access', 'depends_on', 'description', 'evidence_status', 'id', 'kind', 'owner', 'period', 'source', 'unit', 'value', 'verified_on']; +const FIELDS = new Set(['access', 'depends_on', 'description', 'evidence_status', 'id', 'kind', 'owner', 'period', 'source', 'unit', 'value', 'verified_on']); const text = v => typeof v === 'string' && v.trim() !== ''; const isDate = v => typeof v === 'string' && /^\d{4}-\d{2}-\d{2}$/.test(v); @@ -23,10 +23,10 @@ const need = (ok, message) => { // Throw unless `r` is a well-formed input record. `where` names it in errors. export function validateInput(r, where = 'input') { need(r !== null && typeof r === 'object' && !Array.isArray(r), `${where}: an input is an object`); - for (const k of Object.keys(r)) need(FIELDS.includes(k), `${where}: unknown field ${k}`); + for (const k of Object.keys(r)) need(FIELDS.has(k), `${where}: unknown field ${k}`); for (const k of FIELDS) need(k in r, `${where}: missing field ${k}`); need(r.kind === 'input', `${where}: kind is "input"`); - need(typeof r.id === 'string' && /^[A-Za-z][A-Za-z0-9_]*(\.[A-Za-z][A-Za-z0-9_]*)*$/.test(r.id), `${where}: id is a dotted name`); + need(typeof r.id === 'string' && /^[A-Za-z]\w*(\.[A-Za-z]\w*)*$/.test(r.id), `${where}: id is a dotted name`); for (const k of ['description', 'unit', 'source', 'owner']) need(text(r[k]), `${where} (${r.id}): ${k} is text`); need(r.period === null || text(r.period), `${where} (${r.id}): period is text or null`); need(STATUSES.includes(r.evidence_status), `${where} (${r.id}): evidence_status is one of ${STATUSES.join(', ')}`); From ac7fc87ad899dc149d52e50a3891bce2bdace5c5 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 12 Nov 2026 01:41:32 +0000 Subject: [PATCH 3/4] applied: close seven CodeRabbit findings on the schema and the examples - inputs.mjs: verified_on must be a real calendar date (not 2026-02-31 or 2026-13-01); each depends_on entry must be a dotted input id; a non-missing value must be a number or text. - cohort.mjs: an input of a public example must have the source "synthetic"; support_minutes and capacity_minutes are whole numbers (negative minutes could pass a capacity check); an example name is lower case, so no two examples share an Agda module name. - check_controls_test.sh: the missing-read-as-zero control now matches the failing row "Applied/Example/Approximate.agda FAIL", not just the module name. - The two remaining SonarCloud findings: one push call in the view. The new negative tests fail on the previous code and pass on this one. The generated files are unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- scripts/applied/cohort.mjs | 18 +++++++++++++----- scripts/applied/inputs.mjs | 16 ++++++++++++---- tests/applied/applied.test.mjs | 9 +++++++++ tests/golden/check_controls_test.sh | 2 +- 4 files changed, 35 insertions(+), 10 deletions(-) diff --git a/scripts/applied/cohort.mjs b/scripts/applied/cohort.mjs index a7598b6..33bf114 100644 --- a/scripts/applied/cohort.mjs +++ b/scripts/applied/cohort.mjs @@ -38,6 +38,8 @@ const ROW_OUTPUTS = ['members', 'receipts', 'payments', 'closing', 'shortfall', const SUMMARY_OUTPUTS = new Set(['cash_verdict', 'capacity_verdict', 'gap']); const TRUTHS = new Set(['cash_ok', 'capacity_ok', 'cash_verdict', 'capacity_verdict']); const SYNTHETIC = new Set(['illustrative', 'missing']); +// Support time cannot be negative; money can. +const MINUTES = new Set(['support_minutes', 'capacity_minutes']); const EXAMPLE_FIELDS = ['description', 'kind', 'mode', 'name', 'period_length', 'periods', 'synthetic', 'title']; const COHORT_FIELDS = ['description', 'id', 'kind', 'start']; const EXPECTED_FIELDS = ['evidence_status', 'id', 'kind', 'period', 'value']; @@ -69,6 +71,8 @@ function validateHeader(ex, name) { need(ex?.kind === 'example', `${name}: the first record is the example record`); closed(ex, EXAMPLE_FIELDS, `${name}: example`); need(ex.name === name, `${name}: the example name matches the file name`); + // Lower case only, so that no two examples get the same Agda module name. + need(/^[a-z][a-z0-9]*$/.test(name), `${name}: an example name is lower-case letters and digits`); need(MODES.includes(ex.mode), `${name}: mode is one of ${MODES.join(', ')}`); need(ex.synthetic === true, `${name}: a public example is synthetic by construction`); for (const k of ['title', 'description', 'period_length']) need(text(ex[k]), `${name}: ${k} is text`); @@ -88,6 +92,7 @@ function addCohort(acc, r, where) { function addInput(acc, r, where) { validateInput(r, where); need(r.access === 'public', `${where} (${r.id}): Mathesis holds public inputs only`); + need(r.source === 'synthetic', `${where} (${r.id}): the source of an input of a public example is "synthetic"`); need(SYNTHETIC.has(r.evidence_status), `${where} (${r.id}): a synthetic input is illustrative (or missing); it is not evidence about an organisation`); const key = `${r.id}@${r.period}`; @@ -115,8 +120,9 @@ const ADD = {cohort: addCohort, input: addInput, expected: addExpected}; // The inputs that a mode reads, each with its unit and the form of its value. function wantedInputs(ex, cohorts, periodIndex) { const wanted = new Map(); - for (const [id, unit] of Object.entries(COMMON)) wanted.set(`${id}@null`, {unit, form: 'integer'}); - for (const [id, unit] of Object.entries(PER_PERIOD)) for (const p of ex.periods) wanted.set(`${id}@${p}`, {unit, form: 'integer'}); + const form = id => (MINUTES.has(id) ? 'natural' : 'integer'); + for (const [id, unit] of Object.entries(COMMON)) wanted.set(keyOf(id, null), {unit, form: form(id)}); + for (const [id, unit] of Object.entries(PER_PERIOD)) for (const p of ex.periods) wanted.set(keyOf(id, p), {unit, form: form(id)}); const rate = ex.mode === 'approximate' ? {unit: 'per 1000', form: 'permille'} : {unit: 'fraction', form: 'fraction'}; for (const c of cohorts) { if (ex.mode === 'simple') { @@ -277,9 +283,11 @@ export function renderView(examples) { 'say which mode to use.', ]; for (const {ex, cohorts, inputs, expected} of examples) { - out.push('', `== ${ex.title}`, '', `Mode: \`${ex.mode}\`. Periods: ${ex.periods.join(', ')} (${ex.period_length}).`, '', ex.description, ''); - out.push('Cohorts:', '', ...cohorts.map(c => `* ${c.id}, from ${c.start}: ${c.description}`)); - out.push('', '.Inputs', '[cols="2,1,2,1,1",options="header"]', '|===', '|Input |Period |Unit |Value |Status', ''); + out.push( + '', `== ${ex.title}`, '', `Mode: \`${ex.mode}\`. Periods: ${ex.periods.join(', ')} (${ex.period_length}).`, '', ex.description, '', + 'Cohorts:', '', ...cohorts.map(c => `* ${c.id}, from ${c.start}: ${c.description}`), + '', '.Inputs', '[cols="2,1,2,1,1",options="header"]', '|===', '|Input |Period |Unit |Value |Status', '', + ); for (const r of inputs.values()) { out.push(`|${cell(r.description)} (\`${r.id}\`)`, `|${r.period ?? 'all'}`, `|${cell(r.unit)}`, `|${cell(shown(r))}`, `|${r.evidence_status}`, ''); } diff --git a/scripts/applied/inputs.mjs b/scripts/applied/inputs.mjs index f4e5be3..6ea717e 100644 --- a/scripts/applied/inputs.mjs +++ b/scripts/applied/inputs.mjs @@ -15,7 +15,14 @@ export const ACCESS = ['public', 'restricted']; const FIELDS = new Set(['access', 'depends_on', 'description', 'evidence_status', 'id', 'kind', 'owner', 'period', 'source', 'unit', 'value', 'verified_on']); const text = v => typeof v === 'string' && v.trim() !== ''; -const isDate = v => typeof v === 'string' && /^\d{4}-\d{2}-\d{2}$/.test(v); +// A calendar date YYYY-MM-DD that exists (not 2026-02-31). +const isDate = v => { + if (typeof v !== 'string' || !/^\d{4}-\d{2}-\d{2}$/.test(v)) return false; + const d = new Date(`${v}T00:00:00Z`); + return !Number.isNaN(d.getTime()) && d.toISOString().startsWith(v); +}; +const isId = v => typeof v === 'string' && /^[A-Za-z]\w*(\.[A-Za-z]\w*)*$/.test(v); +const isValue = v => (typeof v === 'number' && Number.isFinite(v)) || typeof v === 'string'; const need = (ok, message) => { if (!ok) throw new Error(message); }; @@ -26,18 +33,19 @@ export function validateInput(r, where = 'input') { for (const k of Object.keys(r)) need(FIELDS.has(k), `${where}: unknown field ${k}`); for (const k of FIELDS) need(k in r, `${where}: missing field ${k}`); need(r.kind === 'input', `${where}: kind is "input"`); - need(typeof r.id === 'string' && /^[A-Za-z]\w*(\.[A-Za-z]\w*)*$/.test(r.id), `${where}: id is a dotted name`); + need(isId(r.id), `${where}: id is a dotted name`); for (const k of ['description', 'unit', 'source', 'owner']) need(text(r[k]), `${where} (${r.id}): ${k} is text`); need(r.period === null || text(r.period), `${where} (${r.id}): period is text or null`); need(STATUSES.includes(r.evidence_status), `${where} (${r.id}): evidence_status is one of ${STATUSES.join(', ')}`); need(r.verified_on === null || isDate(r.verified_on), `${where} (${r.id}): verified_on is a date or null`); need(r.evidence_status !== 'verified' || r.verified_on !== null, `${where} (${r.id}): a verified input has a verified_on date`); - need(Array.isArray(r.depends_on) && r.depends_on.every(text), `${where} (${r.id}): depends_on lists input ids`); + need(Array.isArray(r.depends_on) && r.depends_on.every(isId), `${where} (${r.id}): depends_on lists input ids (dotted names)`); need(ACCESS.includes(r.access), `${where} (${r.id}): access is one of ${ACCESS.join(', ')}`); if (r.evidence_status === 'missing') { need(r.value === null, `${where} (${r.id}): a missing input has the value null, not zero or text`); } else { - need(r.value !== null && r.value !== undefined, `${where} (${r.id}): only a missing input has the value null`); + need(r.value !== null, `${where} (${r.id}): only a missing input has the value null`); + need(isValue(r.value), `${where} (${r.id}): the value is a number or text`); } return r; } diff --git a/tests/applied/applied.test.mjs b/tests/applied/applied.test.mjs index ffb7443..7b209a4 100644 --- a/tests/applied/applied.test.mjs +++ b/tests/applied/applied.test.mjs @@ -29,6 +29,11 @@ test('the input schema keeps missing apart from zero', () => { bad({...input, evidence_status: 'guessed'}, /evidence_status/); bad({...input, access: 'secret'}, /access/); bad({...input, extra: 1}, /unknown field/); + bad({...input, evidence_status: 'verified', verified_on: '2026-02-31'}, /verified_on is a date/); + bad({...input, evidence_status: 'verified', verified_on: '2026-13-01'}, /verified_on is a date/); + bad({...input, depends_on: ['???']}, /depends_on lists input ids/); + bad({...input, value: true}, /a number or text/); + bad({...input, value: {n: 1}}, /a number or text/); const {unit, ...noUnit} = input; bad(noUnit, /missing field unit/); }); @@ -48,6 +53,10 @@ test('the example validator fails closed', () => { bad(swap('A.retention', {value: 1001}), /from 0 to 1000/); bad(swap('A.retention', {evidence_status: 'reported'}), /not evidence about an organisation/); bad(swap('A.retention', {access: 'restricted'}), /public inputs only/); + bad(swap('A.retention', {source: 'organisation ledger'}), /"synthetic"/); + bad(swap('support_minutes', {value: -2}), /support_minutes@null is a whole number/); + bad(recs.map(r => (r.kind === 'input' && r.id === 'capacity_minutes' && r.period === 'P2' ? {...r, value: -1} : r)), /capacity_minutes@P2 is a whole number/); + expect(() => validateExample([{...recs[0], name: 'Approximate'}, ...recs.slice(1)], 'Approximate')).toThrow(/lower-case/); bad([{...recs[0], synthetic: false}, ...recs.slice(1)], /synthetic by construction/); bad([{...recs[0], mode: 'exact'}, ...recs.slice(1)], /fraction/); bad(recs.filter(r => !(r.kind === 'expected' && r.id === 'closing' && r.period === 'P4')), /no expected closing for P4/); diff --git a/tests/golden/check_controls_test.sh b/tests/golden/check_controls_test.sh index 9c6daf5..30914db 100644 --- a/tests/golden/check_controls_test.sh +++ b/tests/golden/check_controls_test.sh @@ -48,6 +48,6 @@ f="$d/applied-systems/finance/cohort-economics/examples/approximate.jsonl" grep -qF '{"evidence_status":"missing","id":"closing","kind":"expected","period":"P4","value":null}' "$f" sed -i 's/{"evidence_status":"missing","id":"closing","kind":"expected","period":"P4","value":null}/{"evidence_status":"illustrative","id":"closing","kind":"expected","period":"P4","value":0}/' "$f" (cd "$d" && just --quiet applied-build >/dev/null) -expect_fail "missing read as zero" "$d" check-proofs "Approximate.agda" +expect_fail "missing read as zero" "$d" check-proofs "Applied/Example/Approximate.agda FAIL" exit "$fail" From 9709a546ffb4699d0e57bc42a29d37731c66c045 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 12 Nov 2026 01:49:39 +0000 Subject: [PATCH 4/4] roadmap: record the licence of the JSON Lines data files as an open item CodeRabbit asked for SPDX sidecars on the three example files. No JSON Lines data file in the repository declares a licence. Owner ruling 2026-11-12: one REUSE.toml rule at the root for all of them, written by the owner (doctrine 6). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7Zo9dheFQzYYWV49hAk --- docs/status/ROADMAP.adoc | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 76545b8..a11fafe 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -177,6 +177,10 @@ One pull request that changes census rows is open at a time (atlas README, 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. +* 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 + licence declaration is a manual, owner-only change). * The IANA registration drafts of DEED, K9 and k9-coordination are corrected in a separate session on the standards repository; filing is the owner's act.