proofs/lib/u32half.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend as U32half

6 imports

import Base
import ./logic.bend as L
import ./nat.bend as N
import ./u32.bend as U
import ../../spec/lib/common.bend as SC
import ./lemmas/spec/numeric.bend as S

Definitions

def hlf source · line 21 · raw

@n:Nat -> Nat

The Nat halving the checker can compute structurally (no Nat.div).

def hlf_double source · line 32 · raw

@+q:Nat -> {hlf(Nat.double(q)) == q : Nat}

def hlf_double_succ source · line 39 · raw

@+q:Nat -> {hlf(1n+Nat.double(q)) == q : Nat}

def hlf_bit source · line 46 · raw

@+b:Bool -> @+q:Nat -> {hlf(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bit_value(b), Nat.double(q))) == q : Nat}

def shr_value source · line 53 · raw

@+x:U32 -> {U32.to_nat(U32.shr(x)) == hlf(U32.to_nat(x)) : Nat}

def hlf_le source · line 60 · raw

@+n:Nat -> {Nat.is_le(hlf(n), n) == True{} : Bool}

def hlf_succ_le source · line 71 · raw

@+q:Nat -> {Nat.is_le(hlf(1n+q), q) == True{} : Bool}

def hlf_lower source · line 80 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(a, hlf(Nat.add(a, b))) == True{} : Bool}

The midpoint of a nonempty range lies inside it: a <= hlf(a+b) < b whenever a < b.

def hlf_upper source · line 90 · raw

@+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(hlf(Nat.add(a, b)), b) == True{} : Bool}

def hlf_bound source · line 109 · raw

@+i:Nat -> @+k:Nat -> @+h:{Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k)) == True{} : Bool} -> {Nat.is_lt(hlf(i), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k)) == True{} : Bool}

def shr_bridge source · line 112 · raw

@+i:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k)) == True{} : Bool} -> {U32.shr(U32.from_nat(i)) == U32.from_nat(hlf(i)) : U32}

def hlf_lt source · line 126 · raw

@+s:Nat -> @+m:Nat -> @+h:{Nat.is_lt(s, Nat.double(m)) == True{} : Bool} -> {Nat.is_lt(hlf(s), m) == True{} : Bool}

s < 2m gives s/2 < m: one narrowing step of a search range that started below 2^f lands below 2^(f-1).

def step_bound source · line 138 · raw

@+s2:Nat -> @+s:Nat -> @+m:Nat -> @+hle:{Nat.is_le(s2, hlf(s)) == True{} : Bool} -> @+h:{Nat.is_lt(s, Nat.double(m)) == True{} : Bool} -> {Nat.is_lt(s2, m) == True{} : Bool}

The size after one step is at most s/2, so it stays below the halved bound.

def sub_le source · line 145 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(Nat.sub(a, b), a) == True{} : Bool}

U32.sub is exact whenever the subtrahend is not larger (no borrow), so it is the Nat subtraction of the two indices.

def sub_bridge source · line 154 · raw

@+a:Nat -> @+b:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+ha:{Nat.is_lt(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hb:{Nat.is_le(b, a) == True{} : Bool} -> {U32.sub(U32.from_nat(a), U32.from_nat(b)) == U32.from_nat(Nat.sub(a, b)) : U32}