-
Notifications
You must be signed in to change notification settings - Fork 4
/
rand.lisp
71 lines (52 loc) · 2.32 KB
/
rand.lisp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
#|
Modified by Dale Vaillancourt 14 January 2006
Removed uses of ACL2 state; the seed is now passed functionally.
Modified by Carl Eastlund 14 May 2006
Added next-seed function for updating the seed.
------------------------------------------------------------------
A Simple Random Number Generator Version 0.3
Carl Eastlund <cce@ccs.neu.edu> June 3, 2008
Originally by: Jared Davis <jared@cs.utexas.edu>
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.
You will want to use the following functions:
(rand max seed)
Returns a natural number from 0 to max-1, inclusive, based on seed.
Successive calls should therefore use a new seed.
(initial-seed)
Returns an initial value for the random seed.
(next-seed seed)
Produces a new seed for use after a call to rand.
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 rand/range, initial-seed/seedp, and next-seed/seedp.
|#
(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 next-seed (seed)
(declare (xargs :guard (posp seed)))
(max (mod (* *P1* seed) *M31*) 1))
(defun rand (max seed)
(declare (xargs :guard (and (integerp max) (> max 0) (posp seed))))
(mod seed max))
(defthm initial-seed/posp
(posp (initial-seed)))
(defthm next-seed/posp
(implies (posp seed) (posp (next-seed seed))))
(defthm rand/range
(implies (and (posp s) (integerp n) (< 0 n))
(and (integerp (rand n s))
(<= 0 (rand n s))
(< (rand n s) n))))
(in-theory (disable rand next-seed initial-seed))