~/bend-docscommunity

proofs/containers/binary_heap/u32idx.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/u32idx.bend as U32idx

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

Definitions

def nat_round source · line 20 · raw

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

def inc_bridge source · line 25 · raw

@+j:Nat -> {U32.inc(U32.from_nat(j)) == U32.from_nat(1n+j) : U32}

def shl_nat source · line 30 · raw

@+i:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hd:{Nat.is_lt(Nat.double(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {U32.to_nat(U32.shl(U32.from_nat(i))) == Nat.double(i) : Nat}

def shl_bridge source · line 35 · raw

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

def lt_bridge source · line 43 · raw

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

def eq_bridge source · line 48 · raw

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

def sub_le source · line 55 · raw

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

def sub_one_nat source · line 63 · raw

@+j:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, j) == True{} : Bool} -> {U32.to_nat(U32.sub(U32.from_nat(j), 1)) == Nat.sub(j, 1n) : Nat}

def sub_one source · line 67 · raw

@+j:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, j) == True{} : Bool} -> {U32.sub(U32.from_nat(j), 1) == U32.from_nat(Nat.sub(j, 1n)) : U32}

def half_bit source · line 75 · raw

@+b:Bool -> @+m:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.half(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/numeric.bit_value(b), Nat.double(m))) == m : Nat}

def shr_nat source · line 82 · raw

@+y:U32 -> {U32.to_nat(U32.shr(y)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.half(U32.to_nat(y)) : Nat}

def half_le_go source · line 86 · raw

@j:Nat -> @odd:Bool -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.half_go(j, odd), j) == True{} : Bool}

def half_le source · line 95 · raw

@+j:Nat -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.half(j), j) == True{} : Bool}

def shr_bridge source · line 98 · raw

@+j:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> {U32.shr(U32.from_nat(j)) == U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.half(j)) : U32}

def par_bridge source · line 108 · raw

@+j:Nat -> @+k:Nat -> @+hk:{Nat.is_le(k, 32n) == True{} : Bool} -> @+hj:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(k)) == True{} : Bool} -> @+hpos:{Nat.is_le(1n, j) == True{} : Bool} -> {U32.shr(U32.sub(U32.from_nat(j), 1)) == U32.from_nat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/idx.par(j)) : U32}