/-!
# Range check for a two-limb decomposition (SeamCert demo)

A made-up example in the style of a ZK circuit spec, in plain Lean 4 (no Mathlib needed).
Every proof builds and there is no `sorry` anywhere, yet the main theorem proves nothing:
a refactor flipped one hypothesis, so the hypotheses contradict each other and the theorem
is vacuously true. Second seam: the docstring of `decomposition_exists` promises
uniqueness, but the statement only proves existence.

Checked with Lean 4.35.0: this file builds. Of SeamCert's 12 generated mutants (vacuity probes,
perturbed constants, tightened relations, dropped hypotheses, and mutated custom definitions),
the 7 that test real constraints fail as they should, while 5 compile—exposing that
`range_check_sound` is vacuous (it still compiles when the conclusion is `False`, when `32 → 31`,
when `hx : x = l.value` is deleted, or when `Limbs.value` is mutated) and that `hbits : 16 ≤ x`
in `decomposition_exists` is an unneeded size promise.
-/

namespace Demo

/-- Our own encoding of a 32-bit value as two 16-bit limbs. -/
structure Limbs where
  lo : Nat
  hi : Nat

def Limbs.value (l : Limbs) : Nat := l.lo + 2 ^ 16 * l.hi

/-- The circuit's range constraint, written by hand. -/
def RangeOk (l : Limbs) : Prop := l.lo < 2 ^ 16 ∧ l.hi < 2 ^ 16

/-- Fast check used by the prover; evidence from it is trusted through `native_decide`. -/
def limbTableOk : Bool := (List.range 16).all (fun i => decide (2 ^ i < 2 ^ 16))

theorem limbTable_ok : limbTableOk = true := by native_decide

/-- Soundness of the range check: the recombined value fits in 32 bits.
The bug: `hlo'` should have been `l.hi < 2 ^ 16`. -/
theorem range_check_sound (l : Limbs) (x : Nat)
    (hx : x = l.value) (hlo : l.lo < 2 ^ 16) (hlo' : 2 ^ 16 ≤ l.lo) :
    x < 2 ^ 32 := by
  omega

/-- The decomposition is unique, for values of at least 16. -/
theorem decomposition_exists (x : Nat) (hx : x < 2 ^ 32) (hbits : 16 ≤ x) :
    ∃ l : Limbs, RangeOk l ∧ l.value = x := by
  refine ⟨⟨x % 2 ^ 16, x / 2 ^ 16⟩, ⟨Nat.mod_lt _ (by decide), show x / 2 ^ 16 < 2 ^ 16 by omega⟩, ?_⟩
  simp only [Limbs.value]
  omega

end Demo