1	import Base
2	import ../../src/containers/hash_table.bend as H
3	import ./u32.bend as UW
4	import ../../spec/lib/common.bend as SC
5	import ./nat_list.bend as NL
6	import ./logic.bend as L
7	import ./nat.bend as N
8	import ./u32div.bend as UD
9	import ./words32.bend as W32
10	import ./word.bend as WD
11	
12	# Ids linked through U32 words: lnk(s) is the link word of slot s, fst_or and
13	# last_or the link of a list's first and last id (or a default), and how they
14	# behave over appends and reversed appends.
15	
16	def lnk(+s: Nat) -> U32:
17	  H.link(U32.from_nat(s))
18	
19	def fst_or(t: List<&2, Nat>, +q: U32) -> U32:
20	  match t:
21	    case Nil{}:
22	      q
23	    case Con{+s, t2}:
24	      lnk(s)
25	
26	def last_or(t: List<&2, Nat>, +p: U32) -> U32:
27	  match t:
28	    case Nil{}:
29	      p
30	    case Con{+s, +t2}:
31	      last_or(t2, lnk(s))
32	
33	def u_refl(+x: U32) -> {U32.is_eq(x, x) == True{} : Bool}:
34	  UW.u32_eq_refl(x)
35	
36	def fst_app(+a: List<&2, Nat>, +b: List<&2, Nat>, +q: U32) -> {fst_or(SC.append(Nat, a, b), q) == fst_or(a, fst_or(b, q)) : U32}:
37	  match a:
38	    case Nil{}:
39	      {==}
40	    case Con{+h, +t}:
41	      {==}
42	
43	def last_app(+a: List<&2, Nat>, +b: List<&2, Nat>, +p: U32) -> {last_or(SC.append(Nat, a, b), p) == last_or(b, last_or(a, p)) : U32}:
44	  match a:
45	    case Nil{}:
46	      {==}
47	    case Con{+h, +t}:
48	      last_app(t, b, lnk(h))
49	
50	def last_lnk(+t: List<&2, Nat>, +a: Nat) -> {last_or(t, lnk(a)) == lnk(NL.lastn(t, a)) : U32}:
51	  match t:
52	    case Nil{}:
53	      {==}
54	    case Con{+b, +t2}:
55	      last_lnk(t2, b)
56	
57	def fo_rapp(+l: List<&2, Nat>, +b: List<&2, Nat>, +d: U32) -> {fst_or(NL.rapp(l, b), d) == last_or(l, fst_or(b, d)) : U32}:
58	  match l:
59	    case Nil{}:
60	      {==}
61	    case Con{+x, +r}:
62	      fo_rapp(r, Con{x, b}, d)
63	
64	def slot_link(+one: Nat, +h1: {one == 1n : Nat}, +s: U32, +hs: {Nat.is_lt(1n+UD.v(s), WD.sc(32n, one)) == True{} : Bool}) -> {UD.v(H.slot(H.link(s))) == UD.v(s) : Nat}:
65	  +lv = W32.link_val(one, h1, s, hs)
66	  +hle = L.subst(Nat, z => {Nat.is_le(1n, z) == True{} : Bool}, 1n+UD.v(s), UD.v(H.link(s)), Equal.sym(Nat, UD.v(H.link(s)), 1n+UD.v(s), lv), N.zero_le(UD.v(s)))
67	  Equal.trans(Nat, UD.v(H.slot(H.link(s))), Nat.sub(UD.v(H.link(s)), 1n), UD.v(s), UW.sub_nat(H.link(s), 1, hle), Equal.trans(Nat, Nat.sub(UD.v(H.link(s)), 1n), Nat.sub(1n+UD.v(s), 1n), UD.v(s), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n), UD.v(H.link(s)), 1n+UD.v(s), lv), N.sub_zero(UD.v(s))))
68	
69	def slot_lnk(+one: Nat, +h1: {one == 1n : Nat}, +s: Nat, +sd: Nat, +hsd: {Nat.is_lt(1n+sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(s, SC.pow2(sd)) == True{} : Bool}) -> {UD.v(H.slot(lnk(s))) == s : Nat}:
70	  +hk = N.lt_le(sd, 32n, N.lt_trans(sd, 1n+sd, 32n, N.lt_succ(sd), hsd))
71	  +e1 = UW.to_nat_from_nat(s, sd, hk, hs)
72	  +hs2 = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(sd)) == True{} : Bool}, s, UD.v(U32.from_nat(s)), Equal.sym(Nat, UD.v(U32.from_nat(s)), s, e1), hs)
73	  Equal.trans(Nat, UD.v(H.slot(lnk(s))), UD.v(U32.from_nat(s)), s, slot_link(one, h1, U32.from_nat(s), W32.bound32(one, h1, UD.v(U32.from_nat(s)), sd, hsd, hs2)), e1)