~/bend-docscommunity

proofs/lib/flat.bend checks

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

5 imports
import Base
import ./logic.bend as L
import ./nat.bend as N
import ../../spec/lib/common.bend as SC
import ./lemmas/proofs/nat_algebra.bend as NA

Definitions

def nthc source · line 24 · raw

@xs:List<&2, U32> -> @q:Nat -> U32

def nthc_nth source · line 33 · raw

@xs:List<&2, U32> -> @q:Nat -> @+h:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(U32, xs, q) == Some{nthc(xs, q)} : Maybe<&2, U32>}

def add_one source · line 43 · raw

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

def pow2_split source · line 47 · raw

@+q:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+q) == Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) : Nat}

def lt_split source · line 52 · raw

@+o:Nat -> @+q:Nat -> {Nat.is_lt(o, Nat.add(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q))) == True{} : Bool}

o < o + 2^q o < o + 2^q

def split_assoc source · line 59 · raw

@+o:Nat -> @+q:Nat -> {Nat.add(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+q)) == Nat.add(Nat.add(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) : Nat}

o + 2^(1+q) == (o + 2^q) + 2^q o + 2^(1+q) == (o + 2^q) + 2^q

def mid_lt source · line 65 · raw

@+o:Nat -> @+q:Nat -> {Nat.is_lt(Nat.add(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)), Nat.add(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+q))) == True{} : Bool}

o + 2^q < o + 2^(1+q) o + 2^q < o + 2^(1+q)

def is_eq_sym source · line 71 · raw

@a:Nat -> @b:Nat -> {Nat.is_eq(a, b) == Nat.is_eq(b, a) : Bool}

def ne_gt source · line 82 · raw

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

def base_le source · line 88 · raw

@+d:Nat -> @+t:Nat -> {Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), t)) == True{} : Bool}

2^d <= 2^d + t 2^d <= 2^d + t

def nthc_other source · line 93 · raw

@cl:List<&2, U32> -> @j:Nat -> @k:Nat -> @+v:U32 -> @+ne:{Nat.is_eq(j, k) == False{} : Bool} -> {nthc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, cl, j, v), k) == nthc(cl, k) : U32}

def nthc_same source · line 106 · raw

@cl:List<&2, U32> -> @j:Nat -> @+v:U32 -> @+h:{Nat.is_lt(j, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, cl)) == True{} : Bool} -> {nthc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(U32, cl, j, v), j) == v : U32}

def base_lt source · line 116 · raw

@+d:Nat -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+d)) == True{} : Bool}

2^d < 2^(d+1)

def in_cells source · line 119 · raw

@+cl:List<&2, U32> -> @+d:Nat -> @+k:Nat -> @+hk:{Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, cl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+d) : Nat} -> {Nat.is_lt(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, cl)) == True{} : Bool}

def leaf_in_cells source · line 123 · raw

@+cl:List<&2, U32> -> @+d:Nat -> @+o:Nat -> @+ho:{Nat.is_lt(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hlen:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, cl) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+d) : Nat} -> {Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), o), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, cl)) == True{} : Bool}

def blk_lo source · line 130 · raw

@+o:Nat -> @+p:Nat -> @+d:Nat -> @+hw:{Nat.is_le(Nat.add(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(p)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool}

o < 2^d when the block [o, o+2^p) fits o < 2^d when the block [o, o+2^p) fits

def leaf_lt source · line 136 · raw

@+d:Nat -> @+o:Nat -> @+ho:{Nat.is_lt(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), o), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+d)) == True{} : Bool}

2^d + o < 2^(d+1) and o + 2^q < 2^(d+1)

def node_lt source · line 140 · raw

@+o:Nat -> @+q:Nat -> @+d:Nat -> @+hw:{Nat.is_le(Nat.add(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> {Nat.is_lt(Nat.add(o, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(1n+d)) == True{} : Bool}

def hof source · line 149 · raw

@p:Nat -> Nat

The half size a walk carries at remaining depth p: 2^(p-1), and 0 at a leaf (where it is unused). One machine division steps from one level to the next, so no walk ever recomputes a power of two.

def hof_succ source · line 152 · raw

@+q:Nat -> {hof(1n+q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q) : Nat}

def nthc_rep source · line 157 · raw

@m:Nat -> @k:Nat -> {nthc(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.replicate(U32, m, 0), k) == 0 : U32}

The comparison the source makes against the carried half size is exactly the model's branch decision.