guard-verified-exec-fnsp-tests

(in-package "ACL2")

(assert! (guard-verified-exec-fnsp 'x (w state)))

(assert! (guard-verified-exec-fnsp ''4 (w state)))

(assert! (guard-verified-exec-fnsp '(cons x y) (w state)))

(must-succeed* (defun f (x) (declare (xargs :verify-guards nil)) x)
  (defun g (x) (declare (xargs :verify-guards t)) x)
  (assert! (not (guard-verified-exec-fnsp '(cons (f x) (g (f y))) (w state)))))

(must-succeed* (defun mycar
    (x)
    (declare (xargs :verify-guards nil))
    (car x))
  (assert! (not (guard-verified-exec-fnsp '(cons (mycar z) (len y))
        (w state))))
  (defun f
    (x)
    (mbe :logic (mycar x)
      :exec (if (consp x)
        (car x)
        nil)))
  (assert! (guard-verified-exec-fnsp (body 'f nil (w state)) (w state))))

(must-succeed* (defun f (x) (declare (xargs :verify-guards nil)) x)
  (defun g
    (x)
    (declare (xargs :verify-guards t))
    (cons (ec-call (f x)) (len x)))
  (assert! (guard-verified-exec-fnsp (body 'g nil (w state)) (w state))))