def mask_split

bend-collections-laws-math@1.0.0.0 · proofs/lib/word.bend:286

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A

286# x == (x & mask k) + 2^k (bits above k)
287def mask_split(+n: Nat, +k: Nat, +x: Word(n)) -> {uw(n, x) == Nat.add(uw(n, Word.and(n, x, mask(n, k))), sc(k, hi_part(n, k, x))) : Nat}:
288  match n k x:
289    case 0n _ WNil{}:
290      Equal.sym(Nat, sc(k, 0n), 0n, A.sc_zero(k))
291    case 1n+p 0n WCon{b, t}:
292      %Equal.sym(Nat, uw(1n+p, Word.and(1n+p, WCon{b, t}, mask(1n+p, 0n))), 0n, low0(p, b, t)) : {uw(1n+p, WCon{b, t}) == Nat.add(_, uw(1n+p, WCon{b, t})) : Nat}
293      {==}
294    case 1n+p 1n+j WCon{b, t}:
295      +at = uw(p, Word.and(p, t, mask(p, j)))
296      +hs = sc(j, hi_part(p, j, t))
297      %Equal.sym(Bool, Bool.and(b, True{}), b, U.and_true(b)) : {Nat.add(S.bit_value(b), Nat.double(uw(p, t))) == Nat.add(Nat.add(S.bit_value(_), Nat.double(at)), Nat.double(hs)) : Nat}
298      %Equal.sym(Nat, uw(p, t), Nat.add(at, hs), mask_split(p, j, t)) : {Nat.add(S.bit_value(b), Nat.double(_)) == Nat.add(Nat.add(S.bit_value(b), Nat.double(at)), Nat.double(hs)) : Nat}
299      Equal.trans(Nat, Nat.add(S.bit_value(b), Nat.double(Nat.add(at, hs))), Nat.add(S.bit_value(b), Nat.add(Nat.double(at), Nat.double(hs))), Nat.add(Nat.add(S.bit_value(b), Nat.double(at)), Nat.double(hs)),
300        Equal.cong(Nat, Nat, z => Nat.add(S.bit_value(b), z), Nat.double(Nat.add(at, hs)), Nat.add(Nat.double(at), Nat.double(hs)), Equal.sym(Nat, Nat.add(Nat.double(at), Nat.double(hs)), Nat.double(Nat.add(at, hs)), N.add_double(at, hs))),
301        Equal.sym(Nat, Nat.add(Nat.add(S.bit_value(b), Nat.double(at)), Nat.double(hs)), Nat.add(S.bit_value(b), Nat.add(Nat.double(at), Nat.double(hs))), N.add_assoc(S.bit_value(b), Nat.double(at), Nat.double(hs))))