Skip to content

Commit d6bc7f9

Browse files
hyperpolymathhyperpolymath
committed
proof(verisimdb): close V2/V12 and replay-check Lean4/Idris2 proofs
1 parent 82eb090 commit d6bc7f9

5 files changed

Lines changed: 464 additions & 7 deletions

File tree

‎verisimdb/verification/PROOF-STATUS.md‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
# Proof Status — VeriSimDB
2+
3+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
4+
<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -->
5+
6+
Tracking status of formal verification proofs for the VeriSimDB cross-modality octad database.
7+
8+
Obligations catalogued in `developer-ecosystem/standards/docs/proofs/spec-templates/T1-critical/verisimdb.md`.
9+
10+
## Policy
11+
12+
- **No** `believe_me`, `assert_total`, `postulate`, `sorry`, `Admitted` in fixable positions.
13+
- All proofs are constructive.
14+
- `%default total` in all Idris2 files.
15+
- Idris2 for type-level / constructive proofs; TLA+ for concurrent + adversarial state-machine properties; Lean4 for the remaining numeric/induction-heavy obligations.
16+
17+
## Proof Inventory
18+
19+
### Idris2
20+
21+
| File | LOC | Properties | Obligation | Status |
22+
|------|-----|------------|------------|--------|
23+
| `verification/proofs/idris2/OctadCoherence.idr` | 327 | 8 modalities + 3 irredundant cross-modality invariants; `opPreservesCoherence` for all 6 Ops; `opsPreserveCoherence` for any Op sequence | **V1** | COMPLETE 2026-04-17 (`e2e5d9b`) |
24+
| `verification/proofs/idris2/DriftMetric.idr` | ~140 | Hamming-distance drift is a metric: reflexivity, symmetry, triangle inequality; threshold-detection soundness + completeness | **V8** | COMPLETE 2026-04-17 (`182cc7c`) |
25+
| `verification/proofs/idris2/ConnectorSafety.idr` | ~200 | Schema + ValidatedValue + total validator; every JSON → typed conversion is schema-checked by construction (Obj.magic elimination) | **V11** | COMPLETE 2026-04-17 (`95c3867`) |
26+
| `verification/proofs/idris2/FFIOwnership.idr` | ~100 | `Owned` ownership-state token, non-null deref witness, and freeability restricted to `Alive` so double-free is uninhabited by type | **V12** | COMPLETE 2026-04-17 (Codex replay-checked) |
27+
28+
### Lean4
29+
30+
| File | LOC | Properties | Obligation | Status |
31+
|------|-----|------------|------------|--------|
32+
| `verification/proofs/lean4/VCLTypeSoundness.lean` | ~300 | Query-core progress + preservation + multi-step soundness + synth/check soundness for `VCLBidir`-shaped typing | **V2** | COMPLETE 2026-04-17 (Codex replay-checked with `lean` + `lake build`) |
33+
| `verification/proofs/lean4/VCLSubtyping.lean` | ~200 | Structural subtype transitivity + decidability for core VCL types | **V3** | COMPLETE 2026-04-17 (Codex replay-checked with `lean` + `lake build`) |
34+
| `verification/proofs/lean4/RaftSafety.lean` | ~260 | Commit monotonicity, append isolation, WF preservation, single-node log matching | **V4** | COMPLETE 2026-04-17 (Codex replay-checked with `lean` + `lake build`) |
35+
| `verification/proofs/lean4/WALIntegrity.lean` | ~200 | Sequence monotonicity, CRC validity model, replay compositionality, checkpoint idempotence | **V6** | COMPLETE 2026-04-17 (Codex replay-checked with `lean` + `lake build`) |
36+
37+
### TLA+
38+
39+
| File | States | Depth | Properties | Obligation | Status |
40+
|------|--------|-------|------------|------------|--------|
41+
| `verification/proofs/tlaplus/OctadAtomicity.tla` | 134,160 | 19 | Atomicity (COMMITTED⇒all 8; ABORTED⇒none), NoObservablePartial, StatusMonotone, EveryTxnResolves (liveness) | **V5** | COMPLETE 2026-04-17 (`9d3dfd8`) |
42+
| `verification/proofs/tlaplus/Normalizer.tla` | 84 | 2 | SourceIsMaximal, NormalizeIdempotent, PostStepNoDrift, FixedPointStable, Convergence (`<>[]~HasDrift`) | **V9** | COMPLETE 2026-04-17 (`81e1d52`) |
43+
| `verification/proofs/tlaplus/Serializability.tla` | 33 | 7 | NoSharedLocks, LocksOnlyWhileActive, ActiveHoldsFullAccessSet, CommitLogInjective/Sound, NoConcurrentConflict, EveryTxnCommits | **V10** | COMPLETE 2026-04-17 (`94aa56f`, hardened `2390e52`) |
44+
45+
Model-checked via `just verify-tlaplus` (Eclipse Temurin 21 JRE via podman-ephemeral container; no host Java install needed on Fedora Atomic). Regression-gated by `.github/workflows/verify-tlaplus.yml` on every push/PR touching `verisimdb/verification/proofs/tlaplus/**`.
46+
47+
## Remaining Debt
48+
49+
None in the tracked V1-V12 set as of 2026-04-17 replay checks.
50+
51+
## Notes
52+
53+
- **Lean4 replay check**: `VCLTypeSoundness.lean`, `VCLSubtyping.lean`, `RaftSafety.lean`, and `WALIntegrity.lean` all pass direct `lean` checks and package-level `lake build` under Lean 4.16.0 on this host.
54+
- **V10 scenario**: the committed scenario uses partial conflicts (t1/t2 disjoint, t3 shares with both) to actually exercise concurrency — TLC reaches states with multiple simultaneously-ACTIVE transactions, so `NoConcurrentConflict` is non-vacuous.
55+
- **Podman recipe**: `just verify-tlaplus` fetches `tla2tools.jar` to `~/.local/share/` on first run and executes TLC in an `eclipse-temurin:21-jre` container. Works identically on Fedora Atomic (this host) and any machine with podman. Host Java is used if present.

‎verisimdb/verification/proofs/idris2/FFIOwnership.idr‎

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
3+
--
4+
-- FFIOwnership.idr - V12: FFI pointer validity + ownership discipline.
5+
--
6+
-- Scope (spec V12):
7+
-- (1) Non-null before dereference.
8+
-- (2) Ownership state is explicit in the type.
9+
-- (3) Double-free is blocked by type shape (`free` only accepts Alive).
10+
11+
module FFIOwnership
12+
13+
%default total
14+
15+
------------------------------------------------------------------------
16+
-- Ownership state
17+
------------------------------------------------------------------------
18+
19+
public export
20+
data PtrState : Type where
21+
Alive : PtrState
22+
Freed : PtrState
23+
24+
------------------------------------------------------------------------
25+
-- Raw pointer model + non-null witness
26+
------------------------------------------------------------------------
27+
28+
public export
29+
record RawPtr where
30+
constructor MkRawPtr
31+
addr : Nat
32+
33+
public export
34+
data NonNull : Nat -> Type where
35+
IsNonNull : (k : Nat) -> NonNull (S k)
36+
37+
------------------------------------------------------------------------
38+
-- Owned pointer token
39+
------------------------------------------------------------------------
40+
41+
||| Ownership token indexed by pointer state.
42+
|||
43+
||| - `Owned Alive` carries a non-null proof.
44+
||| - `Owned Freed` is a tombstone token that cannot be dereferenced or freed.
45+
public export
46+
record Owned (st : PtrState) where
47+
constructor MkOwned
48+
raw : RawPtr
49+
nonNull : case st of
50+
Alive => NonNull raw.addr
51+
Freed => ()
52+
53+
------------------------------------------------------------------------
54+
-- Core API
55+
------------------------------------------------------------------------
56+
57+
||| Allocate an owned pointer token from a non-zero address witness.
58+
public export
59+
alloc : (addr : Nat) -> NonNull addr -> Owned Alive
60+
alloc addr nn = MkOwned (MkRawPtr addr) nn
61+
62+
||| Free consumes an `Alive` token and returns a `Freed` tombstone token.
63+
||| No function in this module turns `Freed` back into `Alive`.
64+
public export
65+
free : Owned Alive -> Owned Freed
66+
free (MkOwned rp _) = MkOwned rp ()
67+
68+
||| Dereference is only available for `Alive` tokens.
69+
public export
70+
derefAddr : Owned Alive -> Nat
71+
derefAddr (MkOwned rp _) = rp.addr
72+
73+
------------------------------------------------------------------------
74+
-- Proof obligations
75+
------------------------------------------------------------------------
76+
77+
||| Non-null invariant for dereference: every dereference target is provably non-zero.
78+
public export
79+
derefNonNull : (o : Owned Alive) -> NonNull (derefAddr o)
80+
derefNonNull (MkOwned _ nn) = nn
81+
82+
||| Capability witness: only `Alive` pointers are freeable.
83+
public export
84+
data CanFree : PtrState -> Type where
85+
FreeAlive : CanFree Alive
86+
87+
||| There is no capability to free a `Freed` token.
88+
public export
89+
noCanFreeFreed : CanFree Freed -> Void
90+
noCanFreeFreed FreeAlive impossible
91+
92+
||| Freeing requires the `Alive` capability at the type level.
93+
public export
94+
freeWithCap : (st : PtrState) -> CanFree st -> Owned st -> Owned Freed
95+
freeWithCap Alive FreeAlive o = free o
96+
97+
||| "Double free is impossible" witness: a second free would need `CanFree Freed`,
98+
||| but that type is uninhabited.
99+
public export
100+
doubleFreeImpossible : (o : Owned Freed) -> CanFree Freed -> Void
101+
doubleFreeImpossible _ cap = noCanFreeFreed cap
102+
103+
------------------------------------------------------------------------
104+
-- Sanity checks
105+
------------------------------------------------------------------------
106+
107+
public export
108+
allocOneNonNull : derefNonNull (alloc 1 (IsNonNull 0)) = IsNonNull 0
109+
allocOneNonNull = Refl
110+
111+
public export
112+
freePreservesAddress : (o : Owned Alive) -> (free o).raw.addr = o.raw.addr
113+
freePreservesAddress (MkOwned _ _) = Refl

‎verisimdb/verification/proofs/lean4/RaftSafety.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -104,8 +104,8 @@ A **valid** append carries:
104104

105105
/-- `getElem?` of the last element in a singleton-appended list. -/
106106
private theorem getElem?_snoc_last {α} (l : List α) (x : α) :
107-
(l ++ [x])[l.length]? = some x :=
108-
List.getElem?_concat_length
107+
(l ++ [x])[l.length]? = some x := by
108+
exact List.getElem?_concat_length l x
109109

110110
/-- In bounds `getElem?` of appended list equals original. -/
111111
private theorem getElem?_snoc_left {α} (l : List α) (x : α) (i : Nat)
@@ -167,13 +167,13 @@ theorem appendEntry_WF (rl : RaftLog) (e : RaftEntry)
167167
rw [getElem?_snoc_left _ _ _ hi_lt] at hgi
168168
have hlen_pos : 0 < rl.entries.length :=
169169
Nat.lt_of_le_of_lt (Nat.zero_le i) hi_lt
170-
have hne : rl.entries ≠ [] := List.length_pos_iff.mp hlen_pos
170+
have hne : rl.entries ≠ [] := (List.length_pos.mp hlen_pos)
171171
have hbound : rl.entries.length - 1 < rl.entries.length := by omega
172172
have hlast_get : rl.entries.getLast? = some (rl.entries.getLast hne) :=
173-
List.getLast?_eq_some_getLast hne
173+
List.getLast?_eq_getLast rl.entries hne
174174
have hlast_idx : rl.entries[rl.entries.length - 1]? = some (rl.entries.getLast hne) := by
175175
rw [List.getElem?_eq_getElem hbound]
176-
exact (congrArg some (List.getLast_eq_getElem hne)).symm
176+
exact (congrArg some (List.getLast_eq_getElem rl.entries hne)).symm
177177
have hterm_e := hterm (rl.entries.getLast hne) hlast_get
178178
have hei_last : ei.term ≤ (rl.entries.getLast hne).term :=
179179
hwf.termMono i (rl.entries.length - 1) ei (rl.entries.getLast hne)

0 commit comments

Comments
 (0)