automation to fill sepapps with predicates castable to bytes

LiveVerif/src/LiveVerif/LiveFwd.v

@@ -0,0 +1,37 @@
+Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
+Require Import coqutil.Word.Bitwidth.
+Require Import coqutil.Tactics.autoforward.
+Require Import coqutil.Word.Interface coqutil.Word.Properties coqutil.Map.Interface.
+Require Import bedrock2.Map.SeparationLogic.
+Require Import bedrock2.SepLib.
+Require Import bedrock2.sepapp.
+Require Import bedrock2.HeapletwiseHyps.
+
+Section WithMem.
+  Context {width: Z} {BW: Bitwidth width} {word: word.word width}
+          {mem: map.map word Byte.byte} {word_ok: word.ok word} {mem_ok: map.ok mem}.
+
+  Lemma emp_True_at_addr_sepapp_l: forall p m addr,
+      autoforward (with_mem m (sepapp (emp_at_addr True) p addr))
+                  (with_mem m (p addr)).
+  Proof.
+    unfold autoforward, with_mem. intros.
+    unfold emp_at_addr, sepapp in H.
+    rewrite sep_emp_l in H. apply proj2 in H. rewrite word.add_0_r in H. exact H.
+  Qed.
+
+  Lemma emp_True_at_addr_sepapp_r: forall p sz m addr,
+      autoforward (with_mem m (@sepapp _ _ _ _ p (emp_at_addr True) sz addr))
+                  (with_mem m (p addr)).
+  Proof.
+    unfold autoforward, with_mem. intros.
+    unfold emp_at_addr, sepapp in H.
+    rewrite sep_emp_r in H. apply proj1 in H. exact H.
+  Qed.
+End WithMem.
+
+#[export] Hint Extern 1 (autoforward (with_mem _ (sepapp (emp_at_addr True) _ _)) _)
+=> eapply emp_True_at_addr_sepapp_l : typeclass_instances.
+
+#[export] Hint Extern 1 (autoforward (with_mem _ (sepapp _ (emp_at_addr True) _)) _)
+=> eapply emp_True_at_addr_sepapp_r : typeclass_instances.

LiveVerif/src/LiveVerif/LiveProgramLogic.v

@@ -966,16 +966,33 @@ Ltac evar_tuple t :=
          end
   end.
 
-Ltac evar_for_exists t :=
+Require Import coqutil.Tactics.Records.
+Require Import coqutil.Tactics.rdelta.
+
+Ltac lambda_calls_getter_on_its_arg lam :=
+  lazymatch lam with
+  | (fun x: ?tp => _) =>
+      let dummy := constr:(fun x: tp => ltac:(
+        let body := eval cbv beta in (lam x) in
+        match body with
+        | context[?getter x] => is_getter getter; exact x
+        end)) in
+      idtac
+  end.
+
+Ltac composite_eexists t body :=
   let t := rdelta t in
-  evar_tuple t.
+  tryif lambda_calls_getter_on_its_arg body then
+    refine (@ex_intro t _ (ltac:(constructor) : t) _); record.simp_goal
+  else
+    let e := evar_tuple t in exists e.
 
 Ltac step_hook := fail.
 
 Ltac sidecond_step logger := first
       [ lazymatch goal with
-        | |- exists x: ?t, _ => let e := evar_for_exists t in exists e
-        | |- @ex1 ?t _ _ _ => let e := evar_for_exists t in exists e
+        | |- @ex ?A ?P => composite_eexists A P
+        | |- @ex1 ?A _ ?P _ => composite_eexists A P
         | |- elet _ _ => refine (mk_elet _ _ _ eq_refl _)
         end;
         logger ltac:(fun _ => idtac "eexists")
@@ -1006,12 +1023,29 @@ Ltac sidecond_step logger := first
                     end;
                     lazymatch rhs with
                     | sep _ _ => fail "not an atomic sep clause"
-                    | _ => idtac
-                    end;
-                    solve [ eapply contiguous_implies_anyval_of_fillable;
-                            [ eauto with contiguous
-                            | eauto with fillable] ];
-                    logger ltac:(fun _ => idtac "contiguous_implies_anyval_of_fillable")
+                    | anyval _ _ =>
+                        first [ eapply contiguous_implies_anyval_of_fillable;
+                                [ solve [eauto with contiguous]
+                                | solve [eauto with fillable] ];
+                                logger ltac:(fun _ => idtac
+                                         "contiguous_implies_anyval_of_fillable")
+                              | (* if rhs is a sepapps (potentially behind definitions),
+                                   `eauto with fillable` above failed, so we get here *)
+                                eapply contiguous_implies_anyval_of_sepapps;
+                                [ solve [eauto with contiguous]
+                                | reflexivity (* relies on unification with unfolding,
+                                                 let's hope it won't blow up... *)
+                                | (* solved by further `step` invocations *) ];
+                                logger ltac:(fun _ => idtac
+                                         "contiguous_implies_anyval_of_sepapps") ]
+                    | ?P ?e ?addr =>
+                        is_evar e;
+                        solve [ refine (contiguous_info_implies_proj1 _ _ _ _ _ _ _);
+                                [ eauto with fillable
+                                | eauto with contiguous ] ];
+                        logger ltac:(fun _ => idtac
+                                 "contiguous_implies_anyval_of_sepapps")
+                    end
                   | (* goes last because it might wrap goal in don't_know_how_to_prove *)
                     careful_reflexivity_step_hook;
                     logger ltac:(fun _ => idtac "careful_reflexivity_step_hook") ]

LiveVerif/src/LiveVerif/LiveVerifLib.v

@@ -36,6 +36,7 @@ Require Export coqutil.Datatypes.RecordSetters.
 Require Export LiveVerif.LiveRules.
 Require Export LiveVerif.PackageContext.
 Require Export LiveVerif.LiveProgramLogic.
+Require Export LiveVerif.LiveFwd.
 
 Require Export bedrock2.tweak_tacs. Ltac tweak_sidecond_hook ::= try solve [steps].
 

LiveVerif/src/LiveVerifExamples/convert_bytes_to_record.v

@@ -24,12 +24,12 @@ Record bar := {
   barPayload: list Z
 }.
 
-Definition bar_t(n: N)(b: bar): word -> mem -> Prop := .**/
+Definition bar_t(n: Z)(b: bar): word -> mem -> Prop := .**/
 typedef struct __attribute__ ((__packed__)) {
   uint16_t barA;
   uint16_t barB;
   uintptr_t barC;
-  uint32_t barPayload[/**# Z.of_N n #**/];
+  uint32_t barPayload[/**# n #**/];
 } bar_t;
 /**.
 
@@ -43,7 +43,7 @@ Record foo := {
 Definition foo_t(f: foo): word -> mem -> Prop := .**/
 typedef struct __attribute__ ((__packed__)) {
   uint32_t foobar_n;
-  NOT_C!(bar_t (Z.to_N (foobar_n f))) foobar;
+  NOT_C!(bar_t (foobar_n f)) foobar;
 } foo_t;
 /**.
 
@@ -69,7 +69,7 @@ subst tmp. bottom_up_simpl_in_goal. reflexivity.
 Qed.
 
 
-#[export] Instance spec_of_init_baz0: fnspec :=                                  .**/
+#[export] Instance spec_of_init_baz: fnspec :=                                  .**/
 
 void init_baz(uintptr_t p, uintptr_t bazPayloadLen) /**#
   ghost_args := (R: mem -> Prop);
@@ -81,19 +81,7 @@ void init_baz(uintptr_t p, uintptr_t bazPayloadLen) /**#
 Derive init_baz SuchThat (fun_correct! init_baz) As init_baz_ok.                .**/
 {                                                                          /**. .**/
 }                                                                          /**.
-  unfold anyval at 2. unfold baz_t.
-  clear_mem_split_eqs; clear_heapletwise_hyps; clear_heaplets.
-  intros m ?.
-  set (mAll := m) in |-*.
-  eexists (Build_baz _ _ _). cbn. unfold sepapp.
-  change (m |= array (uint 8) 8 ? p) in H.
-  assert (mmap.du (mmap.Def m) (mmap.Def map.empty) = mmap.Def mAll) as D. {
-    rewrite mmap.du_empty_r. reflexivity.
-  }
-  clearbody mAll.
-  steps.
-  (* evars were created too early! *)
-Abort.
+Qed.
 
 
 #[export] Instance spec_of_init_sepapps: fnspec :=                              .**/
@@ -121,37 +109,6 @@ Derive init_sepapps SuchThat (fun_correct! init_sepapps) As init_sepapps_ok.
   steps.
 Qed.
 
-#[export] Instance spec_of_init_baz: fnspec :=                                  .**/
-
-void init_baz(uintptr_t p, uintptr_t bazPayloadLen) /**#
-  ghost_args := bs (R: mem -> Prop);
-  requires t m := <{ * array (uint 8) 8 bs p
-                     * R }> m;
-  ensures t' m' := t' = t /\
-       <{ * baz_t ? p
-          * R }> m' #**/                                                   /**.
-Derive init_baz SuchThat (fun_correct! init_baz) As init_baz_ok.                .**/
-{                                                                          /**. .**/
-}                                                                          /**.
-  unfold anyval, baz_t.
-  clear_mem_split_eqs; clear_heapletwise_hyps; clear_heaplets.
-  intros m ?.
-  set (mAll := m) in |-*.
-  change (m |= array (uint 8) 8 bs p) in H.
-  assert (mmap.du (mmap.Def m) (mmap.Def map.empty) = mmap.Def mAll) as D. {
-    rewrite mmap.du_empty_r. reflexivity.
-  }
-  clearbody mAll.
-  unfold sepapps. simpl. unfold sepapp.
-  enough (<{ * uint 16 ? p
-             * uint 16 ? (p ^+ /[2])
-             * uintptr ? (p ^+ /[2] ^+ /[2])
-             * emp True }> mAll).
-  { unfold anyval in *. repeat heapletwise_step.
-    eexists (Build_baz _ _ _). cbn. steps. }
-  steps.
-Qed.
-
 
 #[export] Instance spec_of_init_bar: fnspec :=                                  .**/
 
@@ -160,12 +117,12 @@ void init_bar(uintptr_t p, uintptr_t barPayloadLen) /**#
   requires t m := <{ * array (uint 8) (8 + 4 * \[barPayloadLen]) bs p
                      * R }> m;
   ensures t' m' := t' = t /\
-       <{ * bar_t (Z.to_N \[barPayloadLen]) ? p
+       <{ * bar_t \[barPayloadLen] ? p
           * R }> m' #**/                                                   /**.
 Derive init_bar SuchThat (fun_correct! init_bar) As init_bar_ok.                .**/
 {                                                                          /**. .**/
 }                                                                          /**.
-Abort.
+Qed.
 
 
 #[export] Instance spec_of_init_foo: fnspec :=                                  .**/

LiveVerif/src/LiveVerifExamples/mbuf.v

@@ -50,8 +50,7 @@ Definition mbuf
    predicates (eg array, or combinations of array and packet headers) to mbuf. *)
 Definition mbuf(packet: word -> mem -> Prop){packet_sz: PredicateSize packet}
   : word -> mem -> Prop :=
-  <{ + packet
-     + anyval (array (uint 8) (MBUF_SIZE - packet_sz)) }>.
+  sepapp packet (anyval (array (uint 8) (MBUF_SIZE - packet_sz))).
 
 (* Or how about we just make the packet_sz argument explicit:
 

LiveVerif/src/LiveVerifExamples/mini_stagefright.v

@@ -164,7 +164,6 @@ Derive parse_chunk_of_type_bytearr SuchThat (fun_correct! parse_chunk_of_type_by
   uintptr_t dstOfs = load(pDstOfs);                                        /**. .**/
   uintptr_t actual_typ = load32(src + srcOfs + 4);                         /**.
 
-  2: {
 Abort.
 
 End LiveVerif. Comments .**/ //.

LiveVerif/src/LiveVerifExamples/network.v

@@ -5,8 +5,6 @@ Require Import bedrock2.NetworkPackets.
 Require Import bedrock2.e1000_packet_trace.
 Require Import LiveVerifExamples.mbuf.
 
-Require Import coqutil.Map.OfListWord.
-
 Load LiveVerif.
 
 (* in the packet_trace, the excess bytes of mbufs don't appear, but in mbufs, they do *)
@@ -37,34 +35,6 @@ Axiom be_uint16_fillable: fillable (be_uint 16) 2.
   be_uint16_fillable
 : fillable.
 
-Import autoforward.
-Import Coq.Program.Tactics.
-
-Lemma emp_True_at_addr_at_sepapps_head: forall (preds: list sized_predicate) m addr,
-    autoforward (with_mem m (sepapps
-                    (cons (mk_sized_predicate (emp_at_addr True) 0) preds) addr))
-                (with_mem m (sepapps preds addr)).
-Proof.
-  unfold autoforward, with_mem. intros.
-  rewrite sepapps_cons in H. unfold emp_at_addr in H. simpl in H.
-  rewrite sep_emp_l in H. apply proj2 in H. rewrite word.add_0_r in H. exact H.
-Qed.
-
-(*#[export]*) Hint Extern 1 (autoforward (with_mem _ (sepapps
-                    (cons (mk_sized_predicate (emp_at_addr True) 0) _) _)) _)
-  => rapply @emp_True_at_addr_at_sepapps_head : typeclass_instances.
-
-Lemma sepapps_singleton: forall pred sz a m,
-    autoforward (with_mem m (sepapps (cons (mk_sized_predicate pred sz) nil) a))
-                (with_mem m (pred a)).
-Proof.
-  unfold autoforward, with_mem, sepapps. cbn. unfold sepapp. intros.
-  eapply sep_emp_r in H. apply H.
-Qed.
-
-(*#[export]*) Hint Extern 1
-  (autoforward (with_mem ?m (sepapps (cons (mk_sized_predicate ?pred ?sz) nil) ?addr)) _)
-=> apply (sepapps_singleton pred sz addr m) : typeclass_instances.
 
 Instance spec_of_net_alloc_eth: fnspec :=                                          .**/
 
@@ -81,74 +51,6 @@ Derive net_alloc_eth SuchThat (fun_correct! net_alloc_eth) As net_alloc_eth_ok.
   uintptr_t r = alloc_tx_buf(nw);                                          /**. .**/
   return r;                                                                /**. .**/
 }                                                                          /**.
-
-Set Nested Proofs Allowed.
-
-  Lemma contiguous_implies_anyval_of_sepapps[T: Type]:
-    forall (P: word -> mem -> Prop) (F: T -> word -> mem -> Prop) (n: Z) (a: word) preds,
-      contiguous P n ->
-      F = (fun v: T => sepapps (preds v)) ->
-      (forall bs m, sep (array (uint 8) n bs a) (emp True) m ->
-                    sep (EX v, (sepapps (preds v)) a) (emp True) m) ->
-      impl1 (P a) (anyval F a).
-  Admitted.
-
-eapply contiguous_implies_anyval_of_sepapps.
-1: eauto with contiguous.
-1: reflexivity.
-step.
-step. step.
-step. step. step. step.
-
-Require Import coqutil.Tactics.Records.
-Require Import coqutil.Tactics.rdelta.
-
-(* does expression e contain a getter accessing a field of record type tp? *)
-Ltac contains_getter_for e tp :=
-  let tp := rdelta tp in
-  match e with
-  | context[?getter] =>
-      is_getter getter;
-      let t := type of getter in
-      lazymatch type of getter with
-      | tp -> _ => idtac
-      end
-  end.
-
-
-change 8 with (fst (8,9)).
-
-Ltac composite_eexists t body :=
-  let t := rdelta t in
-  tryif contains_getter_for body t then
-    refine (@ex_intro t _ (ltac:(constructor) : t) _); record.simp
-  else
-    let e := evar_tuple t in exists e.
-
-lazymatch goal with
-| |- @ex ?A ?P => composite_eexists A P
-end.
-
-(*
-lazymatch goal with
-| |- @ex ?A ?P =>
-    contains_getter_for P A;
-    refine (@ex_intro A P (ltac:(constructor) : A) _)
-end.
-record.simp.
-*)
-
-step. step. step. step. step. step. step. step. step. step. step. step. step. step.
-step. step. step. step. step. step. step. step. step. step. step.
-step.
-
-  lazymatch goal with
-  | |- impl1 _ (?P2 ?e ?addr) =>
-      is_evar e;
-      solve [ refine (contiguous_info_implies_proj1 _ _ _ _ _ _ _);
-              [ eauto with fillable
-              | eauto with contiguous ] ]
-  end.
 Qed.
 
 Instance spec_of_net_alloc_ip: fnspec :=                                          .**/

LiveVerif/src/LiveVerifExamples/ring_buffer.v

@@ -83,6 +83,13 @@ Ltac predicates_safe_to_cancel_hook hypPred conclPred ::=
       end
   end.
 
+(* TODO can we infer injectivity of predicates automatically? *)
+Lemma raw_ring_buf_t_inj: forall r1 r2 a,
+    safe_implication (r1 = r2) (impl1 (raw_ring_buf_t r1 a) (raw_ring_buf_t r2 a)).
+Proof. unfold safe_implication. intros. subst. reflexivity. Qed.
+
+#[local] Hint Resolve raw_ring_buf_t_inj : safe_implication.
+
 #[export] Instance spec_of_ring_buf_init: fnspec :=                              .**/
 
 void ring_buf_init(uintptr_t addr, uintptr_t cap) /**#
@@ -98,7 +105,6 @@ Derive ring_buf_init SuchThat (fun_correct! ring_buf_init) As ring_buf_init_ok.
   store32(addr + 4, 0);                                                    /**. .**/
   store32(addr + 8, 0);                                                    /**. .**/
 }                                                                          /**.
-  all: record.simp. all: steps.
 Qed.
 
 #[export] Instance spec_of_ring_buf_enq: fnspec :=                              .**/