random-state-basis1

(in-package "DEFDATA")

(set-verify-guards-eagerness 2)

(include-book "std/util/bstar" :dir :system)

(include-book "acl2s/utilities" :dir :system)

(include-book "ihs/basic-definitions" :dir :system)

(local (include-book "ihs/logops-definitions" :dir :system))

(local (include-book "centaur/bitops/ihsext-basics" :dir :system))

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

(make-event (er-progn (assign random-seed 1382728371)
    (value '(value-triple (@ random-seed))))
  :check-expansion t)

(defun getseed
  (state)
  (declare (xargs :stobjs (state)))
  (if (f-boundp-global 'random-seed
      state)
    (b* ((s (@ random-seed)))
      (if (unsigned-byte-p 63 s)
        (the (unsigned-byte 63) s)
        0))
    0))

(defthm getseed-unsigned-byte63
  (unsigned-byte-p 63
    (getseed state))
  :rule-classes (:rewrite :type-prescription))

(defthm getseed-nat
  (natp (getseed state))
  :rule-classes :type-prescription)

(in-theory (disable getseed))

(defun putseed
  (s state)
  (declare (xargs :stobjs (state)
      :guard (unsigned-byte-p 63 s)))
  (declare (type (unsigned-byte 63) s))
  (f-put-global 'random-seed
    s
    state))

(defun genrandom-seed
  (max raw-seed)
  "generates a pseudo-random number less than max, given that the
current random seed is seed. and also returns the new seed."
  (declare (type (unsigned-byte 63) max)
    (type (unsigned-byte 63) raw-seed))
  (declare (xargs :guard (and (unsigned-byte-p 63 max)
        (unsigned-byte-p 63 raw-seed)
        (posp max))))
  (b* (((the (unsigned-byte 64) seed) (logcons 1 raw-seed)) ((the (unsigned-byte 64) next-seed) (loghead 64 (+ seed 7664345821816969130)))
      ((the (unsigned-byte 64) z) (loghead 64
          (* (logxor seed (loghead 64 (ash seed -25)))
            next-seed)))
      ((the (unsigned-byte 64) z) (logxor z (loghead 64 (ash z -22)))))
    (mv (loghead 63 (mod z max))
      (loghead 63 (ash next-seed -1)))))

(defthm genrandom-seed-res-size
  (implies (and (unsigned-byte-p 63 max)
      (posp max)
      (unsigned-byte-p 63 seed))
    (unsigned-byte-p 63
      (mv-nth 0
        (genrandom-seed max seed))))
  :rule-classes :type-prescription)

(defun genrandom-state
  (max state)
  "generates a pseudo-random number less than max"
  (declare (type (unsigned-byte 63) max))
  (declare (xargs :stobjs (state)
      :guard (and (unsigned-byte-p 63 max) (posp max))))
  (b* ((raw-seed (getseed state)) ((mv res next-seed) (genrandom-seed max raw-seed))
      (state (putseed next-seed state)))
    (mv res state)))

(defthm genrandom-state-res-size
  (implies (and (unsigned-byte-p 63 max) (posp max))
    (unsigned-byte-p 63
      (mv-nth 0
        (genrandom-state max state))))
  :rule-classes :type-prescription)

(encapsulate nil
  (local (defthm lemma1
      (implies (and (posp max) (natp x))
        (<= 0 (mod x max)))
      :rule-classes :linear))
  (local (defthm lemma2
      (implies (and (posp max)
          (< max 2147483648)
          (natp x))
        (< (mod x max) 2147483648))
      :rule-classes :linear))
  (defthm genrandom-natural1
    (implies (and (posp max))
      (and (integerp (mv-nth 0
            (genrandom-seed max seed)))
        (>= (mv-nth 0
            (genrandom-seed max seed))
          0)))
    :rule-classes :type-prescription)
  (defthm genrandom-natural2-type
    (implies (and (natp seed))
      (and (integerp (mv-nth 1
            (genrandom-seed max seed)))
        (<= 0
          (mv-nth 1
            (genrandom-seed max seed)))))
    :rule-classes :type-prescription)
  (defthm genrandom-ub63-1
    (implies (and (<= 1 max)
        (unsigned-byte-p 63 max)
        (natp seed))
      (unsigned-byte-p 63
        (mv-nth 0
          (genrandom-seed max seed))))
    :rule-classes (:type-prescription))
  (defthm genrandom-ub63-2
    (implies (and (<= 1 max)
        (unsigned-byte-p 63 max)
        (natp seed))
      (unsigned-byte-p 63
        (mv-nth 1
          (genrandom-seed max seed))))
    :rule-classes :type-prescription)
  (defthm genrandom-minimum1
    (implies (and (posp max) (natp seed))
      (<= 0
        (mv-nth 0
          (genrandom-seed max seed))))
    :rule-classes :linear)
  (defthm genrandom-minimum2
    (implies (and (natp seed))
      (<= 0
        (mv-nth 1
          (genrandom-seed max seed))))
    :rule-classes :linear)
  (local (defthm loghead-lt-help
      (implies (and (natp x)
          (natp y)
          (posp size)
          (< x y))
        (< (loghead size x) y))
      :hints (("Goal" :in-theory (enable loghead)))))
  (defthm genrandom-maximum1
    (implies (and (posp max))
      (< (mv-nth 0
          (genrandom-seed max seed))
        max))
    :rule-classes (:linear))
  (defthm genrandom-maximum2
    (implies (and (posp max)
        (unsigned-byte-p 63 seed))
      (<= (mv-nth 1
          (genrandom-seed max seed))
        (1- (expt 2 63))))
    :rule-classes :linear)
  (defthm genrandom-state-natural
    (natp (mv-nth 0
        (genrandom-state max state)))
    :rule-classes :type-prescription)
  (defthm genrandom-state-minimum
    (<= 0
      (mv-nth 0
        (genrandom-state max state)))
    :rule-classes :linear)
  (local (defthm loghead-lte-help
      (implies (and (natp x)
          (natp y)
          (posp size)
          (<= x y))
        (<= (loghead size x) y))
      :hints (("Goal" :in-theory (enable loghead)))))
  (defthm genrandom-state-maximum
    (implies (posp max)
      (<= (mv-nth 0
          (genrandom-state max state))
        (1- max)))
    :rule-classes :linear))

(in-theory (disable genrandom-seed
    genrandom-state))