Heapster example of how to specify a memcpy-like function

Blah.sawcore

module Blah where

test.c

#include <stddef.h>

void memcpy2(unsigned char dst[80], const unsigned char src[80]) {
    for (size_t i = 0; i < 80; i++) {
        dst[i] = src[i];
    }
}

test.saw

enable_experimental;
env <- heapster_init_env_for_files "Blah.sawcore" ["test.bc"];

heapster_define_perm env "int8"  " " "llvmptr 8"  "exists x:bv 8.eq(llvmword(x))";
heapster_define_perm env "int8array"  "rw:rwmodality, len:bv 64" "llvmptr 64" "array(rw,0,<len,*1,fieldsh(8,int8<>))";

heapster_typecheck_fun env
    "memcpy2"
    "(). arg0:int8array<W,80>, arg1:int8array<W,80> -o \
       \ arg0:int8array<W,80>, arg1:int8array<W,80>";

heapster_export_coq env "test_gen.v";

test_proofs.v

From Coq          Require Import Lia.
From Coq          Require Import Lists.List.
From Coq          Require Import Logic.FunctionalExtensionality.
From Coq          Require Import Program.Tactics.
From Coq          Require Import String.
From Coq          Require Import Vectors.Vector.
From CryptolToCoq Require Import SAWCoreScaffolding.
From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
From CryptolToCoq Require Import SAWCoreBitvectors.
From CryptolToCoq Require Import SAWCoreBitvectorsZifyU64.
From CryptolToCoq Require Import SAWCorePrelude.
From CryptolToCoq Require Import SAWCorePreludeExtra.
From CryptolToCoq Require Import SpecMExtra.
From EnTree       Require Import Automation.

Import SAWCorePrelude.
Import SpecMNotations.
Local Open Scope entree_scope.

Require Import Test.bv_utils.
Require Import Test.test_gen.
Import Blah.

Import VectorNotations.

Lemma UIP_bool :
  forall (x y:bool) (p1 p2:x = y), p1 = p2.
Proof.
  apply UIP_dec. apply Bool.bool_dec.
Qed.

Lemma upd_at_BVVec
        (n : nat) (len : bitvector n) (a : Type)
        (x : BVVec n len a) (idx : bitvector n)
        (prf : isBvult n idx len) :
  updBVVec n len a x idx (atBVVec n len a x idx prf) = x.
Proof.
  unfold updBVVec.
  rewrite <- (gen_at_BVVec n len a x) at 1.
  f_equal.
  extensionality i. extensionality pf.
  destruct (bvEq n i idx) eqn:X.
  - rewrite (bvEq_eq n i idx) in X.
    subst i.
    rewrite (UIP_bool _ _ prf pf).
    reflexivity.
  - reflexivity.
Qed.

Lemma bvAdd_bvSub_cancel w a b :
  isBvule w b a ->
  bvAdd w b (bvSub w a b) = a.
Proof. holds_for_bits_up_to_3. Qed.

Lemma isBvult_bvSub_lemma1 a b :
  isBvult 64 (bvSub 64 a b) a ->
  isBvult 64 (intToBv 64 0) b.
Proof. lia. Qed.

Lemma isBvult_bvSub_lemma2 a b :
  isBvult 64 b a ->
  isBvult 64 (bvSub 64 a (bvAdd 64 b (intToBv 64 1))) (bvSub 64 a b).
Proof. lia. Qed.

Lemma bvSub_bvAdd_distrib_lemma a b c :
  bvAdd 64 (bvSub 64 a b) c = bvSub 64 a (bvSub 64 b c).
Proof. lia. Qed.

Definition memcpy2_loop_body_spec
  (dst src : BVVec 64 (intToBv 64 80) (bitvector 8))
  (i : bitvector 64)
  (pf : isBvult 64 i (intToBv 64 80)) :
  BVVec 64 (intToBv 64 80) (bitvector 8) :=
  updBVVec _ _ _ dst i (atBVVec _ _ _ src i pf).

Lemma memcpy2_up_to_lemma
  (i i' : bitvector 64)
  (pf : isBvule 64 i (intToBv 64 80))
  (pf' : isBvult 64 i' i) :
  isBvult 64 i' (intToBv 64 80).
Proof.
  rewrite <- pf.
  apply pf'.
Qed.

Definition memcpy2_up_to_spec
  (i : bitvector 64)
  (pf : isBvule 64 i (intToBv 64 80))
  (dst src : BVVec 64 (intToBv 64 80) (bitvector 8)) :
  BVVec 64 (intToBv 64 80) (bitvector 8) :=
  foldlBVInRange
    (intToBv 64 0) i
    (fun i' pf' dst' =>
      memcpy2_loop_body_spec dst' src i'
        (memcpy2_up_to_lemma i i' pf pf'))
    dst.

Definition memcpy2_spec :=
  memcpy2_up_to_spec (intToBv 64 80) eq_refl.

Lemma foldlBVInRange_next_iter_lemma1 w finish
  (pf : isBvult w finish (bvumax w)) :
  isBvult w finish (bvAdd w finish (intToBv w 1)).
Proof. holds_for_bits_up_to_3. Qed.

Lemma foldlBVInRange_next_iter_lemma2 w bv finish
  (pf1 : isBvult w bv finish)
  (pf2 : isBvult w finish (bvumax w)) :
  isBvult w bv (bvAdd w finish (intToBv w 1)).
Proof.
  rewrite -> pf1.
  apply foldlBVInRange_next_iter_lemma1.
  apply pf2.
Qed.

(*
Lemma foldlBVInRange_next_iter_lemma3 w bv finish
  (pf1 : isBvult w bv (bvNat w (bvToNat w finish)))
  (pf2 : isBvult w finish (bvumax w)) :
  isBvult w bv (bvAdd w finish (intToBv w 1)).
Proof.
  rewrite -> bvNat_bvToNat in *.
  apply foldlBVInRange_next_iter_lemma2; assumption.
Qed.
*)

Lemma foldlBVInRange_next_iter w A finish f a
        (pf : isBvult w finish (bvumax w)) :
  @foldlBVInRange w A (intToBv w 0) (bvAdd w finish (intToBv w 1)) f a =
  f finish (foldlBVInRange_next_iter_lemma1 w finish pf)
    (@foldlBVInRange
      w A (intToBv w 0) finish
      (fun bv pf' => f bv (foldlBVInRange_next_iter_lemma2 w bv finish pf' pf))
      a).
(* TODO: Prove this *)
Admitted.

Lemma memcpy2_spec_lemma1
  (x : bitvector 64)
  (pf1 : isBvsle 64 (intToBv 64 0) x)
  (pf2 : isBvsle 64 x (intToBv 64 80)) :
  isBvule 64 x (intToBv 64 80).
Proof.
  rewrite -> (isBvule_to_isBvsle_pos 64 x (intToBv 64 80) pf1 eq_refl).
  apply pf2.
Qed.

Lemma memcpy2_spec_lemma2
  (x : bitvector 64)
  f
  (H1 : exists (pf1 : isBvsle 64 (intToBv 64 0) x) (pf2 : isBvsle 64 x (intToBv 64 80)),
       f pf1 pf2)
  (H2 : isBvult 64 x (intToBv 64 80)) :
  isBvsle 64 (bvAdd 64 x (intToBv 64 1)) (intToBv 64 80).
Proof.
  apply isBvslt_to_isBvsle_suc.
  destruct H1 as [pf1 [pf2 H]].
  rewrite <- isBvult_to_isBvslt_pos.
  - apply H2.
  - apply pf1.
  - reflexivity.
Qed.

Lemma memcpy2_spec_lemma3
  (x : bitvector 64)
  f
  (H1 : exists (pf1 : isBvsle 64 (intToBv 64 0) x) (pf2 : isBvsle 64 x (intToBv 64 80)),
       f pf1 pf2) :
  isBvsle 64 (intToBv 64 0) (bvAdd 64 x (intToBv 64 1)).
Proof.
  destruct H1 as [pf1 [pf2 _]].
  rewrite -> pf1.
  apply isBvsle_suc_r.
  rewrite -> pf2.
  reflexivity.
Qed.

Lemma updBVVec_f_equal
  (n : nat)
  (len : bitvector n)
  (a : Type)
  (v v' : Vec (bvToNat n len) a)
  (ix ix' : bitvector n)
  (elem elem' : a) :
  v = v' ->
  ix = ix' ->
  elem = elem' ->
  updBVVec n len a v ix elem = updBVVec n len a v' ix' elem'.
Proof.
  intros H1 H2 H3.
  f_equal; assumption.
Qed.

Lemma atBVVec_f_equal
  (n : nat)
  (len : bitvector n)
  (a : Type)
  (x x' : Vec (bvToNat n len) a)
  (ix : bitvector n)
  (pf pf' : isBvult n ix len) :
  x = x' ->
  pf = pf' ->
  atBVVec n len a x ix pf = atBVVec n len a x' ix pf'.
Proof.
  intros H1 H2.
  f_equal; assumption.
Qed.

Lemma foldlBVInRange_f_equal
  (w : nat)
  (A : Type)
  (start start' finish : bitvector w)
  (f f' : forall bv : bitvector w, isBvult w bv finish -> A -> A)
  (a a' : A) :
  start = start' ->
  f = f' ->
  a = a' ->
  @foldlBVInRange w A start finish f a = @foldlBVInRange w A start' finish f' a'.
Proof.
  intros H1 H2 H3.
  f_equal; assumption.
Qed.

Definition memcpy2_spec_ref (dst src : BVVec 64 (intToBv 64 80) (bitvector 8)) :
  spec_refines eqPreRel eqPostRel eq
    (memcpy2 dst src)
    (total_spec (fun _ => True)
                (fun '(dst_arg_init, _, src_arg, _) r => r = (memcpy2_spec dst_arg_init src_arg, src_arg))
                (dst, dst, src, intToBv 64 81)).
Proof.
  unfold memcpy2, memcpy2__bodies.
  prove_refinement.
  - wellfounded_decreasing_nat.
    exact (bvToNat 64 x).
  - prepost_case 0 0.
    + exact (a = a1 /\ a = a2 /\ a0 = a3 /\ x = intToBv 64 81).
    + exact (r = r1 /\ r0 = r2).
  - prepost_case 1 0.
    + exact ((exists (pf1 : isBvsle 64 (intToBv 64 0) x) (pf2 : isBvsle 64 x (intToBv 64 80)),
              a2 = memcpy2_up_to_spec x (memcpy2_spec_lemma1 x pf1 pf2) a1 a3) /\
             a = a2 /\ a0 = a3 /\ x0 = bvSub 64 (intToBv 64 80) x).
    + exact (r = r1 /\ r0 = r2).
    prepost_exclude_remaining.
  - time "memcpy2_spec_ref" prove_refinement_continue.
    + apply isBvult_bvToNat.
      apply (isBvult_bvSub_lemma2 _ _ a2).
    + rewrite upd_at_BVVec.
      instantiate (1 := a).
      unshelve instantiate (1 := memcpy2_spec_lemma2 call _ H a2).
      unshelve instantiate (1 := memcpy2_spec_lemma3 call _ H).
      generalize
        (memcpy2_spec_lemma1 (bvAdd 64 call (intToBv 64 1))
          (memcpy2_spec_lemma3 call
             (fun (pf1 : isBvsle 64 (intToBv 64 0) call) (pf2 : isBvsle 64 call (intToBv 64 80)) =>
              a0 = memcpy2_up_to_spec call (memcpy2_spec_lemma1 call pf1 pf2) a a1) H)
          (memcpy2_spec_lemma2 call
             (fun (pf1 : isBvsle 64 (intToBv 64 0) call) (pf2 : isBvsle 64 call (intToBv 64 80)) =>
              a0 = memcpy2_up_to_spec call (memcpy2_spec_lemma1 call pf1 pf2) a a1) H a2))
        as X.
      intros X.
      destruct H as [pf1 [pf2 H]].
      unfold memcpy2_up_to_spec, memcpy2_loop_body_spec.

      assert (R : isBvult 64 call (bvumax 64)).
      { change (bvult 64 call (intToBv 64 80) = 1%bool)
          with (isBvult 64 call (intToBv 64 80))
            in a2.
        rewrite a2. reflexivity. }
      rewrite -> (foldlBVInRange_next_iter 64 _ call _ a R).
      f_equal.
      * rewrite -> H.
        unfold memcpy2_up_to_spec.
        apply foldlBVInRange_f_equal.
        - reflexivity.
        - extensionality bv. extensionality pf'. extensionality dst'.
          unfold memcpy2_loop_body_spec.
          apply updBVVec_f_equal.
          + reflexivity.
          + reflexivity.
          + f_equal.
            apply UIP_bool.
        - reflexivity.
      * f_equal.
        apply UIP_bool.
    + rewrite upd_at_BVVec.
      constructor; reflexivity.
    + rewrite and_bool_eq_false, 2 isBvslt_def_opp in e_if0.
      destruct H as [X1 [Y1 _]].
      destruct e_if0 as [X2 | Y2].
      * rewrite <- X1 in X2.
        vm_compute in X2.
        discriminate X2.
      * rewrite Y1 in Y2.
        vm_compute in Y2.
        discriminate Y2.
    + destruct H as [pf1 [pf2 H']].
      rewrite isBvule_def_opp in e_if.
      destruct (isBvule_to_isBvsle_pos 64 (intToBv 64 80) call eq_refl pf1) as [X _].
      apply X in e_if.
      specialize (isBvsle_antisymm 64 (intToBv 64 80) call e_if pf2) as Z.
      revert H'. revert pf1 pf2.
      rewrite <- Z.
      intros pf1 pf2 H'.
      subst a0.
      unfold memcpy2_spec.
      rewrite -> (UIP_bool _ _ (memcpy2_spec_lemma1 (intToBv 64 80) pf1 pf2) eq_refl).
      reflexivity.
    + Unshelve. all: reflexivity.
Qed.

(* An alternative version that uses `with NoRewrite NoSolve` *)
Definition memcpy2_spec_ref_alt (dst src : BVVec 64 (intToBv 64 80) (bitvector 8)) :
  spec_refines eqPreRel eqPostRel eq
    (memcpy2 dst src)
    (total_spec (fun _ => True)
                (fun '(dst_arg_init, _, src_arg, _) r => r = (memcpy2_spec dst_arg_init src_arg, src_arg))
                (dst, dst, src, intToBv 64 81)).
Proof.
  unfold memcpy2, memcpy2__bodies.
  prove_refinement.
  - wellfounded_decreasing_nat.
    exact (bvToNat 64 x).
  - prepost_case 0 0.
    + exact (a = a1 /\ a = a2 /\ a0 = a3 /\ x = intToBv 64 81).
    + exact (r = r1 /\ r0 = r2).
  - prepost_case 1 0.
    + exact ((exists (pf1 : isBvsle 64 (intToBv 64 0) x) (pf2 : isBvsle 64 x (intToBv 64 80)),
              a2 = memcpy2_up_to_spec x (memcpy2_spec_lemma1 x pf1 pf2) a1 a3) /\
             a = a2 /\ a0 = a3 /\ x0 = bvSub 64 (intToBv 64 80) x).
    + exact (r = r1 /\ r0 = r2).
    prepost_exclude_remaining.
  - time "memcpy2_spec_ref_alt" prove_refinement_continue with NoRewrite NoSolve.
    (* These are the only three goals that do not appear in memcpy2_spec_ref.
       Fortunately, they are all easy to prove. *)
    + unfold isBvult in H0.
      rewrite e_if in H0.
      contradiction H0.
    + reflexivity.
    + unfold isBvult in H1.
      rewrite a2 in H1.
      contradiction H1.

    (* The remaining goals are exactly the same as in memcpy2_spec_ref. *)
    + apply isBvult_bvToNat.
      apply (isBvult_bvSub_lemma2 _ _ a2).
    + rewrite upd_at_BVVec.
      instantiate (1 := a).
      unshelve instantiate (1 := memcpy2_spec_lemma2 call _ H a2).
      unshelve instantiate (1 := memcpy2_spec_lemma3 call _ H).
      generalize
        (memcpy2_spec_lemma1 (bvAdd 64 call (intToBv 64 1))
          (memcpy2_spec_lemma3 call
             (fun (pf1 : isBvsle 64 (intToBv 64 0) call) (pf2 : isBvsle 64 call (intToBv 64 80)) =>
              a0 = memcpy2_up_to_spec call (memcpy2_spec_lemma1 call pf1 pf2) a a1) H)
          (memcpy2_spec_lemma2 call
             (fun (pf1 : isBvsle 64 (intToBv 64 0) call) (pf2 : isBvsle 64 call (intToBv 64 80)) =>
              a0 = memcpy2_up_to_spec call (memcpy2_spec_lemma1 call pf1 pf2) a a1) H a2))
        as X.
      intros X.
      destruct H as [pf1 [pf2 H]].
      unfold memcpy2_up_to_spec, memcpy2_loop_body_spec.

      assert (R : isBvult 64 call (bvumax 64)).
      { change (bvult 64 call (intToBv 64 80) = 1%bool)
          with (isBvult 64 call (intToBv 64 80))
            in a2.
        rewrite a2. reflexivity. }
      rewrite -> (foldlBVInRange_next_iter 64 _ call _ a R).
      f_equal.
      * rewrite -> H.
        unfold memcpy2_up_to_spec.
        apply foldlBVInRange_f_equal.
        - reflexivity.
        - extensionality bv. extensionality pf'. extensionality dst'.
          unfold memcpy2_loop_body_spec.
          apply updBVVec_f_equal.
          + reflexivity.
          + reflexivity.
          + f_equal.
            apply UIP_bool.
        - reflexivity.
      * f_equal.
        apply UIP_bool.
    + rewrite upd_at_BVVec.
      constructor; reflexivity.
    + rewrite and_bool_eq_false, 2 isBvslt_def_opp in e_if0.
      destruct H as [X1 [Y1 _]].
      destruct e_if0 as [X2 | Y2].
      * rewrite <- X1 in X2.
        vm_compute in X2.
        discriminate X2.
      * rewrite Y1 in Y2.
        vm_compute in Y2.
        discriminate Y2.
    + destruct H as [pf1 [pf2 H']].
      rewrite isBvule_def_opp in e_if.
      destruct (isBvule_to_isBvsle_pos 64 (intToBv 64 80) call eq_refl pf1) as [X _].
      apply X in e_if.
      specialize (isBvsle_antisymm 64 (intToBv 64 80) call e_if pf2) as Z.
      revert H'. revert pf1 pf2.
      rewrite <- Z.
      intros pf1 pf2 H'.
      subst a0.
      unfold memcpy2_spec.
      rewrite -> (UIP_bool _ _ (memcpy2_spec_lemma1 (intToBv 64 80) pf1 pf2) eq_refl).
      reflexivity.
    + Unshelve. all: reflexivity.
Qed.