support functions that don't use the heap

LiveVerif/src/LiveVerif/LiveProgramLogic.v

@@ -431,7 +431,15 @@ Ltac call lhs fname arges :=
         eapply H
     end
   | (* one dexprs1 goal containing argument evaluation, precondition, and continuation
-       after the call *) ].
+       after the call: *)
+    lazymatch goal with
+    | |- dexprs1 ?m ?l ?es ?vs (?calleePre /\ enable_frame_trick.enable_frame_trick ?cont) =>
+        lazymatch calleePre with
+        | context[m] => idtac (* default case: callee uses memory *)
+        | _ => (* special case: callee does not use memory *)
+            change (dexprs1 m l es vs (calleePre /\ cont))
+        end
+    end ].
 
 (* Assigns default well_founded relations to types.
    Use lower costs to override existing entries. *)
@@ -1446,6 +1454,79 @@ Notation "'void' fname ( ) /* *# 'ghost_args' := g1 .. gn ; 'requires' t1 m1 :=
  osemi custom optional_semicolon at level 1,
  only parsing).
 
+
+(* Same definitions but without ghost_args: *)
+
+(* One return value: *)
+Notation "'uintptr_t' fname ( 'uintptr_t' a1 , 'uintptr_t' .. , 'uintptr_t' an ) /* *# 'requires' t1 m1 := pre ; 'ensures' t2 m2 r := post #* osemi *" :=
+  (fun fname: String.string =>
+     (fun fs =>
+        (forall a1, .. (forall an,
+           (forall t1 m1, pre ->
+              WeakestPrecondition.call fs fname t1 m1
+                (@cons (@word.rep _ _) a1 .. (@cons (@word.rep _ _) an nil) ..)
+                (fun t2 m2 retvs => exists r, retvs = cons r nil /\ post))) .. ))
+     : ProgramLogic.spec_of fname)
+(in custom funspec at level 1,
+ fname name,
+ a1 closed binder, an closed binder,
+ t1 name, t2 name, m1 name, m2 name, r name,
+ pre constr at level 200,
+ post constr at level 200,
+ osemi custom optional_semicolon at level 1,
+ only parsing).
+
+(* One return value and no arguments: *)
+Notation "'uintptr_t' fname ( ) /* *# 'requires' t1 m1 := pre ; 'ensures' t2 m2 r := post #* osemi *" :=
+  (fun fname: String.string =>
+     (fun fs =>
+           (forall t1 m1, pre ->
+              WeakestPrecondition.call fs fname t1 m1 nil
+                (fun t2 m2 retvs => exists r, retvs = cons r nil /\ post)))
+     : ProgramLogic.spec_of fname)
+(in custom funspec at level 1,
+ fname name,
+ t1 name, t2 name, m1 name, m2 name, r name,
+ pre constr at level 200,
+ post constr at level 200,
+ osemi custom optional_semicolon at level 1,
+ only parsing).
+
+(* No return value: *)
+Notation "'void' fname ( 'uintptr_t' a1 , 'uintptr_t' .. , 'uintptr_t' an ) /* *# 'requires' t1 m1 := pre ; 'ensures' t2 m2 := post #* osemi *" :=
+  (fun fname: String.string =>
+     (fun fs =>
+        (forall a1, .. (forall an,
+           (forall t1 m1, pre ->
+              WeakestPrecondition.call fs fname t1 m1
+                (@cons (@word.rep _ _) a1 .. (@cons (@word.rep _ _) an nil) ..)
+                (fun t2 m2 retvs => retvs = nil /\ post))) .. ))
+     : ProgramLogic.spec_of fname)
+(in custom funspec at level 1,
+ fname name,
+ a1 closed binder, an closed binder,
+ t1 name, t2 name, m1 name, m2 name,
+ pre constr at level 200,
+ post constr at level 200,
+ osemi custom optional_semicolon at level 1,
+ only parsing).
+
+(* No return value an no arguments: *)
+Notation "'void' fname ( ) /* *# 'requires' t1 m1 := pre ; 'ensures' t2 m2 := post #* osemi *" :=
+  (fun fname: String.string =>
+     (fun fs =>
+        (forall t1 m1, pre ->
+           WeakestPrecondition.call fs fname t1 m1 nil
+              (fun t2 m2 retvs => retvs = nil /\ post)))
+     : ProgramLogic.spec_of fname)
+(in custom funspec at level 1,
+ fname name,
+ t1 name, t2 name, m1 name, m2 name,
+ pre constr at level 200,
+ post constr at level 200,
+ osemi custom optional_semicolon at level 1,
+ only parsing).
+
 Notation ".* */ x" :=
   (match x with (* <-- typecheck x before passing it to Ltac, to get better error messages *)
    | _ => ltac:(let r := with_ident_as_string_no_beta x in exact r)

LiveVerif/src/LiveVerif/PackageContext.v

@@ -192,12 +192,22 @@ Ltac add_equality_to_post x Post :=
   (* y (t or m or l or measure) will be patterned out at end of package_context *)
   move y at top.
 
+Ltac add_mem_equality_to_Post_or_move_at_top m Post :=
+  lazymatch type of Post with
+  | context[m] =>
+      (* current packaged context contains an assertion about memory (the usual case) *)
+      move m at top
+  | _ =>
+      (* we're in a function that does not use the heap at all *)
+      add_equality_to_post m Post
+  end.
+
 Ltac add_equalities_to_post Post :=
   lazymatch goal with
   (* loop pre/post *)
   | |- ?E (?Ghosts, ?Measure, ?T, ?M, ?L) =>
       add_equality_to_post L Post;
-      move M at top;
+      add_mem_equality_to_Post_or_move_at_top M Post;
       lazymatch type of Post with
       | context[T] => idtac (* current packaged context already says something about the
                                trace, so only keep that *)
@@ -208,13 +218,13 @@ Ltac add_equalities_to_post Post :=
   (* loop invariant *)
   | |- ?E ?Measure ?T ?M ?L =>
       add_equality_to_post L Post;
-      move M at top;
+      add_mem_equality_to_Post_or_move_at_top M Post;
       add_equality_to_post T Post;
       add_equality_to_post Measure Post
   (* if branch post *)
   | |- ?E ?T ?M ?L =>
       add_equality_to_post L Post;
-      move M at top;
+      add_mem_equality_to_Post_or_move_at_top M Post;
       add_equality_to_post T Post
   end.
 
@@ -237,7 +247,7 @@ Ltac move_mem_hyp_just_below_scope_marker :=
       end
       (* Note: the two above moves should be replaced by one single `move H below s`,
          but `below` is not implemented yet: https://github.com/coq/coq/issues/15209 *)
-  | |- _ => fail "No separation logic hypothesis about" m "found"
+  | |- _ => idtac (* do nothing if this function does not use the heap *)
   end.
 
 (* can be overridden with
@@ -700,12 +710,15 @@ Ltac merge_sep_pair_step :=
 
 Ltac merge_seps_done :=
   lazymatch goal with
-  | H: seps ((seps (if ?b then nil else nil)) :: ?Rs) ?m |- _ =>
+  | H: seps ((seps (if ?b then nil else nil)) :: ?Rs) ?m |- exec _ _ _ ?m _ _ =>
       (* memory was modified in different ways in then/else branch *)
       eapply merge_seps_done in H; cbn [seps] in H
-  | H: seps _ _ |- _ =>
+  | H: seps _ ?m |- exec _ _ _ ?m _ _ =>
       (* memory was not modified (or in exactly the same way in both branches) *)
       cbn [seps] in H
+  | H: ?m = _ |- exec _ _ _ ?m _ _ =>
+      (* this function does not use the heap *)
+      idtac
   | |- _ => fail 1000 "failed to match the sepclauses of the then-branch and else-branch"
   end.
 

LiveVerif/src/LiveVerifExamples/critbit.v

@@ -2517,11 +2517,8 @@ Qed.
 #[export] Instance spec_of_critical_bit: fnspec :=                              .**/
 
 uintptr_t critical_bit(uintptr_t k1, uintptr_t k2) /**#
-  (* heaplet packaging doesn't work well then there's just one item in the heap
-     [or I was doing something wrong] *)
-  ghost_args := (R1 R2: mem -> Prop);
-  requires t m := <{ * R1 * R2 }> m /\ k1 <> k2;
-  ensures t' m' res := t = t' /\ <{ * R1 * R2 }> m'
+  requires t m := k1 <> k2;
+  ensures t' m' res := t = t' /\ m' = m
                 /\ 0 <= \[res] < 32
                 /\ \[res] = pfx_len (pfx_meet (pfx_emb k1) (pfx_emb k2)) #**/
 /**.
@@ -2757,9 +2754,7 @@ Derive cbt_insert SuchThat (fun_correct! cbt_insert) As cbt_insert_ok.
       return tp;                                                           /**. .**/
     }                                                                      /**. .**/
     else {                                                                 /**. .**/
-      uintptr_t cb = critical_bit(k, best_k);                              /**.
-  instantiate (3:=emp True). steps.
-  unfold enable_frame_trick.enable_frame_trick. steps. .**/
+      uintptr_t cb = critical_bit(k, best_k);                              /**. .**/
       uintptr_t result = cbt_insert_at(tp, cb, k, v);                      /**.
   subst. steps. unfold enable_frame_trick.enable_frame_trick. steps. .**/
       return result;                                                       /**. .**/

LiveVerif/src/LiveVerifExamples/fibonacci.v

@@ -16,9 +16,6 @@ Definition fib(n: word): word := /[Z.of_nat (fib_nat (Z.to_nat \[n]))].
 
 Set Default Proof Mode "Classic".
 
-(* TODO support functions that don't access any memory *)
-Definition dummy: mem -> Prop := emp True.
-
 Lemma fib_recursion: forall n,
     0 < \[n] ->
     \[n] + 1 < 2 ^ 32 ->
@@ -46,9 +43,8 @@ Proof. intros. destruct c; auto. Qed.
 #[export] Instance spec_of_fibonacci: fnspec :=                                 .**/
 
 uintptr_t fibonacci(uintptr_t n) /**#
-  ghost_args := (R: mem -> Prop);
-  requires t m := sep dummy R m;
-  ensures t' m' res := t' = t /\ sep dummy R m' /\ res = fib n #**/   /**.
+  requires t m := True;
+  ensures t' m' res := t' = t /\ m' = m /\ res = fib n #**/                /**.
 Derive fibonacci SuchThat (fun_correct! fibonacci) As fibonacci_ok.             .**/
 {                                                                          /**. .**/
   if (n == 0) /* split */ {                                                /**. .**/

LiveVerif/src/LiveVerifExamples/linked_list.v

@@ -5,9 +5,6 @@ Require Import Lia.
 
 Load LiveVerif.
 
-(* TODO support functions that don't access any memory *)
-Definition dummy: mem -> Prop := emp True.
-
 Record node := {
   data: word;
   next: word;

LiveVerif/src/LiveVerifExamples/min.v

@@ -1,15 +1,11 @@
 (* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *)
 Require Import LiveVerif.LiveVerifLib. Load LiveVerif.
 
-(* TODO support functions that don't access any memory *)
-Definition dummy: mem -> Prop := emp True.
-
 #[export] Instance spec_of_u_min: fnspec :=                                     .**/
 
 uintptr_t u_min (uintptr_t a, uintptr_t b) /**#
-  ghost_args := (R: mem -> Prop);
-  requires t m := sep dummy R m;
-  ensures t' m' retv := t' = t /\ sep dummy R m' /\
+  requires t m := True;
+  ensures t' m' retv := t' = t /\ m' = m /\
       (\[a] < \[b] /\ retv = a \/ \[b] <= \[a] /\ retv = b) #**/           /**.
 Derive u_min SuchThat (fun_correct! u_min) As u_min_ok.                         .**/
 {                                                                          /**. .**/
@@ -18,19 +14,16 @@ Derive u_min SuchThat (fun_correct! u_min) As u_min_ok.
     r = a;                                                                 /**. .**/
   } else {                                                                 /**. .**/
     r = b;                                                                 /**. .**/
-  } /**.                                                                        .**/
+  }                                                                        /**. .**/
   return r;                                                                /**. .**/
 }                                                                          /**.
 Qed.
 
 #[export] Instance spec_of_u_min3: fnspec :=                                    .**/
 
 uintptr_t u_min3 (uintptr_t a, uintptr_t b, uintptr_t c) /**#
-  ghost_args := (R: mem -> Prop);
-  requires t m := sep dummy R m;
-  (* TODO make start_canceling work if just one R, or better, specialcase memoryless
-     functions with m'=m in postcondition? *)
-  ensures t' m' retv := t' = t /\ sep dummy R m' /\
+  requires t m := True;
+  ensures t' m' retv := t' = t /\ m' = m /\
       \[retv] = Z.min \[a] (Z.min \[b] \[c]) #**/                          /**.
 Derive u_min3 SuchThat (fun_correct! u_min3) As u_min3_ok.                      .**/
 {                                                                          /**. .**/
@@ -43,9 +36,8 @@ Qed.
 #[export] Instance spec_of_u_min3_alt: fnspec :=                                 .**/
 
 uintptr_t u_min3_alt (uintptr_t a, uintptr_t b, uintptr_t c) /**#
-  ghost_args := (R: mem -> Prop);
-  requires t m := sep dummy R m;
-  ensures t' m' retv := t' = t /\ sep dummy R m' /\
+  requires t m := True;
+  ensures t' m' retv := t' = t /\ m' = m /\
       \[retv] = Z.min \[a] (Z.min \[b] \[c]) #**/                          /**.
 Derive u_min3_alt SuchThat (fun_correct! u_min3_alt) As u_min3_alt_ok.          .**/
 {                                                                          /**. .**/

bedrock2/src/bedrock2/HeapletwiseHyps.v

@@ -1231,6 +1231,7 @@ Ltac collect_heaplets_into_one_sepclause :=
       eapply start_collecting_heaplets in D;
       repeat collecting_heaplets_step D;
       eapply done_collecting_heaplets in D
+  | |- _ => idtac (* do nothing if this function does not use the heap *)
   end.
 
 Ltac start_canceling_in_hyp H :=