1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/u32.bend as U
5	import ../../../spec/lib/common.bend as SC
6	import ../../lib/lemmas/spec/numeric.bend as S
7	import ./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	
20	def 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	
25	def inc_bridge(+j: Nat) -> {U32.inc(U32.from_nat(j)) == U32.from_nat(1n+j) : U32}:
26	  {==}
27	
28	# ---- doubling ----
29	
30	def 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	
35	def 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	
43	def 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	
48	def 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	
55	def 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	
63	def 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	
67	def 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	
75	def 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	
82	def 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	
86	def 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	
95	def half_le(+j: Nat) -> {Nat.is_le(IX.half(j), j) == True{} : Bool}:
96	  half_le_go(j, False{})
97	
98	def 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	
108	def 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))