proofs/lib/lemmas/proofs/division_candidate_bound.bend
bend-collections-laws-math@1.0.0.0 · 23 lines · 4 definitions
1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
3import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
4import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend as Overflow
5import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend as Bounds
6import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_comparison.bend as Compare
7
8def lt_le(c: Cmp, e: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_le(c) == True{} : Bool}:
9 match c:
10 case LT{}: {==}
11 case EQ{}: {==}
12 case GT{}: e
13
14def smaller_high(r: U32, d: U32, high: {W.last(32n, Overflow.bits(d)) == False{} : Bool}, less: {U32.is_lt(r, d) == True{} : Bool}) -> {W.last(32n, Overflow.bits(r)) == False{} : Bool}:
15 match r d:
16 case U32{+a} U32{+b}:
17 Overflow.high_monotone(31n, a, b, high, lt_le(Word.cmp(32n, a, b), less))
18
19def native(+r: U32, +d: U32, +bit: Bool, +high: {W.last(32n, Overflow.bits(d)) == False{} : Bool}, +less: {U32.is_lt(r, d) == True{} : Bool}) -> {U32.is_lt(U32.add(U32.mul(r, 2), W.bit_u32(bit)), U32.shl(d)) == True{} : Bool}:
20 Equal.trans(Bool, U32.is_lt(U32.add(U32.mul(r, 2), W.bit_u32(bit)), U32.shl(d)), Nat.is_lt(U32.to_nat(U32.add(U32.mul(r, 2), W.bit_u32(bit))), U32.to_nat(U32.shl(d))), True{}, Compare.u32_lt(U32.add(U32.mul(r, 2), W.bit_u32(bit)), U32.shl(d)), Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.add(U32.mul(r, 2), W.bit_u32(bit))), U32.to_nat(U32.shl(d))), Nat.is_lt(Nat.add(S.bit_value(bit), Nat.double(U32.to_nat(r))), U32.to_nat(U32.shl(d))), True{}, Equal.cong(Nat, Bool, x => Nat.is_lt(x, U32.to_nat(U32.shl(d))), U32.to_nat(U32.add(U32.mul(r, 2), W.bit_u32(bit))), Nat.add(S.bit_value(bit), Nat.double(U32.to_nat(r))), Overflow.high_candidate(r, bit, smaller_high(r, d, high, less))), Equal.trans(Bool, Nat.is_lt(Nat.add(S.bit_value(bit), Nat.double(U32.to_nat(r))), U32.to_nat(U32.shl(d))), Nat.is_lt(Nat.add(S.bit_value(bit), Nat.double(U32.to_nat(r))), Nat.double(U32.to_nat(d))), True{}, Equal.cong(Nat, Bool, x => Nat.is_lt(Nat.add(S.bit_value(bit), Nat.double(U32.to_nat(r))), x), U32.to_nat(U32.shl(d)), Nat.double(U32.to_nat(d)), Overflow.double_value(d, high)), Bounds.candidate(U32.to_nat(r), U32.to_nat(d), bit, Equal.trans(Bool, Nat.is_lt(U32.to_nat(r), U32.to_nat(d)), U32.is_lt(r, d), True{}, Equal.sym(Bool, U32.is_lt(r, d), Nat.is_lt(U32.to_nat(r), U32.to_nat(d)), Compare.u32_lt(r, d)), less)))))
21
22def million(+r: U32, +bit: Bool, less: {U32.is_lt(r, 1000000) == True{} : Bool}) -> {U32.is_lt(U32.add(U32.mul(r, 2), W.bit_u32(bit)), 2000000) == True{} : Bool}:
23 native(r, 1000000, bit, {==}, less)