def atop

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

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

120def atop(+p: Nat, +w: Word(1n+p)) -> {S.unsigned(1n+p, Word.and(1n+p, w, WD.pw(1n+p, p))) == C.shift(p, C.high(p, S.unsigned(1n+p, w))) : Nat}:
121  match p:
122    case 0n:
123      match w:
124        case WCon{+b, +t}:
125          match b:
126            case True{}:
127              {==}
128            case False{}:
129              {==}
130    case 1n+ +q:
131      match w:
132        case WCon{+b, +t}:
133          astep(q, b, t, atop(q, t))