#|
Modified by Dale Vaillancourt 14 January 2006
Removed uses of ACL2 state; the seed is now passed functionally.
------------------------------------------------------------------
A Simple Random Number Generator Version 0.1
Jared Davis February 25, 2004
This file is in the public domain. You can freely use it for any
purpose without restriction.
This is just a basic pure multiplicative pseudorandom number gen-
erator. *M31* is the 31st mersenne prime, and *P1* is 7^5 which
is a primitive root of *M31*, ensuring that our period is M31 - 1.
This idea is described in "Elementary Number Theory and its Appli-
cations" by Kenneth H. Rosen, Fourth Edition, Addison Wesley 1999,
in Chapter 10.1, pages 356-358.
The random number generator uses a stobj, rand, to store the seed.
You will want to use the following functions:
(genrandom rand)
Returns (mv k rand) where 0 <= k < max.
(update-seed rand)
Manually switch to a new seed. By default, a large messy num-
ber will be used. You probably don't need to change it, but
it might be good if you want to be able to reproduce your re-
sults in the future.
Normally we are not particularly interested in reasoning about ran-
dom numbers. However, we can say that the number k generated is an
an integer, and that 0 <= k < max when max is a positive integer.
See the theorems genrandom-minimum and genrandom-maximum.
|#
(in-package "ACL2")
(set-verify-guards-eagerness 2)
(local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))
(defconst *M31* 2147483647)
(defconst *P1* 16807)
(defun initial-seed () 1382728371)
(defun seedp (x) (and (integerp x) (> x 0)))
(defun next-seed (seed)
(declare (xargs :guard (seedp seed)))
(max (mod (* *P1* seed) *M31*) 1))
(defun rand (max seed)
(declare (xargs :guard (and (integerp max) (> max 0) (seedp seed))))
(mod seed max))
(defthm initial-seed/seedp
(seedp (initial-seed)))
(defthm next-seed/seedp
(implies (seedp seed) (seedp (next-seed seed))))
(defthm rand/range
(implies (and (seedp s) (integerp n) (< 0 n))
(and (integerp (rand n s))
(<= 0 (rand n s))
(< (rand n s) n))))
(in-theory (disable rand next-seed seedp initial-seed))