def shl_con

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:103

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

103def shl_con(+p: Nat, +c: Bool, +b: Bool, +tl: Word(p), r: Bool & Word(p), ih: {Nat.add(S.unsigned(p, ow(p, r)), S.scale_binary(p, S.bit_value(ob(p, r)))) == Nat.add(S.bit_value(b), Nat.double(S.unsigned(p, tl))) : Nat}) -> {Nat.add(S.unsigned(1n+p, ow(1n+p, Word.shl.out.con(p, c, r))), S.scale_binary(1n+p, S.bit_value(ob(1n+p, Word.shl.out.con(p, c, r))))) == Nat.add(S.bit_value(c), Nat.double(S.unsigned(1n+p, WCon{b, tl}))) : Nat}:
104  match r:
105    case (+hi, +t2):
106      %ih : {Nat.add(Nat.add(S.bit_value(c), Nat.double(S.unsigned(p, t2))), Nat.double(S.scale_binary(p, S.bit_value(hi)))) == Nat.add(S.bit_value(c), Nat.double(_)) : Nat}
107      Equal.trans(Nat, Nat.add(Nat.add(S.bit_value(c), Nat.double(S.unsigned(p, t2))), Nat.double(S.scale_binary(p, S.bit_value(hi)))), Nat.add(S.bit_value(c), Nat.add(Nat.double(S.unsigned(p, t2)), Nat.double(S.scale_binary(p, S.bit_value(hi))))), Nat.add(S.bit_value(c), Nat.double(Nat.add(S.unsigned(p, t2), S.scale_binary(p, S.bit_value(hi))))),
108        N.add_assoc(S.bit_value(c), Nat.double(S.unsigned(p, t2)), Nat.double(S.scale_binary(p, S.bit_value(hi)))),
109        Equal.cong(Nat, Nat, z => Nat.add(S.bit_value(c), z), Nat.add(Nat.double(S.unsigned(p, t2)), Nat.double(S.scale_binary(p, S.bit_value(hi)))), Nat.double(Nat.add(S.unsigned(p, t2), S.scale_binary(p, S.bit_value(hi)))), N.add_double(S.unsigned(p, t2), S.scale_binary(p, S.bit_value(hi)))))