proofs/containers/binary_heap/u32idx.bend
bend-collections-laws-containers@1.0.0.0 · 110 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/idx.bend as IX
8
9# The index arithmetic the heap performs is done in U32 (a unary Nat in a sift
10# loop would make the loop cost the index instead of its logarithm). These are
11# the bridges: every U32 operation the implementation uses equals the Nat
12# operation the proofs reason about, as long as the index is representable.
13#
14# The implementation uses `U32.inc`, `U32.shl`, `U32.shr` and `U32.sub`
15# instead of `U32.add`, because those four have a Nat meaning that can be
16# stated with a bound `i < 2^k` for a VARIABLE k <= 32. A bound written as
17# `i < 2^32` would make the checker expand a unary Nat of four billion
18# successors.
19
20def nat_round(+i: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +h: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(i)) == i : Nat}:
21 U.to_nat_from_nat(i, k, hk, h)
22
23# ---- +1 is definitional ----
24
25def inc_bridge(+j: Nat) -> {U32.inc(U32.from_nat(j)) == U32.from_nat(1n+j) : U32}:
26 {==}
27
28# ---- doubling ----
29
30def shl_nat(+i: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hd: {Nat.is_lt(Nat.double(i), SC.pow2(k)) == True{} : Bool}) -> {U32.to_nat(U32.shl(U32.from_nat(i))) == Nat.double(i) : Nat}:
31 +ri = nat_round(i, k, hk, hi)
32 %ri : {U32.to_nat(U32.shl(U32.from_nat(i))) == Nat.double(_) : Nat}
33 U.shl_value(U32.from_nat(i), k, hk, L.subst(Nat, z => {Nat.is_lt(Nat.double(z), SC.pow2(k)) == True{} : Bool}, i, U32.to_nat(U32.from_nat(i)), Equal.sym(Nat, U32.to_nat(U32.from_nat(i)), i, ri), hd))
34
35def shl_bridge(+i: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hd: {Nat.is_lt(Nat.double(i), SC.pow2(k)) == True{} : Bool}) -> {U32.shl(U32.from_nat(i)) == U32.from_nat(Nat.double(i)) : U32}:
36 U.injective(U32.shl(U32.from_nat(i)), U32.from_nat(Nat.double(i)),
37 Equal.trans(Nat, U32.to_nat(U32.shl(U32.from_nat(i))), Nat.double(i), U32.to_nat(U32.from_nat(Nat.double(i))),
38 shl_nat(i, k, hk, hi, hd),
39 Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.double(i))), Nat.double(i), nat_round(Nat.double(i), k, hk, hd))))
40
41# ---- comparisons ----
42
43def lt_bridge(+i: Nat, +j: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(i), U32.from_nat(j)) == Nat.is_lt(i, j) : Bool}:
44 %nat_round(i, k, hk, hi) : {U32.is_lt(U32.from_nat(i), U32.from_nat(j)) == Nat.is_lt(_, j) : Bool}
45 %nat_round(j, k, hk, hj) : {U32.is_lt(U32.from_nat(i), U32.from_nat(j)) == Nat.is_lt(U32.to_nat(U32.from_nat(i)), _) : Bool}
46 U.is_lt_nat(U32.from_nat(i), U32.from_nat(j))
47
48def eq_bridge(+i: Nat, +j: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}) -> {U32.is_eq(U32.from_nat(i), U32.from_nat(j)) == Nat.is_eq(i, j) : Bool}:
49 %nat_round(i, k, hk, hi) : {U32.is_eq(U32.from_nat(i), U32.from_nat(j)) == Nat.is_eq(_, j) : Bool}
50 %nat_round(j, k, hk, hj) : {U32.is_eq(U32.from_nat(i), U32.from_nat(j)) == Nat.is_eq(U32.to_nat(U32.from_nat(i)), _) : Bool}
51 Equal.cong(Cmp, Bool, c => Cmp.is_eq(c), U32.cmp(U32.from_nat(i), U32.from_nat(j)), Nat.cmp(U32.to_nat(U32.from_nat(i)), U32.to_nat(U32.from_nat(j))), U.u32_cmp(U32.from_nat(i), U32.from_nat(j)))
52
53# ---- subtracting one ----
54
55def sub_le(+j: Nat) -> {Nat.is_le(Nat.sub(j, 1n), j) == True{} : Bool}:
56 match j:
57 case 0n:
58 {==}
59 case 1n+k:
60 %Equal.sym(Nat, Nat.sub(k, 0n), k, N.sub_zero(k)) : {Nat.is_le(_, 1n+k) == True{} : Bool}
61 N.le_succ(k)
62
63def sub_one_nat(+j: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hpos: {Nat.is_le(1n, j) == True{} : Bool}) -> {U32.to_nat(U32.sub(U32.from_nat(j), 1)) == Nat.sub(j, 1n) : Nat}:
64 %nat_round(j, k, hk, hj) : {U32.to_nat(U32.sub(U32.from_nat(j), 1)) == Nat.sub(_, 1n) : Nat}
65 U.sub_nat(U32.from_nat(j), 1, L.subst(Nat, z => {Nat.is_le(U32.to_nat(1), z) == True{} : Bool}, j, U32.to_nat(U32.from_nat(j)), Equal.sym(Nat, U32.to_nat(U32.from_nat(j)), j, nat_round(j, k, hk, hj)), hpos))
66
67def sub_one(+j: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hpos: {Nat.is_le(1n, j) == True{} : Bool}) -> {U32.sub(U32.from_nat(j), 1) == U32.from_nat(Nat.sub(j, 1n)) : U32}:
68 U.injective(U32.sub(U32.from_nat(j), 1), U32.from_nat(Nat.sub(j, 1n)),
69 Equal.trans(Nat, U32.to_nat(U32.sub(U32.from_nat(j), 1)), Nat.sub(j, 1n), U32.to_nat(U32.from_nat(Nat.sub(j, 1n))),
70 sub_one_nat(j, k, hk, hj, hpos),
71 Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.sub(j, 1n))), Nat.sub(j, 1n), nat_round(Nat.sub(j, 1n), k, hk, N.le_lt_trans(Nat.sub(j, 1n), j, SC.pow2(k), sub_le(j), hj)))))
72
73# ---- halving ----
74
75def half_bit(+b: Bool, +m: Nat) -> {IX.half(Nat.add(S.bit_value(b), Nat.double(m))) == m : Nat}:
76 match b:
77 case False{}:
78 IX.half_double(m)
79 case True{}:
80 IX.half_succ_double(m)
81
82def shr_nat(+y: U32) -> {U32.to_nat(U32.shr(y)) == IX.half(U32.to_nat(y)) : Nat}:
83 %Equal.sym(Nat, U32.to_nat(y), Nat.add(S.bit_value(U.low_bit(y)), Nat.double(U32.to_nat(U32.shr(y)))), U.shr_split(y)) : {U32.to_nat(U32.shr(y)) == IX.half(_) : Nat}
84 Equal.sym(Nat, IX.half(Nat.add(S.bit_value(U.low_bit(y)), Nat.double(U32.to_nat(U32.shr(y))))), U32.to_nat(U32.shr(y)), half_bit(U.low_bit(y), U32.to_nat(U32.shr(y))))
85
86def half_le_go(j: Nat, odd: Bool) -> {Nat.is_le(IX.half_go(j, odd), j) == True{} : Bool}:
87 match j odd:
88 case 0n _:
89 {==}
90 case 1n+ +p False{}:
91 N.le_trans(IX.half_go(p, True{}), p, 1n+p, half_le_go(p, True{}), N.le_succ(p))
92 case 1n+p True{}:
93 half_le_go(p, False{})
94
95def half_le(+j: Nat) -> {Nat.is_le(IX.half(j), j) == True{} : Bool}:
96 half_le_go(j, False{})
97
98def shr_bridge(+j: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}) -> {U32.shr(U32.from_nat(j)) == U32.from_nat(IX.half(j)) : U32}:
99 U.injective(U32.shr(U32.from_nat(j)), U32.from_nat(IX.half(j)),
100 Equal.trans(Nat, U32.to_nat(U32.shr(U32.from_nat(j))), IX.half(j), U32.to_nat(U32.from_nat(IX.half(j))),
101 Equal.trans(Nat, U32.to_nat(U32.shr(U32.from_nat(j))), IX.half(U32.to_nat(U32.from_nat(j))), IX.half(j),
102 shr_nat(U32.from_nat(j)),
103 Equal.cong(Nat, Nat, z => IX.half(z), U32.to_nat(U32.from_nat(j)), j, nat_round(j, k, hk, hj))),
104 Equal.sym(Nat, U32.to_nat(U32.from_nat(IX.half(j))), IX.half(j), nat_round(IX.half(j), k, hk, N.le_lt_trans(IX.half(j), j, SC.pow2(k), half_le(j), hj)))))
105
106# ---- the parent index, as the implementation computes it ----
107
108def par_bridge(+j: Nat, +k: Nat, +hk: {Nat.is_le(k, 32n) == True{} : Bool}, +hj: {Nat.is_lt(j, SC.pow2(k)) == True{} : Bool}, +hpos: {Nat.is_le(1n, j) == True{} : Bool}) -> {U32.shr(U32.sub(U32.from_nat(j), 1)) == U32.from_nat(IX.par(j)) : U32}:
109 %Equal.sym(U32, U32.sub(U32.from_nat(j), 1), U32.from_nat(Nat.sub(j, 1n)), sub_one(j, k, hk, hj, hpos)) : {U32.shr(_) == U32.from_nat(IX.par(j)) : U32}
110 shr_bridge(Nat.sub(j, 1n), k, hk, N.le_lt_trans(Nat.sub(j, 1n), j, SC.pow2(k), sub_le(j), hj))