module mach.int.Random63: less spec and OCaml driver

parent 3a34dce6
......@@ -226,8 +226,8 @@ 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 self_init "Random.self_init %1"
syntax val random_bool "Random.bool %1"
syntax val random_int63 "Random.int %1"
end
......
......@@ -329,14 +329,12 @@ module Random63
let self_init () = self_init s
let random_bool ()
ensures { s.state = next (old s.state) }
ensures { result = get_bool s.state }
writes { s }
= random_bool s
let random_int63 (n: int63) : int63
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 }
writes { s }
ensures { 0 <= result < n }
= random_int63 s 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