(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module ECI.LowStar.Exercise1
open ECI.Deps

(**
    An exercise with F* and Low*
    Copying a buffer of bytes 
**)

/// Attempt: copy just the first byte
[@(expect_failure [19])]
let copy0 (src dest:buffer uint8) : St unit =
  dest.(0ul) <- src.(0ul)

/// Attempt: copy just the first byte, but add a bounds check
[@(expect_failure [19])]
let copy1 (len:uint32) (src dest:lbuffer len uint8) : St unit =
  if 0ul < len
  then dest.(0ul) <- src.(0ul)

/// Copy just the first byte, but add checks to ensure
///    -- No out of bounds memory access
///    -- No use after free
[@(expect_failure [19])]
let copy_first_byte (len:uint32) (src dest:lbuffer len uint8)
  : ST unit 
       (requires fun h -> True //fill me in
       )
       (ensures fun h0 _ h1 -> //fill me in
         False
       )
  = if 0ul < len
    then dest.(0ul) <- src.(0ul)


/// Copy the entire buffer, in a recursive function
///   -- just prove that it is safe
let rec copy_buffer0
        (len:uint32)
        (cur:uint32{cur <= len})
        (src dest:lbuffer len uint8)
  : ST unit 
       (requires fun h ->
         True
       )
       (ensures fun h0 _ h1 ->
         False
       )
  = admit()


/// Copy the entire buffer, in a recursive function
///   -- prove that it is safe
///   -- and correct
let rec memcpy
        (len:uint32)
        (cur:uint32{cur <= len})
        (src dest:lbuffer len uint8)
  : ST unit 
       (requires fun h ->
         True
       )
       (ensures fun h0 _ h1 ->
         False
       )
  = admit()