def astep

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:106

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

106# keeping only the top bit
107def astep(+q: Nat, +b: Bool, +t: Word(1n+q), +ih: {S.unsigned(1n+q, Word.and(1n+q, t, WD.pw(1n+q, q))) == C.shift(q, C.high(q, S.unsigned(1n+q, t))) : Nat}) -> {S.unsigned(2n+q, Word.and(2n+q, WCon{b, t}, WD.pw(2n+q, 1n+q))) == C.shift(1n+q, C.high(1n+q, S.unsigned(2n+q, WCon{b, t}))) : Nat}:
108  match b:
109    case True{}:
110      +T = S.unsigned(1n+q, t)
111      +A0 = S.unsigned(1n+q, Word.and(1n+q, t, WD.pw(1n+q, q)))
112      +U0 = Nat.add(1n, Nat.double(T))
113      Equal.trans(Nat, Nat.double(A0), Nat.double(C.shift(q, C.high(q, T))), Nat.double(C.shift(q, C.high(q, C.half(U0)))), Equal.cong(Nat, Nat, z => Nat.double(z), A0, C.shift(q, C.high(q, T)), ih), Equal.cong(Nat, Nat, z => Nat.double(C.shift(q, C.high(q, z))), T, C.half(U0), Equal.sym(Nat, C.half(U0), T, WW.half_dbl(1n, T))))
114    case False{}:
115      +T = S.unsigned(1n+q, t)
116      +A0 = S.unsigned(1n+q, Word.and(1n+q, t, WD.pw(1n+q, q)))
117      +U0 = Nat.add(0n, Nat.double(T))
118      Equal.trans(Nat, Nat.double(A0), Nat.double(C.shift(q, C.high(q, T))), Nat.double(C.shift(q, C.high(q, C.half(U0)))), Equal.cong(Nat, Nat, z => Nat.double(z), A0, C.shift(q, C.high(q, T)), ih), Equal.cong(Nat, Nat, z => Nat.double(C.shift(q, C.high(q, z))), T, C.half(U0), Equal.sym(Nat, C.half(U0), T, WW.half_dbl(0n, T))))