1	import Base
2	import ../../lib/array.bend as AR
3	import ../../../spec/containers/lru.bend as SP
4	import ../../../src/containers/lru.bend as LR
5	import ./state.bend as ST
6	import ../../lib/words32.bend as W32
7	
8	# new: the implementation's new is the specification's new.
9	
10	def empty(~V: Data, +cap: U32) -> ST.Sh<V>:
11	  ST.LS{cap, 0, 0, 0, 0, AR.freeze(U32, LR.meta0()), 1n, 0n, AR.freeze(U32, Array.new(U32, 2n, 0)), AR.freeze(String, Array.new(String, 0n, "")), AR.TLeaf{None{}}, AR.freeze(U32, Array.new(U32, 3n, 0)), Nil{}, Nil{}}
12	
13	def MadeOK(~V: Data, r: LR.Made<&2, V>, s: SP.Made<V>) -> Type:
14	  match r s:
15	    case LR.Made{f} SP.Made{l}:
16	      Sigma<&1, &1, ST.Sh<V>, sh => {f == ST.real(~V, sh) : LR.LRU<&2, V>} & ({l == ST.model(~V, sh) : SP.Lru<V>} & {ST.good(~V, sh) == True{} : Bool})>
17	    case LR.Made{f} SP.Rejected{b}:
18	      Empty
19	    case LR.Rejected{a} SP.Made{l}:
20	      Empty
21	    case LR.Rejected{a} SP.Rejected{b}:
22	      {a == b : String}
23	
24	def good_empty(~V: Data, +cap: U32, +hz: {U32.is_eq(cap, 0) == False{} : Bool}) -> {ST.good(~V, empty(~V, cap)) == True{} : Bool}:
25	  +m = AR.freeze(U32, LR.meta0())
26	  +t = AR.freeze(U32, Array.new(U32, 2n, 0))
27	  +kt = AR.freeze(String, Array.new(String, 0n, ""))
28	  +l = AR.freeze(U32, Array.new(U32, 3n, 0))
29	  +kl = AR.slots(String, kt)
30	  +pk = AR.perfect(String, 0n, kt)
31	  +e = {AR.TLeaf{None{}} : AR.Tree<Maybe<&2, V>>}
32	  ST.good_intro(~V, cap, 0, 0, 0, 0, W32.nth0(AR.slots(U32, m), 0n), W32.nth0(AR.slots(U32, m), 1n), W32.nth0(AR.slots(U32, m), 2n), W32.nth0(AR.slots(U32, m), 6n), W32.nth0(AR.slots(U32, m), 7n), AR.perfect(U32, 5n, m), 1n, 0n, t, kl, pk, e, l, Nil{}, Nil{}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, Equal.cong(Bool, Bool, b => Bool.not(b), U32.is_eq(cap, 0), False{}, hz), {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==}, {==})
33	
34	def new_c(~V: Data, +cap: U32, +z: Bool, +hz: {U32.is_eq(cap, 0) == z : Bool}, +r: Bool) -> MadeOK(~V, LR.new_checked(&2, V, cap, z, r), SP.new_c(~V, cap, z, r)):
35	  match z r:
36	    case True{} r2:
37	      {==}
38	    case False{} True{}:
39	      {==}
40	    case False{} False{}:
41	      (empty(~V, cap), ({==}, ({==}, good_empty(~V, cap, hz))))
42	
43	# THEOREM: new rejects what the specification rejects, with its reason, and
44	# otherwise builds the specification's empty cache.
45	def new_ok(~V: Data, +cap: U32) -> MadeOK(~V, LR.new(&2, V, cap), SP.new(~V, cap)):
46	  new_c(~V, cap, U32.is_eq(cap, 0), {==}, U32.is_eq(cap, 4294967295))