proofs/lib/u32alg.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as U32alg

7 imports

import Base
import ./logic.bend as L
import ./nat.bend as N
import ./u32.bend as U
import ./lemmas/spec/numeric.bend as S
import ./lemmas/proofs/addition.bend as AD
import ./lemmas/proofs/division_quotient.bend as DQ

Definitions

def sc source · line 14 · raw

@+n:Nat -> @+k:Nat -> Nat

def uw source · line 17 · raw

@+n:Nat -> @+w:Word(n) -> Nat

def cy source · line 20 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+c:Bool -> Nat

def add_cancel_r source · line 25 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+e:{Nat.add(a, c) == Nat.add(b, c) : Nat} -> {a == b : Nat}

def add_rot source · line 33 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}

(a + b) + c == (a + c) + b

def sc_zero source · line 39 · raw

@+n:Nat -> {sc(n, 0n) == 0n : Nat}

def sc_add source · line 47 · raw

@+n:Nat -> @+x:Nat -> @+y:Nat -> {Nat.add(sc(n, x), sc(n, y)) == sc(n, Nat.add(x, y)) : Nat}

def le_shift source · line 56 · raw

@+r:Nat -> @+m:Nat -> @+s:Nat -> {Nat.is_le(m, Nat.add(r, Nat.add(m, s))) == True{} : Bool}

M <= r + (M + s)

def sc_succ source · line 61 · raw

@+n:Nat -> @+x:Nat -> {sc(n, 1n+x) == Nat.add(sc(n, 1n), sc(n, x)) : Nat}

def uniq_gap source · line 65 · raw

@+n:Nat -> @+r1:Nat -> @+r2:Nat -> @+q:Nat -> @+h:{Nat.add(r1, sc(n, 0n)) == Nat.add(r2, sc(n, 1n+q)) : Nat} -> @+b1:{Nat.is_lt(r1, sc(n, 1n)) == True{} : Bool} -> Empty

r1 < 2^n cannot equal r2 + 2^n (1 + q).

def uniq source · line 74 · raw

@+n:Nat -> @+r1:Nat -> @+r2:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.add(r1, sc(n, x)) == Nat.add(r2, sc(n, y)) : Nat} -> @+b1:{Nat.is_lt(r1, sc(n, 1n)) == True{} : Bool} -> @+b2:{Nat.is_lt(r2, sc(n, 1n)) == True{} : Bool} -> {r1 == r2 : Nat}

r1 + 2^n x == r2 + 2^n y with r1, r2 < 2^n forces r1 == r2.

def w_inj source · line 93 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+e:{uw(n, a) == uw(n, b) : Nat} -> {a == b : Word(n)}

def cons source · line 97 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Nat.add(uw(n, Word.add(n, a, b)), sc(n, cy(n, a, b, False{}))) == Nat.add(uw(n, a), uw(n, b)) : Nat}

def uw_zero source · line 100 · raw

@+n:Nat -> {uw(n, Word.zero(n)) == 0n : Nat}

def w_zero_add source · line 108 · raw

@+n:Nat -> @+b:Word(n) -> {Word.add(n, Word.zero(n), b) == b : Word(n)}

def w_assoc source · line 116 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+c:Word(n) -> {Word.add(n, Word.add(n, a, b), c) == Word.add(n, a, Word.add(n, b, c)) : Word(n)}

def adc_con_not source · line 154 · raw

@+p:Nat -> @+at:Word(p) -> @+bt:Word(p) -> @sk:Pair(Bool, Bool) -> @ih:(@+k:Bool -> {Word.adc(p, at, bt, True{}, k) == Word.adc(p, at, Word.not(p, bt), False{}, k) : Word(p)}) -> {Word.adc.con(p, at, bt, True{}, sk) == Word.adc.con(p, at, Word.not(p, bt), False{}, sk) : Word(1n+p)}

def adc_not source · line 160 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+c:Bool -> {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}

Subtraction is addition of the complement with an incoming carry.

def not_value source · line 170 · raw

@+n:Nat -> @+b:Word(n) -> {Nat.add(1n, Nat.add(uw(n, Word.not(n, b)), uw(n, b))) == sc(n, 1n) : Nat}

1 + unsigned(not b) + unsigned(b) == 2^n

def cons_sub source · line 189 · raw

@+n:Nat -> @+x:Word(n) -> @+a:Word(n) -> {Nat.add(uw(n, Word.sub(n, x, a)), sc(n, cy(n, x, Word.not(n, a), True{}))) == Nat.add(1n, Nat.add(uw(n, x), uw(n, Word.not(n, a)))) : Nat}

def arith_sub source · line 194 · raw

@+ux:Nat -> @+un:Nat -> @+ua:Nat -> @+ub:Nat -> @+k:Nat -> @+e:{Nat.add(ux, k) == Nat.add(ua, ub) : Nat} -> {Nat.add(Nat.add(1n, Nat.add(ux, un)), k) == Nat.add(ub, Nat.add(1n, Nat.add(un, ua))) : Nat}

(a + b) - a == b

def w_add_sub source · line 202 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> {Word.sub(n, Word.add(n, a, b), a) == b : Word(n)}

(v - a) + a == v

def w_sub_add source · line 223 · raw

@+n:Nat -> @+v:Word(n) -> @+a:Word(n) -> {Word.add(n, Word.sub(n, v, a), a) == v : Word(n)}

(v - a) + a == v

def shl_adc source · line 247 · raw

@+n:Nat -> @+w:Word(n) -> @+c:Bool -> {Word.shl.put(n, c, w) == Word.adc(n, w, w, False{}, c) : Word(n)}

Doubling by shifting: shl.put n c w == w + w + c.

def w_shl source · line 268 · raw

@+n:Nat -> @+w:Word(n) -> {Word.shl(n, w) == Word.add(n, w, w) : Word(n)}

def assoc source · line 281 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> {U32.add(U32.add(a, b), c) == U32.add(a, U32.add(b, c)) : U32}

def comm source · line 286 · raw

@+a:U32 -> @+b:U32 -> {U32.add(a, b) == U32.add(b, a) : U32}

def zero_add source · line 289 · raw

@+b:U32 -> {U32.add(0, b) == b : U32}

def add_zero source · line 294 · raw

@+b:U32 -> {U32.add(b, 0) == b : U32}

def add_sub source · line 297 · raw

@+a:U32 -> @+b:U32 -> {U32.sub(U32.add(a, b), a) == b : U32}

def sub_add source · line 302 · raw

@+v:U32 -> @+a:U32 -> {U32.add(U32.sub(v, a), a) == v : U32}

def shl_add source · line 307 · raw

@+x:U32 -> {U32.shl(x) == U32.add(x, x) : U32}

def swap source · line 313 · raw

@+a:U32 -> @+b:U32 -> @+c:U32 -> {U32.add(a, U32.add(b, c)) == U32.add(b, U32.add(a, c)) : U32}

a + (b + c) == b + (a + c)

def eq_of source · line 321 · raw

@+a:U32 -> @+b:U32 -> @+h:{U32.is_eq(a, b) == True{} : Bool} -> {a == b : U32}

def eq_refl source · line 324 · raw

@+a:U32 -> {U32.is_eq(a, a) == True{} : Bool}

def eq_true source · line 328 · raw

@+a:U32 -> @+b:U32 -> @+e:{a == b : U32} -> {U32.is_eq(a, b) == True{} : Bool}