add succint 'unit test-like' demonstrator

Author: squell

proofs/sudoers.mlw

@@ -436,4 +436,37 @@ let expand_all_aliases (items: seq (spec 'tag 'a)) (table: seq (def 'a)) (ghost
   done;
   !cur
 
+let demonstration (items: seq (spec 'tag 'a)) (table: seq (def 'a)) (pred: 'a -> bool)
+  (* make sure the keys are uniquely defined *)
+  requires { forall i j. 0 <= i < j < length table ->
+               let (k1, _) = table[i] in
+               let (k2, _) = table[j] in
+               k1 <> k2 }
+
+  (* require all aliases to be defined in the table *)
+  requires { forall i. 0 <= i < length items ->
+               forall key. who items[i] = Alias key ->
+                 exists j. 0 <= j < length table /\ let (id, _) = table[j] in id = key }
+
+  (* make sure the table is topologically sorted *)
+  requires { forall i j. 0 <= i <= j < length table ->
+               let (_, items) = table[i] in
+               let (key, _) = table[j] in
+               forall k. 0 <= k < length items -> who items[k] <> Alias key }
+
+  (* this function also requires that it is grounded *)
+  requires { forall i. 0 <= i < length table ->
+               let (_, items) = table[i] in
+               forall k, key. 0 <= k < length items -> who items[k] = Alias key ->
+               exists j. 0 <= j < length table /\ let (id, _) = table[j] in id = key }
+
+= let aliases = get_aliases table pred in
+
+  let expanded = expand_all_aliases items table (ghost pred) (ghost aliases) in
+
+  let a = find_item expanded pred (any found_aliases) in
+  let b = find_item items pred aliases in
+
+  assert { a = b }
+
 end