Commit 7ba519d5 authored by Mário Pereira's avatar Mário Pereira

Driver for randomize operations

parent 932f1898
......@@ -224,6 +224,13 @@ module mach.int.Int63
syntax val of_bv "(fun x -> x)"*)
end
module mach.int.Random63
syntax val init "Random.init %1"
syntax val self_init "Random.self_init"
syntax val random_bool "Random.bool"
syntax val random_int63 "Random.int %1"
end
module mach.peano.Peano
syntax type t "int"
syntax val to_int "Z.of_int %1"
......
......@@ -334,7 +334,7 @@ module Random63
= random_bool s
let random_int63 (n: int63) : int63
requires { 0 < n }
requires { 0 < n } (* FIXME: n should be less than 2^30 *)
ensures { s.state = next (old s.state) }
ensures { result = get_int s.state n }
ensures { 0 <= result < n }
......
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