From 3c67fba09557b7242e63f14ba3ad1a28e9250433 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Sat, 23 Mar 2024 01:17:47 -0400
Subject: [PATCH] memcpy

---
 LiveVerif/src/LiveVerifExamples/memcpy.v | 39 ++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 LiveVerif/src/LiveVerifExamples/memcpy.v

diff --git a/LiveVerif/src/LiveVerifExamples/memcpy.v b/LiveVerif/src/LiveVerifExamples/memcpy.v
new file mode 100644
index 000000000..7c6221c09
--- /dev/null
+++ b/LiveVerif/src/LiveVerifExamples/memcpy.v
@@ -0,0 +1,39 @@
+(* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *)
+Require Import LiveVerif.LiveVerifLib.
+
+Load LiveVerif.
+
+#[export] Instance spec_of_Memcpy: fnspec :=                                    .**/
+
+void Memcpy(uintptr_t dst, uintptr_t src, uintptr_t n) /**#
+  ghost_args := srcData oldDstData (R: mem -> Prop);
+  requires t m :=
+      <{ * array (uint 8) \[n] oldDstData dst
+         * array (uint 8) \[n] srcData src
+         * R }> m;
+  ensures t' m' := t' = t /\
+      <{ * array (uint 8) \[n] srcData dst
+         * array (uint 8) \[n] srcData src
+         * R }> m' #**/                                                    /**.
+Derive Memcpy SuchThat (fun_correct! Memcpy) As Memcpy_ok.                      .**/
+{                                                                          /**. .**/
+  uintptr_t i = 0;                                                         /**.
+
+  prove (len srcData = \[n]) as L1. move L1 before t.
+  prove (len oldDstData = \[n]) as L2. move L2 before t.
+  swap oldDstData with (srcData[:\[i]] ++ oldDstData[\[i]:]) in #(dst).
+  loop invariant above i.
+  delete #(i = ??).
+                                                                                .**/
+  while (i < n) /* decreases (n ^- i) */ {                                 /**. .**/
+    store8(dst + i, load8(src + i));                                       /**.
+
+    (* TODO automate *)
+    bottom_up_simpl_in_goal. assumption.
+                                                                                .**/
+    i = i + 1;                                                             /**. .**/
+  }                                                                        /**. .**/
+}                                                                          /**.
+Qed.
+
+End LiveVerif. Comments .**/ //.