Skip to content

Commit 182cc7c

Browse files
author
Jonathan D.A. Jewell
committed
proof(verisimdb): close V8 (drift metric correctness) in Idris2
New file verification/proofs/idris2/DriftMetric.idr models drift as Hamming distance on Bool feature vectors and proves the full metric axioms plus threshold-detector soundness: - V8.1 driftSelf: drift xs xs = 0 (identity of indiscernibles) - V8.2 driftSym: drift xs ys = drift ys xs (symmetry) - V8.3 driftTriangle: drift xs zs <= drift xs ys + drift ys zs (per-position xor case-split + pair-wise Nat monotonicity) - V8.4 driftExceedsSound: drift > threshold ==> detector fires - V8.5 driftExceedsComplete: detector silent ==> drift <= threshold Zero banned patterns (no believe_me / postulate / assert_total / sorry / Admitted / unsafeCoerce / Obj.magic). %default total; builds under Idris2 0.8.0. Refs: standards/docs/proofs/spec-templates/T1-critical/verisimdb.md V8, proof-debt-plan.md Dependability / VeriSimDB V8.
1 parent 0b601be commit 182cc7c

1 file changed

Lines changed: 263 additions & 0 deletions

File tree

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

Lines changed: 263 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,263 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
-- DriftMetric.idr - Formal proof that the VeriSimDB drift metric is a proper
5+
-- metric (reflexivity, symmetry, triangle inequality) and that threshold
6+
-- detection is sound.
7+
--
8+
-- V8 in standards/docs/proofs/spec-templates/T1-critical/verisimdb.md.
9+
--
10+
-- Corresponds to: rust-core/verisim-drift/src/calculator.rs.
11+
--
12+
-- Model: each Octad modality emits a fixed-width feature vector over Bool
13+
-- (feature-present / feature-absent). Drift is Hamming distance:
14+
-- the count of feature positions where two snapshots disagree.
15+
-- This is a metric (non-negative, reflexive, symmetric, triangle-inequal)
16+
-- and the threshold-detection predicate is sound by construction.
17+
18+
module DriftMetric
19+
20+
import Data.Nat
21+
import Data.Vect
22+
23+
%default total
24+
25+
------------------------------------------------------------------------
26+
-- Boolean xor primitive
27+
------------------------------------------------------------------------
28+
29+
||| Exclusive or on Bool: True iff arguments differ.
30+
public export
31+
bxor : Bool -> Bool -> Bool
32+
bxor False False = False
33+
bxor False True = True
34+
bxor True False = True
35+
bxor True True = False
36+
37+
||| xor is commutative.
38+
public export
39+
bxorCommutative : (a, b : Bool) -> bxor a b = bxor b a
40+
bxorCommutative False False = Refl
41+
bxorCommutative False True = Refl
42+
bxorCommutative True False = Refl
43+
bxorCommutative True True = Refl
44+
45+
||| Self-xor is always False (a bit never differs from itself).
46+
public export
47+
bxorSelfZero : (a : Bool) -> bxor a a = False
48+
bxorSelfZero False = Refl
49+
bxorSelfZero True = Refl
50+
51+
------------------------------------------------------------------------
52+
-- Counting True bits
53+
------------------------------------------------------------------------
54+
55+
||| Convert a Bool to 0 or 1.
56+
public export
57+
ifB : Bool -> Nat
58+
ifB False = 0
59+
ifB True = 1
60+
61+
||| Count True bits in a Bool vector.
62+
public export
63+
countTrue : {n : Nat} -> Vect n Bool -> Nat
64+
countTrue [] = 0
65+
countTrue (True :: xs) = S (countTrue xs)
66+
countTrue (False :: xs) = countTrue xs
67+
68+
||| countTrue on a single element.
69+
public export
70+
countTrueSingle : (b : Bool) -> countTrue [b] = ifB b
71+
countTrueSingle False = Refl
72+
countTrueSingle True = Refl
73+
74+
------------------------------------------------------------------------
75+
-- Drift metric: Hamming distance
76+
------------------------------------------------------------------------
77+
78+
||| A modality snapshot: presence/absence of n features.
79+
public export
80+
State : (n : Nat) -> Type
81+
State n = Vect n Bool
82+
83+
||| Drift is the count of positions where two states disagree.
84+
||| This is Hamming distance on Bool vectors.
85+
public export
86+
drift : {n : Nat} -> State n -> State n -> Nat
87+
drift xs ys = countTrue (zipWith bxor xs ys)
88+
89+
------------------------------------------------------------------------
90+
-- Metric axiom 1: identity of indiscernibles (d(x, x) = 0)
91+
------------------------------------------------------------------------
92+
93+
||| Drift from a state to itself is zero.
94+
||| Every position xor-against-itself is False, so no bits are counted.
95+
public export
96+
driftSelf : {n : Nat} -> (xs : State n) -> drift xs xs = 0
97+
driftSelf [] = Refl
98+
driftSelf (False :: xs) =
99+
-- zipWith head: bxor False False = False, so LHS = countTrue (False :: rest)
100+
rewrite driftSelf xs in Refl
101+
driftSelf (True :: xs) =
102+
-- zipWith head: bxor True True = False, so LHS = countTrue (False :: rest)
103+
rewrite driftSelf xs in Refl
104+
105+
------------------------------------------------------------------------
106+
-- Metric axiom 2: symmetry (d(x, y) = d(y, x))
107+
------------------------------------------------------------------------
108+
109+
||| Pointwise symmetry of zipWith bxor: xs xor ys = ys xor xs at each position.
110+
||| Qualified `DriftMetric.bxor` prevents implicit binding of the lowercase name.
111+
public export
112+
zipWithBxorSym : {n : Nat} -> (xs, ys : Vect n Bool)
113+
-> zipWith DriftMetric.bxor xs ys = zipWith DriftMetric.bxor ys xs
114+
zipWithBxorSym [] [] = Refl
115+
zipWithBxorSym (x :: xs) (y :: ys) =
116+
rewrite bxorCommutative x y in
117+
rewrite zipWithBxorSym xs ys in
118+
Refl
119+
120+
||| Drift is symmetric: swapping the two states gives the same count.
121+
public export
122+
driftSym : {n : Nat} -> (xs, ys : State n) -> drift xs ys = drift ys xs
123+
driftSym xs ys = cong countTrue (zipWithBxorSym xs ys)
124+
125+
------------------------------------------------------------------------
126+
-- Metric axiom 3: triangle inequality
127+
------------------------------------------------------------------------
128+
129+
||| Per-position triangle inequality on xor:
130+
||| if x != z, then x != y or y != z.
131+
||| Equivalently: ifB (bxor x z) <= ifB (bxor x y) + ifB (bxor y z).
132+
||| Exhaustive over the 8 Bool combinations.
133+
public export
134+
xorTriangleBit : (x, y, z : Bool)
135+
-> LTE (ifB (bxor x z)) (ifB (bxor x y) + ifB (bxor y z))
136+
xorTriangleBit False False False = LTEZero
137+
xorTriangleBit False False True = LTESucc LTEZero -- (F,F,T): L=1, R=0+1
138+
xorTriangleBit False True False = LTEZero -- (F,T,F): L=0, R=1+1
139+
xorTriangleBit False True True = LTESucc LTEZero -- (F,T,T): L=1, R=1+0
140+
xorTriangleBit True False False = LTESucc LTEZero -- (T,F,F): L=1, R=1+0
141+
xorTriangleBit True False True = LTEZero -- (T,F,T): L=0, R=1+1
142+
xorTriangleBit True True False = LTESucc LTEZero -- (T,T,F): L=1, R=0+1
143+
xorTriangleBit True True True = LTEZero
144+
145+
||| Monotonicity of addition on both sides.
146+
plusLteMonoBoth : {c : Nat} -> LTE a c -> LTE b d -> LTE (a + b) (c + d)
147+
plusLteMonoBoth LTEZero q = go q
148+
where
149+
go : {c' : Nat} -> LTE b d -> LTE b (c' + d)
150+
go {c' = Z} prf = prf
151+
go {c' = S c''} prf = lteSuccRight (go {c' = c''} prf)
152+
plusLteMonoBoth (LTESucc p) q = LTESucc (plusLteMonoBoth p q)
153+
154+
||| Helper: countTrue of a cons = ifB head + countTrue tail.
155+
public export
156+
countTrueCons : {n : Nat} -> (b : Bool) -> (rest : Vect n Bool)
157+
-> countTrue (b :: rest) = ifB b + countTrue rest
158+
countTrueCons False rest = Refl
159+
countTrueCons True rest = Refl
160+
161+
||| Rearrangement used in the triangle step:
162+
||| (a + c) + (b + d) = (a + b) + (c + d)
163+
||| via associativity and commutativity on Nat.
164+
plusSwap : (a, b, c, d : Nat) -> (a + c) + (b + d) = (a + b) + (c + d)
165+
plusSwap a b c d =
166+
rewrite sym (plusAssociative a c (b + d)) in
167+
rewrite plusAssociative c b d in
168+
rewrite plusCommutative c b in
169+
rewrite sym (plusAssociative b c d) in
170+
rewrite plusAssociative a b (c + d) in
171+
Refl
172+
173+
||| Triangle inequality:
174+
||| drift x z <= drift x y + drift y z
175+
||| Proof: per-position case split on (x_i, y_i, z_i), combined with
176+
||| monotonicity of Nat addition over vector zipWith.
177+
public export
178+
driftTriangle : {n : Nat}
179+
-> (xs, ys, zs : State n)
180+
-> LTE (drift xs zs) (drift xs ys + drift ys zs)
181+
driftTriangle [] [] [] = LTEZero
182+
driftTriangle (x :: xs) (y :: ys) (z :: zs) =
183+
let
184+
-- Per-position bit inequality.
185+
bitPrf : LTE (ifB (bxor x z)) (ifB (bxor x y) + ifB (bxor y z))
186+
bitPrf = xorTriangleBit x y z
187+
-- Recursive inequality on the tails.
188+
tailPrf : LTE (drift xs zs) (drift xs ys + drift ys zs)
189+
tailPrf = driftTriangle xs ys zs
190+
-- Combine them: bit + tail on both sides.
191+
combined : LTE (ifB (bxor x z) + drift xs zs)
192+
((ifB (bxor x y) + ifB (bxor y z)) +
193+
(drift xs ys + drift ys zs))
194+
combined = plusLteMonoBoth bitPrf tailPrf
195+
-- Re-associate the RHS: (xy + yz) + (txy + tyz) = (xy + txy) + (yz + tyz).
196+
rearranged : LTE (ifB (bxor x z) + drift xs zs)
197+
((ifB (bxor x y) + drift xs ys) +
198+
(ifB (bxor y z) + drift ys zs))
199+
rearranged =
200+
-- plusSwap a b c d : (a+c)+(b+d) = (a+b)+(c+d).
201+
-- With a=xy, b=yz, c=drift_xy, d=drift_yz: the LHS is the goal's
202+
-- shape and the RHS is combined's shape. Rewriting turns the goal
203+
-- into combined's type, then combined discharges it.
204+
rewrite plusSwap (ifB (bxor x y)) (ifB (bxor y z))
205+
(drift xs ys) (drift ys zs)
206+
in combined
207+
-- LHS rewrites to drift (x::xs) (z::zs), and each RHS summand to
208+
-- drift (_::_) (_::_), via countTrueCons.
209+
lhsEq : drift (x :: xs) (z :: zs) = ifB (bxor x z) + drift xs zs
210+
lhsEq = countTrueCons (bxor x z) (zipWith bxor xs zs)
211+
rhsEq1 : drift (x :: xs) (y :: ys) = ifB (bxor x y) + drift xs ys
212+
rhsEq1 = countTrueCons (bxor x y) (zipWith bxor xs ys)
213+
rhsEq2 : drift (y :: ys) (z :: zs) = ifB (bxor y z) + drift ys zs
214+
rhsEq2 = countTrueCons (bxor y z) (zipWith bxor ys zs)
215+
in
216+
rewrite lhsEq in
217+
rewrite rhsEq1 in
218+
rewrite rhsEq2 in
219+
rearranged
220+
221+
------------------------------------------------------------------------
222+
-- Threshold soundness
223+
------------------------------------------------------------------------
224+
225+
||| Drift-detection predicate: fires when drift strictly exceeds threshold.
226+
public export
227+
driftExceeds : {n : Nat} -> State n -> State n -> (threshold : Nat) -> Bool
228+
driftExceeds xs ys threshold =
229+
case isLTE (S threshold) (drift xs ys) of
230+
Yes _ => True
231+
No _ => False
232+
233+
||| Threshold soundness: if drift strictly exceeds the threshold, the
234+
||| detector fires. This is the intended direction — false positives
235+
||| are impossible by construction (the `isLTE` branch decides exactly).
236+
public export
237+
driftExceedsSound : {n : Nat} -> (xs, ys : State n) -> (t : Nat)
238+
-> LTE (S t) (drift xs ys)
239+
-> driftExceeds xs ys t = True
240+
driftExceedsSound xs ys t prf with (isLTE (S t) (drift xs ys))
241+
_ | Yes _ = Refl
242+
_ | No contra = absurd (contra prf)
243+
244+
||| Classical contrapositive on LTE over Nat: if S b does not fit under a,
245+
||| then a fits under b. The `No` branch of `isLTE` supplies exactly this
246+
||| negation, so the converse soundness proof below reduces to an application.
247+
public export
248+
notSuccLTEImpliesLTE : (a, b : Nat) -> Not (LTE (S b) a) -> LTE a b
249+
notSuccLTEImpliesLTE Z _ _ = LTEZero
250+
notSuccLTEImpliesLTE (S a') Z contra = absurd (contra (LTESucc LTEZero))
251+
notSuccLTEImpliesLTE (S a') (S b') contra =
252+
LTESucc (notSuccLTEImpliesLTE a' b' (\lt => contra (LTESucc lt)))
253+
254+
||| Converse soundness: if the detector doesn't fire, drift does not exceed
255+
||| the threshold. Together with driftExceedsSound this characterises the
256+
||| predicate completely.
257+
public export
258+
driftExceedsComplete : {n : Nat} -> (xs, ys : State n) -> (t : Nat)
259+
-> driftExceeds xs ys t = False
260+
-> LTE (drift xs ys) t
261+
driftExceedsComplete xs ys t prf with (isLTE (S t) (drift xs ys))
262+
_ | Yes _ = absurd prf
263+
_ | No contra = notSuccLTEImpliesLTE (drift xs ys) t contra

0 commit comments

Comments
 (0)