Skip to content

Commit 9a49587

Browse files
hyperpolymathhyperpolymath
authored
feat(formal): foundation-pack D1 + C2 — drift unit-interval + txn state machine (#90)
## Summary Lands two more foundation-pack theorems from #77, building on #87 (P2 + P3). - **D1 `drift_score_in_unit_interval`** — every public drift_score function in `rust-core/verisim-drift/src/calculator.rs` returns a value in [0, 1]. Audit confirmed all 9 functions end with `.clamp(0.0, 1.0)`. Generic `clamped_in_unit_interval` lemma + 9 named corollaries (one per Rust function). - **C2 `txn_state_machine_well_formed`** — three theorems modelling the transaction lifecycle in `rust-core/verisim-octad/src/transaction.rs`: - `terminal_states_have_no_outgoing` — neither Committed nor RolledBack has outgoing steps - `reachable_states_enumerable` — every reachable state is one of the three declared variants - `committed_and_rolledback_distinct` — sanity check on the inductive enumeration ## Audit findings (parallel sub-agent fan-out) Three concurrent audits ran during PR #87's CI cycle: | Theorem | Status | Spec gaps | |---|---|---| | D1 (drift) | ✓ Proof-ready | 0 of 9 functions miss the clamp. Tensor & temporal would unclamp to >1; clamps are load-bearing. | | C2 (txn) | ✓ Basic proof-ready | 5 follow-up gaps: deadlock-detection trigger, atomicity, MVCC, completed-but-retained state. This PR proves the basic well-formedness; gaps are deferred. | | C7 (WAL) | ✗ Blocked | Replay is **not** application-level idempotent (HashMap "last op per entity" reduction). Filed #89 with three remediation options. | ## CI tripwires - **D1**: adding a 10th drift function to `calculator.rs` without a corresponding `<name>_in_unit_interval` corollary in `Drift.v` is the canonical "you forgot to clamp" signal. - **C2**: `Transaction.v` whitelist asserts **0 axioms**. Any future change that introduces an `Admitted.`, `Axiom`, or `Parameter` will fail the build. ## Local verify ```text $ just -f formal/Justfile check-assumptions OK(Provenance): 3 theorems x 4 Parameters whitelisted OK(Drift): whitelisted Parameters + 9 drift fns OK(Transaction): 3 theorems closed under global context (0 axioms) ``` ## Test plan - [x] All 3 modules compile under Coq 8.18.0 with no errors or admits - [x] Per-module Print Assumptions matches declared whitelist - [x] Transaction.v assumptions guard asserts empty set - [ ] CI workflow `Coq Build Oracle` passes (verify on PR) ## Cumulative foundation-pack progress | Theorem | Module | Status | PR | |---|---|---|---| | P2 record_verify_iff_unchanged | Provenance.v | ✓ MERGED | #87 | | P3 chain_linked_step + chain_linked | Provenance.v | ✓ MERGED | #87 | | **D1 drift_score_in_unit_interval** | **Drift.v** | **THIS PR** | #88 | | **C2 txn_state_machine_well_formed** | **Transaction.v** | **THIS PR** | #88 | | D2 detect_drift_sound | _todo_ | pending | | | C7 wal_replay_idempotent | _todo_ | blocked on #89 | | | Q1 planner_logical_physical_equivalence | _todo_ | pending | | | V2 vql_preservation | _todo_ | pending | | | N2 normalize_idempotent | _todo_ | pending | | 4 of 8 foundation-pack theorems land here (P2 + P3 + D1 + C2), 3 fall out cleanly per-module audit, and C7 has a blocking spec gap captured in #89. Refs #77 (foundation pack tracking).
1 parent 521ecc4 commit 9a49587

4 files changed

Lines changed: 332 additions & 24 deletions

File tree

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

Lines changed: 50 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -48,22 +48,65 @@ jobs:
4848
set -euo pipefail
4949
coqc -q Provenance.v | tee Provenance.out
5050
51-
- name: Verify Print Assumptions whitelist
51+
- name: Compile Drift.v
5252
working-directory: formal
5353
run: |
5454
set -euo pipefail
55-
# Whitelist:
56-
# content, hash, sha256, genesis_hash (Parameters)
57-
# sha256_collision_resistant (declared Axiom)
58-
# Any other axiom name in Print Assumptions output fails.
55+
coqc -q Drift.v | tee Drift.out
56+
57+
- name: Compile Transaction.v
58+
working-directory: formal
59+
run: |
60+
set -euo pipefail
61+
coqc -q Transaction.v | tee Transaction.out
62+
63+
- name: Verify Provenance assumptions whitelist
64+
working-directory: formal
65+
run: |
66+
set -euo pipefail
67+
# Whitelist: 4 Parameters + 1 declared Axiom
5968
UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Provenance.out \
6069
| sort -u \
6170
| grep -vE '^(content|hash|sha256|genesis_hash|sha256_collision_resistant)$' || true)
6271
if [ -n "$UNEXPECTED" ]; then
63-
echo "ERROR: unexpected axiom(s)/parameter(s) in Print Assumptions:"
72+
echo "ERROR(Provenance): unexpected axiom(s) in Print Assumptions:"
6473
echo "$UNEXPECTED"
6574
echo "---"
6675
cat Provenance.out
6776
exit 1
6877
fi
69-
echo "OK: Print Assumptions matches whitelist (3 theorems x 4 Parameters)"
78+
echo "OK(Provenance): 3 theorems x 4 Parameters whitelisted"
79+
80+
- name: Verify Drift assumptions whitelist
81+
working-directory: formal
82+
run: |
83+
set -euo pipefail
84+
# Whitelist: 5 ordering Parameters + 3 ordering axioms + 9 f_*_drift Parameters
85+
UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Drift.out \
86+
| sort -u \
87+
| grep -vE '^(score|zero|one|le|clamp|le_refl|clamp_lower|clamp_upper|f_semantic_vector_drift|f_graph_document_drift|f_temporal_consistency_drift|f_tensor_drift|f_provenance_drift|f_spatial_drift|f_schema_drift|f_quality_drift|f_quality_drift_octad)$' || true)
88+
if [ -n "$UNEXPECTED" ]; then
89+
echo "ERROR(Drift): unexpected axiom(s) in Print Assumptions:"
90+
echo "$UNEXPECTED"
91+
echo "---"
92+
cat Drift.out
93+
exit 1
94+
fi
95+
echo "OK(Drift): whitelisted Parameters + 9 drift fns"
96+
97+
- name: Verify Transaction assumptions (must be empty)
98+
working-directory: formal
99+
run: |
100+
set -euo pipefail
101+
# Transaction.v has zero Parameters/Axioms — every theorem must
102+
# close under the global context.
103+
UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Transaction.out \
104+
| sort -u || true)
105+
if [ -n "$UNEXPECTED" ]; then
106+
echo "ERROR(Transaction): expected 0 axioms, found:"
107+
echo "$UNEXPECTED"
108+
echo "---"
109+
cat Transaction.out
110+
exit 1
111+
fi
112+
echo "OK(Transaction): 3 theorems closed under global context (0 axioms)"

‎formal/Drift.v‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
(* SPDX-License-Identifier: MPL-2.0 *)
2+
(* Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
3+
4+
(** * VeriSimDB Drift Score Unit-Interval Invariant
5+
6+
Mechanises the foundation-pack theorem D1 (drift_score_in_unit_interval)
7+
for the drift modality defined in
8+
[rust-core/verisim-drift/src/calculator.rs].
9+
10+
Every public drift-score function in calculator.rs ends with
11+
[.clamp(0.0, 1.0)] (audit confirmed all 9 of 9: semantic_vector_drift,
12+
graph_document_drift, temporal_consistency_drift, tensor_drift,
13+
provenance_drift, spatial_drift, schema_drift, quality_drift,
14+
quality_drift_octad). We abstract each as a [clamped] computation
15+
and prove the unit-interval invariant once at the general level,
16+
then derive 9 named corollaries — one per Rust function.
17+
18+
The 9 corollaries serve as a CI tripwire: adding a 10th drift
19+
function to calculator.rs without a corresponding corollary here
20+
is the canonical "you forgot to clamp" signal.
21+
22+
Declared axioms: 3 ordering laws on the abstract score type. No
23+
classical-reals dependency.
24+
25+
Tracking issue: hyperpolymath/verisimdb#77 (follows #87 P2+P3).
26+
*)
27+
28+
Require Import Coq.Init.Logic.
29+
30+
(** ** Domain *)
31+
32+
(** Opaque score type. In the Rust source this is [f64]. *)
33+
Parameter score : Type.
34+
35+
(** The constants 0.0 and 1.0. *)
36+
Parameter zero : score.
37+
Parameter one : score.
38+
39+
(** Order relation. *)
40+
Parameter le : score -> score -> Prop.
41+
42+
(** Clamp: [clamp lo hi x] yields [max lo (min hi x)] in the Rust source. *)
43+
Parameter clamp : score -> score -> score -> score.
44+
45+
(** Ordering and clamp laws — minimal axiomatisation. *)
46+
Axiom le_refl : forall x : score, le x x.
47+
Axiom clamp_lower : forall lo hi x : score, le lo (clamp lo hi x).
48+
Axiom clamp_upper : forall lo hi x : score, le (clamp lo hi x) hi.
49+
50+
(** A score is in the unit interval if it is between [zero] and [one]. *)
51+
Definition in_unit_interval (x : score) : Prop :=
52+
le zero x /\ le x one.
53+
54+
(** ** General lemma: every clamped computation is unit-interval-bound
55+
56+
The Rust functions all have the form [.clamp(0.0, 1.0)] as their
57+
last operation. We model this as composing an arbitrary inner
58+
function [f] with [clamp zero one]. *)
59+
Definition clamped (f : score -> score) : score -> score :=
60+
fun input => clamp zero one (f input).
61+
62+
Theorem clamped_in_unit_interval :
63+
forall (f : score -> score) (input : score),
64+
in_unit_interval (clamped f input).
65+
Proof.
66+
intros f input. unfold in_unit_interval, clamped. split.
67+
- apply clamp_lower.
68+
- apply clamp_upper.
69+
Qed.
70+
71+
(** ** D1 corollaries — one per Rust function
72+
73+
Each [Parameter f_<name>] stands for the internal pre-clamp
74+
formula in the corresponding Rust function. Each corollary
75+
states that the [clamped]-wrapped version is unit-interval-bound. *)
76+
77+
Parameter f_semantic_vector_drift : score -> score.
78+
Parameter f_graph_document_drift : score -> score.
79+
Parameter f_temporal_consistency_drift : score -> score.
80+
Parameter f_tensor_drift : score -> score.
81+
Parameter f_provenance_drift : score -> score.
82+
Parameter f_spatial_drift : score -> score.
83+
Parameter f_schema_drift : score -> score.
84+
Parameter f_quality_drift : score -> score.
85+
Parameter f_quality_drift_octad : score -> score.
86+
87+
Definition semantic_vector_drift := clamped f_semantic_vector_drift.
88+
Definition graph_document_drift := clamped f_graph_document_drift.
89+
Definition temporal_consistency_drift := clamped f_temporal_consistency_drift.
90+
Definition tensor_drift := clamped f_tensor_drift.
91+
Definition provenance_drift := clamped f_provenance_drift.
92+
Definition spatial_drift := clamped f_spatial_drift.
93+
Definition schema_drift := clamped f_schema_drift.
94+
Definition quality_drift := clamped f_quality_drift.
95+
Definition quality_drift_octad := clamped f_quality_drift_octad.
96+
97+
Theorem semantic_vector_drift_in_unit_interval :
98+
forall input, in_unit_interval (semantic_vector_drift input).
99+
Proof. intros. apply clamped_in_unit_interval. Qed.
100+
101+
Theorem graph_document_drift_in_unit_interval :
102+
forall input, in_unit_interval (graph_document_drift input).
103+
Proof. intros. apply clamped_in_unit_interval. Qed.
104+
105+
Theorem temporal_consistency_drift_in_unit_interval :
106+
forall input, in_unit_interval (temporal_consistency_drift input).
107+
Proof. intros. apply clamped_in_unit_interval. Qed.
108+
109+
Theorem tensor_drift_in_unit_interval :
110+
forall input, in_unit_interval (tensor_drift input).
111+
Proof. intros. apply clamped_in_unit_interval. Qed.
112+
113+
Theorem provenance_drift_in_unit_interval :
114+
forall input, in_unit_interval (provenance_drift input).
115+
Proof. intros. apply clamped_in_unit_interval. Qed.
116+
117+
Theorem spatial_drift_in_unit_interval :
118+
forall input, in_unit_interval (spatial_drift input).
119+
Proof. intros. apply clamped_in_unit_interval. Qed.
120+
121+
Theorem schema_drift_in_unit_interval :
122+
forall input, in_unit_interval (schema_drift input).
123+
Proof. intros. apply clamped_in_unit_interval. Qed.
124+
125+
Theorem quality_drift_in_unit_interval :
126+
forall input, in_unit_interval (quality_drift input).
127+
Proof. intros. apply clamped_in_unit_interval. Qed.
128+
129+
Theorem quality_drift_octad_in_unit_interval :
130+
forall input, in_unit_interval (quality_drift_octad input).
131+
Proof. intros. apply clamped_in_unit_interval. Qed.
132+
133+
(** ** Print Assumptions guard
134+
135+
Each theorem must close under the global context. The whitelist
136+
in the CI workflow allows: score, zero, one, le, clamp, le_refl,
137+
clamp_lower, clamp_upper, and the 9 [f_*_drift] parameters. *)
138+
139+
Print Assumptions clamped_in_unit_interval.
140+
Print Assumptions semantic_vector_drift_in_unit_interval.
141+
Print Assumptions quality_drift_octad_in_unit_interval.

‎formal/Justfile‎

Lines changed: 37 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -12,32 +12,52 @@
1212
COQC := "coqc"
1313

1414
# Compile every proof module.
15-
all: provenance
15+
all: provenance drift transaction
16+
17+
# --- Per-module compile recipes -------------------------------------------
1618

17-
# Compile the provenance module (P2 + P3).
1819
provenance:
1920
{{COQC}} -q Provenance.v | tee Provenance.out
2021

21-
# Verify that every Print Assumptions block in compiled output mentions
22-
# only the whitelist of declared parameters/axioms. Fails if any new
23-
# axiom name leaks into a theorem's transitive closure.
24-
#
25-
# Whitelist:
26-
# - content : Type (Parameter, domain)
27-
# - hash : Type (Parameter, domain)
28-
# - genesis_hash : hash (Parameter, SHA-256 of "")
29-
# - sha256 : content -> hash -> hash (Parameter)
30-
# - sha256_collision_resistant (Axiom, declared but unused)
31-
check-assumptions: provenance
22+
drift:
23+
{{COQC}} -q Drift.v | tee Drift.out
24+
25+
transaction:
26+
{{COQC}} -q Transaction.v | tee Transaction.out
27+
28+
# --- Whitelist guards -----------------------------------------------------
29+
# Each module declares its own set of Parameters/Axioms; the guard greps
30+
# Print Assumptions output for any name outside that module's whitelist.
31+
32+
check-assumptions: check-provenance check-drift check-transaction
33+
34+
check-provenance: provenance
3235
@awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Provenance.out \
3336
| sort -u \
3437
| grep -vE '^(content|hash|sha256|genesis_hash|sha256_collision_resistant)$' \
3538
| { if read -r line; then \
36-
echo "ERROR: unexpected axiom/parameter in Print Assumptions: $line"; \
37-
cat; \
38-
exit 1; \
39+
echo "ERROR(Provenance): unexpected axiom: $line"; cat; exit 1; \
40+
else \
41+
echo "OK(Provenance): 3 theorems x 4 Parameters whitelisted"; \
42+
fi; }
43+
44+
check-drift: drift
45+
@awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Drift.out \
46+
| sort -u \
47+
| grep -vE '^(score|zero|one|le|clamp|le_refl|clamp_lower|clamp_upper|f_semantic_vector_drift|f_graph_document_drift|f_temporal_consistency_drift|f_tensor_drift|f_provenance_drift|f_spatial_drift|f_schema_drift|f_quality_drift|f_quality_drift_octad)$' \
48+
| { if read -r line; then \
49+
echo "ERROR(Drift): unexpected axiom: $line"; cat; exit 1; \
50+
else \
51+
echo "OK(Drift): whitelisted Parameters + 9 drift fns"; \
52+
fi; }
53+
54+
check-transaction: transaction
55+
@awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Transaction.out \
56+
| sort -u \
57+
| { if read -r line; then \
58+
echo "ERROR(Transaction): expected 0 axioms, found: $line"; cat; exit 1; \
3959
else \
40-
echo "OK: Print Assumptions matches whitelist (3 theorems × 4 Parameters)"; \
60+
echo "OK(Transaction): 3 theorems closed under global context (0 axioms)"; \
4161
fi; }
4262

4363
# Remove all build artefacts.

‎formal/Transaction.v‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
(* SPDX-License-Identifier: MPL-2.0 *)
2+
(* Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> *)
3+
4+
(** * VeriSimDB Transaction State Machine Well-Formedness
5+
6+
Mechanises the foundation-pack theorem C2
7+
(txn_state_machine_well_formed) for the transaction lifecycle
8+
defined in [rust-core/verisim-octad/src/transaction.rs].
9+
10+
The Rust source declares:
11+
12+
pub enum TransactionState { Active, Committed, RolledBack }
13+
14+
with transitions:
15+
- begin : (nothing) -> Active
16+
- commit : Active -> Committed (when MVCC validation passes)
17+
- rollback : Active -> RolledBack
18+
19+
and the invariant that Committed and RolledBack are terminal —
20+
any commit/rollback attempt from a terminal state returns
21+
TransactionError::InvalidState.
22+
23+
This module proves three things:
24+
25+
- [terminal_states_have_no_outgoing] — neither Committed nor
26+
RolledBack can transition.
27+
- [reachable_states_enumerable] — every reachable state is one of
28+
Active, Committed, RolledBack.
29+
- [committed_and_rolledback_distinct] — the two terminal states
30+
are not equal (sanity check for the inductive enumeration).
31+
32+
Out-of-scope (deferred follow-ups): deadlock-detection trigger,
33+
MVCC version-conflict trigger, atomicity guarantee under shared
34+
state. See verisimdb#77 C2 sub-gaps.
35+
36+
Tracking issue: hyperpolymath/verisimdb#77.
37+
*)
38+
39+
Require Import Coq.Init.Logic.
40+
41+
(** ** Domain *)
42+
43+
Inductive txn_state : Type :=
44+
| Active
45+
| Committed
46+
| RolledBack.
47+
48+
(** The two transition operations the Rust source exposes. *)
49+
Inductive txn_op : Type :=
50+
| OpCommit
51+
| OpRollback.
52+
53+
(** Transition relation. [step s op s'] holds when applying [op] in
54+
state [s] yields state [s']. Mirrors the if-guarded match in
55+
[Transaction::commit] and [Transaction::rollback]. *)
56+
Inductive step : txn_state -> txn_op -> txn_state -> Prop :=
57+
| step_commit : step Active OpCommit Committed
58+
| step_rollback : step Active OpRollback RolledBack.
59+
60+
(** ** C2.a: terminal states have no outgoing transitions *)
61+
62+
Theorem terminal_states_have_no_outgoing :
63+
forall (op : txn_op) (s' : txn_state),
64+
~ step Committed op s' /\ ~ step RolledBack op s'.
65+
Proof.
66+
intros op s'. split.
67+
- intros H. inversion H.
68+
- intros H. inversion H.
69+
Qed.
70+
71+
(** Reachability from genesis: a state is reachable iff it equals
72+
[Active] (after [begin]) or there is a [step] from another
73+
reachable state. *)
74+
Inductive reachable : txn_state -> Prop :=
75+
| reach_begin : reachable Active
76+
| reach_step : forall s op s',
77+
reachable s -> step s op s' -> reachable s'.
78+
79+
(** ** C2.b: every reachable state is one of the three declared states *)
80+
81+
Theorem reachable_states_enumerable :
82+
forall s, reachable s -> s = Active \/ s = Committed \/ s = RolledBack.
83+
Proof.
84+
intros s Hr.
85+
induction Hr as [|s op s' Hs IH Hstep].
86+
- left. reflexivity.
87+
- inversion Hstep; subst.
88+
+ right. left. reflexivity.
89+
+ right. right. reflexivity.
90+
Qed.
91+
92+
(** ** C2.c: Committed and RolledBack are distinct terminal states *)
93+
94+
Theorem committed_and_rolledback_distinct :
95+
Committed <> RolledBack.
96+
Proof.
97+
intros H. discriminate H.
98+
Qed.
99+
100+
(** ** Print Assumptions guard *)
101+
102+
Print Assumptions terminal_states_have_no_outgoing.
103+
Print Assumptions reachable_states_enumerable.
104+
Print Assumptions committed_and_rolledback_distinct.

0 commit comments

Comments
 (0)