proofs/word_power_of_two.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as Word_power_of_two

Power-of-two capacities and masks, by bit-width induction.

3 imports

import Base
import ./word_encoding.bend as WordEncoding
import ./word_arithmetic.bend as WordArithmetic

Laws

law put_into_zero provedsource · line 28 · raw

@+width:Nat -> @+bit:Bool -> {Word.shl.put(width, bit, Word.zero(width)) == Bool.pick(Word(width), bit, power(width, 0n), Word.zero(width)) : Word(width)}

law shift_power provedsource · line 48 · raw

@+width:Nat -> @+depth:Nat -> {Word.shl(width, power(width, depth)) == power(width, 1n+depth) : Word(width)}

law native_power provedsource · line 67 · raw

@+depth:Nat -> {U32.shln(1, depth) == U32{power(32n, depth)} : U32}

law subtract_one provedsource · line 78 · raw

@+width:Nat -> @+word:Word(width) -> {Word.sub(width, word, power(width, 0n)) == Word.adc(width, word, Word.zero(width), True{}, False{}) : Word(width)}

law zero_subtract_zero provedsource · line 91 · raw

@+width:Nat -> {Word.adc(width, Word.zero(width), Word.zero(width), True{}, True{}) == Word.zero(width) : Word(width)}

law decrement_power provedsource · line 102 · raw

@+width:Nat -> @+depth:Nat -> {Word.adc(width, power(width, depth), Word.zero(width), True{}, False{}) == mask(width, depth) : Word(width)}

law mask_preserves_bounded provedsource · line 120 · raw

@+width:Nat -> @+depth:Nat -> @+word:Word(width) -> @bound:{Cmp.is_lt(Word.cmp(width, word, power(width, depth))) == True{} : Bool} -> {Word.and(width, word, mask(width, depth)) == word : Word(width)}

law native_mask_preserves_bounded provedsource · line 162 · raw

@+depth:Nat -> @+index:U32 -> @_:{U32.is_lt(index, U32.shln(1, depth)) == True{} : Bool} -> {U32.and(index, U32.sub(U32.shln(1, depth), 1)) == index : U32}

law compare_zero provedsource · line 174 · raw

@+width:Nat -> {Word.cmp(width, Word.zero(width), Word.zero(width)) == EQ{} : Cmp}

law positive_power provedsource · line 185 · raw

@+width:Nat -> @+depth:Nat -> @fits:{Nat.is_lt(depth, width) == True{} : Bool} -> {Word.cmp(width, Word.zero(width), power(width, depth)) == LT{} : Cmp}

law compare_equal_low_bits provedsource · line 207 · raw

@+comparison:Cmp -> {Word.cmp.fin(False{}, False{}, comparison) == comparison : Cmp}

law power_monotone provedsource · line 217 · raw

@+width:Nat -> @+lower:Nat -> @+upper:Nat -> @fits:{Nat.is_lt(upper, width) == True{} : Bool} -> @ordered:{Nat.is_le(lower, upper) == True{} : Bool} -> {Cmp.is_le(Word.cmp(width, power(width, lower), power(width, upper))) == True{} : Bool}

law power_value provedsource · line 245 · raw

@+width:Nat -> @+depth:Nat -> @fits:{Nat.is_lt(depth, width) == True{} : Bool} -> {Word.to_nat(width, power(width, depth)) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.shift(depth, 1n) : Nat}

law pad_zero provedsource · line 266 · raw

@+width:Nat -> {Word.shr.pad(width, Word.zero(width)) == Word.zero(1n+width) : Word(1n+width)}

law pad_power provedsource · line 277 · raw

@+width:Nat -> @+depth:Nat -> @fits:{Nat.is_lt(depth, width) == True{} : Bool} -> {Word.shr.pad(width, power(width, depth)) == power(1n+width, depth) : Word(1n+width)}

law native_half_power provedsource · line 298 · raw

@+depth:Nat -> @fits:{Nat.is_lt(depth, 31n) == True{} : Bool} -> {U32.shr(U32.shln(1, 1n+depth)) == U32.shln(1, depth) : U32}

law native_power_bound provedsource · line 308 · raw

@+depth:Nat -> @bound:{Nat.is_le(depth, 31n) == True{} : Bool} -> {U32.is_le(U32.shln(1, depth), 2147483648) == True{} : Bool}

Definitions

def power source · line 6 · raw

@+width:Nat -> @depth:Nat -> Word(width)

def mask source · line 17 · raw

@+width:Nat -> @depth:Nat -> Word(width)

def native_word_mask source · line 155 · raw

@+depth:Nat -> @+word:Word(32n) -> @bound:{Cmp.is_lt(Word.cmp(32n, word, power(32n, depth))) == True{} : Bool} -> {U32.and(U32{word}, U32.sub(U32{power(32n, depth)}, 1)) == U32{word} : U32}

def native_allocatable source · line 317 · raw

@+depth:Nat -> @bound:{Nat.is_le(depth, 30n) == True{} : Bool} -> {U32.is_le(U32.shln(1, depth), 1073741824) == True{} : Bool}

def positive_double source · line 322 · raw

@value:Nat -> @positive:{Nat.is_lt(0n, Nat.double(value)) == True{} : Bool} -> {Nat.is_lt(0n, value) == True{} : Bool}

def nonempty_power_depth source · line 329 · raw

@+width:Nat -> @+depth:Nat -> @positive:{Nat.is_lt(0n, Word.to_nat(width, power(width, depth))) == True{} : Bool} -> {Nat.is_lt(depth, width) == True{} : Bool}

A nonempty checked owner cannot have a power-of-two capacity truncated to zero. This recovers the full machine-depth bound from its existing guard.

def native_nonempty_depth source · line 339 · raw

@+depth:Nat -> @positive:{Nat.is_lt(0n, U32.to_nat(U32.shln(1, depth))) == True{} : Bool} -> {Nat.is_lt(depth, 32n) == True{} : Bool}