module WarmUp1

/// Lab Session: Programming in Low*. This is intended as a warm-up to get
/// familiar with Low*. Target time: 20 minutes.

module B = LowStar.Buffer
module U32 = FStar.UInt32
module HS = FStar.HyperStack

open LowStar.BufferOps
open FStar.HyperStack.ST

(***** Machine integers *)

/// First exercise, related to machine integers. Complete the definition below
/// for the absolute value. This is, of course, tricky, since with fixed-width
/// integers, one cannot always compute the absolute value (why?). You will need
/// to craft a suitable pre-condition to make the function go through.

/// We first define the pure specification.
let abs (x: int): Tot int = if x > 0 then x else -x

/// Then show that our function that operates on machine integers performs that
/// operation properly.
let abs1 (x: Int32.t): Pure Int32.t
  (requires True) // need something better!
  (ensures (fun y -> Int32.v y = abs (Int32.v x))) =
  admit ()

/// A second variant: this one will take True as a precondition, but will return
/// an option type for those inputs whose absolute value cannot be computed.
let abs2 (x: Int32.t): Pure (option Int32.t)
  (requires True) // must leave True here
  (ensures fun _ -> True) // must change this line to say: if the return value is (Some y),
                    // then y is the absolute value of input x
=
  None

(***** Working with references *)

/// The classic swap on references: provide suitable pre- and post-conditions.
/// Two useful operations: b *= (e), for writing into a pointer, and !*(e), for
/// dereferencing a pointer.
let swap (x: B.pointer UInt32.t) (y: B.pointer UInt32.t): Stack unit
  (requires fun _ -> True)
  (ensures fun _ _ _ -> True) 
=
  ()

(***** Working with buffers *)

/// For this first version, the goal is only to have memory safety. 
let rec copy1 (dst src: B.buffer U32.t) (remaining: U32.t): Stack unit
  (requires fun _ -> True)
  (ensures fun _ _ _ -> True)
=
  ()

/// For this version, you are expected to provide a useful post-condition that
/// states not only that the buffers are live, but also that the contents of dst
/// is the same as the contents of src.
let rec copy2 (dst src: B.buffer U32.t) (remaining: U32.t): Stack unit
  (requires fun _ -> True)
  (ensures fun _ _ _ -> True)
=
  ()