proofs/math/typed/shrn.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/shrn.bend as Shrn

13 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../src/math/w64.bend as X
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/u32.bend as U
import ../../lib/u32div.bend as UD
import ../../lib/u32half.bend as UH
import ../../lib/u32alg.bend as A
import ../u64/u64div.bend as PD
import ./u32.bend as U32P
import ./width.bend as WW

Definitions

def v source · line 21 · raw

@+x:U32 -> Nat

def hlf_half source · line 25 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32half.hlf(n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.half(n) : Nat}

halving, as the word library and the spec write it

def high_half source · line 35 · raw

@+p:Nat -> @+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(p, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.half(n)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.half(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(p, n)) : Nat}

high(p, half(n)) == half(high(p, n)): both halve p + 1 times

def shrn_high source · line 43 · raw

@+x:U32 -> @+k:Nat -> {v(U32.shrn(x, k)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(k, v(x)) : Nat}

the value of a shift right: high(k, x), for every k

def p2w source · line 53 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.pow2(k) == U32{0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.pw(32n, k)} : U32}

the 2^k table is the word with bit k set

def p2v source · line 121 · raw

@+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> {v(0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.pow2(k)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k) : Nat}

def pow2_eq source · line 124 · raw

@+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k) == 1n+Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k), 1n) : Nat}

def is_zero_c source · line 127 · raw

@+a:U32 -> @+c:Bool -> @+hc:{U32.is_zero(a) == c : Bool} -> @+n:Nat -> @+hn:{v(a) == n : Nat} -> {c == Nat.is_eq(v(a), 0n) : Bool}

def zero_nat source · line 141 · raw

@+a:U32 -> {U32.is_zero(a) == Nat.is_eq(v(a), 0n) : Bool}

def div_p2 source · line 145 · raw

@+x:U32 -> @+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> {v(U32.div(x, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.pow2(k))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(k, v(x)) : Nat}

x / 2^k on a word is high(k, x)

def shrn_div source · line 152 · raw

@+x:U32 -> @+k:Nat -> @+hk:{Nat.is_lt(k, 32n) == True{} : Bool} -> {U32.shrn(x, k) == U32.div(x, 0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.pow2(k)) : U32}

U32.shrn(x, k) is U32.div(x, 2^k) for k < 32

def shr16 source · line 156 · raw

@+x:U32 -> {U32.shrn(x, 16n) == U32.div(x, 65536) : U32}

the 16-bit split of the limb code