Skip to content

Commit 48591a3

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(SafeDateTime): discharge the 5-line stub — real machine-checked proofs (#132) (#28)
**Refs** hyperpolymath/standards#124 and hyperpolymath/standards#132. **NOT Closes** — the 88 single-file `Safe*` modules without `Proofs.idr`, and the ledger's named overclaim modules (SafeDigest constant-time, SafeArchive, SafeCBOR, SafeLRU, SafeConsensus, …) remain OWED under #132. This PR discharges only the named "stubs first" CRITICAL recommendation. Draft / human-gated. Build is the only oracle. ### What `src/Proven/SafeDateTime/Proofs.idr` was a **5-line header-only stub** — flagged CRITICAL in `PROOF-NEEDS.md` ("proof absence disguised as presence") and named in the ledger's top recommendation: > **Stubs first** — populate or delete the misleading `SafeCommand` / `SafeDateTime` `Proofs.idr`; a stub is worse than an honest absence. `SafeCommand` was discharged by proven#21; this PR discharges `SafeDateTime`, **closing the audited stub class** (`PROOF-NEEDS.md` honest-count `2 → 0`). The new `Proofs.idr` ships three genuine, machine-checked theorems about the actual `SafeDateTime` exported surface. `idris2 0.8.0 --check` returns exit 0, `%default total` holds, and there are **no `believe_me` / `idris_crash` / `assert_*` / `%default partial` / holes**: - **`daysInMonthLowerBound` / `daysInMonthUpperBound` / `daysInMonthNonZero`** — `daysInMonth y m` is always in the Gregorian-calendar band `28..31` (so non-zero — no degenerate month that could underflow day arithmetic or an indexer). This is the concrete content of the module's "overflow protection" claim. Per-month `Refl`, plus a `with (isLeapYear y)` split for February. - **`makeDateSound`** — soundness of the `makeDate` smart constructor: > `makeDate y mn d = Just dt -> dateGuard dt.year dt.month dt.day = True` Proof inverts the `Maybe` do-block: `with (natToMonth mn)` (the `Nothing` branch contradicts `Just dt` via `absurd`); then `with (dateGuard y m d) proof gEq`. The `True` branch fixes `dt = MkDate y m d` by `case prf of Refl =>`, transporting `gEq` onto `dt`'s own fields by record-projection reduction. The `False` branch is again `Nothing = Just dt`, absurd. This is the **genuine content** of "validated via smart constructors" / "safe parsing without exceptions" — `makeDate` cannot manufacture an out-of-range date. ### Verification ``` $ export IDRIS2_PREFIX=/.../idris2/0.8.0 $ export IDRIS2_PACKAGE_PATH=$IDRIS2_PREFIX/idris2-0.8.0 $ cd src && idris2 --check Proven/SafeDateTime/Proofs.idr 1/6: Building Proven.Core 2/6: Building Proven.SafeDateTime.Types 3/6: Building Proven.SafeDateTime.Parse 4/6: Building Proven.SafeDateTime.Zones 5/6: Building Proven.SafeDateTime 6/6: Building Proven.SafeDateTime.Proofs $ echo $? 0 ``` `Proven.SafeDateTime.Proofs` is already enumerated in `proven.ipkg`, so the new body builds in CI alongside the rest of the library. ### Ledger update `PROOF-NEEDS.md`: - "Honest counts" stub-count `2 → 0` (both audited stubs discharged: SafeCommand by proven#21, SafeDateTime by this PR). - "Stubs — proof absence disguised as presence (CRITICAL)" table reframed as historical/closed. - Priority list item #1 ("Stubs first") marked done for the audited set. The rest of #132 (88 single-file `Safe*` modules without `Proofs.idr`; ledger-named security overclaims SafeDigest constant-time, SafeArchive, SafeCBOR, SafeLRU, SafeConsensus, etc.; sibling-audited SafeMCP/SafeOAuth/SafeWebAuthn/SafeWebSocket/SafeWebhook/SafeCapability/SafeAttestation/SafeJWK/SafeSecretShare class) is untouched and remains OWED — hence **NOT Closes #132**. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 536d9e4 commit 48591a3

2 files changed

Lines changed: 135 additions & 10 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@
3535
| Bucket | Count |
3636
|--------|------:|
3737
| Safe\* directories with a companion `Proofs.idr` | 41 |
38-
| — of which are **stubs** (header only, no theorem) → treat as UNPROVEN | 2 (`SafeCommand` 8 ln, `SafeDateTime` 5 ln) |
38+
| — of which are **stubs** (header only, no theorem) → treat as UNPROVEN | **0** (`SafeCommand` discharged by proven#21; `SafeDateTime` discharged on branch `proof-debt/standards-132-safedatetime-stub`) |
3939
| Single-file `src/Proven/Safe*.idr` modules (no `Proofs.idr` dir) | 133 |
4040
| — single-file modules shipping a safety/security **doc claim** | **76** |
4141

@@ -148,17 +148,22 @@ SafeShell, SafeString, SafeTOML, SafeUrl, SafeXML, SafeYAML — **plus**
148148
SafeOrdering (single-file, one discharged theorem). These are *claimed*
149149
proven; their `Proofs.idr` bodies are not re-verified by this pass.
150150

151-
## Stubs — proof absence disguised as presence (CRITICAL)
151+
## Stubs — proof absence disguised as presence (CRITICAL) — *now empty*
152152

153-
| Module | State | Risk |
154-
|--------|-------|------|
155-
| **SafeCommand** | `Proofs.idr` 8 ln, header only; doc claims escaping/injection proofs that do not exist | CRITICAL — shell command construction; comment misrepresents verification |
156-
| SafeDateTime | `Proofs.idr` 5 ln, header only | LOW — parse/format |
153+
Both audited stubs have been discharged (no remaining "header-only"
154+
`Proofs.idr` in the audited set):
155+
156+
| Module | Was | Now |
157+
|--------|-----|-----|
158+
| SafeCommand | `Proofs.idr` 8 ln, header only — CRITICAL | proven#21 — 160 ln real injection-safety proofs, `idris2 --check` exit 0, no escapes |
159+
| SafeDateTime | `Proofs.idr` 5 ln, header only — LOW | real `daysInMonth` band lemmas (28..31, non-zero) + `makeDate` smart-constructor soundness (`makeDate ... = Just dt -> dateGuard dt.year dt.month dt.day = True`), `idris2 --check` exit 0, no escapes — landed in this PR |
157160

158161
## What needs proving (priority)
159162

160-
1. **Stubs first** — populate or delete the misleading `SafeCommand` /
161-
`SafeDateTime` `Proofs.idr`; a stub is worse than an honest absence.
163+
1. **Stubs first** — done. Both audited stubs (`SafeCommand`,
164+
`SafeDateTime`) now carry genuine machine-checked theorems
165+
(proven#21 + this PR); the misleading "proof-absence-as-presence"
166+
class is closed for the audited set.
162167
2. **Strip or discharge the security overclaims** — for every ✗ module either
163168
discharge the claimed theorem or downgrade the doc header to a non-promising
164169
description. Lead with **SafeDigest** ("formally verified" is actively

‎src/Proven/SafeDateTime/Proofs.idr‎

Lines changed: 122 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,126 @@
11
-- SPDX-License-Identifier: PMPL-1.0-or-later
22
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3-
||| Proofs for DateTime operations
3+
||| Safety proofs for SafeDateTime.
4+
|||
5+
||| This module discharges the SafeDateTime safety contract with genuine,
6+
||| machine-checked theorems. There are no `believe_me`, `idris_crash`,
7+
||| `assert_*`, holes, or `%default partial` — `%default total` holds and
8+
||| `idris2 0.8.0 --check` returns exit 0.
9+
|||
10+
||| It replaces what was a 5-line header-only stub (a "proof absence
11+
||| disguised as presence", flagged CRITICAL in PROOF-NEEDS.md). The
12+
||| theorems below are about the module's actual exported surface:
13+
|||
14+
||| * `daysInMonth` always returns a value in the calendar-valid band
15+
||| 28..31 (so it is non-zero — no division/indexing hazard, and the
16+
||| "overflow protection" claim has a concrete lower/upper bound).
17+
||| * `makeDate` is *sound*: any `Date` it returns satisfies the full
18+
||| validation guard (year 1..9999, day 1..daysInMonth) — i.e. the
19+
||| smart constructor cannot manufacture an out-of-range date. This
20+
||| is the real "validated via smart constructors" / "safe parsing
21+
||| without exceptions" guarantee.
422
module Proven.SafeDateTime.Proofs
523

6-
%default total
24+
import Proven.SafeDateTime
25+
26+
%default total
27+
28+
--------------------------------------------------------------------------------
29+
-- daysInMonth is always within the Gregorian-calendar band 28..31
30+
--------------------------------------------------------------------------------
31+
32+
||| Every month has at least 28 days. For February this holds in both the
33+
||| leap (29) and common (28) cases, so the result is never zero — there
34+
||| is no degenerate month that could underflow day arithmetic or an
35+
||| indexer.
36+
export
37+
daysInMonthLowerBound : (y : Nat) -> (m : Month) -> (daysInMonth y m >= 28) = True
38+
daysInMonthLowerBound y February with (isLeapYear y)
39+
daysInMonthLowerBound y February | True = Refl
40+
daysInMonthLowerBound y February | False = Refl
41+
daysInMonthLowerBound _ January = Refl
42+
daysInMonthLowerBound _ March = Refl
43+
daysInMonthLowerBound _ April = Refl
44+
daysInMonthLowerBound _ May = Refl
45+
daysInMonthLowerBound _ June = Refl
46+
daysInMonthLowerBound _ July = Refl
47+
daysInMonthLowerBound _ August = Refl
48+
daysInMonthLowerBound _ September = Refl
49+
daysInMonthLowerBound _ October = Refl
50+
daysInMonthLowerBound _ November = Refl
51+
daysInMonthLowerBound _ December = Refl
52+
53+
||| Every month has at most 31 days — an upper bound on the day
54+
||| component, pairing with the lower bound to pin `daysInMonth` to the
55+
||| valid band.
56+
export
57+
daysInMonthUpperBound : (y : Nat) -> (m : Month) -> (daysInMonth y m <= 31) = True
58+
daysInMonthUpperBound y February with (isLeapYear y)
59+
daysInMonthUpperBound y February | True = Refl
60+
daysInMonthUpperBound y February | False = Refl
61+
daysInMonthUpperBound _ January = Refl
62+
daysInMonthUpperBound _ March = Refl
63+
daysInMonthUpperBound _ April = Refl
64+
daysInMonthUpperBound _ May = Refl
65+
daysInMonthUpperBound _ June = Refl
66+
daysInMonthUpperBound _ July = Refl
67+
daysInMonthUpperBound _ August = Refl
68+
daysInMonthUpperBound _ September = Refl
69+
daysInMonthUpperBound _ October = Refl
70+
daysInMonthUpperBound _ November = Refl
71+
daysInMonthUpperBound _ December = Refl
72+
73+
||| Corollary: no month has zero days (immediate from the lower bound; a
74+
||| convenient form for callers that only need non-degeneracy).
75+
export
76+
daysInMonthNonZero : (y : Nat) -> (m : Month) -> (daysInMonth y m >= 1) = True
77+
daysInMonthNonZero y February with (isLeapYear y)
78+
daysInMonthNonZero y February | True = Refl
79+
daysInMonthNonZero y February | False = Refl
80+
daysInMonthNonZero _ January = Refl
81+
daysInMonthNonZero _ March = Refl
82+
daysInMonthNonZero _ April = Refl
83+
daysInMonthNonZero _ May = Refl
84+
daysInMonthNonZero _ June = Refl
85+
daysInMonthNonZero _ July = Refl
86+
daysInMonthNonZero _ August = Refl
87+
daysInMonthNonZero _ September = Refl
88+
daysInMonthNonZero _ October = Refl
89+
daysInMonthNonZero _ November = Refl
90+
daysInMonthNonZero _ December = Refl
91+
92+
--------------------------------------------------------------------------------
93+
-- makeDate soundness: a returned Date always satisfies the validation guard
94+
--------------------------------------------------------------------------------
95+
96+
||| The exact boolean guard `makeDate` checks before it will return a
97+
||| `Date`. Naming the predicate makes the soundness theorem read as
98+
||| "any returned Date satisfies the guard", which is its meaning.
99+
public export
100+
dateGuard : (year : Nat) -> (month : Month) -> (day : Nat) -> Bool
101+
dateGuard year month day =
102+
year >= 1 && year <= 9999 && day >= 1 && day <= daysInMonth year month
103+
104+
||| Soundness of the `makeDate` smart constructor: if it returns
105+
||| `Just dt`, then `dt` satisfies the full validation guard. Hence
106+
||| `makeDate` can never manufacture an out-of-range date — the genuine
107+
||| content of "validated via smart constructors" / "safe parsing
108+
||| without exceptions".
109+
|||
110+
||| Proof outline: invert the `Maybe` do-block. `natToMonth mn` is
111+
||| `Nothing` (then `makeDate = Nothing`, contradicting `Just dt`) or
112+
||| `Just m`; then split the `if` guard. The `True` branch fixes
113+
||| `dt = MkDate y m d` by injectivity of `Just`, so the guard proof
114+
||| transports onto `dt`'s own fields. The `False` branch is again
115+
||| `Nothing = Just dt`, absurd.
116+
export
117+
makeDateSound : (y, mn, d : Nat) -> (dt : Date) ->
118+
makeDate y mn d = Just dt ->
119+
dateGuard dt.year dt.month dt.day = True
120+
makeDateSound y mn d dt prf with (natToMonth mn)
121+
makeDateSound y mn d dt prf | Nothing = absurd prf
122+
makeDateSound y mn d dt prf | (Just m) with (dateGuard y m d) proof gEq
123+
makeDateSound y mn d dt prf | (Just m) | True =
124+
case prf of
125+
Refl => gEq
126+
makeDateSound y mn d dt prf | (Just m) | False = absurd prf

0 commit comments

Comments
 (0)