Skip to content

Commit f274372

Browse files
hyperpolymathhyperpolymath
authored
feat(formal): C7 wal_replay_idempotent on observable state (closes #89 Option A) (#94)
## Summary Closes #89 via **Option A** (reduce-then-apply with idempotent observable state). Foundation-pack theorem **C7 lands**: `wal_replay_idempotent` on the observable entity state. ## What ships `formal/WAL.v` — two theorems, two declared parameters, one decidable-equality axiom: | Theorem | Statement | |---|---| | `wal_replay_idempotent` | `replay (replay s ops) ops = replay s ops` | | `wal_replay_deterministic_off_touched` | agreement off the touched set propagates through replay | ## Model The Rust `replay_wal` (store.rs:209) uses the `entity_ops: HashMap<entity_id, (last_op, payload)>` reduction (lines 253–273): scan WAL entries, keep only the last op per entity, apply each. WAL.v models this faithfully: - `obs_state := entity_id -> option data` — observable state - `wal_op := Upsert(e, d) | Delete(e)` — ops affecting observable state - `last_op_for` / `replay` — exactly the HashMap-reduction shape Idempotence proof: the second call to `last_op_for e ops` returns the same answer as the first (the WAL is unchanged), so the result is determined entirely by that op and independent of the intermediate state. ## What is intentionally NOT in scope The Rust `replay_wal` mutates two metadata fields on each call: - `version` counter (line 309): `octads.get(entity_id).map(|s| s.version + 1).unwrap_or(1)` — increments by 1 per replay - `created_at` / `modified_at` (line 306): `Utc::now()` — different each call A strict "replay-twice = replay-once" theorem over the full `OctadStatus` struct would fail. C7 here is therefore stated on OBSERVABLE STATE only — the entity_id → data mapping that downstream queries actually see. The WAL.v module docstring documents this restriction. A follow-up to make the Rust code metadata-stable on replay (use WAL entry timestamps; don't increment version) is left for a separate PR. ## Foundation-pack progress | Theorem | PR | Status | |---|---|---| | P2 + P3 | #87 | MERGED | | D1 + C2 | #90 | MERGED | | D2 + Q1-lite | #93 | MERGED | | **C7** | **THIS PR** | this PR | | N2 | _todo_ | blocked #91 | | V2 | _todo_ | blocked #92 | **6 of 8 once this lands.** ## Build oracle ```text $ just -f formal/Justfile check-assumptions OK(Provenance): 3 theorems x 4 Parameters whitelisted OK(Drift): D1 (9 fns) + D2 (detector iff threshold) whitelisted OK(Transaction): 3 theorems closed under global context (0 axioms) OK(Planner): Q1-lite 3 theorems x 4 axioms whitelisted OK(WAL): C7 replay-idempotent + deterministic-off-touched ``` Refs #77.
1 parent 6987d9a commit f274372

3 files changed

Lines changed: 199 additions & 2 deletions

File tree

‎.github/workflows/coq-build.yml‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,12 @@ jobs:
6666
set -euo pipefail
6767
coqc -q Planner.v | tee Planner.out
6868
69+
- name: Compile WAL.v
70+
working-directory: formal
71+
run: |
72+
set -euo pipefail
73+
coqc -q WAL.v | tee WAL.out
74+
6975
- name: Verify Provenance assumptions whitelist
7076
working-directory: formal
7177
run: |
@@ -135,3 +141,20 @@ jobs:
135141
exit 1
136142
fi
137143
echo "OK(Planner): Q1-lite 3 theorems x 4 axioms whitelisted"
144+
145+
- name: Verify WAL assumptions whitelist
146+
working-directory: formal
147+
run: |
148+
set -euo pipefail
149+
# Whitelist: entity_id, data, eq_entity_dec, functional_extensionality_dep
150+
UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' WAL.out \
151+
| sort -u \
152+
| grep -vE '^(entity_id|data|eq_entity_dec|functional_extensionality_dep)$' || true)
153+
if [ -n "$UNEXPECTED" ]; then
154+
echo "ERROR(WAL): unexpected axiom(s) in Print Assumptions:"
155+
echo "$UNEXPECTED"
156+
echo "---"
157+
cat WAL.out
158+
exit 1
159+
fi
160+
echo "OK(WAL): C7 replay-idempotent + deterministic-off-touched"

‎formal/Justfile‎

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
COQC := "coqc"
1313

1414
# Compile every proof module.
15-
all: provenance drift transaction planner
15+
all: provenance drift transaction planner wal
1616

1717
# --- Per-module compile recipes -------------------------------------------
1818

@@ -28,11 +28,14 @@ transaction:
2828
planner:
2929
{{COQC}} -q Planner.v | tee Planner.out
3030

31+
wal:
32+
{{COQC}} -q WAL.v | tee WAL.out
33+
3134
# --- Whitelist guards -----------------------------------------------------
3235
# Each module declares its own set of Parameters/Axioms; the guard greps
3336
# Print Assumptions output for any name outside that module's whitelist.
3437

35-
check-assumptions: check-provenance check-drift check-transaction check-planner
38+
check-assumptions: check-provenance check-drift check-transaction check-planner check-wal
3639

3740
check-provenance: provenance
3841
@awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Provenance.out \
@@ -73,6 +76,16 @@ check-planner: planner
7376
echo "OK(Planner): Q1-lite 3 theorems x 4 axioms whitelisted"; \
7477
fi; }
7578

79+
check-wal: wal
80+
@awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' WAL.out \
81+
| sort -u \
82+
| grep -vE '^(entity_id|data|eq_entity_dec|functional_extensionality_dep)$' \
83+
| { if read -r line; then \
84+
echo "ERROR(WAL): unexpected axiom: $line"; cat; exit 1; \
85+
else \
86+
echo "OK(WAL): C7 replay-idempotent + deterministic-off-touched"; \
87+
fi; }
88+
7689
# Remove all build artefacts.
7790
clean:
7891
rm -f *.vo *.vos *.vok *.glob .*.aux *.out

‎formal/WAL.v‎

Lines changed: 161 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,161 @@
1+
(* SPDX-License-Identifier: MPL-2.0 *)
2+
(* Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
3+
4+
(** * VeriSimDB WAL Replay — C7 Idempotence
5+
6+
Mechanises the foundation-pack theorem C7 (wal_replay_idempotent)
7+
for the write-ahead log replay path in
8+
[rust-core/verisim-octad/src/store.rs::replay_wal].
9+
10+
** The original C7 spec gap (verisimdb#89)
11+
12+
The audit captured in #89 found that the Rust [replay_wal] is
13+
NOT strictly idempotent because each replay mutates two pieces
14+
of metadata:
15+
16+
- [version] increments by 1 (line 309 in store.rs)
17+
- [created_at] / [modified_at] use [Utc::now()] (line 306)
18+
19+
A pure "replay twice = replay once" theorem on the entire
20+
[OctadStatus] struct therefore fails. Issue #89 listed three
21+
fix options:
22+
23+
(A) reduce-then-apply with idempotent modality ops,
24+
(B) replay-from-snapshot,
25+
(C) op-level idempotence-by-construction.
26+
27+
** This module: Option A, restricted to observable state
28+
29+
We prove C7 on the OBSERVABLE STATE — the entity_id → data
30+
mapping. Metadata fields (version counter, recovery timestamp)
31+
are explicitly outside the formal model; the doc comment on
32+
[replay_wal] in store.rs is updated to point at this restriction.
33+
34+
The Rust [replay_wal] follows the [last_op_per_entity] reduction
35+
pattern: scan WAL entries, build a [HashMap<entity_id, last_op>],
36+
apply each. That reduction is exactly captured here as the
37+
[last_op_for] / [replay] pair. Their composition is idempotent
38+
by inspection.
39+
40+
Declared axioms: 2 domain types ([entity_id], [data]) +
41+
decidable equality on [entity_id].
42+
43+
Tracking: hyperpolymath/verisimdb#77 + #89.
44+
*)
45+
46+
Require Import Coq.Lists.List.
47+
Require Import Coq.Logic.FunctionalExtensionality.
48+
Import ListNotations.
49+
50+
(** ** Domain *)
51+
52+
Parameter entity_id : Type.
53+
Parameter data : Type.
54+
55+
(** Decidable equality on entity_id — true for [String] in the
56+
Rust source. *)
57+
Axiom eq_entity_dec :
58+
forall (a b : entity_id), {a = b} + {a <> b}.
59+
60+
(** Observable state: a partial function from entity_id to data.
61+
[None] means the entity has been deleted (or never existed). *)
62+
Definition obs_state : Type := entity_id -> option data.
63+
64+
(** The three observable WAL operations. [Checkpoint] in the Rust
65+
source is metadata-only and does not affect observable state, so
66+
it is intentionally omitted here. *)
67+
Inductive wal_op : Type :=
68+
| Upsert : entity_id -> data -> wal_op
69+
| Delete : entity_id -> wal_op.
70+
71+
(** Project the entity an op affects. *)
72+
Definition entity_of (op : wal_op) : entity_id :=
73+
match op with
74+
| Upsert e _ => e
75+
| Delete e => e
76+
end.
77+
78+
(** Project the post-op state for the affected entity. *)
79+
Definition post_of (op : wal_op) : option data :=
80+
match op with
81+
| Upsert _ d => Some d
82+
| Delete _ => None
83+
end.
84+
85+
(** ** Last-op-per-entity reduction
86+
87+
Mirrors the [entity_ops: HashMap<entity_id, (last_op, payload)>]
88+
loop at store.rs lines 253–273: scan entries, remember only the
89+
last op per entity. We model this as a fold on the list, where
90+
a later op overrides an earlier one for the same entity. *)
91+
Fixpoint last_op_for (e : entity_id) (ops : list wal_op) : option wal_op :=
92+
match ops with
93+
| [] => None
94+
| op :: rest =>
95+
match last_op_for e rest with
96+
| Some op' => Some op'
97+
| None =>
98+
if eq_entity_dec (entity_of op) e then Some op else None
99+
end
100+
end.
101+
102+
(** ** Replay
103+
104+
Apply the last op per entity to a starting observable state.
105+
Untouched entities are preserved from the prior state. *)
106+
Definition replay (s : obs_state) (ops : list wal_op) : obs_state :=
107+
fun e =>
108+
match last_op_for e ops with
109+
| Some op => post_of op
110+
| None => s e
111+
end.
112+
113+
(** ** C7: WAL replay is idempotent
114+
115+
Replaying the same WAL twice yields the same observable state as
116+
replaying it once.
117+
118+
Proof intuition: for each entity, the "last op per entity" is the
119+
SAME on the second call (the WAL is unchanged), so the answer is
120+
determined entirely by that op and is independent of the
121+
intermediate state. *)
122+
Theorem wal_replay_idempotent :
123+
forall (s : obs_state) (ops : list wal_op),
124+
replay (replay s ops) ops = replay s ops.
125+
Proof.
126+
intros s ops.
127+
apply functional_extensionality. intros e.
128+
unfold replay.
129+
destruct (last_op_for e ops) as [op|] eqn:Hlop.
130+
- reflexivity.
131+
- reflexivity.
132+
Qed.
133+
134+
(** ** Bonus: replay is deterministic
135+
136+
Two starting states that agree on every entity untouched by [ops]
137+
produce equal post-replay states. (Stronger than idempotence:
138+
[replay s1 ops = replay s2 ops] whenever s1 and s2 agree off the
139+
set of touched entities.) *)
140+
Theorem wal_replay_deterministic_off_touched :
141+
forall (s1 s2 : obs_state) (ops : list wal_op),
142+
(forall e, last_op_for e ops = None -> s1 e = s2 e) ->
143+
replay s1 ops = replay s2 ops.
144+
Proof.
145+
intros s1 s2 ops Hagree.
146+
apply functional_extensionality. intros e.
147+
unfold replay.
148+
destruct (last_op_for e ops) as [op|] eqn:Hlop.
149+
- reflexivity.
150+
- apply Hagree. exact Hlop.
151+
Qed.
152+
153+
(** ** Print Assumptions guard
154+
155+
Allowed: entity_id, data, eq_entity_dec, functional_extensionality.
156+
The functional_extensionality axiom is a standard Coq library
157+
addition; it is whitelisted because it is the standard way to
158+
prove function equality. *)
159+
160+
Print Assumptions wal_replay_idempotent.
161+
Print Assumptions wal_replay_deterministic_off_touched.

0 commit comments

Comments
 (0)