proofs/lib/lemmas/proofs/word_shift.bend checks
raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend as Word_shift
6 imports
import Base import ../spec/numeric.bend as S import ./addition.bend as Add import ./addition_bounds.bend as Bounds import ./modular_addition.bend as M import ./string_compare.bend as Natural
Definitions
def carry source · line 8 · raw
@n:Nat -> @input:Bool -> @word:Word(n) -> Bool
def conservation source · line 16 · raw
@+n:Nat -> @+input:Bool -> @word:Word(n) -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, Word.shl.put(n, input, word)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.scale_binary(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(carry(n, input, word)))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(input), Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, word))) : Nat}Integer conservation for actual Base.shl.put, retaining the discarded bit.
def same_as_put source · line 27 · raw
@+n:Nat -> @word:Word(n) -> {Word.shl(n, word) == Word.shl.put(n, False{}, word) : Word(n)}
def shift_conservation source · line 34 · raw
@+n:Nat -> @+word:Word(n) -> {Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, Word.shl(n, word)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.scale_binary(n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.bit_value(carry(n, False{}, word)))) == Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, word)) : Nat}
def refines source · line 38 · raw
@+n:Nat -> @+word:Word(n) -> {Word.shl(n, word) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.from_nat(n, Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, word))) : Word(n)}
def exact source · line 42 · raw
@+n:Nat -> @+word:Word(n) -> @bound:{Nat.is_lt(Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, word)), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.scale_binary(n, 1n)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, Word.shl(n, word)) == Nat.double(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/lemmas/spec/numeric.unsigned(n, word)) : Nat}