One-time integers

This module implements the idea described in this paper: How to avoid proving the absence of integer overflows

When extracted to OCaml, the following type OneTime.t will be mapped to OCaml's type int (63-bit signed integers).

See also mach.peano.

module OneTime

  use int.Int

  type t = abstract { v: int; mutable valid: bool }
  meta coercion function v

  val to_int (x: t) : int
    ensures { result = x.v }

  val zero (): t
    ensures { result.valid }
    ensures { result.v = 0 }

  val one () : t
    ensures { result.valid }
    ensures { result.v = 1 }

  val succ (x: t) : t
    requires { x.valid }
    writes   { x.valid }
    ensures  { result.valid /\ not x.valid }
    ensures  { result.v = x.v + 1 }

  val pred (x: t) : t
    requires { x.valid }
    writes   { x.valid }
    ensures  { result.valid /\ not x.valid }
    ensures  { result.v = x.v - 1 }

  val lt (x y: t) : bool
    ensures { result <-> x.v < y.v }
  val le (x y: t) : bool
    ensures { result <-> x.v <= y.v }
  val gt (x y: t) : bool
    ensures { result <-> x.v > y.v }
  val ge (x y: t) : bool
    ensures { result <-> x.v >= y.v }
  val eq (x y: t) : bool
    ensures { result <-> x.v = y.v }
  val ne (x y: t) : bool
    ensures { result <-> x.v <> y.v }

  use mach.peano.Peano as P

  val to_peano (x: t) : P.t
    ensures { result.P.v = x.v }

  val transfer (x: t) : t
    requires { x.valid }
    writes   { x.valid }
    ensures  { result.valid /\ not x.valid }
    ensures  { result.v = x.v }

  val neg (x: t) : t
    requires { x.valid }
    writes   { x.valid }
    ensures  { result.valid /\ not x.valid }
    ensures  { result.v = - x.v }

  val abs (x: t) : t
    requires { x.valid }
    writes   { x.valid }
    ensures  { result.valid /\ not x.valid }
    ensures  { result.v = if x.v >= 0 then x.v else - x.v }

  val add (x y: t) : t
    requires { x.valid /\ y.valid }
    writes   { x.valid, y.valid }
    ensures  { result.valid /\ not x.valid /\ not y.valid }
    ensures  { result.v = x.v + y.v }

  val sub (x y: t) : t
    requires { x.valid /\ y.valid }
    writes   { x.valid, y.valid }
    ensures  { result.valid /\ not x.valid /\ not y.valid }
    ensures  { result.v = x.v - y.v }

  val split (x: t) (p: P.t) : (t, t)
    requires { x.valid }
    requires { 0 <= p.P.v <= x.v \/ x.v <= p.P.v <= 0 }
    writes   { x.valid }
    ensures  { not x.valid }
    returns  { a, b -> a.valid /\ b.valid /\ a.v = x.v - b.v /\ b.v = p.P.v }

end