Peano arithmetic

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 Peano.t will be mapped to OCaml's type int (63-bit signed integers).

See also mach.onetime.

module Peano

  use int.Int

  type t = abstract { v: int }
  meta coercion function v

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

  val constant zero : t
    ensures { result.v = 0 }

  val constant one : t
    ensures { result.v = 1 }

  val succ (x: t) : t
    ensures { result.v = x.v + 1 }

  val pred (x: t) : t
    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
    returns { True -> x = y | False -> x.v <> y.v }
  val ne (x y: t) : bool
    returns { True -> x.v <> y.v | False -> x = y }

  val neg (x: t) : t
    ensures { result.v = - x.v }
  val abs (x: t) : t
    ensures { result.v = if x.v >= 0 then x.v else - x.v }
  val add (x y: t) (low high: t) : t
    requires { low.v <= x.v + y.v <= high.v }
    ensures  { result.v = x.v + y.v }
  val sub (x y: t) (low high: t) : t
    requires { low.v <= x.v - y.v <= high.v }
    ensures  { result.v = x.v - y.v }
  val mul (x y: t) (low high: t) : t
    requires { low.v <= x.v * y.v <= high.v }
    ensures  { result.v = x.v * y.v }

  val of_int (x: int) (low high: t) : t
    requires { low.v <= x <= high.v }
    ensures  { result.v = x }

  (* FIXME could replace low.v  by - max (abs low) (abs high)
                         high.v by   max (abs low) (abs high)
     avoid the computation of the bounds
     e.g. addition of two values of different signs
  *)

end

module ComputerDivision

  use int.Int
  use int.ComputerDivision
  use Peano

  val div (x y: t) : t
    requires { y.v <> 0 }
    ensures  { result.v = div x.v y.v }

  val mod (x y: t) : t
    requires { y.v <> 0 }
    ensures  { result.v = mod x.v y.v }

end

module MinMax

  use int.Int
  use int.MinMax
  use Peano

  val max (x y: t) : t
    ensures { result.v = max x.v y.v }

  val min (x y: t) : t
    ensures { result.v = min x.v y.v }

end

module Int63
  use int.Int
  use mach.int.Int63
  use Peano

  val defensive_to_int63 (x:t) : int63
    requires { Int63.in_bounds x.v }
    ensures { result = x.v }

  val partial to_int63 (x:t) : int63
    ensures { result = x.v }

  val of_int63 (x:int63) (low high: t) : t
    requires { low.v <= x <= high.v }
    ensures { result.v = x }

end

module SetPeano

  use Peano

  clone export set.SetApp with type elt = Peano.t, val eq = Peano.eq

end

module MapPeano

  use Peano
  clone export fmap.MapApp with type key = Peano.t, val eq = Peano.eq

  val mapi (f: Peano.t -> 'v -> 'w) (m: t 'v) : t 'w
    ensures {forall i. S.mem i m.domain -> result i = f i (m i)}

  scope Iter  (* iteration over maps *)

    type iter 'v = abstract {
              initial: fmap Peano.t 'v;
      mutable visited: S.fset Peano.t;
    } invariant {
      S.subset visited initial.domain
    }  by {
      initial = empty;
      visited = S.empty;
    }

    val create (m: t 'v) : iter 'v
      ensures { result.initial = m.to_fmap }
      ensures { S.is_empty result.visited }

    exception Done

    val next (it: iter 'v) : (Peano.t, 'v)
      writes { it }
      raises  { Done -> it.visited = (old it).visited = it.initial.domain}
      returns { (r,v) -> S.mem r it.initial.domain /\ it.initial r = v /\
                     not (S.mem r (old it).visited) /\
                     it.visited = S.add r (old it).visited }

  end

end