Filtering...

random-state

books/acl2s/defdata/random-state
other
(in-package "DEFDATA")
other
(set-verify-guards-eagerness 2)
other
(include-book "random-state-basis1")
other
(include-book "builtin-combinators")
other
(include-book "number-enums-sampling")
random-booleanfunction
(defun random-boolean
  (state)
  (declare (xargs :stobjs (state)))
  (mv-let (num state)
    (genrandom-state 2 state)
    (mv (= 1 num) state)))
other
(defthm random-boolean-type
  (booleanp (mv-nth 0 (random-boolean r)))
  :rule-classes :type-prescription)
other
(in-theory (disable random-boolean))
random-natural-basemax1function
(defun random-natural-basemax1
  (base maxdigits seed.)
  (declare (type (integer 1 16) base)
    (type (integer 0 19) maxdigits)
    (type (unsigned-byte 63) seed.)
    (xargs :guard (and (unsigned-byte-p 63 seed.)
        (posp base)
        (<= base 16)
        (> base 0)
        (natp maxdigits)
        (< maxdigits 20)
        (>= maxdigits 0))))
  (if (zp maxdigits)
    (mv 0 seed.)
    (b* (((mv (the (integer 0 64) v)
          (the (unsigned-byte 63) seed.)) (genrandom-seed (*f 2 base)
           seed.)))
      (if (>= v base)
        (b* (((mv v2 seed.) (random-natural-basemax1 base
               (1- maxdigits)
               seed.)))
          (mv (+ (- v base)
              (* base (nfix v2)))
            seed.))
        (mv v seed.)))))
random-natural-seed/0.5function
(defun random-natural-seed/0.5
  (seed.)
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :guard (unsigned-byte-p 63 seed.)))
  (mbe :logic (if (unsigned-byte-p 63 seed.)
      (random-natural-basemax1 10 6 seed.)
      (random-natural-basemax1 10 6 1382728371))
    :exec (random-natural-basemax1 10 6 seed.)))
random-natural-basemax2function
(defun random-natural-basemax2
  (base maxdigits seed.)
  (declare (type (integer 1 16) base)
    (type (integer 0 20) maxdigits)
    (type (unsigned-byte 63) seed.)
    (xargs :guard (and (unsigned-byte-p 63 seed.)
        (posp base)
        (<= base 16)
        (> base 0)
        (natp maxdigits)
        (< maxdigits 20)
        (>= maxdigits 0))))
  (if (zp maxdigits)
    (b* (((mv (the (integer 0 16) v)
          (the (unsigned-byte 63) seed.)) (genrandom-seed base seed.)))
      (mv v seed.))
    (b* (((mv (the (integer 0 64) v)
          (the (unsigned-byte 63) seed.)) (genrandom-seed (*f 4 base)
           seed.)))
      (if (>= v base)
        (b* (((mv v2 seed.) (random-natural-basemax2 base
               (1- maxdigits)
               seed.)))
          (mv (+ (- v base)
              (* base (nfix v2)))
            seed.))
        (mv v seed.)))))
random-natural-seed/0.25function
(defun random-natural-seed/0.25
  (seed.)
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :guard (unsigned-byte-p 63 seed.)))
  (mbe :logic (if (unsigned-byte-p 63 seed.)
      (random-natural-basemax2 10 6 seed.)
      (random-natural-basemax2 10 6 1382728371))
    :exec (random-natural-basemax2 10 6 seed.)))
other
(encapsulate (((random-natural-seed *) =>
     (mv * *)
     :formals (seed.)
     :guard (unsigned-byte-p 63 seed.)))
  (local (defun random-natural-seed
      (seed.)
      (declare (xargs :guard (unsigned-byte-p 63 seed.)))
      (mbe :logic (if (unsigned-byte-p 63 seed.)
          (mv 0 seed.)
          (mv 0 1382728371))
        :exec (mv 0 seed.))))
  (defthm random-natural-seed-type-consp
    (consp (random-natural-seed r))
    :rule-classes (:type-prescription))
  (defthm random-natural-seed-type-car
    (implies (unsigned-byte-p 63 r)
      (natp (mv-nth 0
          (random-natural-seed r))))
    :rule-classes (:type-prescription))
  (defthm random-natural-seed-type-car-type
    (implies (natp r)
      (and (integerp (mv-nth 0
            (random-natural-seed r)))
        (>= (mv-nth 0
            (random-natural-seed r))
          0)))
    :rule-classes :type-prescription)
  (defthm random-natural-seed-type-cadr
    (implies (unsigned-byte-p 63 r)
      (unsigned-byte-p 63
        (mv-nth 1
          (random-natural-seed r))))
    :rule-classes (:type-prescription))
  (defthm random-natural-seed-type-cadr-linear
    (and (<= 0
        (mv-nth 1
          (random-natural-seed r)))
      (< (mv-nth 1
          (random-natural-seed r))
        9223372036854775808))
    :rule-classes (:linear :tau-system))
  (defthm random-natural-seed-type-cadr-type
    (and (integerp (mv-nth 1
          (random-natural-seed r)))
      (>= (mv-nth 1
          (random-natural-seed r))
        0))
    :rule-classes (:type-prescription)))
random-small-natural-seedfunction
(defun random-small-natural-seed
  (seed.)
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :guard (unsigned-byte-p 63 seed.)))
  (mbe :logic (if (unsigned-byte-p 63 seed.)
      (random-natural-basemax1 10 3 seed.)
      (random-natural-basemax1 10 3 1382728371))
    :exec (random-natural-basemax1 10 3 seed.)))
random-index-seedmacro
(defmacro random-index-seed
  (max seed.)
  `(genrandom-seed ,MAX ,DEFDATA::SEED.))
other
(defthm random-natural-basemax1-type-car
  (implies (and (posp b)
      (natp d)
      (natp r))
    (and (integerp (mv-nth 0
          (random-natural-basemax1 b
            d
            r)))
      (>= (mv-nth 0
          (random-natural-basemax1 b
            d
            r))
        0)))
  :rule-classes (:type-prescription))
other
(defthm random-natural-basemax1-type-cadr
  (implies (and (posp b)
      (natp d)
      (unsigned-byte-p 63 r))
    (unsigned-byte-p 63
      (mv-nth 1
        (random-natural-basemax1 b
          d
          r))))
  :rule-classes :type-prescription)
other
(defthm random-natural-basemax1-type-cadr-0
  (implies (and (posp b)
      (natp d)
      (unsigned-byte-p 63 r))
    (and (<= 0
        (mv-nth 1
          (random-natural-basemax1 b
            d
            r)))
      (< (mv-nth 1
          (random-natural-basemax1 b
            d
            r))
        9223372036854775808)))
  :rule-classes (:linear :type-prescription))
other
(defthm random-natural-basemax1-type-cadr-type
  (implies (and (posp b)
      (natp d)
      (natp r))
    (and (integerp (mv-nth 1
          (random-natural-basemax1 b
            d
            r)))
      (>= (mv-nth 1
          (random-natural-basemax1 b
            d
            r))
        0)))
  :rule-classes (:type-prescription))
other
(defthm random-natural-basemax2-type-car
  (implies (and (posp b)
      (natp d)
      (natp r))
    (and (integerp (mv-nth 0
          (random-natural-basemax2 b
            d
            r)))
      (>= (mv-nth 0
          (random-natural-basemax2 b
            d
            r))
        0)))
  :rule-classes (:type-prescription))
other
(defthm random-natural-basemax2-type-cadr
  (implies (and (posp b)
      (natp d)
      (unsigned-byte-p 63 r))
    (unsigned-byte-p 63
      (mv-nth 1
        (random-natural-basemax2 b
          d
          r))))
  :rule-classes :type-prescription)
other
(defthm random-natural-basemax2-type-cadr-0
  (implies (and (posp b)
      (natp d)
      (unsigned-byte-p 63 r))
    (and (<= 0
        (mv-nth 1
          (random-natural-basemax2 b
            d
            r)))
      (< (mv-nth 1
          (random-natural-basemax2 b
            d
            r))
        9223372036854775808)))
  :rule-classes (:linear :type-prescription))
other
(defthm random-natural-basemax2-type-cadr-type
  (implies (and (posp b)
      (natp d)
      (natp r))
    (and (integerp (mv-nth 1
          (random-natural-basemax2 b
            d
            r)))
      (>= (mv-nth 1
          (random-natural-basemax2 b
            d
            r))
        0)))
  :rule-classes (:type-prescription))
other
(defthm random-natural-seed-type/0.5-car
  (implies (unsigned-byte-p 63 r)
    (natp (mv-nth 0
        (random-natural-seed/0.5 r))))
  :rule-classes (:type-prescription))
other
(defthm random-natural-seed-type/0.5-car-type
  (implies (natp r)
    (and (integerp (mv-nth 0
          (random-natural-seed/0.5 r)))
      (>= (mv-nth 0
          (random-natural-seed/0.5 r))
        0)))
  :rule-classes :type-prescription)
other
(defthm random-natural-seed-type/0.5-cadr
  (implies (unsigned-byte-p 63 r)
    (unsigned-byte-p 63
      (mv-nth 1
        (random-natural-seed/0.5 r))))
  :rule-classes (:type-prescription))
other
(defthm random-natural-seed-type/0.5-cadr-linear
  (and (<= 0
      (mv-nth 1
        (random-natural-seed/0.5 r)))
    (< (mv-nth 1
        (random-natural-seed/0.5 r))
      9223372036854775808))
  :rule-classes (:linear :tau-system))
other
(defthm random-natural-seed-type/0.5-cadr-type
  (and (integerp (mv-nth 1
        (random-natural-seed/0.5 r)))
    (>= (mv-nth 1
        (random-natural-seed/0.5 r))
      0))
  :rule-classes (:type-prescription))
other
(defthm random-natural-seed-type/0.25-car
  (implies (unsigned-byte-p 63 r)
    (natp (mv-nth 0
        (random-natural-seed/0.25 r))))
  :rule-classes (:type-prescription))
other
(defthm random-natural-seed-type/0.25-car-type
  (implies (natp r)
    (and (integerp (mv-nth 0
          (random-natural-seed/0.25 r)))
      (>= (mv-nth 0
          (random-natural-seed/0.25 r))
        0)))
  :rule-classes :type-prescription)
other
(defthm random-natural-seed-type/0.25-cadr
  (implies (unsigned-byte-p 63 r)
    (unsigned-byte-p 63
      (mv-nth 1
        (random-natural-seed/0.25 r))))
  :rule-classes (:type-prescription))
other
(defthm random-natural-seed-type/0.25-cadr-linear
  (and (<= 0
      (mv-nth 1
        (random-natural-seed/0.25 r)))
    (< (mv-nth 1
        (random-natural-seed/0.25 r))
      9223372036854775808))
  :rule-classes (:linear :tau-system))
other
(defthm random-natural-seed-type/0.25-cadr-type
  (and (integerp (mv-nth 1
        (random-natural-seed/0.25 r)))
    (>= (mv-nth 1
        (random-natural-seed/0.25 r))
      0))
  :rule-classes (:type-prescription))
other
(defattach random-natural-seed
  random-natural-seed/0.25)
other
(in-theory (disable random-natural-basemax1
    random-natural-seed/0.25
    random-natural-seed/0.5))
random-index-list-seedfunction
(defun random-index-list-seed
  (k max seed.)
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :verify-guards nil
      :guard (unsigned-byte-p 63 seed.)))
  (if (zp k)
    (mv 'nil seed.)
    (b* (((mv rest seed.) (random-index-list-seed (1- k)
           max
           seed.)) ((mv n1 seed.) (if (zp max)
            (mv 0 seed.)
            (random-index-seed max seed.))))
      (mv (cons n1 rest) seed.))))
random-natural-list-seedfunction
(defun random-natural-list-seed
  (k seed.)
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :verify-guards nil
      :guard (unsigned-byte-p 63 seed.)))
  (if (zp k)
    (mv 'nil seed.)
    (b* (((mv rest seed.) (random-natural-list-seed (1- k)
           seed.)) ((mv n1 seed.) (random-natural-seed seed.)))
      (mv (cons n1 rest) seed.))))
random-probability-seedfunction
(defun random-probability-seed
  (seed.)
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :verify-guards nil
      :guard (unsigned-byte-p 63 seed.)))
  (mbe :logic (if (unsigned-byte-p 63 seed.)
      (mv-let (a seed.)
        (random-natural-seed seed.)
        (let ((denom (if (int= a 0)
               (1+ a)
               a)))
          (mv-let (numer seed.)
            (genrandom-seed (1+ denom) seed.)
            (mv (/ numer denom)
              seed.))))
      (mv 0 seed.))
    :exec (mv-let (a seed.)
      (random-natural-seed seed.)
      (let ((denom (if (int= a 0)
             (1+ a)
             a)))
        (mv-let (numer seed.)
          (genrandom-seed (1+ denom) seed.)
          (mv (/ numer denom)
            seed.))))))
random-rational-between-seedfunction
(defun random-rational-between-seed
  (lo hi seed.)
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :verify-guards nil
      :guard (unsigned-byte-p 63 seed.)))
  (mv-let (p seed.)
    (random-probability-seed seed.)
    (mv (rfix (+ lo (* p (- hi lo))))
      seed.)))
random-integer-seedfunction
(defun random-integer-seed
  (seed.)
  (declare (type (unsigned-byte 63) seed.))
  (declare (xargs :guard (unsigned-byte-p 63 seed.)))
  (mv-let (num seed.)
    (genrandom-seed 2 seed.)
    (mv-let (nat seed.)
      (random-natural-seed seed.)
      (mv (if (int= num 0)
          nat
          (- nat))
        seed.))))
random-integer-between-seedfunction
(defun random-integer-between-seed
  (lo hi seed.)
  (declare (type (unsigned-byte 63) seed.)
    (type (signed-byte 62) lo)
    (type (signed-byte 62) hi))
  (declare (xargs :guard (and (unsigned-byte-p 63 seed.)
        (integerp lo)
        (integerp hi)
        (signed-byte-p 62 lo)
        (signed-byte-p 62 hi)
        (natp (- hi lo)))))
  (mv-let (num seed.)
    (genrandom-seed (1+ (- hi lo))
      seed.)
    (mv (+ lo num) seed.)))
random-complex-rational-between-seedfunction
(defun random-complex-rational-between-seed
  (lo hi seed.)
  (declare (xargs :verify-guards nil
      :guard (unsigned-byte-p 63 seed.)))
  (declare (type (unsigned-byte 63) seed.))
  (b* (((mv rp seed.) (random-rational-between-seed (realpart lo)
         (realpart hi)
         seed.)) ((mv ip seed.) (random-rational-between-seed (imagpart lo)
          (imagpart hi)
          seed.)))
    (mv (complex rp ip)
      seed.)))
random-acl2-number-between-seedfunction
(defun random-acl2-number-between-seed
  (lo hi seed.)
  (declare (xargs :verify-guards nil
      :guard (unsigned-byte-p 63 seed.)))
  (b* (((mv choice seed.) (random-index-seed 6 seed.)))
    (case choice
      (0 (random-integer-between-seed lo
          hi
          seed.))
      (1 (random-rational-between-seed lo
          hi
          seed.))
      (5 (random-complex-rational-between-seed lo
          hi
          seed.))
      (t (random-integer-between-seed lo
          hi
          seed.)))))
random-number-between-seed-fnfunction
(defun random-number-between-seed-fn
  (lo hi seed. type)
  (declare (xargs :verify-guards nil
      :guard (unsigned-byte-p 63 seed.)))
  (case type
    (integer (random-integer-between-seed lo
        hi
        seed.))
    (rational (random-rational-between-seed lo
        hi
        seed.))
    (complex-rational (random-complex-rational-between-seed lo
        hi
        seed.))
    (t (random-acl2-number-between-seed lo
        hi
        seed.))))
random-number-between-seedmacro
(defmacro random-number-between-seed
  (lo hi seed. &key type)
  `(random-number-between-seed-fn ,DEFDATA::LO
    ,DEFDATA::HI
    ,DEFDATA::SEED.
    (or ,TYPE 'acl2-number)))
other
(logic)
other
(encapsulate (((sampling-dist-rec * *) =>
     *
     :formals (min max)
     :guard (and (natp min) (posp max) (<= min max))))
  (local (defun sampling-dist-rec
      (min max)
      (declare (xargs :guard (and (natp min) (posp max) (<= min max))))
      (list min max))))
sampling-dist-rec-builtinfunction
(defun sampling-dist-rec-builtin
  (min max)
  (declare (xargs :guard (and (natp min) (posp max) (<= min max))))
  (b* ((lo-1 (force-between *dist-lo1* min max)) (hi-1 (force-between *dist-hi1* min max))
      (lo-2 (force-between *dist-lo2* min max))
      (hi-2 (force-between *dist-hi2* min max))
      (lo-3 (force-between *dist-lo3* min max))
      (hi-3 (force-between *dist-hi3* min max))
      (lo-4 (force-between *dist-lo4* min max))
      (hi-4 (force-between *dist-hi4* min max))
      (lo-5 (force-between *dist-lo5* min max))
      (hi-5 (force-between *dist-hi5* min max))
      (mid (floor (+ min max) 2))
      (mid-lo-1 (force-between (- mid hi-1)
          min
          max))
      (mid-hi-1 (force-between (+ mid hi-1)
          min
          max))
      (mid-lo-2 (force-between (- mid hi-2)
          min
          max))
      (mid-hi-2 (force-between (+ mid hi-2)
          min
          max))
      (mid-lo-3 (force-between (- mid hi-3)
          min
          max))
      (mid-hi-3 (force-between (+ mid hi-3)
          min
          max))
      (mid-lo-4 (force-between (- mid hi-4)
          min
          max))
      (mid-hi-4 (force-between (+ mid hi-4)
          min
          max))
      (mid-lo-5 (force-between (- mid hi-5)
          min
          max))
      (mid-hi-5 (force-between (+ mid hi-5)
          min
          max)))
    `((1 :eq ,MIN) (1 :eq ,MAX)
      (1 :eq ,DEFDATA::MID)
      (4 :uniform ,DEFDATA::LO-1 ,DEFDATA::HI-1)
      (4 :uniform ,DEFDATA::LO-2 ,DEFDATA::HI-2)
      (4 :uniform ,DEFDATA::LO-3 ,DEFDATA::HI-3)
      (4 :uniform ,DEFDATA::LO-4 ,DEFDATA::HI-4)
      (4 :uniform ,DEFDATA::LO-5 ,DEFDATA::HI-5)
      (4 :uniform ,DEFDATA::MID-LO-1 ,DEFDATA::MID-HI-1)
      (4 :uniform ,DEFDATA::MID-LO-2 ,DEFDATA::MID-HI-2)
      (4 :uniform ,DEFDATA::MID-LO-3 ,DEFDATA::MID-HI-3)
      (4 :uniform ,DEFDATA::MID-LO-4 ,DEFDATA::MID-HI-4)
      (4 :uniform ,DEFDATA::MID-LO-5 ,DEFDATA::MID-HI-5)
      (5 :geometric :leq-bnd ,MAX ,MIN)
      (24 :geometric :geq-bnd ,MIN ,MAX)
      (14 :geometric :between ,MIN ,MAX)
      (14 :uniform ,MIN ,MAX))))
other
(defattach sampling-dist-rec
  sampling-dist-rec-builtin)
other
(include-book "switchnat")
choose-sizefunction
(defun choose-size
  (min max seed.)
  (declare (type (unsigned-byte 63) seed.)
    (type (signed-byte 62) min)
    (type (signed-byte 62) max))
  (declare (xargs :verify-guards nil
      :guard (and (unsigned-byte-p 63 seed.)
        (natp min)
        (natp max)
        (signed-byte-p 62 min)
        (signed-byte-p 62 max))))
  (b* ((ctx 'choose-size) ((mv idx
         (the (unsigned-byte 63) seed.)) (random-index-seed 100 seed.))
      (sampling-dist (sampling-dist-rec min max))
      (weights (strip-cars sampling-dist))
      ((mv choice &) (weighted-switch-nat weights idx))
      (chosen (nth choice sampling-dist))
      (sp (cdr chosen))
      ((mv n
         (the (unsigned-byte 63) seed.)) (random-small-natural-seed seed.))
      ((mv uniform-n
         (the (unsigned-byte 63) seed.)) (random-integer-between-seed min
          max
          seed.))
      (size (case-match sp
          ((':eq x) x)
          ((':geometric ':around x) (geometric-int-around x n))
          ((':geometric ':leq x) (geometric-int-leq x n))
          ((':geometric ':geq x) (geometric-int-geq x n))
          ((':geometric ':around-bnd
             x
             lo
             hi) (geometric-int-around-bnd x
              lo
              hi
              n))
          ((':geometric ':leq-bnd x lo) (geometric-int-leq-bnd x
              lo
              n))
          ((':geometric ':geq-bnd x hi) (geometric-int-geq-bnd x
              hi
              n))
          ((':geometric ':between lo hi) (geometric-int-between lo
              hi
              n))
          ((':uniform & &) uniform-n)
          (& (er hard
              ctx
              "~| Unsupported case ~x0.~%"
              sp)))))
    (mv size
      (the (unsigned-byte 63) seed.))))