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)
=
()