proofs/containers/bitset/depth.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/depth.bend as Depth

6 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../spec/lib/common.bend as SC
import ../../../src/containers/bitset.bend as B
import ./index.bend as IX

Definitions

def pow2_same source · line 17 · raw

@+d:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.pow2(d) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d) : Nat}

def depth_go_le source · line 24 · raw

@fuel:Nat -> @+n:Nat -> @+d:Nat -> @+cap:Nat -> @done:Bool -> @+hd:{Nat.is_le(Nat.add(d, fuel), 31n) == True{} : Bool} -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_go(fuel, n, d, cap, done), 31n) == True{} : Bool}

def depth_le source · line 37 · raw

@+n:Nat -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n), 31n) == True{} : Bool}

The depth is always below 32, so every word index is a representable U32 and Base's index masking over the word array is the identity.

def depth_lt source · line 40 · raw

@+n:Nat -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n), 32n) == True{} : Bool}

def wordix_small_alias source · line 44 · raw

@+i:Nat -> @+h:{Nat.is_lt(i, 32n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i) == 0n : Nat}

re-exports so proofs/bitset/state.bend does not need proofs/bitset/index.bend

def wordix_step_alias source · line 47 · raw

@+i:Nat -> @+h:{Nat.is_lt(i, 32n) == False{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i) == 1n+0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(Nat.sub(i, 32n)) : Nat}