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/bitlist.bend as BLI
6	import ../dynamic_array/state.bend as DAS
7	import ../bitset/lists.bend as BL
8	import ../bitset/state.bend as ST
9	import ../../../spec/containers/bitlist.bend as S
10	import ./da.bend as DI
11	
12	# Shadow, invariant and abstraction of a bitlist.
13	#   shadow  BSh{limit, len, w}: w is a good dynamic-array shadow of the words
14	#   F       ST.flat(DI.ws(w)): every stored bit, word by word, bit 0 first
15	#   good    the word array is good and ST.invf(len, F): len <= |F| and every
16	#           stored bit at a position >= len is zero (the masked tail)
17	#   model   S.M{limit, DI.lim(w), take(F, len)}: the storage capacity exponent
18	#           is the word array's depth limit (2^lim words of 32 bits)
19	# (source: proofs/containers/bitlist/state.src)
20	
21	
22	type Sh is Data:
23	  BSh{limit: Maybe<&2, Nat>, len: Nat, w: DAS.Shadow<U32>}
24	
25	def fl(w: DAS.Shadow<U32>) -> List<&2, Bool>:
26	  ST.flat(DI.ws(w))
27	
28	def real(sh: Sh) -> BLI.Bitlist:
29	  match sh:
30	    case BSh{l, n, w}:
31	      BLI.BL{l, n, DAS.real(U32, w)}
32	
33	def good(sh: Sh) -> Bool:
34	  match sh:
35	    case BSh{l, +n, +w}:
36	      Bool.and(DAS.good(U32, w), ST.invf(n, fl(w)))
37	
38	def model(sh: Sh) -> S.Model:
39	  match sh:
40	    case BSh{l, +n, +w}:
41	      S.M{l, DI.lim(w), SC.take(Bool, fl(w), n)}
42	
43	
44	def g_w(+l: Maybe<&2, Nat>, +n: Nat, +w: DAS.Shadow<U32>, +g: {good(BSh{l, n, w}) == True{} : Bool}) -> {DAS.good(U32, w) == True{} : Bool}:
45	  L.and_left(DAS.good(U32, w), ST.invf(n, fl(w)), g)
46	
47	def g_inv(+l: Maybe<&2, Nat>, +n: Nat, +w: DAS.Shadow<U32>, +g: {good(BSh{l, n, w}) == True{} : Bool}) -> {ST.invf(n, fl(w)) == True{} : Bool}:
48	  L.and_right(DAS.good(U32, w), ST.invf(n, fl(w)), g)
49	
50	def g_mk(+l: Maybe<&2, Nat>, +n: Nat, +w: DAS.Shadow<U32>, +gw: {DAS.good(U32, w) == True{} : Bool}, +gi: {ST.invf(n, fl(w)) == True{} : Bool}) -> {good(BSh{l, n, w}) == True{} : Bool}:
51	  L.and_intro(DAS.good(U32, w), ST.invf(n, fl(w)), gw, gi)
52	
53	# A word array with the same words: the invariant and the model carry over.
54	def same_good(+l: Maybe<&2, Nat>, +n: Nat, +w: DAS.Shadow<U32>, +w2: DAS.Shadow<U32>, +gw2: {DAS.good(U32, w2) == True{} : Bool}, +e: {DI.ws(w2) == DI.ws(w) : List<&2, U32>}, +g: {good(BSh{l, n, w}) == True{} : Bool}) -> {good(BSh{l, n, w2}) == True{} : Bool}:
55	  g_mk(l, n, w2, gw2, L.subst(List<&2, U32>, z => {ST.invf(n, ST.flat(z)) == True{} : Bool}, DI.ws(w), DI.ws(w2), Equal.sym(List<&2, U32>, DI.ws(w2), DI.ws(w), e), g_inv(l, n, w, g)))
56	
57	# The model of a shadow with given words and depth limit.
58	def model_of(+l: Maybe<&2, Nat>, +n: Nat, +w2: DAS.Shadow<U32>, +xs: List<&2, U32>, +c: Nat, +e: {DI.ws(w2) == xs : List<&2, U32>}, +ec: {DI.lim(w2) == c : Nat}) -> {model(BSh{l, n, w2}) == S.M{l, c, SC.take(Bool, ST.flat(xs), n)} : S.Model}:
59	  %Equal.sym(List<&2, U32>, DI.ws(w2), xs, e) : {S.M{l, DI.lim(w2), SC.take(Bool, ST.flat(_), n)} == S.M{l, c, SC.take(Bool, ST.flat(xs), n)} : S.Model}
60	  %Equal.sym(Nat, DI.lim(w2), c, ec) : {S.M{l, _, SC.take(Bool, ST.flat(xs), n)} == S.M{l, c, SC.take(Bool, ST.flat(xs), n)} : S.Model}
61	  {==}
62	
63	def good_of(+l: Maybe<&2, Nat>, +n: Nat, +w2: DAS.Shadow<U32>, +xs: List<&2, U32>, +gw2: {DAS.good(U32, w2) == True{} : Bool}, +e: {DI.ws(w2) == xs : List<&2, U32>}, +gi: {ST.invf(n, ST.flat(xs)) == True{} : Bool}) -> {good(BSh{l, n, w2}) == True{} : Bool}:
64	  g_mk(l, n, w2, gw2, L.subst(List<&2, U32>, z => {ST.invf(n, ST.flat(z)) == True{} : Bool}, xs, DI.ws(w2), Equal.sym(List<&2, U32>, DI.ws(w2), xs, e), gi))