def AP.mask_lt

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

import Base
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

908# a word masked to its low d bits is below 2^d
909def AP.mask_lt(n: Nat, w: Word(n), +d: Nat) -> {Nat.is_lt(Word.to_nat(n, Word.and(n, w, AP.lm(n, d))), A.Arrays.slots(d)) == True{} : Bool}:
910  match n:
911    case 0n:
912      AP.slots_pos(d)
913    case 1n+ +q:
914      match w d:
915        case WCon{False{}, +t} 0n:
916          %Equal.sym(Word(q), Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t)) : {Nat.is_lt(Nat.double(Word.to_nat(q, _)), 1n) == True{} : Bool}
917          %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, UL.word_zero_value(q)) : {Nat.is_lt(Nat.double(_), 1n) == True{} : Bool}
918          {==}
919        case WCon{True{}, +t} 0n:
920          %Equal.sym(Word(q), Word.and(q, t, Word.zero(q)), Word.zero(q), AP.and_zero(q, t)) : {Nat.is_lt(Nat.double(Word.to_nat(q, _)), 1n) == True{} : Bool}
921          %Equal.sym(Nat, Word.to_nat(q, Word.zero(q)), 0n, UL.word_zero_value(q)) : {Nat.is_lt(Nat.double(_), 1n) == True{} : Bool}
922          {==}
923        case WCon{False{}, +t} 1n+ +e:
924          AP.lt_bv(False{}, Word.to_nat(q, Word.and(q, t, AP.lm(q, e))), A.Arrays.slots(e), AP.mask_lt(q, t, e))
925        case WCon{True{}, +t} 1n+ +e:
926          AP.lt_bv(True{}, Word.to_nat(q, Word.and(q, t, AP.lm(q, e))), A.Arrays.slots(e), AP.mask_lt(q, t, e))