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.