1	import Base
2	import ../lib/common.bend as SC
3	import ../../src/containers/hash_table.bend as H
4	
5	# Independent model: a map from String keys to values is an association
6	# list with at most one entry per key. Nothing here refers to buckets,
7	# hashing, probing or slots.
8	
9	type Entry<-V: Data> is Data:
10	  E{key: String, val: V}
11	
12	def chr_eq(a: Char, b: Char) -> Bool:
13	  match a b:
14	    case Chr{x} Chr{y}:
15	      U32.is_eq(x, y)
16	
17	def str_eq(a: String, b: String) -> Bool:
18	  match a b:
19	    case SNil{} SNil{}:
20	      True{}
21	    case SNil{} SCon{h, t}:
22	      False{}
23	    case SCon{h, t} SNil{}:
24	      False{}
25	    case SCon{x, s} SCon{y, t}:
26	      Bool.and(chr_eq(x, y), str_eq(s, t))
27	
28	def lookup(~V: Data, m: List<&2, Entry<V>>, +k: String) -> Maybe<&2, V>:
29	  match m:
30	    case Nil{}:
31	      None{}
32	    case Con{E{+j, +v}, t}:
33	      Bool.pick(Maybe<&2, V>, str_eq(j, k), Some{v}, lookup(~V, t, k))
34	
35	def is_some(~V: Data, m: Maybe<&2, V>) -> Bool:
36	  match m:
37	    case None{}:
38	      False{}
39	    case Some{v}:
40	      True{}
41	
42	def has(~V: Data, m: List<&2, Entry<V>>, +k: String) -> Bool:
43	  is_some(~V, lookup(~V, m, k))
44	
45	# Replace the entry of k in place, or add it at the end.
46	def set(~V: Data, m: List<&2, Entry<V>>, +k: String, +x: V) -> List<&2, Entry<V>>:
47	  match m:
48	    case Nil{}:
49	      Con{E{k, x}, Nil{}}
50	    case Con{E{+j, +v}, +t}:
51	      Bool.pick(List<&2, Entry<V>>, str_eq(j, k), Con{E{k, x}, t}, Con{E{j, v}, set(~V, t, k, x)})
52	
53	def remove(~V: Data, m: List<&2, Entry<V>>, +k: String) -> List<&2, Entry<V>>:
54	  match m:
55	    case Nil{}:
56	      Nil{}
57	    case Con{E{+j, +v}, +t}:
58	      Bool.pick(List<&2, Entry<V>>, str_eq(j, k), t, Con{E{j, v}, remove(~V, t, k)})
59	
60	def keys(~V: Data, m: List<&2, Entry<V>>) -> List<&2, String>:
61	  match m:
62	    case Nil{}:
63	      Nil{}
64	    case Con{E{j, v}, t}:
65	      Con{j, keys(~V, t)}
66	
67	def size(~V: Data, m: List<&2, Entry<V>>) -> Nat:
68	  match m:
69	    case Nil{}:
70	      0n
71	    case Con{e, t}:
72	      1n+size(~V, t)
73	
74	def mem(+k: String, ks: List<&2, String>) -> Bool:
75	  match ks:
76	    case Nil{}:
77	      False{}
78	    case Con{j, t}:
79	      Bool.or(str_eq(j, k), mem(k, t))
80	
81	def nodup(ks: List<&2, String>) -> Bool:
82	  match ks:
83	    case Nil{}:
84	      True{}
85	    case Con{+j, +t}:
86	      Bool.and(Bool.not(mem(j, t)), nodup(t))
87	
88	def get_m(~V: Data, dflt: V, m: Maybe<&2, V>) -> V:
89	  match m:
90	    case None{}:
91	      dflt
92	    case Some{v}:
93	      v
94	
95	# the value of key, or dflt
96	def get(~V: Data, dflt: V, m: List<&2, Entry<V>>, +key: String) -> V:
97	  get_m(~V, dflt, lookup(~V, m, key))
98	
99	# ---- contract (SPARK formal containers) ----
100	# Each `<Subprogram>.<clause>` definition below states one Post clause of
101	# that SPARK subprogram, as a proposition on this model; the table names the
102	# clauses. proofs/containers/hash_table/ proves every clause under its clause name,
103	# and its `impl` lemma carries them to the implementation.
104	#
105	# Contracts of the hash map in the style of SPARK's formal hashed maps
106	# (SPARKlib spark-containers-formal-hashed_maps.ads). The proofs in
107	# set/pop/keysw.bend relate every operation to the specification's
108	# association list; this module states, per operation, what changes and
109	# what is preserved, over three views of a map sh:
110	#   Model   S.lookup(ST.model(sh), q)  the value of every key q
111	#   Length  S.size(ST.model(sh))
112	#   Keys    S.keys(ST.model(sh))       the keys, in iteration order
113	# Keys are compared by S.str_eq, which is an equivalence under which equal
114	# keys are identical strings (so, like SPARK's Equivalent_Keys, every
115	# function of a key, the hash included, agrees on equivalent keys).
116	# SPARK's cursor model (Positions) has no counterpart: the map has no
117	# cursors.
118	#
119	#   SPARK subprogram (hashed_maps.ads line, AdaCore/SPARKlib master)   ours   lemmas
120	#   Empty_Map (103)                   new     new_model, new_length, new_absent
121	#   Length (117)                      size    length_value, length_frame (P.size_ok)
122	#   Element (Key) (1039)              get     element_value, element_default (P.get_ok)
123	#   Contains (1032)                   has     contains_value (P.has_ok)
124	#   Include (729)                     set     SetContract / SetPost (set_post)
125	#   Delete (Key) (891), Exclude (851) pop, del  PopContract, DelContract / DelPost
126	#   Iter_Model / Keys (1078)          keys    KeysContract / KeysPost
127	#   Equivalent_Keys                   str_eq  key_refl, key_sym, key_trans, key_same, key_respect
128	# Not in this API: "=", Capacity, Reserve_Capacity, Is_Empty, Clear,
129	# Assign/Copy/Move, Replace_Element/Reference (by cursor), Insert (fails
130	# if present) and Replace (fails if absent), which Include subsumes,
131	# First/Next/Has_Element/Key (cursors), Find, Default_Modulus.
132	
133	# ---- keys ----
134	# The key sequence (SPARK's Keys): no key twice, as long as the map, and
135	# holding exactly the keys the model has.
136	def KeysPost(~V: Data, m: List<&2, Entry<V>>) -> Type:
137	  {nodup(keys(~V, m)) == True{} : Bool} & ({SC.length(String, keys(~V, m)) == size(~V, m) : Nat} & (@+q: String -> {mem(q, keys(~V, m)) == has(~V, m, q) : Bool}))
138	
139	# ---- set (SPARK's Include: insert, or replace the value) ----
140	def SetPost(~V: Data, m: List<&2, Entry<V>>, m2: List<&2, Entry<V>>, key: String, x: V) -> Type:
141	  {has(~V, m2, key) == True{} : Bool} & ((@+q: String -> @+hq: {str_eq(key, q) == True{} : Bool} -> {lookup(~V, m2, q) == Some{x} : Maybe<&2, V>}) & ((@+q: String -> @+hq: {str_eq(key, q) == False{} : Bool} -> {lookup(~V, m2, q) == lookup(~V, m, q) : Maybe<&2, V>}) & ({size(~V, m2) == Bool.pick(Nat, has(~V, m, key), size(~V, m), 1n+size(~V, m)) : Nat} & ((@+q: String -> {mem(q, keys(~V, m2)) == Bool.or(str_eq(key, q), mem(q, keys(~V, m))) : Bool}) & ({nodup(keys(~V, m2)) == True{} : Bool} & (@+hp: {has(~V, m, key) == True{} : Bool} -> {keys(~V, m2) == keys(~V, m) : List<&2, String>}))))))
142	
143	# ---- pop and del (SPARK's Delete/Exclude) ----
144	def DelPost(~V: Data, m: List<&2, Entry<V>>, m2: List<&2, Entry<V>>, key: String) -> Type:
145	  {has(~V, m2, key) == False{} : Bool} & ((@+q: String -> @+hq: {str_eq(key, q) == False{} : Bool} -> {lookup(~V, m2, q) == lookup(~V, m, q) : Maybe<&2, V>}) & ((@+hn: {has(~V, m, key) == False{} : Bool} -> @+q: String -> {lookup(~V, m2, q) == lookup(~V, m, q) : Maybe<&2, V>}) & ({Bool.pick(Nat, has(~V, m, key), 1n+size(~V, m2), size(~V, m2)) == size(~V, m) : Nat} & ((@+q: String -> {mem(q, keys(~V, m2)) == Bool.and(Bool.not(str_eq(key, q)), mem(q, keys(~V, m))) : Bool}) & {nodup(keys(~V, m2)) == True{} : Bool}))))
146	
147	# Equivalent_Keys
148	def Equivalent_Keys.key_refl(+a: String) -> Type:
149	  {str_eq(a, a) == True{} : Bool}
150	
151	# Equivalent_Keys
152	def Equivalent_Keys.key_sym(+a: String, +b: String) -> Type:
153	  {str_eq(a, b) == str_eq(b, a) : Bool}
154	
155	# Equivalent_Keys
156	def Equivalent_Keys.key_trans(+a: String, +b: String, +c: String, +hab: {str_eq(a, b) == True{} : Bool}, +hbc: {str_eq(b, c) == True{} : Bool}) -> Type:
157	  {str_eq(a, c) == True{} : Bool}
158	
159	# Equivalent_Keys
160	def Equivalent_Keys.key_same(+a: String, +b: String, +h: {str_eq(a, b) == True{} : Bool}) -> Type:
161	  {a == b : String}
162	
163	# Equivalent_Keys
164	def Equivalent_Keys.key_respect(~A: Data, ~f: String -> A, +a: String, +b: String, +h: {str_eq(a, b) == True{} : Bool}) -> Type:
165	  {f(a) == f(b) : A}
166	
167	# Include (729)
168	def Include.set_post(~V: Data, ~m: List<&2, Entry<V>>, ~m2: List<&2, Entry<V>>, ~key: String, ~x: V, ~hp: (@+q: String -> {lookup(~V, m2, q) == lookup(~V, set(~V, m, key, x), q) : Maybe<&2, V>}) & {size(~V, m2) == size(~V, set(~V, m, key, x)) : Nat}, +hnd: {nodup(keys(~V, m2)) == True{} : Bool}, hk: @+hq0: {has(~V, m, key) == True{} : Bool} -> {keys(~V, m2) == keys(~V, m) : List<&2, String>}) -> Type:
169	  SetPost(~V, m, m2, key, x)
170	
171	# The queries are stated on what they return: `r` is the value the operation
172	# produces on a map whose model is `m` (the proof package instantiates it with
173	# the implementation's result).
174	
175	# Element (SPARKlib formal-hashed-maps.ads): Element (Container, Key) = Get (Model, Key)
176	def Element.element_value(~V: Data, m: List<&2, Entry<V>>, +key: String, +x: V, +hl: {lookup(~V, m, key) == Some{x} : Maybe<&2, V>}, r: V) -> Type:
177	  {r == x : V}
178	
179	# Element without the key: get returns the caller's default (the Pre of
180	# Element is Contains; here the absent case is defined, not excluded)
181	def Element.element_default(~V: Data, m: List<&2, Entry<V>>, +key: String, +dflt: V, +hl: {lookup(~V, m, key) == None{} : Maybe<&2, V>}, r: V) -> Type:
182	  {r == dflt : V}
183	
184	# Contains: Contains (Container, Key) = Has_Key (Model, Key)
185	def Contains.contains_value(~V: Data, m: List<&2, Entry<V>>, +key: String, r: Bool) -> Type:
186	  {r == is_some(~V, lookup(~V, m, key)) : Bool}
187	
188	# Length: Length (Container) = M.Length (Model)
189	def Length.length_value(~V: Data, m: List<&2, Entry<V>>, +n: Nat) -> Type:
190	  {n == SC.length(String, keys(~V, m)) : Nat}
191	
192	# Length is a query: the map is returned unchanged
193	def Length.length_frame(~V: Data, a: H.HashMap<&2, V>, b: H.HashMap<&2, V>) -> Type:
194	  {b == a : H.HashMap<&2, V>}
195	
196	# Empty_Map: Is_Empty (Model), Length = 0, no key present
197	def Empty_Map.new_model(~V: Data, m: List<&2, Entry<V>>) -> Type:
198	  {m == Nil{} : List<&2, Entry<V>>}
199	
200	def Empty_Map.new_length(~V: Data, m: List<&2, Entry<V>>) -> Type:
201	  {size(~V, m) == 0n : Nat}
202	
203	def Empty_Map.new_absent(~V: Data, m: List<&2, Entry<V>>, +key: String) -> Type:
204	  {lookup(~V, m, key) == None{} : Maybe<&2, V>}