def AP.wrap

bend-osdev-array@0.1.0.1 · PROOF.bend:1706

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

1706# a word of value 2^d + k, k < 2^d, masked to its low d bits, is k
1707def AP.wrap(n: Nat, w: Word(n), +d: Nat, +k: Nat, +e: {Word.to_nat(n, w) == Nat.add(A.Arrays.slots(d), k) : Nat}, hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}, hd: {Nat.is_lt(d, n) == True{} : Bool}) -> {Word.to_nat(n, Word.and(n, w, AP.lm(n, d))) == k : Nat}:
1708  match n:
1709    case 0n:
1710      Empty.absurd({Word.to_nat(0n, Word.and(0n, w, AP.lm(0n, d))) == k : Nat}, AP.tf(Equal.trans(Bool, True{}, Nat.is_lt(d, 0n), False{}, Equal.sym(Bool, Nat.is_lt(d, 0n), True{}, hd), AP.lt_zero(d))))
1711    case 1n+ +q:
1712      match w d:
1713        case WCon{+b0, +t0} 0n:
1714          +x = Word.to_nat(1n+q, Word.and(1n+q, WCon{b0, t0}, AP.lm(1n+q, 0n)))
1715          Equal.trans(Nat, x, 0n, k, AP.lt_one(x, AP.mask_lt(1n+q, WCon{b0, t0}, 0n)), Equal.sym(Nat, k, 0n, AP.lt_one(k, hk)))
1716        case WCon{False{}, +t} 1n+ +dd:
1717          +s = A.Arrays.slots(dd)
1718          +v = Nat.sub(Word.to_nat(q, t), s)
1719          +ek = AP.wh(Word.to_nat(q, t), s, False{}, k, e)
1720          +ev = AP.wh2(Word.to_nat(q, t), s, False{}, k, e)
1721          +hv = AP.lt_bv_inv(False{}, v, s, AP.lt_rw_k(k, Nat.double(v), Nat.double(s), ek, hk))
1722          +x = Word.to_nat(q, Word.and(q, t, AP.lm(q, dd)))
1723          Equal.trans(Nat, Nat.double(x), Nat.double(v), k, AP.double_cong(x, v, AP.wrap(q, t, dd, v, ev, hv, hd)), Equal.sym(Nat, k, Nat.double(v), ek))
1724        case WCon{True{}, +t} 1n+ +dd:
1725          +s = A.Arrays.slots(dd)
1726          +v = Nat.sub(Word.to_nat(q, t), s)
1727          +ek = AP.wh(Word.to_nat(q, t), s, True{}, k, e)
1728          +ev = AP.wh2(Word.to_nat(q, t), s, True{}, k, e)
1729          +hv = AP.lt_bv_inv(True{}, v, s, AP.lt_rw_k(k, 1n+Nat.double(v), Nat.double(s), ek, hk))
1730          +x = Word.to_nat(q, Word.and(q, t, AP.lm(q, dd)))
1731          Equal.trans(Nat, 1n+Nat.double(x), 1n+Nat.double(v), k, AP.succ_cong(Nat.double(x), Nat.double(v), AP.double_cong(x, v, AP.wrap(q, t, dd, v, ev, hv, hd))), Equal.sym(Nat, k, 1n+Nat.double(v), ek))