random

other

(in-package "ACL2")

other

(set-verify-guards-eagerness 2)

local

(local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))

*m31*constant

(defconst *m31* 2147483647)

*p1*constant

(defconst *p1* 16807)

other

(defstobj rand (seed :type integer :initially 1382728371))

getseedfunction

(defun getseed
  (rand)
  (declare (xargs :stobjs (rand)))
  (let ((s (seed rand)))
    (if (and (integerp s) (<= 0 s))
      s
      0)))

local

(local (defthm getseed-integer
    (and (integerp (getseed rand)) (<= 0 (getseed rand)))
    :rule-classes :type-prescription))

in-theory

(in-theory (disable getseed))

genrandomfunction

(defun genrandom
  (max rand)
  (declare (xargs :stobjs (rand) :guard (and (integerp max) (> max 0))))
  (let* ((new-seed (mod (* *p1* (getseed rand)) *m31*)) (rand (update-seed new-seed rand)))
    (mv (mod new-seed max) rand)))

genrandom-integertheorem

(defthm genrandom-integer
  (implies (integerp max)
    (integerp (car (genrandom max rand)))))

genrandom-minimumtheorem

(defthm genrandom-minimum
  (implies (and (integerp max) (< 0 max))
    (<= 0 (car (genrandom max rand)))))

genrandom-maximumtheorem

(defthm genrandom-maximum
  (implies (and (integerp max) (< 0 max))
    (< (car (genrandom max rand)) max)))

in-theory

(in-theory (disable genrandom))

Included Books