proofs/u32_shift.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32_shift

8 imports

import Base
import ./natural_addition.bend as Addition
import ./u32_successor.bend as U32Successor
import ./word_arithmetic.bend as WordArithmetic
import ./bounded_u32_arithmetic.bend as Arithmetic
import ./u32_comparison.bend as Comparison
import ./nat_to_u32_bounds.bend as Bounds
import ./word_encoding.bend as WordEncoding

Laws

law out_pad provedsource · line 10 · raw

@+n:Nat -> @+c:Bool -> @+w:Word(n) -> {Word.shl.out(1n+n, c, Word.shr.pad(n, w)) == (False{}, Word.shl.put(1n+n, c, Word.shr.pad(n, w))) : Pair(Bool, Word(1n+n))}

Definitions

def Goal source · line 25 · raw

@+w:Word(32n) -> @+c:Bool -> Type

def parts source · line 28 · raw

@+c:Bool -> @+parts:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.Split<31n, 1n> -> Goal(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.join(31n, 1n, parts), c)

def no_carry source · line 37 · raw

@+w:Word(32n) -> @+c:Bool -> Goal(w, c)

def put_inc source · line 41 · raw

@+n:Nat -> @+w:Word(n) -> {Word.shl.put(n, True{}, w) == Word.inc(n, Word.shl(n, w)) : Word(n)}

def encoded_shift source · line 49 · raw

@+w:Word(32n) -> {U32{Word.shl(32n, w)} == U32.from_nat(Nat.double(Word.to_nat(32n, w))) : U32}

def encoded_put source · line 54 · raw

@+c:Bool -> @+w:Word(32n) -> {U32{Word.shl.put(32n, c, w)} == U32.from_nat(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.digit(c, Word.to_nat(32n, w))) : U32}

def bounded_put source · line 65 · raw

@+c:Bool -> @+w:Word(32n) -> @+cap:U32 -> @cap_ok:{U32.is_le(cap, 2147483648) == True{} : Bool} -> @h:{Nat.is_le(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.digit(c, Word.to_nat(32n, w)), U32.to_nat(cap)) == True{} : Bool} -> {U32.to_nat(U32{Word.shl.put(32n, c, w)}) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.digit(c, Word.to_nat(32n, w)) : Nat}

def put_pad source · line 72 · raw

@+n:Nat -> @+c:Bool -> @+w:Word(n) -> {Word.shl.put(1n+n, c, Word.shr.pad(n, w)) == WCon{c, w} : Word(1n+n)}

def DoubleGoal source · line 82 · raw

@+w:Word(32n) -> Type

def double_parts source · line 85 · raw

@+parts:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.Split<31n, 1n> -> DoubleGoal(0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.join(31n, 1n, parts))

def double_word source · line 99 · raw

@+w:Word(32n) -> DoubleGoal(w)

def double source · line 103 · raw

@+x:U32 -> @h:{U32.is_lt(x, 2147483648) == True{} : Bool} -> {U32.to_nat(U32.shl(x)) == Nat.double(U32.to_nat(x)) : Nat}