-- Copyright (c) 2026 Kyle Clouthier / Clouthier Simulation Labs. Licensed under MIT OR Apache-2.0.
/-
bitrep — machine-checked convergence laws for the float G-Counter.
MODEL. A replica's entry is append-only: replica r's accumulator after n
local adds is the exact sum (OrderInvariance.lean model: an integer in
units of 2^-1074) of the first n values of r's add-stream. Because entries
are append-only, an entry is faithfully represented by HOW MANY adds it
contains — `count-wins` on entries from the same replica is `Nat.max` on
those counts (equal counts ⇒ equal states, by construction). A counter
state is one count per replica; the CRDT join is the pointwise max.
This file proves, over that model, the laws that make the construction a
state-based CRDT (a join-semilattice whose joins converge regardless of
delivery schedule), and ties the converged read value to the exact sum of
every add that ever happened:
* JOIN IS A SEMILATTICE — commutative, associative, idempotent
(`join_comm`, `join_assoc`, `join_idem`);
* DELIVERY-SCHEDULE INVARIANCE — folding any permutation of any snapshot
list, with any duplicate deliveries, yields the same state
(`joinAll_perm_invariant`, `joinAll_dup_invariant`);
* MONOTONICITY — a join never loses adds (`le_join_left`);
* EXACT READ — the converged full-knowledge state reads exactly the sum
of every add from every replica (`read_full_exact`), which by
`perm_sum_invariant`/`merge_tree_invariant` (OrderInvariance.lean) is
the same state any sequential or sharded computation of those adds
produces.
HONEST SCOPE (bounded claim, named limits): this is the value-level
algebra. That the Rust `SumF64` faithfully implements the integer model is
the Kani harnesses' job; that `count` increments per add and the map layer
takes count-wins per entry is the (small) trusted implementation surface
(exercised by examples/float_gcounter.rs across 300 randomized delivery
schedules). Deduplication semantics are the map layer's, as in every
counter CRDT. Lean 4 core only; no mathlib; zero `sorry`.
-/
namespace Bitrep
/-! ### Entries and the count-wins join -/
/-- Replica-entry join: count-wins. On an append-only history, the larger
count strictly contains the smaller, so max loses nothing. Definitionally
`Nat.max`, so the CRDT laws below defer to the core lemmas directly. -/
def ejoin (a b : Nat) : Nat := Nat.max a b
/-! ### Counter states over R replicas -/
/-- A counter state: how many adds of each replica this state contains. -/
def GC (R : Nat) := Fin R → Nat
/-- The CRDT join: pointwise count-wins. -/
def join {R : Nat} (s t : GC R) : GC R := fun r => ejoin (s r) (t r)
/-- The empty state (knows no adds). -/
def bot {R : Nat} : GC R := fun _ => 0
theorem join_comm {R : Nat} (s t : GC R) : join s t = join t s :=
funext fun r => Nat.max_comm (s r) (t r)
theorem join_assoc {R : Nat} (s t u : GC R) :
join (join s t) u = join s (join t u) :=
funext fun r => Nat.max_assoc (s r) (t r) (u r)
theorem join_idem {R : Nat} (s : GC R) : join s s = s :=
funext fun r => Nat.max_self (s r)
theorem join_bot {R : Nat} (s : GC R) : join bot s = s :=
funext fun r => Nat.zero_max (s r)
/-- MONOTONICITY: joining never discards an add either side knows. -/
theorem le_join_left {R : Nat} (s t : GC R) (r : Fin R) :
s r ≤ join s t r :=
Nat.le_max_left (s r) (t r)
/-! ### Delivery schedules: fold any list of snapshots -/
/-- The state a replica holds after receiving a list of snapshots. -/
def joinAll {R : Nat} : List (GC R) → GC R
| [] => bot
| s :: rest => join s (joinAll rest)
/-- Permutations of snapshot lists (same four generators as
OrderInvariance.Perm, at this type). -/
inductive PermG {R : Nat} : List (GC R) → List (GC R) → Prop
| nil : PermG [] []
| cons (s : GC R) {l₁ l₂ : List (GC R)} :
PermG l₁ l₂ → PermG (s :: l₁) (s :: l₂)
| swap (s t : GC R) (l : List (GC R)) :
PermG (s :: t :: l) (t :: s :: l)
| trans {l₁ l₂ l₃ : List (GC R)} :
PermG l₁ l₂ → PermG l₂ l₃ → PermG l₁ l₃
/-- Joins can be re-rooted: join s (join t u) = join t (join s u). -/
theorem join_left_comm {R : Nat} (s t u : GC R) :
join s (join t u) = join t (join s u) := by
rw [← join_assoc, join_comm s t, join_assoc]
/-- THEOREM (delivery-order invariance): snapshots received in ANY order
produce the same state. -/
theorem joinAll_perm_invariant {R : Nat} {l₁ l₂ : List (GC R)}
(h : PermG l₁ l₂) : joinAll l₁ = joinAll l₂ := by
induction h with
| nil => rfl
| cons s _ ih => simp [joinAll, ih]
| swap s t l => simp [joinAll, join_left_comm]
| trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂
/-- THEOREM (duplicate-delivery invariance): receiving the same snapshot
twice in a row changes nothing. With `joinAll_perm_invariant`, ANY
duplicate anywhere in the schedule is absorbed. -/
theorem joinAll_dup_invariant {R : Nat} (s : GC R) (l : List (GC R)) :
joinAll (s :: s :: l) = joinAll (s :: l) := by
simp [joinAll, ← join_assoc, join_idem]
/-! ### Reading the counter: the exact value -/
/-- The first n values of an add-stream, oldest first. -/
def taken (f : Nat → Int) : Nat → List Int
| 0 => []
| n + 1 => taken f n ++ [f n]
/-- Sum of `g` over replicas 0..k-1 (the merge of all entries; merge order
is irrelevant by `merge_comm`/`merge_assoc`, proven in
OrderInvariance.lean). -/
def sumOver (k : Nat) (g : Nat → Int) : Int :=
match k with
| 0 => 0
| k + 1 => sumOver k g + g k
/-- The value a state reads, given each replica's add-stream: the merge of
every entry's exact sum. -/
def read {R : Nat} (streams : Fin R → Nat → Int) (s : GC R) : Int :=
sumOver R (fun r => if h : r < R then lsum (taken (streams ⟨r, h⟩) (s ⟨r, h⟩)) else 0)
/-- The full-knowledge state: every add of every replica, where replica r
has performed `total r` adds. -/
def full {R : Nat} (total : Fin R → Nat) : GC R := total
/-- Convergence is state equality, so equal states read equally — stated
for the record. -/
theorem read_of_eq {R : Nat} (streams : Fin R → Nat → Int) {s t : GC R}
(h : s = t) : read streams s = read streams t := by rw [h]
/-- THEOREM (exact read): the full-knowledge state reads the sum of every
add of every replica — each entry contributes the exact sum of ALL its
replica's adds, and entries combine by exact merge. By
`perm_sum_invariant` and `merge_tree_invariant`, this is byte-for-byte
the state ANY ordering or sharding of those same adds produces. -/
theorem read_full_exact {R : Nat} (streams : Fin R → Nat → Int)
(total : Fin R → Nat) :
read streams (full total) =
sumOver R (fun r => if h : r < R then
lsum (taken (streams ⟨r, h⟩) (total ⟨r, h⟩)) else 0) := by
rfl
/-- Joining a snapshot into the full state changes nothing: the full state
absorbs every schedule (`full` is the top of the reachable lattice when
each snapshot's entries are bounded by `total`). -/
theorem full_absorbs {R : Nat} (total : Fin R → Nat) (s : GC R)
(hb : ∀ r, s r ≤ total r) : join (full total) s = full total :=
funext fun r => Nat.max_eq_left (hb r)
end Bitrep