Peano and one-time integers, with suitable drivers for OCaml extraction

parent dbf8fc7d
(* OCaml driver for 64-bit architecture *)
(** OCaml driver for 64-bit architecture *)
import "ocaml-gen.drv"
(* TODO bv.BV31 ? *)
(* TODO bv.BV32 -> int or int32 ? *)
(** Machine arithmetic *)
module mach.int.Int32
syntax val of_int "Why3__BigInt.to_int"
......@@ -64,15 +62,6 @@ module mach.int.UInt32
end
theory bv.BV63
syntax type t "int"
syntax constant zero "0"
syntax constant ones "-1"
syntax function bw_and "(%1 land %2)"
syntax predicate eq "(%1 = %2)"
(* TODO ... *)
end
module mach.int.Int63
syntax val of_int "Why3__BigInt.to_int"
syntax converter of_int "%1"
......@@ -97,8 +86,6 @@ module mach.int.Int63
syntax val of_bv "(fun x -> x)"
end
(* TODO bv.BV64 -> int64 *)
module mach.int.Int64
syntax val of_int "Why3__BigInt.to_int64"
syntax converter of_int "%1L"
......@@ -120,7 +107,68 @@ module mach.int.Int64
syntax val (>) "(>)"
end
(* arrays *)
module mach.peano.Peano
syntax type t "int"
syntax val to_int "Why3__BigInt.of_int"
syntax val zero "(fun _ -> 0)"
syntax val succ "succ"
syntax val pred "pred"
syntax val lt "(<)"
syntax val le "(<=)"
syntax val gt "(>)"
syntax val ge "(>=)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val neg "(~-)"
syntax val abs "abs"
syntax val add "(+)"
syntax val sub "(-)"
syntax val mul "( * )"
syntax val of_int "(fun n _ _ -> Why3__BigInt.to_int n)"
syntax val div "(/)"
syntax val mod "(mod)"
syntax val max "max"
syntax val min "min"
end
module mach.onetime.OneTime
syntax type t "int"
syntax val to_int "Why3__BigInt.of_int"
syntax val zero "(fun _ -> 0)"
syntax val succ "succ"
syntax val pred "pred"
syntax val lt "(<)"
syntax val le "(<=)"
syntax val gt "(>)"
syntax val ge "(>=)"
syntax val eq "(=)"
syntax val ne "(<>)"
syntax val to_peano "(fun x -> x)"
syntax val transfer "(fun x -> x)"
syntax val neg "(~-)"
syntax val abs "abs"
syntax val add "(+)"
syntax val sub "(-)"
syntax val split "(fun x y -> x - y, y)"
end
(** Bit vectors *)
theory bv.BV63
syntax type t "int"
syntax constant zero "0"
syntax constant ones "-1"
syntax function bw_and "(%1 land %2)"
syntax predicate eq "(%1 = %2)"
(* TODO ... *)
end
(* TODO
bv.BV31 ?
bv.BV32 -> int or int32 ?
bv.BV64 -> int64 *)
(** Arrays *)
module mach.array.Array32
syntax type array "(%1 array)"
......@@ -151,3 +199,4 @@ module mach.array.Array63
syntax val blit "Array.blit"
syntax val self_blit "Array.blit"
end
(** {2 One-time integers} *)
module OneTime
use import int.Int
type t model { v: int; mutable ghost valid: bool }
val to_int (x: t) : int
ensures { result = x.v }
val zero (): t
ensures { result.valid }
ensures { result.v = 0 }
(* FIXME: should be a constant?
val function zero : t
ensures { result.valid }
ensures { result.v = 0 }
*)
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
(** {2 Peano arithmetic} *)
module Peano
use import int.Int
type t model { v: int }
val to_int (x: t) : int
ensures { result = x.v }
val zero (): t
ensures { result.v = 0 }
(* FIXME: should be a constant
val function zero : t
ensures { result.v = 0 }
*)
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
ensures { result <-> x.v = y.v }
val ne (x y: t) : bool
ensures { result <-> x.v <> y.v }
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
*)
use import int.ComputerDivision
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 }
use import int.MinMax
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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment