proofs/containers/bitset/index.bend checks

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

4 imports

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../../src/containers/bitset.bend as B

Definitions

def bump source · line 17 · raw

@p:Pair(Nat, Nat) -> Pair(Nat, Nat)

def acc source · line 22 · raw

@i:Nat -> @m:Nat -> @+d:Nat -> @+r:Nat -> {Nat.divmod.go(i, m, 1n+d, r) == bump(Nat.divmod.go(i, m, d, r)) : Pair(Nat, Nat)}

The quotient accumulator of Nat.divmod.go is exactly an accumulator.

def peel_go source · line 32 · raw

@+i:Nat -> @+d:Nat -> {Nat.divmod.go(Nat.add(32n, i), 31n, d, 0n) == Nat.divmod.go(i, 31n, 1n+d, 0n) : Pair(Nat, Nat)}

32 unfoldings: the dividend loses 32, the quotient gains one.

def peel source · line 35 · raw

@+i:Nat -> {Nat.divmod(Nat.add(32n, i), 32n) == bump(Nat.divmod(i, 32n)) : Pair(Nat, Nat)}

def fst_bump source · line 39 · raw

@p:Pair(Nat, Nat) -> {Pair.fst(Nat, Nat, bump(p)) == 1n+Pair.fst(Nat, Nat, p) : Nat}

def snd_bump source · line 43 · raw

@p:Pair(Nat, Nat) -> {Pair.snd(Nat, Nat, bump(p)) == Pair.snd(Nat, Nat, p) : Nat}

def wordix_peel source · line 47 · raw

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

def bitix_peel source · line 52 · raw

@+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bitix(Nat.add(32n, i)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bitix(i) : Nat}

def small_go source · line 58 · raw

@i:Nat -> @m:Nat -> @+r:Nat -> @+h:{Nat.is_le(i, m) == True{} : Bool} -> {Nat.divmod.go(i, m, 0n, r) == (0n, Nat.add(r, i)) : Pair(Nat, Nat)}

A dividend that never reaches the divisor never advances the quotient.

def small source · line 69 · raw

@+i:Nat -> @+h:{Nat.is_lt(i, 32n) == True{} : Bool} -> {Nat.divmod(i, 32n) == (0n, i) : Pair(Nat, Nat)}

def wordix_small source · line 72 · raw

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

def bitix_small source · line 75 · raw

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

def add_sub32 source · line 79 · raw

@+i:Nat -> @+h:{Nat.is_lt(i, 32n) == False{} : Bool} -> {Nat.add(32n, Nat.sub(i, 32n)) == i : Nat}

The form the word walk needs: for i >= 32, i = 32 + (i - 32).

def wordix_step source · line 82 · 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}

def bitix_step source · line 86 · raw

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