1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../../spec/lib/common.bend as SC
5	import ../../../src/containers/bitset.bend as B
6	import ./model.bend as MD
7	import ./index.bend as IX
8	
9	# The word-list walks of proofs/bitset/model.bend, re-expressed as a single
10	# indexed access. This is the step that lets src/bitset.bend address the word
11	# directly (Base.Array, O(1)) instead of walking the list:
12	#
13	#   get_walk(ws, i)    = word_get(word wordix(i) of ws, bitix(i))
14	#   put_walk(ws, i, v) = ws with word wordix(i) replaced by
15	#                        word_put(v, that word, bitix(i))
16	
17	# Word q of the list (0 beyond the end; the callers always stay in range).
18	def nthw(ws: List<&2, U32>, q: Nat) -> U32:
19	  match ws q:
20	    case Nil{} _:
21	      0
22	    case Con{w, t} 0n:
23	      w
24	    case Con{w, t} 1n+p:
25	      nthw(t, p)
26	
27	def shrn_zero(+k: Nat) -> {U32.shrn(0, k) == 0 : U32}:
28	  match k:
29	    case 0n:
30	      {==}
31	    case 1n+p:
32	      %Equal.sym(U32, U32.shrn(0, p), 0, shrn_zero(p)) : {U32.shr(_) == 0 : U32}
33	      {==}
34	
35	def word_get_zero(+k: Nat) -> {B.word_get(0, k) == False{} : Bool}:
36	  %Equal.sym(U32, U32.shrn(0, k), 0, shrn_zero(k)) : {B.low(_) == False{} : Bool}
37	  {==}
38	
39	# ---- get ----
40	
41	def get_case(+w: U32, +t: List<&2, U32>, +i: Nat, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +ih: {MD.get_walk(t, Nat.sub(i, 32n)) == B.word_get(nthw(t, B.wordix(Nat.sub(i, 32n))), B.bitix(Nat.sub(i, 32n))) : Bool}) -> {MD.get_pick(b, w, i, MD.get_walk(t, Nat.sub(i, 32n))) == B.word_get(nthw(Con{w, t}, B.wordix(i)), B.bitix(i)) : Bool}:
42	  match b:
43	    case True{}:
44	      %Equal.sym(Nat, B.wordix(i), 0n, IX.wordix_small(i, eb)) : {B.word_get(w, i) == B.word_get(nthw(Con{w, t}, _), B.bitix(i)) : Bool}
45	      %Equal.sym(Nat, B.bitix(i), i, IX.bitix_small(i, eb)) : {B.word_get(w, i) == B.word_get(w, _) : Bool}
46	      {==}
47	    case False{}:
48	      %Equal.sym(Nat, B.wordix(i), 1n+B.wordix(Nat.sub(i, 32n)), IX.wordix_step(i, eb)) : {MD.get_walk(t, Nat.sub(i, 32n)) == B.word_get(nthw(Con{w, t}, _), B.bitix(i)) : Bool}
49	      %Equal.sym(Nat, B.bitix(i), B.bitix(Nat.sub(i, 32n)), IX.bitix_step(i, eb)) : {MD.get_walk(t, Nat.sub(i, 32n)) == B.word_get(nthw(t, B.wordix(Nat.sub(i, 32n))), _) : Bool}
50	      ih
51	
52	def get_index(ws: List<&2, U32>, +i: Nat) -> {MD.get_walk(ws, i) == B.word_get(nthw(ws, B.wordix(i)), B.bitix(i)) : Bool}:
53	  match ws:
54	    case Nil{}:
55	      Equal.sym(Bool, B.word_get(0, B.bitix(i)), False{}, word_get_zero(B.bitix(i)))
56	    case Con{+w, +t}:
57	      get_case(w, t, i, Nat.is_lt(i, 32n), {==}, get_index(t, Nat.sub(i, 32n)))
58	
59	# ---- put ----
60	
61	def put_case(+v: Bool, +w: U32, +t: List<&2, U32>, +i: Nat, b: Bool, +eb: {Nat.is_lt(i, 32n) == b : Bool}, +ih: {MD.put_walk(t, Nat.sub(i, 32n), v) == SC.update(U32, t, B.wordix(Nat.sub(i, 32n)), B.word_put(v, nthw(t, B.wordix(Nat.sub(i, 32n))), B.bitix(Nat.sub(i, 32n)))) : List<&2, U32>}) -> {MD.put_pick(b, v, w, i, t, MD.put_walk(t, Nat.sub(i, 32n), v)) == SC.update(U32, Con{w, t}, B.wordix(i), B.word_put(v, nthw(Con{w, t}, B.wordix(i)), B.bitix(i))) : List<&2, U32>}:
62	  match b:
63	    case True{}:
64	      %Equal.sym(Nat, B.wordix(i), 0n, IX.wordix_small(i, eb)) : {Con{B.word_put(v, w, i), t} == SC.update(U32, Con{w, t}, _, B.word_put(v, nthw(Con{w, t}, _), B.bitix(i))) : List<&2, U32>}
65	      %Equal.sym(Nat, B.bitix(i), i, IX.bitix_small(i, eb)) : {Con{B.word_put(v, w, i), t} == Con{B.word_put(v, w, _), t} : List<&2, U32>}
66	      {==}
67	    case False{}:
68	      %Equal.sym(Nat, B.wordix(i), 1n+B.wordix(Nat.sub(i, 32n)), IX.wordix_step(i, eb)) : {Con{w, MD.put_walk(t, Nat.sub(i, 32n), v)} == SC.update(U32, Con{w, t}, _, B.word_put(v, nthw(Con{w, t}, _), B.bitix(i))) : List<&2, U32>}
69	      %Equal.sym(Nat, B.bitix(i), B.bitix(Nat.sub(i, 32n)), IX.bitix_step(i, eb)) : {Con{w, MD.put_walk(t, Nat.sub(i, 32n), v)} == Con{w, SC.update(U32, t, B.wordix(Nat.sub(i, 32n)), B.word_put(v, nthw(t, B.wordix(Nat.sub(i, 32n))), _))} : List<&2, U32>}
70	      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{w, z},
71	        MD.put_walk(t, Nat.sub(i, 32n), v),
72	        SC.update(U32, t, B.wordix(Nat.sub(i, 32n)), B.word_put(v, nthw(t, B.wordix(Nat.sub(i, 32n))), B.bitix(Nat.sub(i, 32n)))),
73	        ih)
74	
75	def put_index(ws: List<&2, U32>, +i: Nat, +v: Bool) -> {MD.put_walk(ws, i, v) == SC.update(U32, ws, B.wordix(i), B.word_put(v, nthw(ws, B.wordix(i)), B.bitix(i))) : List<&2, U32>}:
76	  match ws:
77	    case Nil{}:
78	      {==}
79	    case Con{+w, +t}:
80	      put_case(v, w, t, i, Nat.is_lt(i, 32n), {==}, put_index(t, Nat.sub(i, 32n), v))
81	
82	# ---- nthw is nth in range ----
83	
84	def nthw_nth(ws: List<&2, U32>, q: Nat, +h: {Nat.is_lt(q, SC.length(U32, ws)) == True{} : Bool}) -> {SC.nth(U32, ws, q) == Some{nthw(ws, q)} : Maybe<&2, U32>}:
85	  match ws q:
86	    case Nil{} _:
87	      Empty.absurd({SC.nth(U32, Nil{}, q) == Some{nthw(Nil{}, q)} : Maybe<&2, U32>}, N.lt_zero_absurd(q, h))
88	    case Con{w, t} 0n:
89	      {==}
90	    case Con{w, t} 1n+p:
91	      nthw_nth(t, p, h)