From 889197535fdca93f493df55fd4271155b18cd16a Mon Sep 17 00:00:00 2001
From: Viktor Fukala <5254810+vfukala@users.noreply.github.com>
Date: Sun, 11 Aug 2024 15:52:32 +0100
Subject: [PATCH] Document some missing automation

---
 .../failing_sepapps_initialization.v          | 50 +++++++++++++++
 .../missing_simplification.v                  | 64 +++++++++++++++++++
 2 files changed, 114 insertions(+)
 create mode 100644 LiveVerif/src/LiveVerifExamples/failing_sepapps_initialization.v
 create mode 100644 LiveVerif/src/LiveVerifExamples/missing_simplification.v

diff --git a/LiveVerif/src/LiveVerifExamples/failing_sepapps_initialization.v b/LiveVerif/src/LiveVerifExamples/failing_sepapps_initialization.v
new file mode 100644
index 000000000..51542624e
--- /dev/null
+++ b/LiveVerif/src/LiveVerifExamples/failing_sepapps_initialization.v
@@ -0,0 +1,50 @@
+(* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *)
+Require Import LiveVerif.LiveVerifLib.
+Require Import LiveVerifExamples.onesize_malloc.
+
+Load LiveVerif.
+
+Context {word_map: map.map word word}.
+Context {word_map_ok: map.ok word_map}.
+
+Context {consts: malloc_constants}.
+
+(* This file showcases a scenario where the framework cannot automatically prove
+   that we properly initialized a record for which we allocated memory using `Malloc`.
+
+   Inspired by what came up in the crit-bit tree verification. *)
+
+#[export] Instance spec_of_allocate_two: fnspec :=                        .**/
+
+uintptr_t allocate_two( ) /**#
+  ghost_args := (R: mem -> Prop);
+  requires t m := <{ * allocator * R }> m;
+  ensures t' m' res := t' = t
+           /\ <{ * (if \[res] =? 0 then
+                     allocator_failed_below 8
+                    else
+                     <{ * allocator
+                        * freeable 8 res
+                        * <{ + uintptr /[0]
+                             + uintptr /[0] }> res }>)
+                 * R }> m' #**/                                            /**.
+Derive allocate_two SuchThat (fun_correct! allocate_two)
+  As allocate_two_ok.                                                           .**/
+{                                                                          /**. .**/
+  uintptr_t p = Malloc(2 * sizeof(uintptr_t));                             /**. .**/
+  if (p == 0) /* split */ {                                                /**. .**/
+    return 0;                                                              /**. .**/
+  }                                                                        /**.
+  replace \[/[0]] with 0 in * by hwlia.
+  change (0 =? 0) with true in *. cbv iota in *. steps. .**/
+  else {                                                                   /**.
+  replace (\[p] =? 0) with false in * by hwlia. .**/
+    store(p, 0);                                                           /**. .**/
+    store(p + 4, 0);                                                       /**. .**/
+    return p;                                                              /**. .**/
+  }                                                                        /**.
+  replace (\[p] =? 0) with false in * by hwlia. steps.
+  assert_fails (
+                                                                                .**/
+}                                                                          /**).
+Abort.
diff --git a/LiveVerif/src/LiveVerifExamples/missing_simplification.v b/LiveVerif/src/LiveVerifExamples/missing_simplification.v
new file mode 100644
index 000000000..24c5a307a
--- /dev/null
+++ b/LiveVerif/src/LiveVerifExamples/missing_simplification.v
@@ -0,0 +1,64 @@
+(* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *)
+Require Import LiveVerif.LiveVerifLib.
+
+Load LiveVerif.
+
+Context {word_map: map.map word word}.
+Context {word_map_ok: map.ok word_map}.
+
+(* This file showcases scenarios where the framework cannot automatically prove
+   something because it misses a simplification involving word and/or Z.
+
+   Inspired by what came up in the crit-bit tree verification. *)
+
+#[export] Instance spec_of_return_zero: fnspec :=                                   .**/
+
+uintptr_t return_zero( ) /**#
+  ghost_args := (R: mem -> Prop);
+  requires t m := True;
+  ensures t' m' res := t' = t
+           /\ <{ * (if \[res] =? 0 then emp True else emp False) * R }> m'
+           #**/                         /**.
+Derive return_zero SuchThat (fun_correct! return_zero)
+  As return_zero_ok.                                                                .**/
+{                                                                              /**. .**/
+  return 0;                                                                    /**. .**/
+}                                                                              /*?.
+  step. step. step.
+
+  (* the condition of the `if` should simplify here *)
+  assert_fails step.
+Abort.
+
+#[export] Instance spec_of_zero_out: fnspec :=                                      .**/
+
+void zero_out(uintptr_t p) /**#
+  ghost_args := (R: mem -> Prop);
+  requires t m := <{ * (if \[p] =? 0 then emp True else EX v, uintptr v p) * R  }> m;
+  ensures t' m' := t' = t
+           /\ <{ * (if \[p] =? 0 then emp True else uintptr /[0] p)
+                 * R }> m' #**/                                                /**.
+Derive zero_out SuchThat (fun_correct! zero_out)
+  As zero_out_ok.                                                                   .**/
+{                                                                              /**. .**/
+  if (p != 0) /* split */ {                                                    /**. .**/
+    store(p, 0);                                                               /**.
+  (* this should actually work without errors *)
+  match goal with
+  | H: tactic_error _ |- _ => clear H
+  end.
+  replace (\[p] =? 0) with false in * by hwlia.
+  steps. .**/
+  }                                                                            /**. .**/
+  else {                                                                       /**. .**/
+  }                                                                            /**.
+  (* this should be immediately `ready` *)
+  Fail
+    match goal with
+    | |- ready => idtac
+    end.
+  replace (\[p] =? 0) with true in * by hwlia.
+  replace (0 =? 0) with true in * by hwlia.
+  steps.                                                                            .**/
+}                                                                              /**.
+Qed.