# Example: memcpy¶

The snippet below implements a classic `memcpy`

function, copying `len`

elements of type `a`

from `src`

into `dst`

.

```
module MemCpy
open FStar.HyperStack.ST
module S = FStar.Seq
module B = LowStar.Buffer
module M = LowStar.Modifies
module U32 = FStar.UInt32
module ST = FStar.HyperStack.ST
let slice_plus_one #a (s1 s2: S.seq a) (i: nat): Lemma
(requires (
i < S.length s1 /\
i < S.length s2 /\
S.equal (S.slice s1 0 i) (S.slice s2 0 i) /\
S.index s1 i == S.index s2 i))
(ensures (
S.equal (S.slice s1 0 (i + 1)) (S.slice s2 0 (i + 1))))
[ SMTPat (S.slice s1 0 (i + 1)); SMTPat (S.slice s2 0 (i + 1)) ]
=
let x = S.index s1 i in
let s1' = S.append (S.slice s1 0 i) (S.cons x S.empty) in
let s2' = S.append (S.slice s2 0 i) (S.cons x S.empty) in
assert (S.equal s1' (S.slice s1 0 (i + 1)));
assert (S.equal s2' (S.slice s2 0 (i + 1)))
open LowStar.BufferOps
#set-options "--max_fuel 0 --max_ifuel 0"
val memcpy: #a:eqtype -> src:B.buffer a -> dst:B.buffer a -> len:U32.t -> Stack unit
(requires fun h0 ->
let l_src = M.loc_buffer src in
let l_dst = M.loc_buffer dst in
B.live h0 src /\ B.live h0 dst /\
B.length src = U32.v len /\
B.length dst = U32.v len /\
M.loc_disjoint l_src l_dst)
(ensures fun h0 () h1 ->
let l_src = M.loc_buffer src in
let l_dst = M.loc_buffer dst in
B.live h1 src /\
B.live h1 dst /\
M.(modifies l_dst h0 h1) /\
S.equal (B.as_seq h1 dst) (B.as_seq h0 src))
let memcpy #a src dst len =
let h0 = ST.get () in
let inv h (i: nat) =
B.live h src /\ B.live h dst /\
M.(modifies (loc_buffer dst) h0 h) /\
i <= U32.v len /\
S.equal (Seq.slice (B.as_seq h src) 0 i) (Seq.slice (B.as_seq h dst) 0 i)
in
let body (i: U32.t{ 0 <= U32.v i /\ U32.v i < U32.v len }): Stack unit
(requires (fun h -> inv h (U32.v i)))
(ensures (fun h0 () h1 -> inv h0 (U32.v i) /\ inv h1 (U32.v i + 1)))
=
let open B in
dst.(i) <- src.(i)
in
C.Loops.for 0ul len inv body
let main (): Stack C.exit_code
(requires fun _ -> True)
(ensures fun h _ h' -> M.modifies M.loc_none h h')
=
push_frame ();
let src = B.alloca_of_list [ 1UL; 2UL ] in
let dst = B.alloca 0UL 2ul in
memcpy src dst 2ul;
pop_frame ();
C.EXIT_SUCCESS
```

This example showcases several features of Low*. We only present the code from a high-level point of view.

The code starts by opening several modules that are part of the “Low* standard library”.

`Buffer`

is our model of stack- and heap- allocated C arrays (described in The buffer library)`Seq`

is the sequence abstraction from the F* standard library, which`Buffer`

uses to reflect the contents of a given buffer in a given heap at the proof level`Modifies`

provides a universal modifies clause over buffers, references and regions (described in The modifies clauses library)`UInt32`

is a model of the C11`uint32_t`

type, reflected at the proof level using natural numbers (described in Machine integers)`HyperStack`

is our model of the C memory layout (described in The memory model)`C`

and`C.Loops`

expose some C concepts to F* (described in Low* system libraries)

The first definition is a lemma over sequences: if two sequences are equal over
the slice `[0; i)`

and their `i`

-th element is equal, then they are equal
over the slice `[0; i + 1)`

. This lemma is required to prove the functional
correctness of `memcpy`

. Lemmas are erased and do not appear in the generated
code, so it is safe to mix lemmas with Low* code.

Next, then `memcpy`

function is defined and annotated with pre- and
post-conditions, using liveness and disjointness predicates. The post-condition
states that after calling `memcpy src dst len`

, the destination and the source
have the same contents up to index `len`

.

The implementation of `memcpy`

uses a C-style `for`

loop with a loop
invariant and a loop body. Alternatively, one could write a recursive function,
relying on the C compiler to hopefully perform tail-call optimization.

Finally, the `main`

function uses `push_frame`

and `pop_frame`

, two
combinators from the memory model that indicate that this code conceptually
executes in a new stack frame. In this new stack frame, two test arrays are
allocated on the stack. These are arrays of 64-bit unsigned integers, as denoted
by the `UL`

Low* suffix for machine integers. The `memcpy`

function is
called over these two arrays. From a verification perspective, since the stack
frame is freed after calling `main`

, we can successfully state that `main`

modifies no buffer.