; C Library
;
; Copyright (C) 2022 Kestrel Institute (http://www.kestrel.edu)
; Copyright (C) 2022 Kestrel Technology LLC (http://kestreltechnology.com)
;
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
;
; Author: Alessandro Coglio (coglio@kestrel.edu)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(in-package "C")

(include-book "execution")

(local (include-book "std/typed-lists/symbol-listp" :dir :system))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defxdoc+ atc-execution-rules
  :parents (atc-execution)
  :short "Execution rules for ATC."
  :long
  (xdoc::topstring
   (xdoc::p
    "We collect some rules about the execution of C.
     Some of these rules are used for the symbolic execution
     in the proofs generated by ATC.
     The other rules are used to prove
     the rules used for the symbolic execution.")
   (xdoc::p
    "Some of the rules that are used in the symbolic execution
     rewrite calls of functions used in the deeply embedded dynamic semantics
     into their shallowly embedded counterparts,
     under hypothesis on the types of the arguments.
     For instance, @('(exec-unary op x)')
     is rewritten to @('(<op>-<type> x)')
     when @('op') is @('<op>')
     and @('x') has type @('<type>').
     These shallowly embedded counterparts are used
     in the ACL2 functions from which C code is represented:
     thus, the rewrite rules serve to turn (the execution of) the C code
     into the ACL2 terms from which the C code is generated,
     which is at the core of proving the correctness of the generated C code.")
   (xdoc::p
    "For recursive ACL2 functions that model C execution
     (e.g. @(tsee exec-expr-pure)),
     we introduce opener rules,
     which include @(tsee syntaxp) hypotheses requiring that
     the C abstract syntax being executed is a quoted constant.
     Some of these opener rules include binding hypotheses,
     which avoid symbolically executing the same pieces of C abstract syntax
     multiple times in some situations.")
   (xdoc::p
    "We collect the rules in lists,
     each of which serves a particular symbolic execution purpose.
     Certain rules (proved elsewhere) may appear in multiple lists,
     when they serve multiple symbolic execution purposes."))
  :order-subtopics t
  :default-parent t)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define atc-syntaxp-hyp-for-expr-pure ((var symbolp))
  :returns (hyp pseudo-termp :hyp (symbolp var))
  :short "Construct a @(tsee syntaxp) hypothesis for
          a symbolic execution rule for pure expressions."
  :long
  (xdoc::topstring
   (xdoc::p
    "We use these hypotheses to ensure that
     certain execution subterms are rewritten
     to their shallow embedding counterparts
     before their enclosing terms are rewritten.
     These hypotheses require that the (sub)term in question
     does not contain any of the execution functions
     that are expected to be rewritten
     to their shallow embedding counterparts."))
  `(syntaxp (or (atom ,var)
                (not (member-eq ,var '(exec-ident
                                       exec-const
                                       exec-iconst
                                       exec-arrsub
                                       exec-memberp
                                       exec-arrsub-of-memberp
                                       exec-unary
                                       exec-cast
                                       exec-binary-strict-pure
                                       exec-test
                                       exec-expr-pure))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-tyname-to-type-rules
  :short "Rules for turning type names into types."
  :long
  (xdoc::topstring
   (xdoc::p
    "Type names arise, in quoted constant form,
     from the abstract syntax that is symbolically executed.
     In some circumstance, these type names are turned into types,
     via @(tsee tyname-to-type).
     If we just enabled the executable counterpart of this function
     we would end up with types in quoted constant form.
     Instead, we want to keep types as terms with constructors,
     particularly because some types include identifiers (e.g. structure types),
     and we want to keep identifiers as terms with constructors
     instead of in quoted constant form (see @(see atc-identifier-rules).")
   (xdoc::p
    "Thus, here we collect rules to rewrite quoted type names
     to types that are terms with constructors."))

  (defval *atc-tyname-to-type-rules*
    '(tyname-to-type
      tyname-to-type-aux
      (:e tyname->tyspec)
      (:e tyname->declor)
      (:e obj-adeclor-kind)
      (:e obj-adeclor-pointer->decl)
      (:e obj-adeclor-array->decl)
      tyspecseq-to-type
      (:e tyspecseq-kind)
      (:e tyspecseq-struct->tag))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-valuep-rules
  :short "Rules for discharging @(tsee valuep) hypotheses."
  :long
  (xdoc::topstring
   (xdoc::p
    "Some symbolic execution rules have hypotheses saying that
     certain terms are values, i.e. satisfy @(tsee valuep).
     These are discharged by backchaining to
     the fact that those terms satisfy specific value predicates,
     such as @(tsee sintp)."))

  (defval *atc-valuep-rules*
    '(valuep-when-scharp
      valuep-when-ucharp
      valuep-when-sshortp
      valuep-when-ushortp
      valuep-when-sintp
      valuep-when-uintp
      valuep-when-slongp
      valuep-when-ulongp
      valuep-when-sllongp
      valuep-when-ullongp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-value-listp-rules
  :short "Rules for discharging @(tsee value-listp) hypotheses."
  :long
  (xdoc::topstring
   (xdoc::p
    "Some symbolic execution rules have hypotheses saying that
     certain terms are lists of values, i.e. satisfy @(tsee value-listp).
     These are discharged by the rules here,
     in conjunction with the rules in @(see atc-valuep-rules)."))

  (defval *atc-value-listp-rules*
    '((:e value-listp)
      value-listp-of-cons)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-value-optionp-rules
  :short "Rules for discharging @(tsee value-optionp) hypotheses."
  :long
  (xdoc::topstring
   (xdoc::p
    "Some symbolic execution rules have hypotheses saying that
     certain terms are optional values, i.e. satisfy @(tsee value-optionp).
     These are discharged by the rules here.
     The executable counterpart of @(tsee value-optionp)
     takes care of the @('nil') case.
     The non-@('nil') case is taken care by backchaining to
     the rules in @(see atc-valuep-rules)."))

  (defval *atc-value-optionp-rules*
    '((:e value-optionp)
      value-optionp-when-valuep)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-type-of-value-rules
  :short "Rules about @(tsee type-of-value)."
  :long
  (xdoc::topstring
   (xdoc::p
    "These rules rewrite @(tsee type-of-value) to specific types
     under hypotheses on different types of values
     that occur during symbolic execution."))

  (defruled type-of-value-when-uchar-arrayp
    (implies (uchar-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-uchar)
                                (value-array->length x))))
    :enable (type-of-value
             uchar-arrayp
             value-array->elemtype
             value-array->length))

  (defruled type-of-value-when-schar-arrayp
    (implies (schar-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-schar)
                                (value-array->length x))))
    :enable (type-of-value
             schar-arrayp
             value-array->elemtype
             value-array->length))

  (defruled type-of-value-when-ushort-arrayp
    (implies (ushort-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-ushort)
                                (value-array->length x))))
    :enable (type-of-value
             ushort-arrayp
             value-array->elemtype
             value-array->length))

  (defruled type-of-value-when-sshort-arrayp
    (implies (sshort-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-sshort)
                                (value-array->length x))))
    :enable (type-of-value
             sshort-arrayp
             value-array->elemtype
             value-array->length))

  (defruled type-of-value-when-uint-arrayp
    (implies (uint-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-uint)
                                (value-array->length x))))
    :enable (type-of-value
             uint-arrayp
             value-array->elemtype
             value-array->length))

  (defruled type-of-value-when-sint-arrayp
    (implies (sint-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-sint)
                                (value-array->length x))))
    :enable (type-of-value
             sint-arrayp
             value-array->elemtype
             value-array->length))

  (defruled type-of-value-when-ulong-arrayp
    (implies (ulong-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-ulong)
                                (value-array->length x))))
    :enable (type-of-value
             ulong-arrayp
             value-array->elemtype
             value-array->length))

  (defruled type-of-value-when-slong-arrayp
    (implies (slong-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-slong)
                                (value-array->length x))))
    :enable (type-of-value
             slong-arrayp
             value-array->elemtype
             value-array->length))

  (defruled type-of-value-when-ullong-arrayp
    (implies (ullong-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-ullong)
                                (value-array->length x))))
    :enable (type-of-value
             ullong-arrayp
             value-array->elemtype
             value-array->length))

  (defruled type-of-value-when-sllong-arrayp
    (implies (sllong-arrayp x)
             (equal (type-of-value x)
                    (type-array (type-sllong)
                                (value-array->length x))))
    :enable (type-of-value
             sllong-arrayp
             value-array->elemtype
             value-array->length))

  (defval *atc-type-of-value-rules*
    '(type-of-value-when-ucharp
      type-of-value-when-scharp
      type-of-value-when-ushortp
      type-of-value-when-sshortp
      type-of-value-when-uintp
      type-of-value-when-sintp
      type-of-value-when-ulongp
      type-of-value-when-slongp
      type-of-value-when-ullongp
      type-of-value-when-sllongp
      type-of-value-when-value-pointer
      type-of-value-when-uchar-arrayp
      type-of-value-when-schar-arrayp
      type-of-value-when-ushort-arrayp
      type-of-value-when-sshort-arrayp
      type-of-value-when-uint-arrayp
      type-of-value-when-sint-arrayp
      type-of-value-when-ulong-arrayp
      type-of-value-when-slong-arrayp
      type-of-value-when-ullong-arrayp
      type-of-value-when-sllong-arrayp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-type-of-value-option-rules
  :short "Rules about @(tsee type-of-value-option)."
  :long
  (xdoc::topstring
   (xdoc::p
    "These rules reduce @(tsee type-of-value-option)
     to @(tsee type-of-value) when the argument is a value,
     and to @('void') when the argument is @('nil').
     During execution, the argument is always either @('nil')
     or a term that is easily proved to be a value;
     so these rules suffice to eliminate @(tsee type-of-value-option)."))

  (defruled type-of-value-option-when-valuep
    (implies (valuep x)
             (equal (type-of-value-option x)
                    (type-of-value x)))
    :enable (type-of-value-option
             value-option-some->val))

  (defruled type-of-value-option-of-nil
    (equal (type-of-value-option nil)
           (type-void)))

  (defval *atc-type-of-value-option-rules*
    '(type-of-value-option-when-valuep
      type-of-value-option-of-nil)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-value-array->elemtype-rules
  :short "Rules about @(tsee value-array->elemtype)."
  :long
  (xdoc::topstring
   (xdoc::p
    "These turn @(tsee value-array->elemtype) into specific types
     given that the argument satisfies predicates like @(tsee uchar-arrayp).
     Hypotheses that arrays satisfy these predicates
     are in the generated theorems,
     so they can be discharged."))

  (defruled value-array->elemtype-when-uchar-arrayp
    (implies (uchar-arrayp x)
             (equal (value-array->elemtype x)
                    (type-uchar)))
    :enable (value-array->elemtype
             uchar-arrayp))

  (defruled value-array->elemtype-when-schar-arrayp
    (implies (schar-arrayp x)
             (equal (value-array->elemtype x)
                    (type-schar)))
    :enable (value-array->elemtype
             schar-arrayp))

  (defruled value-array->elemtype-when-ushort-arrayp
    (implies (ushort-arrayp x)
             (equal (value-array->elemtype x)
                    (type-ushort)))
    :enable (value-array->elemtype
             ushort-arrayp))

  (defruled value-array->elemtype-when-sshort-arrayp
    (implies (sshort-arrayp x)
             (equal (value-array->elemtype x)
                    (type-sshort)))
    :enable (value-array->elemtype
             sshort-arrayp))

  (defruled value-array->elemtype-when-uint-arrayp
    (implies (uint-arrayp x)
             (equal (value-array->elemtype x)
                    (type-uint)))
    :enable (value-array->elemtype
             uint-arrayp))

  (defruled value-array->elemtype-when-sint-arrayp
    (implies (sint-arrayp x)
             (equal (value-array->elemtype x)
                    (type-sint)))
    :enable (value-array->elemtype
             sint-arrayp))

  (defruled value-array->elemtype-when-ulong-arrayp
    (implies (ulong-arrayp x)
             (equal (value-array->elemtype x)
                    (type-ulong)))
    :enable (value-array->elemtype
             ulong-arrayp))

  (defruled value-array->elemtype-when-slong-arrayp
    (implies (slong-arrayp x)
             (equal (value-array->elemtype x)
                    (type-slong)))
    :enable (value-array->elemtype
             slong-arrayp))

  (defruled value-array->elemtype-when-ullong-arrayp
    (implies (ullong-arrayp x)
             (equal (value-array->elemtype x)
                    (type-ullong)))
    :enable (value-array->elemtype
             ullong-arrayp))

  (defruled value-array->elemtype-when-sllong-arrayp
    (implies (sllong-arrayp x)
             (equal (value-array->elemtype x)
                    (type-sllong)))
    :enable (value-array->elemtype
             sllong-arrayp))

  (defval *atc-value-array->elemtype-rules*
    '(value-array->elemtype-when-uchar-arrayp
      value-array->elemtype-when-schar-arrayp
      value-array->elemtype-when-ushort-arrayp
      value-array->elemtype-when-sshort-arrayp
      value-array->elemtype-when-uint-arrayp
      value-array->elemtype-when-sint-arrayp
      value-array->elemtype-when-ulong-arrayp
      value-array->elemtype-when-slong-arrayp
      value-array->elemtype-when-ullong-arrayp
      value-array->elemtype-when-sllong-arrayp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-array-length-rules
  :short "Rules for array length operations."
  :long
  (xdoc::topstring
   (xdoc::p
    "These are not operations in C, as we know,
     but we have functions in our C semantics for array length.
     We introduce rules to turn @(tsee value-array->length)
     into more specific array length functions like @(tsee uchar-array-length).
     We also add existing (i.e. proved elsewhere) rules
     about @(tsee uchar-array-length) and the others being @(tsee natp)."))

  (defruled array-length-when-uchar-array-length
    (implies (uchar-arrayp x)
             (equal (value-array->length x)
                    (uchar-array-length x)))
    :enable (value-array->length
             uchar-array-length
             uchar-array->elements
             value-array->elements))

  (defruled array-length-when-schar-array-length
    (implies (schar-arrayp x)
             (equal (value-array->length x)
                    (schar-array-length x)))
    :enable (value-array->length
             schar-array-length
             schar-array->elements
             value-array->elements))

  (defruled array-length-when-ushort-array-length
    (implies (ushort-arrayp x)
             (equal (value-array->length x)
                    (ushort-array-length x)))
    :enable (value-array->length
             ushort-array-length
             ushort-array->elements
             value-array->elements))

  (defruled array-length-when-sshort-array-length
    (implies (sshort-arrayp x)
             (equal (value-array->length x)
                    (sshort-array-length x)))
    :enable (value-array->length
             sshort-array-length
             sshort-array->elements
             value-array->elements))

  (defruled array-length-when-uint-array-length
    (implies (uint-arrayp x)
             (equal (value-array->length x)
                    (uint-array-length x)))
    :enable (value-array->length
             uint-array-length
             uint-array->elements
             value-array->elements))

  (defruled array-length-when-sint-array-length
    (implies (sint-arrayp x)
             (equal (value-array->length x)
                    (sint-array-length x)))
    :enable (value-array->length
             sint-array-length
             sint-array->elements
             value-array->elements))

  (defruled array-length-when-ulong-array-length
    (implies (ulong-arrayp x)
             (equal (value-array->length x)
                    (ulong-array-length x)))
    :enable (value-array->length
             ulong-array-length
             ulong-array->elements
             value-array->elements))

  (defruled array-length-when-slong-array-length
    (implies (slong-arrayp x)
             (equal (value-array->length x)
                    (slong-array-length x)))
    :enable (value-array->length
             slong-array-length
             slong-array->elements
             value-array->elements))

  (defruled array-length-when-ullong-array-length
    (implies (ullong-arrayp x)
             (equal (value-array->length x)
                    (ullong-array-length x)))
    :enable (value-array->length
             ullong-array-length
             ullong-array->elements
             value-array->elements))

  (defruled array-length-when-sllong-array-length
    (implies (sllong-arrayp x)
             (equal (value-array->length x)
                    (sllong-array-length x)))
    :enable (value-array->length
             sllong-array-length
             sllong-array->elements
             value-array->elements))

  (defval *atc-array-length-rules*
    '(array-length-when-uchar-array-length
      array-length-when-schar-array-length
      array-length-when-ushort-array-length
      array-length-when-sshort-array-length
      array-length-when-uint-array-length
      array-length-when-sint-array-length
      array-length-when-ulong-array-length
      array-length-when-slong-array-length
      array-length-when-ullong-array-length
      array-length-when-sllong-array-length
      natp-of-uchar-array-length
      natp-of-schar-array-length
      natp-of-ushort-array-length
      natp-of-sshort-array-length
      natp-of-uint-array-length
      natp-of-sint-array-length
      natp-of-ulong-array-length
      natp-of-slong-array-length
      natp-of-ullong-array-length
      natp-of-sllong-array-length)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-array-length-write-rules
  :short "Rules for array lengths and array write operations."
  :long
  (xdoc::topstring
   (xdoc::p
    "These rules say that the array write operations preserve array lengths.
     There is one rule for each @('<type1>-array-write-<type2>') function,
     so generate the list programmatically."))

  (define atc-array-length-write-rules-loop-itypes ((atype typep)
                                                    (itypes type-listp))
    :guard (and (type-integerp atype)
                (type-integer-listp itypes))
    :returns (names symbol-listp)
    :parents nil
    (cond ((endp itypes) nil)
          (t (b* ((afixtype (integer-type-to-fixtype atype))
                  (ifixtype (integer-type-to-fixtype (car itypes))))
               (cons
                (pack afixtype
                      '-array-length-of-
                      afixtype
                      '-array-write-
                      ifixtype)
                (atc-array-length-write-rules-loop-itypes atype
                                                          (cdr itypes)))))))

  (define atc-array-length-write-rules-loop-atypes ((atypes type-listp)
                                                    (itypes type-listp))
    :guard (and (type-integer-listp atypes)
                (type-integer-listp itypes))
    :returns (name symbol-listp)
    :parents nil
    (cond ((endp atypes) nil)
          (t (append (atc-array-length-write-rules-loop-itypes (car atypes)
                                                               itypes)
                     (atc-array-length-write-rules-loop-atypes (cdr atypes)
                                                               itypes)))))

  (defval *atc-array-length-write-rules*
    (atc-array-length-write-rules-loop-atypes *integer-nonbool-nonchar-types*
                                              *integer-nonbool-nonchar-types*)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-ident-rules
  :short "Rules for executing identifiers."
  :long
  (xdoc::topstring
   (xdoc::p
    "To symbolically execute an identifier (as an expression),
     we use a rule that is like the definition,
     but provides a bit of separation/abstraction from the definition,
     and it also avoids the binding of @('__function__').
     The @(tsee read-var) call may undergo further rewriting,
     as explained in @(see atc-read-var-rules)."))

  (defruled exec-ident-open
    (equal (exec-ident id compst)
           (read-var id compst))
    :enable exec-ident)

  (defval *atc-exec-ident-rules*
    '(exec-ident-open)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-const-rules
  :short "Rules for executing constants."
  :long
  (xdoc::topstring
   (xdoc::p
    "To symbolically execute a constant,
     which in our current C subset may only be an integer constant,
     we use rules corresponding to the possible integer types of the constant.
     The rules are openers for @(tsee exec-const),
     under suitable conditions.
     The argument of @(tsee exec-const) is a quoted constant
     during symbolic execution,
     because it is taken from the ASTs being executed;
     thus, we enable the executable counterparts
     of the fixtype functions that operate on constants
     and of the @('<type>-integerp') predicates."))

  (defruled exec-const-to-sint
    (implies (and (syntaxp (quotep const))
                  (const-case const :int)
                  (equal iconst (const-int->get const))
                  (not (iconst->unsignedp iconst))
                  (iconst-length-case (iconst->length iconst) :none)
                  (equal value (iconst->value iconst))
                  (sint-integerp value))
             (equal (exec-const const)
                    (sint value)))
    :enable (exec-const
             exec-iconst))

  (defruled exec-const-to-slong
    (implies (and (syntaxp (quotep const))
                  (const-case const :int)
                  (equal iconst (const-int->get const))
                  (not (iconst->unsignedp iconst))
                  (equal value (iconst->value iconst))
                  (slong-integerp value)
                  (equal length (iconst->length iconst))
                  (equal base (iconst->base iconst))
                  (or (and (iconst-length-case length :none)
                           (not (sint-integerp value))
                           (or (iconst-base-case base :dec)
                               (not (uint-integerp value))))
                      (iconst-length-case length :long)))
             (equal (exec-const const)
                    (slong value)))
    :enable (exec-const
             exec-iconst))

  (defruled exec-const-to-sllong
    (implies (and (syntaxp (quotep const))
                  (const-case const :int)
                  (equal iconst (const-int->get const))
                  (not (iconst->unsignedp iconst))
                  (equal value (iconst->value iconst))
                  (sllong-integerp value)
                  (equal length (iconst->length iconst))
                  (equal base (iconst->base iconst))
                  (or (and (iconst-length-case length :none)
                           (not (slong-integerp value))
                           (or (iconst-base-case base :dec)
                               (not (ulong-integerp value))))
                      (and (iconst-length-case length :long)
                           (not (slong-integerp value))
                           (or (iconst-base-case base :dec)
                               (not (ulong-integerp value))))
                      (iconst-length-case length :llong)))
             (equal (exec-const const)
                    (sllong value)))
    :enable (exec-const
             exec-iconst
             slong-integerp-alt-def
             sint-integerp-alt-def
             ulong-integerp-alt-def
             uint-integerp-alt-def))

  (defruled exec-const-to-uint
    (implies (and (syntaxp (quotep const))
                  (const-case const :int)
                  (equal iconst (const-int->get const))
                  (iconst-length-case (iconst->length iconst) :none)
                  (equal value (iconst->value iconst))
                  (uint-integerp value)
                  (or (iconst->unsignedp iconst)
                      (and (not (iconst-base-case (iconst->base iconst) :dec))
                           (not (sint-integerp value)))))
             (equal (exec-const const)
                    (uint value)))
    :enable (exec-const
             exec-iconst))

  (defruled exec-const-to-ulong
    (implies (and (syntaxp (quotep const))
                  (const-case const :int)
                  (equal iconst (const-int->get const))
                  (equal value (iconst->value iconst))
                  (ulong-integerp value)
                  (equal length (iconst->length iconst))
                  (equal base (iconst->base iconst))
                  (or (and (iconst->unsignedp iconst)
                           (or (and (iconst-length-case length :none)
                                    (not (uint-integerp value)))
                               (iconst-length-case length :long)))
                      (and (not (iconst-base-case base :dec))
                           (not (slong-integerp value))
                           (or (and (iconst-length-case length :none)
                                    (not (uint-integerp value)))
                               (iconst-length-case length :long)))))
             (equal (exec-const const)
                    (ulong value)))
    :enable (exec-const
             exec-iconst
             sint-integerp-alt-def
             slong-integerp-alt-def))

  (defruled exec-const-to-ullong
    (implies (and (syntaxp (quotep const))
                  (const-case const :int)
                  (equal iconst (const-int->get const))
                  (equal value (iconst->value iconst))
                  (ullong-integerp value)
                  (equal length (iconst->length iconst))
                  (equal base (iconst->base iconst))
                  (or (and (iconst->unsignedp iconst)
                           (or (iconst-length-case length :llong)
                               (not (ulong-integerp value))))
                      (and (not (iconst-base-case base :dec))
                           (not (sllong-integerp value))
                           (or (iconst-length-case length :llong)
                               (not (ulong-integerp value))))))
             (equal (exec-const const)
                    (ullong value)))
    :enable (exec-const
             exec-iconst
             sint-integerp-alt-def
             slong-integerp-alt-def
             sllong-integerp-alt-def
             uint-integerp-alt-def
             ulong-integerp-alt-def))

  (defval *atc-exec-const-rules*
    '(exec-const-to-sint
      exec-const-to-uint
      exec-const-to-slong
      exec-const-to-ulong
      exec-const-to-sllong
      exec-const-to-ullong
      (:e const-kind)
      (:e const-int->get)
      (:e iconst->base)
      (:e iconst->length)
      (:e iconst->unsignedp)
      (:e iconst->value)
      (:e iconst-length-kind)
      (:e iconst-base-kind)
      (:e sint-integerp)
      (:e uint-integerp)
      (:e slong-integerp)
      (:e ulong-integerp)
      (:e sllong-integerp)
      (:e ullong-integerp))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-integer-value-rules
  :short "Rules about the composition of @(tsee sint-integer-value)
          with @('sint-from-<type>') functions."
  :long
  (xdoc::topstring
   (xdoc::p
    "These are not used during the symbolic execution;
     they are used to prove rules used during the symbolic execution."))

  (defruled sint-integer-value-of-sint-from-schar
    (implies (scharp x)
             (equal (sint-integer-value (sint-from-schar x))
                    (schar-integer-value x)))
    :enable (sint-integer-value
             schar-integer-value
             sint-from-schar
             sint-integerp-alt-def))

  (defruled sint-integer-value-of-sint-from-uchar
    (implies (ucharp x)
             (equal (sint-integer-value (sint-from-uchar x))
                    (uchar-integer-value x)))
    :enable (sint-integer-value
             uchar-integer-value
             sint-from-uchar
             sint-integerp-alt-def))

  (defruled sint-integer-value-of-sint-from-sshort
    (implies (sshortp x)
             (equal (sint-integer-value (sint-from-sshort x))
                    (sshort-integer-value x)))
    :enable (sint-integer-value
             sshort-integer-value
             sint-from-sshort
             sint-integerp-alt-def))

  (defruled sint-integer-value-of-sint-from-ushort
    (implies (ushortp x)
             (equal (sint-integer-value (sint-from-ushort x))
                    (ushort-integer-value x)))
    :enable (sint-integer-value
             ushort-integer-value
             sint-from-ushort
             sint-integerp-alt-def))

  (defval *atc-integer-value-rules*
    '(sint-integer-value-of-sint-from-schar
      sint-integer-value-of-sint-from-uchar
      sint-integer-value-of-sint-from-sshort
      sint-integer-value-of-sint-from-ushort)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-integer-conv-rules
  :short "Rules about the composition of integer conversions."
  :long
  (xdoc::topstring
   (xdoc::p
    "These are not used during the symbolic execution;
     they are used to prove rules used during the symbolic execution."))

  ;; unsigned int as final type:

  (defruled uint-from-sint-of-sint-from-schar
    (equal (uint-from-sint (sint-from-schar x))
           (uint-from-schar x))
    :enable (uint-from-sint
             sint-from-schar
             uint-from-schar
             sint-integerp-alt-def))

  (defruled uint-from-sint-of-sint-from-uchar
    (equal (uint-from-sint (sint-from-uchar x))
           (uint-from-uchar x))
    :enable (uint-from-sint
             sint-from-uchar
             uint-from-uchar
             sint-integerp-alt-def))

  (defruled uint-from-sint-of-sint-from-sshort
    (equal (uint-from-sint (sint-from-sshort x))
           (uint-from-sshort x))
    :enable (uint-from-sint
             sint-from-sshort
             uint-from-sshort
             sint-integerp-alt-def))

  (defruled uint-from-sint-of-sint-from-ushort
    (equal (uint-from-sint (sint-from-ushort x))
           (uint-from-ushort x))
    :enable (uint-from-sint
             sint-from-ushort
             uint-from-ushort
             sint-integerp-alt-def))

  ;; signed long as final type:

  (defruled slong-from-sint-of-sint-from-schar
    (equal (slong-from-sint (sint-from-schar x))
           (slong-from-schar x))
    :enable (slong-from-sint
             sint-from-schar
             slong-from-schar
             sint-integerp-alt-def))

  (defruled slong-from-sint-of-sint-from-uchar
    (equal (slong-from-sint (sint-from-uchar x))
           (slong-from-uchar x))
    :enable (slong-from-sint
             sint-from-uchar
             slong-from-uchar
             sint-integerp-alt-def))

  (defruled slong-from-sint-of-sint-from-sshort
    (equal (slong-from-sint (sint-from-sshort x))
           (slong-from-sshort x))
    :enable (slong-from-sint
             sint-from-sshort
             slong-from-sshort
             sint-integerp-alt-def))

  (defruled slong-from-sint-of-sint-from-ushort
    (equal (slong-from-sint (sint-from-ushort x))
           (slong-from-ushort x))
    :enable (slong-from-sint
             sint-from-ushort
             slong-from-ushort
             sint-integerp-alt-def))

  ;; unsigned long as final type:

  (defruled ulong-from-sint-of-sint-from-schar
    (equal (ulong-from-sint (sint-from-schar x))
           (ulong-from-schar x))
    :enable (ulong-from-sint
             sint-from-schar
             ulong-from-schar
             sint-integerp-alt-def))

  (defruled ulong-from-sint-of-sint-from-uchar
    (equal (ulong-from-sint (sint-from-uchar x))
           (ulong-from-uchar x))
    :enable (ulong-from-sint
             sint-from-uchar
             ulong-from-uchar
             sint-integerp-alt-def))

  (defruled ulong-from-sint-of-sint-from-sshort
    (equal (ulong-from-sint (sint-from-sshort x))
           (ulong-from-sshort x))
    :enable (ulong-from-sint
             sint-from-sshort
             ulong-from-sshort
             sint-integerp-alt-def))

  (defruled ulong-from-sint-of-sint-from-ushort
    (equal (ulong-from-sint (sint-from-ushort x))
           (ulong-from-ushort x))
    :enable (ulong-from-sint
             sint-from-ushort
             ulong-from-ushort
             sint-integerp-alt-def))

  ;; signed long long as final type:

  (defruled sllong-from-sint-of-sint-from-schar
    (equal (sllong-from-sint (sint-from-schar x))
           (sllong-from-schar x))
    :enable (sllong-from-sint
             sint-from-schar
             sllong-from-schar
             sint-integerp-alt-def))

  (defruled sllong-from-sint-of-sint-from-uchar
    (equal (sllong-from-sint (sint-from-uchar x))
           (sllong-from-uchar x))
    :enable (sllong-from-sint
             sint-from-uchar
             sllong-from-uchar
             sint-integerp-alt-def))

  (defruled sllong-from-sint-of-sint-from-sshort
    (equal (sllong-from-sint (sint-from-sshort x))
           (sllong-from-sshort x))
    :enable (sllong-from-sint
             sint-from-sshort
             sllong-from-sshort
             sint-integerp-alt-def))

  (defruled sllong-from-sint-of-sint-from-ushort
    (equal (sllong-from-sint (sint-from-ushort x))
           (sllong-from-ushort x))
    :enable (sllong-from-sint
             sint-from-ushort
             sllong-from-ushort
             sint-integerp-alt-def))

  ;; unsigned long long as final type:

  (defruled ullong-from-sint-of-sint-from-schar
    (equal (ullong-from-sint (sint-from-schar x))
           (ullong-from-schar x))
    :enable (ullong-from-sint
             sint-from-schar
             ullong-from-schar
             sint-integerp-alt-def))

  (defruled ullong-from-sint-of-sint-from-uchar
    (equal (ullong-from-sint (sint-from-uchar x))
           (ullong-from-uchar x))
    :enable (ullong-from-sint
             sint-from-uchar
             ullong-from-uchar
             sint-integerp-alt-def))

  (defruled ullong-from-sint-of-sint-from-sshort
    (equal (ullong-from-sint (sint-from-sshort x))
           (ullong-from-sshort x))
    :enable (ullong-from-sint
             sint-from-sshort
             ullong-from-sshort
             sint-integerp-alt-def))

  (defruled ullong-from-sint-of-sint-from-ushort
    (equal (ullong-from-sint (sint-from-ushort x))
           (ullong-from-ushort x))
    :enable (ullong-from-sint
             sint-from-ushort
             ullong-from-ushort
             sint-integerp-alt-def))

  (defval *atc-integer-conv-rules*
    '(uint-from-sint-of-sint-from-schar
      uint-from-sint-of-sint-from-uchar
      uint-from-sint-of-sint-from-sshort
      uint-from-sint-of-sint-from-ushort
      slong-from-sint-of-sint-from-schar
      slong-from-sint-of-sint-from-uchar
      slong-from-sint-of-sint-from-sshort
      slong-from-sint-of-sint-from-ushort
      ulong-from-sint-of-sint-from-schar
      ulong-from-sint-of-sint-from-uchar
      ulong-from-sint-of-sint-from-sshort
      ulong-from-sint-of-sint-from-ushort
      sllong-from-sint-of-sint-from-schar
      sllong-from-sint-of-sint-from-uchar
      sllong-from-sint-of-sint-from-sshort
      sllong-from-sint-of-sint-from-ushort
      ullong-from-sint-of-sint-from-schar
      ullong-from-sint-of-sint-from-uchar
      ullong-from-sint-of-sint-from-sshort
      ullong-from-sint-of-sint-from-ushort)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-promote-value-rules
  :short "Rules about @(tsee promote-value) on values of given types."
  :long
  (xdoc::topstring
   (xdoc::p
    "These are not used during the symbolic execution;
     they are used to prove rules used during the symbolic execution."))

  (defruled promote-value-when-scharp
    (implies (scharp x)
             (equal (promote-value x)
                    (sint-from-schar x)))
    :enable promote-value)

  (defruled promote-value-when-ucharp
    (implies (ucharp x)
             (equal (promote-value x)
                    (if (<= (uchar-max) (sint-max))
                        (sint-from-uchar x)
                      (uint-from-uchar x))))
    :enable promote-value)

  (defruled promote-value-when-sshortp
    (implies (sshortp x)
             (equal (promote-value x)
                    (sint-from-sshort x)))
    :enable promote-value)

  (defruled promote-value-when-ushortp
    (implies (ushortp x)
             (equal (promote-value x)
                    (if (<= (ushort-max) (sint-max))
                        (sint-from-ushort x)
                      (uint-from-ushort x))))
    :enable promote-value)

  (defruled promote-value-when-sintp
    (implies (sintp x)
             (equal (promote-value x)
                    x))
    :enable promote-value)

  (defruled promote-value-when-uintp
    (implies (uintp x)
             (equal (promote-value x)
                    x))
    :enable promote-value)

  (defruled promote-value-when-slongp
    (implies (slongp x)
             (equal (promote-value x)
                    x))
    :enable promote-value)

  (defruled promote-value-when-ulongp
    (implies (ulongp x)
             (equal (promote-value x)
                    x))
    :enable promote-value)

  (defruled promote-value-when-sllongp
    (implies (sllongp x)
             (equal (promote-value x)
                    x))
    :enable promote-value)

  (defruled promote-value-when-ullongp
    (implies (ullongp x)
             (equal (promote-value x)
                    x))
    :enable promote-value)

  (defval *atc-promote-value-rules*
    '(promote-value-when-scharp
      promote-value-when-ucharp
      promote-value-when-sshortp
      promote-value-when-ushortp
      promote-value-when-sintp
      promote-value-when-uintp
      promote-value-when-slongp
      promote-value-when-ulongp
      promote-value-when-sllongp
      promote-value-when-ullongp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-uaconvert-rules-generation
  :short "Code to generate the rules for @(tsee uaconvert-values)."

  (define atc-uaconvert-values-rules-gen ((ltype typep) (rtype typep))
    :guard (and (type-integerp ltype)
                (type-integerp rtype))
    :returns (mv (name symbolp)
                 (event pseudo-event-formp))
    :parents nil
    (b* ((lfixtype (integer-type-to-fixtype ltype))
         (rfixtype (integer-type-to-fixtype rtype))
         (lpred (pack lfixtype 'p))
         (rpred (pack rfixtype 'p))
         (type (uaconvert-types ltype rtype))
         (fixtype (integer-type-to-fixtype type))
         (lterm (if (equal type ltype)
                    'x
                  `(,(pack fixtype '-from- lfixtype) x)))
         (rterm (if (equal type rtype)
                    'y
                  `(,(pack fixtype '-from- rfixtype) y)))
         (name (pack 'uaconvert-values-when- lpred '-and- rpred))
         (event `(defruled ,name
                   (implies (and (,lpred x)
                                 (,rpred y))
                            (equal (uaconvert-values x y)
                                   (mv ,lterm ,rterm)))
                   :enable (uaconvert-values
                            ,@*atc-promote-value-rules*
                            ,@*atc-integer-conv-rules*))))
      (mv name event))
    :guard-hints (("Goal" :in-theory (enable type-arithmeticp type-realp))))

  (define atc-uaconvert-values-rules-gen-loop-rtypes ((ltype typep)
                                                      (rtypes type-listp))
    :guard (and (type-integerp ltype)
                (type-integer-listp rtypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp rtypes)) (mv nil nil))
         ((mv name event) (atc-uaconvert-values-rules-gen ltype (car rtypes)))
         ((mv names events)
          (atc-uaconvert-values-rules-gen-loop-rtypes ltype (cdr rtypes))))
      (mv (cons name names) (cons event events))))

  (define atc-uaconvert-values-rules-gen-loop-ltypes ((ltypes type-listp)
                                                      (rtypes type-listp))
    :guard (and (type-integer-listp ltypes)
                (type-integer-listp rtypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp ltypes)) (mv nil nil))
         ((mv names events)
          (atc-uaconvert-values-rules-gen-loop-rtypes (car ltypes) rtypes))
         ((mv names1 events1)
          (atc-uaconvert-values-rules-gen-loop-ltypes (cdr ltypes) rtypes)))
      (mv (append names names1) (append events events1))))

  (define atc-uaconvert-values-rules-gen-all ()
    :returns (event pseudo-event-formp)
    :parents nil
    (b* (((mv names events)
          (atc-uaconvert-values-rules-gen-loop-ltypes
           *integer-nonbool-nonchar-types*
           *integer-nonbool-nonchar-types*)))
      `(progn
         (defsection atc-uaconvert-values-rules
           :short "Rules about @(tsee uaconvert-values)
                   on values of given types."
           :long
           (xdoc::topstring
            (xdoc::p
             "These are not used during the symbolic execution;
              they are used to prove rules
              used during the symbolic execution."))
           ,@events
           (defval *atc-uaconvert-values-rules*
             '(,@names)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(make-event (atc-uaconvert-values-rules-gen-all))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-arrsub-rules-generation
  :short "Code to generate the rules for executing array subscript expressions."

  (define atc-exec-arrsub-rules-gen ((atype typep) (itype typep))
    :guard (and (type-integerp atype)
                (type-integerp itype))
    :returns (mv (name symbolp)
                 (event pseudo-event-formp))
    :parents nil
    (b* ((afixtype (integer-type-to-fixtype atype))
         (ifixtype (integer-type-to-fixtype itype))
         (apred (pack afixtype '-arrayp))
         (ipred (pack ifixtype 'p))
         (atype-array-itype-index-okp
          (pack afixtype '-array- ifixtype '-index-okp))
         (atype-array-index-okp
          (pack afixtype '-array-index-okp))
         (atype-array-read-itype
          (pack afixtype '-array-read- ifixtype))
         (atype-array-read
          (pack afixtype '-array-read))
         (atype-array-read-alt-def
          (pack atype-array-read '-alt-def))
         (elemtype-when-apred
          (pack 'value-array->elemtype-when- apred))
         (name (pack 'exec-arrsub-when- apred '-and- ipred))
         (formula `(implies
                    (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                         ,(atc-syntaxp-hyp-for-expr-pure 'y)
                         (valuep x)
                         (value-case x :pointer)
                         (not (value-pointer-nullp x))
                         (equal (value-pointer->reftype x)
                                ,(type-to-maker atype))
                         (equal array
                                (read-object (value-pointer->designator x)
                                             compst))
                         (,apred array)
                         (,ipred y)
                         (,atype-array-itype-index-okp array y))
                    (equal (exec-arrsub x y compst)
                           (,atype-array-read-itype array y))))
         (event `(defruled ,name
                   ,formula
                   :enable (exec-arrsub
                            exec-integer
                            ,atype-array-itype-index-okp
                            ,atype-array-read-itype
                            ,atype-array-read-alt-def
                            ,elemtype-when-apred)
                   :prep-lemmas
                   ((defrule lemma
                      (implies (and (,atype-array-index-okp array index)
                                    (integerp index))
                               (not (< index 0)))
                      :enable ,atype-array-index-okp)))))
      (mv name event)))

  (define atc-exec-arrsub-rules-gen-loop-itypes ((atype typep)
                                                 (itypes type-listp))
    :guard (and (type-integerp atype)
                (type-integer-listp itypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp itypes)) (mv nil nil))
         ((mv name event) (atc-exec-arrsub-rules-gen atype (car itypes)))
         ((mv names events)
          (atc-exec-arrsub-rules-gen-loop-itypes atype (cdr itypes))))
      (mv (cons name names) (cons event events))))

  (define atc-exec-arrsub-rules-gen-loop-atypes ((atypes type-listp)
                                                 (itypes type-listp))
    :guard (and (type-integer-listp atypes)
                (type-integer-listp itypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp atypes)) (mv nil nil))
         ((mv names events)
          (atc-exec-arrsub-rules-gen-loop-itypes (car atypes) itypes))
         ((mv more-names more-events)
          (atc-exec-arrsub-rules-gen-loop-atypes (cdr atypes) itypes)))
      (mv (append names more-names) (append events more-events))))

  (define atc-exec-arrsub-rules-gen-all ()
    :returns (event pseudo-event-formp)
    :parents nil
    (b* (((mv names events)
          (atc-exec-arrsub-rules-gen-loop-atypes
           *integer-nonbool-nonchar-types*
           *integer-nonbool-nonchar-types*)))
      `(progn
         (defsection atc-exec-arrsub-rules
           :short "Rules for executing array subscript expressions."
           ,@events
           (defval *atc-exec-arrsub-rules*
             '(,@names)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(make-event (atc-exec-arrsub-rules-gen-all))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-unary-rules-generation
  :short "Code to generate the rules for executing unary operations."

  (define atc-exec-unary-rules-gen ((op unopp) (type typep))
    :guard (type-integerp type)
    :returns (mv (name symbolp)
                 (event pseudo-event-formp))
    :parents nil
    (b* ((fixtype (integer-type-to-fixtype type))
         (pred (pack fixtype 'p))
         (op-kind (unop-kind op))
         (exec-op (pack 'exec- op-kind))
         (name (pack exec-op '-when- pred))
         (op-type (pack op-kind '- fixtype))
         (op-type-okp (and (unop-case op :minus)
                           (member-eq (type-kind type)
                                      '(:schar :sshort :sint :slong :sllong
                                        :uchar :ushort))
                           (pack op-type '-okp)))
         (hyps `(and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                     (equal op (,(pack 'unop- op-kind)))
                     (,pred x)
                     ,@(and op-type-okp
                            `((,op-type-okp x)))))
         (formula `(implies ,hyps
                            (equal (exec-unary op x)
                                   (,op-type x))))
         (event `(defruled ,name
                   ,formula
                   :enable (exec-unary
                            ,exec-op
                            ,@(and (member-eq op-kind
                                              '(:plus :minus :bitnot))
                                   (member-eq (type-kind type)
                                              '(:schar :uchar :sshort :ushort))
                                   (list op-type))
                            ,@*atc-promote-value-rules*
                            ,@(and op-type-okp
                                   (member-equal op
                                                 (list (unop-plus)
                                                       (unop-minus)
                                                       (unop-bitnot)))
                                   (member-eq (type-kind type)
                                              '(:schar :uchar :sshort :ushort))
                                   (list op-type-okp))))))
      (mv name event)))

  (define atc-exec-unary-rules-gen-loop-types ((op unopp) (types type-listp))
    :guard (type-integer-listp types)
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp types)) (mv nil nil))
         ((mv name event) (atc-exec-unary-rules-gen op (car types)))
         ((mv names events) (atc-exec-unary-rules-gen-loop-types op (cdr types))))
      (mv (cons name names) (cons event events))))

  (define atc-exec-unary-rules-gen-loop-ops ((ops unop-listp) (types type-listp))
    :guard (type-integer-listp types)
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp ops)) (mv nil nil))
         ((mv names events) (atc-exec-unary-rules-gen-loop-types (car ops) types))
         ((mv more-names more-events)
          (atc-exec-unary-rules-gen-loop-ops (cdr ops) types)))
      (mv (append names more-names) (append events more-events))))

  (define atc-exec-unary-rules-gen-all ()
    :returns (event pseudo-event-formp)
    :parents nil
    (b* ((ops (list (unop-plus)
                    (unop-minus)
                    (unop-bitnot)
                    (unop-lognot)))
         ((mv names events)
          (atc-exec-unary-rules-gen-loop-ops ops
                                             *integer-nonbool-nonchar-types*)))
      `(progn
         (defsection atc-exec-unary-rules
           :short "Rules for executing unary operations"
           ,@events
           (defval *atc-exec-unary-rules*
             '(,@names
               (:e unop-plus)
               (:e unop-minus)
               (:e unop-bitnot)
               (:e unop-lognot))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(make-event (atc-exec-unary-rules-gen-all))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-cast-rules-generation
  :short "Code to generate the rules for executing cast operations."

  (define atc-exec-cast-rules-gen ((dtype typep) (stype typep))
    :guard (and (type-integerp dtype)
                (type-integerp stype))
    :returns (mv (name symbolp) (event pseudo-event-formp))
    :parents nil
    (b* ((dfixtype (integer-type-to-fixtype dtype))
         (sfixtype (integer-type-to-fixtype stype))
         (spred (pack sfixtype 'p))
         (name (pack 'exec-cast-of- dfixtype '-when- spred))
         (dtyname (type-to-tyname dtype))
         (dtype-from-stype (pack dfixtype '-from- sfixtype))
         (dtype-from-stype-okp (pack dtype-from-stype '-okp))
         (hyps `(and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                     (,spred x)
                     ,@(and (not (equal dtype stype))
                            (or (type-case dtype :schar)
                                (and (type-case dtype :sshort)
                                     (not (member-eq (type-kind stype)
                                                     '(:schar))))
                                (and (type-case dtype :sint)
                                     (not (member-eq (type-kind stype)
                                                     '(:schar :sshort))))
                                (and (type-case dtype :slong)
                                     (not (member-eq (type-kind stype)
                                                     '(:schar :sshort :sint))))
                                (and (type-case dtype :sllong)
                                     (not (member-eq (type-kind stype)
                                                     '(:schar :sshort
                                                       :sint :slong)))))
                            `((,dtype-from-stype-okp x)))))
         (rhs (if (equal dtype stype)
                  'x
                `(,dtype-from-stype x)))
         (formula `(implies ,hyps
                            (equal (exec-cast ',dtyname x)
                                   ,rhs)))
         (event `(defruled ,name
                   ,formula
                   :enable (exec-cast))))
      (mv name event)))

  (define atc-exec-cast-rules-gen-loop-stypes ((dtype typep)
                                               (stypes type-listp))
    :guard (and (type-integerp dtype)
                (type-integer-listp stypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp stypes)) (mv nil nil))
         ((mv name event) (atc-exec-cast-rules-gen dtype
                                                   (car stypes)))
         ((mv names events) (atc-exec-cast-rules-gen-loop-stypes dtype
                                                                 (cdr stypes))))
      (mv (cons name names) (cons event events))))

  (define atc-exec-cast-rules-gen-loop-dtypes ((dtypes type-listp)
                                               (stypes type-listp))
    :guard (and (type-integer-listp dtypes)
                (type-integer-listp stypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp dtypes)) (mv nil nil))
         ((mv names events) (atc-exec-cast-rules-gen-loop-stypes (car dtypes)
                                                                 stypes))
         ((mv names1 events1) (atc-exec-cast-rules-gen-loop-dtypes (cdr dtypes)
                                                                   stypes)))
      (mv (append names names1) (append events events1))))

  (define atc-exec-cast-rules-gen-all ()
    :returns (event pseudo-event-formp)
    :parents nil
    (b* (((mv names events)
          (atc-exec-cast-rules-gen-loop-dtypes
           *integer-nonbool-nonchar-types*
           *integer-nonbool-nonchar-types*)))
      `(progn
         (defsection atc-exec-cast-rules
           :short "Rules for executing casts."
           ,@events
           (defval *atc-exec-cast-rules*
             '(,@names)))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(make-event (atc-exec-cast-rules-gen-all))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-binary-strict-pure-rules-generation
  :short "Code to generate the rules for executing
          strict pure binary operations."

  (define atc-exec-binary-rules-gen-op-ltype-rtype ((op binopp)
                                                    (ltype typep)
                                                    (rtype typep))
    :guard (and (type-integerp ltype)
                (type-integerp rtype))
    :returns (mv (name symbolp) (event pseudo-event-formp))
    :parents nil
    (b* ((lfixtype (integer-type-to-fixtype ltype))
         (rfixtype (integer-type-to-fixtype rtype))
         (rpred (pack rfixtype 'p))
         (op-kind (binop-kind op))
         (exec-op (pack 'exec- op-kind))
         (exec-binary-strict-pure-of-op-and-ltype
          (pack 'exec-binary-strict-pure-of- op-kind '-and- lfixtype))
         (type (uaconvert-types ltype rtype))
         (name (pack exec-binary-strict-pure-of-op-and-ltype '-when- rfixtype))
         (op-ltype-rtype (pack op-kind '- lfixtype '- rfixtype))
         (op-ltype-rtype-okp (and (or (member-eq op-kind
                                                 '(:div :rem :shl :shr))
                                      (and (member-eq op-kind
                                                      '(:add :sub :mul))
                                           (type-signed-integerp type)))
                                  (pack op-ltype-rtype '-okp)))
         (formula `(implies (and ,(atc-syntaxp-hyp-for-expr-pure 'y)
                                 (,rpred y)
                                 ,@(and op-ltype-rtype-okp
                                        `((,op-ltype-rtype-okp x y))))
                            (equal
                             (,exec-binary-strict-pure-of-op-and-ltype x y)
                             (,op-ltype-rtype x y))))
         (event `(defruled ,name
                   ,formula
                   :enable (,exec-binary-strict-pure-of-op-and-ltype
                            ,exec-op
                            ,@(and (or (not (equal type ltype))
                                       (not (equal type rtype))
                                       (member-eq op-kind '(:shl :shr)))
                                   (list op-ltype-rtype))
                            ,@(and op-ltype-rtype-okp
                                   (or (not (equal type ltype))
                                       (not (equal type rtype))
                                       (member-eq op-kind '(:shl :shr)))
                                   (list op-ltype-rtype-okp))
                            ,@(and (member-eq op-kind '(:shl :shr))
                                   (not (equal ltype (promote-type ltype)))
                                   (list
                                    (pack op-kind '- lfixtype)
                                    (pack op-kind '- lfixtype '-okp)))
                            ,@(and (member-eq op-kind '(:shl :shr))
                                   (cons 'exec-integer
                                         *atc-integer-value-rules*))
                            ,@*atc-uaconvert-values-rules*
                            ,@*atc-promote-value-rules*))))
      (mv name event))
    :guard-hints (("Goal" :in-theory (enable type-arithmeticp type-realp))))

  (define atc-exec-binary-rules-gen-op-ltype ((op binopp)
                                              (ltype typep)
                                              (rtypes type-listp))
    :guard (and (type-integerp ltype)
                (type-integer-listp rtypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp rtypes)) (mv nil nil))
         ((mv name event)
          (atc-exec-binary-rules-gen-op-ltype-rtype op ltype (car rtypes)))
         ((mv names events)
          (atc-exec-binary-rules-gen-op-ltype op ltype (cdr rtypes))))
      (mv (cons name names) (cons event events))))

  (define atc-exec-binary-rules-gen-op ((op binopp)
                                        (ltypes type-listp)
                                        (rtypes type-listp))
    :guard (and (type-integer-listp ltypes)
                (type-integer-listp rtypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp ltypes)) (mv nil nil))
         (ltype (car ltypes))
         (lfixtype (integer-type-to-fixtype ltype))
         (lpred (pack lfixtype 'p))
         (ltype-fix (pack lfixtype '-fix))
         (op-kind (binop-kind op))
         (exec-op (pack 'exec- op-kind))
         (exec-binary-strict-pure-of-op
          (pack 'exec-binary-strict-pure-of- op-kind))
         (exec-binary-strict-pure-of-op-and-ltype
          (pack 'exec-binary-strict-pure-of- op-kind '-and- lfixtype))
         (exec-binary-strict-pure-of-op-when-ltype
          (pack 'exec-binary-strict-pure-of- op-kind '-when- lfixtype))
         (fun-event
          `(defund ,exec-binary-strict-pure-of-op-and-ltype (x y)
             (b* ((y (value-result-fix y))
                  ((when (errorp y)) y))
               (,exec-op (,ltype-fix x) y))))
         (thm-event
          `(defruled ,exec-binary-strict-pure-of-op-when-ltype
             (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                           (,lpred x))
                      (equal (,exec-binary-strict-pure-of-op x y)
                             (,exec-binary-strict-pure-of-op-and-ltype x y)))
             :enable (,exec-binary-strict-pure-of-op
                      ,exec-binary-strict-pure-of-op-and-ltype)))
         ((mv names events)
          (atc-exec-binary-rules-gen-op-ltype op (car ltypes) rtypes))
         ((mv more-names more-events)
          (atc-exec-binary-rules-gen-op op (cdr ltypes) rtypes)))
      (mv (append (list exec-binary-strict-pure-of-op-when-ltype)
                  names
                  more-names)
          (append (list fun-event thm-event)
                  events
                  more-events))))

  (define atc-exec-binary-rules-gen ((ops binop-listp)
                                     (ltypes type-listp)
                                     (rtypes type-listp))
    :guard (and (type-integer-listp ltypes)
                (type-integer-listp rtypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp ops)) (mv nil nil))
         (op (car ops))
         (op-kind (binop-kind op))
         (exec-op (pack 'exec- op-kind))
         (exec-binary-strict-pure-of-op
          (pack 'exec-binary-strict-pure-of- op-kind))
         (exec-binary-strict-pure-when-op
          (pack 'exec-binary-strict-pure-when- op-kind))
         (fun-event
          `(defund ,exec-binary-strict-pure-of-op (x y)
             (b* ((x (value-result-fix x))
                  (y (value-result-fix y))
                  ((when (errorp x)) x)
                  ((when (errorp y)) y))
               (,exec-op x y))))
         (thm-event
          `(defruled ,exec-binary-strict-pure-when-op
             (implies (and (equal op (,(pack 'binop- op-kind))))
                      (equal (exec-binary-strict-pure op x y)
                             (,exec-binary-strict-pure-of-op x y)))
             :enable (exec-binary-strict-pure
                      ,exec-binary-strict-pure-of-op)))
         ((mv names events)
          (atc-exec-binary-rules-gen-op op ltypes rtypes))
         ((mv more-names more-events)
          (atc-exec-binary-rules-gen (cdr ops) ltypes rtypes)))
      (mv (append (list exec-binary-strict-pure-when-op)
                  names
                  more-names)
          (append (list fun-event thm-event)
                  events
                  more-events))))

  (define atc-exec-binary-rules-gen-all ()
    :returns (event pseudo-event-formp)
    :parents nil
    (b* ((ops (list (binop-mul)
                    (binop-div)
                    (binop-rem)
                    (binop-add)
                    (binop-sub)
                    (binop-shl)
                    (binop-shr)
                    (binop-lt)
                    (binop-gt)
                    (binop-le)
                    (binop-ge)
                    (binop-eq)
                    (binop-ne)
                    (binop-bitand)
                    (binop-bitxor)
                    (binop-bitior)))
         ((mv names events)
          (atc-exec-binary-rules-gen ops
                                     *integer-nonbool-nonchar-types*
                                     *integer-nonbool-nonchar-types*)))
      `(progn
         (defsection atc-exec-binary-strict-pure-rules
           :short "Rules for executing strict pure binary operations."
           :long
           (xdoc::topstring
            (xdoc::p
             "The goal of these rules is to
              rewrite @('(exec-binary-strict-pure op x y)')
              to @('(op-type1-type2 x y)')
              when @('x') has type @('type1'),
              and @('y') has type @('type2').
              We could have a rule for each combination of
              @('op'), @('type1'), and @('type2'),
              but that would lead to 1,600 rules being applicable to
              @('(exec-binary-strict-pure op x y)').
              So we stage the rewriting as follows:")
            (xdoc::ul
             (xdoc::li
              "First, we rewrite @('(exec-binary-strict-pure op x y)')
               to a call @('(exec-binary-strict-pure-of-op x y)'),
               under the hypothesis that @('op') is a specific operator,
               where @('exec-binary-strict-pure-of-op') is one of 16 functions,
               one per binary strict operator.")
             (xdoc::li
              "Next, we rewrite @('(exec-binary-strict-pure-of-op x y)')
               to a call @('(exec-binary-strict-pure-of-op-and-type1 x y)'),
               under the hypothesis that @('x') has type @('type1'),
               where @('exec-binary-strict-pure-of-op-and-type1')
               is one of 10 functions,
               one per supported integer type.")
             (xdoc::li
              "Finally, we rewrite
               @('(exec-binary-strict-pure-of-op-and-type1 x y)')
               to the call @('(op-type1-type2 x y)'),
               under the hypothesis the @('y') has type @('type2'),
               for each of the 10 supported integer types."))
            (xdoc::p
             "Note that the intermediate functions used here
              do not need guard verification."))
           ,@events
           (defval *atc-exec-binary-strict-pure-rules*
             '(,@names
               (:e binop-mul)
               (:e binop-div)
               (:e binop-rem)
               (:e binop-add)
               (:e binop-sub)
               (:e binop-shl)
               (:e binop-shr)
               (:e binop-lt)
               (:e binop-gt)
               (:e binop-le)
               (:e binop-ge)
               (:e binop-eq)
               (:e binop-ne)
               (:e binop-bitand)
               (:e binop-bitxor)
               (:e binop-bitior))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(make-event (atc-exec-binary-rules-gen-all))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-test-rules
  :short "Rules for executing tests on values."
  :long
  (xdoc::topstring
   (xdoc::p
    "Each rule turns @('(exec-test x)')
     into @('(boolean-from-<type> x)'),
     where @('<type>') is the type of @('x').
     The @(tsee exec-test) terms result
     from the symbolic execution of the C code,
     while the @('boolean-from-<type>') terms occur
     in the ACL2 functions that represent the C code."))

  (make-event
   `(defruled exec-test-when-scharp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (scharp x))
               (equal (exec-test x)
                      (boolean-from-schar x)))
      :enable exec-test))

  (make-event
   `(defruled exec-test-when-ucharp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (ucharp x))
               (equal (exec-test x)
                      (boolean-from-uchar x)))
      :enable exec-test))

  (make-event
   `(defruled exec-test-when-sshortp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (sshortp x))
               (equal (exec-test x)
                      (boolean-from-sshort x)))
      :enable exec-test))

  (make-event
   `(defruled exec-test-when-ushortp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (ushortp x))
               (equal (exec-test x)
                      (boolean-from-ushort x)))
      :enable exec-test))

  (make-event
   `(defruled exec-test-when-sintp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (sintp x))
               (equal (exec-test x)
                      (boolean-from-sint x)))
      :enable exec-test))

  (make-event
   `(defruled exec-test-when-uintp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (uintp x))
               (equal (exec-test x)
                      (boolean-from-uint x)))
      :enable exec-test))

  (make-event
   `(defruled exec-test-when-slongp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (slongp x))
               (equal (exec-test x)
                      (boolean-from-slong x)))
      :enable exec-test))

  (make-event
   `(defruled exec-test-when-ulongp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (ulongp x))
               (equal (exec-test x)
                      (boolean-from-ulong x)))
      :enable exec-test))

  (make-event
   `(defruled exec-test-when-sllongp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (sllongp x))
               (equal (exec-test x)
                      (boolean-from-sllong x)))
      :enable exec-test))

  (make-event
   `(defruled exec-test-when-ullongp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'x)
                    (ullongp x))
               (equal (exec-test x)
                      (boolean-from-ullong x)))
      :enable exec-test))

  (defval *atc-exec-test-rules*
    '(exec-test-when-scharp
      exec-test-when-ucharp
      exec-test-when-sshortp
      exec-test-when-ushortp
      exec-test-when-sintp
      exec-test-when-uintp
      exec-test-when-slongp
      exec-test-when-ulongp
      exec-test-when-sllongp
      exec-test-when-ullongp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-expr-pure-rules
  :short "Rules for @(tsee exec-expr-pure)."
  :long
  (xdoc::topstring
   (xdoc::p
    "For @('&&') and @('||'),
     we use the auxiliary function @('sint-from-boolean-with-error')
     as an intermediate rewriting stage.")
   (xdoc::p
    "We include the executable counterpart of @(tsee member-equal),
     needed to discharge the hypothesis of
     the rule for strict pure binary expressions.")
   (xdoc::p
    "We include executable counterparts of accessor functions for expressions,
     used to check the kind of expression and to retrieve its constituents."))

  (defruled exec-expr-pure-when-ident
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :ident))
             (equal (exec-expr-pure e compst)
                    (exec-ident (expr-ident->get e) compst)))
    :enable exec-expr-pure)

  (defruled exec-expr-pure-when-const
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :const))
             (equal (exec-expr-pure e compst)
                    (exec-const (expr-const->get e))))
    :enable exec-expr-pure)

  (defruled exec-expr-pure-when-arrsub
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :arrsub)
                  (equal arr (expr-arrsub->arr e))
                  (not (expr-case arr :memberp)))
             (equal (exec-expr-pure e compst)
                    (exec-arrsub (exec-expr-pure arr compst)
                                 (exec-expr-pure (expr-arrsub->sub e) compst)
                                 compst)))
    :enable exec-expr-pure)

  (defruled exec-expr-pure-when-memberp
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :memberp))
             (equal (exec-expr-pure e compst)
                    (exec-memberp (exec-expr-pure (expr-memberp->target e)
                                                  compst)
                                  (expr-memberp->name e)
                                  compst)))
    :enable exec-expr-pure)

  (defruled exec-expr-pure-when-arrsub-of-memberp
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :arrsub)
                  (equal arr (expr-arrsub->arr e))
                  (expr-case arr :memberp))
             (equal (exec-expr-pure e compst)
                    (exec-arrsub-of-memberp
                     (exec-expr-pure (expr-memberp->target arr) compst)
                     (expr-memberp->name arr)
                     (exec-expr-pure (expr-arrsub->sub e) compst)
                     compst)))
    :enable exec-expr-pure)

  (defruled exec-expr-pure-when-unary
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :unary))
             (equal (exec-expr-pure e compst)
                    (exec-unary (expr-unary->op e)
                                (exec-expr-pure (expr-unary->arg e) compst))))
    :enable exec-expr-pure)

  (defruled exec-expr-pure-when-cast
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :cast))
             (equal (exec-expr-pure e compst)
                    (exec-cast (expr-cast->type e)
                               (exec-expr-pure (expr-cast->arg e) compst))))
    :enable exec-expr-pure)

  (defruled exec-expr-pure-when-strict-pure-binary
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :binary)
                  (equal op (expr-binary->op e))
                  (member-equal (binop-kind op)
                                '(:mul :div :rem :add :sub :shl :shr
                                  :lt :gt :le :ge :eq :ne
                                  :bitand :bitxor :bitior)))
             (equal (exec-expr-pure e compst)
                    (exec-binary-strict-pure op
                                             (exec-expr-pure (expr-binary->arg1 e)
                                                             compst)
                                             (exec-expr-pure (expr-binary->arg2 e)
                                                             compst))))
    :enable (exec-expr-pure binop-purep))

  (defund sint-from-boolean-with-error (test)
    (if (errorp test)
        test
      (if test
          (sint 1)
        (sint 0))))

  (defruled exec-expr-pure-when-binary-logand
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :binary)
                  (equal op (expr-binary->op e))
                  (equal (binop-kind op) :logand)
                  (equal test1 (exec-test
                                (exec-expr-pure (expr-binary->arg1 e)
                                                compst)))
                  (booleanp test1))
             (equal (exec-expr-pure e compst)
                    (if test1
                        (sint-from-boolean-with-error
                         (exec-test
                          (exec-expr-pure (expr-binary->arg2 e) compst)))
                      (sint 0))))
    :enable (exec-expr-pure binop-purep sint-from-boolean-with-error))

  (defruled exec-expr-pure-when-binary-logor
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :binary)
                  (equal op (expr-binary->op e))
                  (equal (binop-kind op) :logor)
                  (equal test1 (exec-test
                                (exec-expr-pure (expr-binary->arg1 e)
                                                compst)))
                  (booleanp test1))
             (equal (exec-expr-pure e compst)
                    (if test1
                        (sint 1)
                      (sint-from-boolean-with-error
                       (exec-test
                        (exec-expr-pure (expr-binary->arg2 e) compst))))))
    :enable (exec-expr-pure binop-purep sint-from-boolean-with-error))

  (make-event
   `(defruled sint-from-boolean-with-error-when-booleanp
      (implies (and ,(atc-syntaxp-hyp-for-expr-pure 'test)
                    (booleanp test))
               (equal (sint-from-boolean-with-error test)
                      (if test
                          (sint 1)
                        (sint 0))))
      :enable sint-from-boolean-with-error))

  (defruled exec-expr-pure-when-cond
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :cond)
                  (equal test (exec-test
                               (exec-expr-pure (expr-cond->test e) compst)))
                  (booleanp test))
             (equal (exec-expr-pure e compst)
                    (if test
                        (exec-expr-pure (expr-cond->then e) compst)
                      (exec-expr-pure (expr-cond->else e) compst))))
    :enable exec-expr-pure)

  (defval *atc-exec-expr-pure-rules*
    '(exec-expr-pure-when-ident
      exec-expr-pure-when-const
      exec-expr-pure-when-arrsub
      exec-expr-pure-when-memberp
      exec-expr-pure-when-arrsub-of-memberp
      exec-expr-pure-when-unary
      exec-expr-pure-when-cast
      exec-expr-pure-when-strict-pure-binary
      exec-expr-pure-when-binary-logand
      exec-expr-pure-when-binary-logor
      sint-from-boolean-with-error-when-booleanp
      exec-expr-pure-when-cond
      (:e member-equal)
      (:e expr-kind)
      (:e expr-ident->get)
      (:e expr-const->get)
      (:e expr-arrsub->arr)
      (:e expr-arrsub->sub)
      (:e expr-memberp->target)
      (:e expr-memberp->name)
      (:e expr-unary->op)
      (:e expr-unary->arg)
      (:e expr-cast->type)
      (:e expr-cast->arg)
      (:e expr-binary->op)
      (:e expr-binary->arg1)
      (:e expr-binary->arg2)
      (:e binop-kind)
      (:e expr-cond->test)
      (:e expr-cond->then)
      (:e expr-cond->else))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-expr-pure-list-rules
  :short "Rules for @(tsee exec-expr-pure-list)."

  (defruled exec-expr-pure-list-of-nil
    (equal (exec-expr-pure-list nil compst)
           nil)
    :enable exec-expr-pure-list)

  (defruled exec-expr-pure-list-when-consp
    (implies (and (syntaxp (quotep es))
                  (consp es)
                  (equal val (exec-expr-pure (car es) compst))
                  (valuep val)
                  (equal vals (exec-expr-pure-list (cdr es) compst))
                  (value-listp vals))
             (equal (exec-expr-pure-list es compst)
                    (cons val vals)))
    :enable exec-expr-pure-list)

  (defval *atc-exec-expr-pure-list-rules*
    '(exec-expr-pure-list-of-nil
      exec-expr-pure-list-when-consp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-expr-call-rules
  :short "Rules for @(tsee exec-expr-call)."

  (defruled exec-expr-call-open
    (implies (and (not (zp limit))
                  (equal vals (exec-expr-pure-list args compst))
                  (value-listp vals))
             (equal (exec-expr-call fun args compst fenv limit)
                    (exec-fun fun vals compst fenv (1- limit))))
    :enable exec-expr-call)

  (defval *atc-exec-expr-call-rules*
    '(exec-expr-call-open)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-expr-call-or-pure-rules
  :short "Rules for @(tsee exec-expr-call-or-pure)."

  (defruled exec-expr-call-or-pure-when-pure
    (implies (and (syntaxp (quotep e))
                  (not (equal (expr-kind e) :call))
                  (not (zp limit))
                  (compustatep compst))
             (equal (exec-expr-call-or-pure e compst fenv limit)
                    (mv (exec-expr-pure e compst)
                        compst)))
    :enable exec-expr-call-or-pure)

  (defruled exec-expr-call-of-pure-when-call
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :call)
                  (not (zp limit)))
             (equal (exec-expr-call-or-pure e compst fenv limit)
                    (exec-expr-call (expr-call->fun e)
                                    (expr-call->args e)
                                    compst
                                    fenv
                                    (1- limit))))
    :enable exec-expr-call-or-pure)

  (defval *atc-exec-expr-call-or-pure-rules*
    '(exec-expr-call-or-pure-when-pure
      exec-expr-call-of-pure-when-call
      (:e expr-kind)
      (:e expr-call->fun)
      (:e expr-call->args))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-expr-asg-ident-rules
  :short "Rules for executing assignment expressions to identifier expressions."

  (defruled exec-expr-asg-ident
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :binary)
                  (equal (binop-kind (expr-binary->op e)) :asg)
                  (not (zp limit))
                  (equal e1 (expr-binary->arg1 e))
                  (equal (expr-kind e1) :ident)
                  (equal val+compst1
                         (exec-expr-call-or-pure (expr-binary->arg2 e)
                                                 compst
                                                 fenv
                                                 (1- limit)))
                  (equal val (mv-nth 0 val+compst1))
                  (equal compst1 (mv-nth 1 val+compst1))
                  (valuep val))
             (equal (exec-expr-asg e compst fenv limit)
                    (write-var (expr-ident->get e1) val compst1)))
    :enable exec-expr-asg)

  (defval *atc-exec-expr-asg-ident-rules*
    '(exec-expr-asg-ident
      (:e expr-kind)
      (:e expr-binary->op)
      (:e expr-binary->arg1)
      (:e expr-binary->arg2)
      (:e expr-ident->get)
      (:e binop-kind))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-expr-asg-arrsub-rules-generation
  :short "Code to generate the rules for executing
          assignments to array subscript expressions."

  (define atc-exec-expr-asg-arrsub-rules-gen ((atype typep) (itype typep))
    :guard (and (type-integerp atype)
                (type-integerp itype))
    :returns (mv (name symbolp)
                 (event pseudo-event-formp))
    :parents nil
    (b* ((afixtype (integer-type-to-fixtype atype))
         (ifixtype (integer-type-to-fixtype itype))
         (apred (pack afixtype '-arrayp))
         (epred (pack afixtype 'p))
         (ipred (pack ifixtype 'p))
         (atype-array-itype-index-okp
          (pack afixtype '-array- ifixtype '-index-okp))
         (atype-array-index-okp
          (pack afixtype '-array-index-okp))
         (atype-array-write-itype
          (pack afixtype '-array-write- ifixtype))
         (atype-array-write-alt-def
          (pack afixtype '-array-write-alt-def))
         (elemtype-when-apred
          (pack 'value-array->elemtype-when- apred))
         (name (pack 'exec-expr-asg-arrsub-when- apred '-and- ipred))
         (formula
          `(implies
            (and (syntaxp (quotep e))
                 (equal (expr-kind e) :binary)
                 (equal (binop-kind (expr-binary->op e)) :asg)
                 (equal left (expr-binary->arg1 e))
                 (equal right (expr-binary->arg2 e))
                 (equal (expr-kind left) :arrsub)
                 (equal arr (expr-arrsub->arr left))
                 (equal sub (expr-arrsub->sub left))
                 (equal (expr-kind arr) :ident)
                 (not (zp limit))
                 (equal ptr (read-var (expr-ident->get arr) compst))
                 (valuep ptr)
                 (value-case ptr :pointer)
                 (not (value-pointer-nullp ptr))
                 (equal (value-pointer->reftype ptr)
                        ,(type-to-maker atype))
                 (equal array
                        (read-object (value-pointer->designator ptr) compst))
                 (,apred array)
                 (equal index (exec-expr-pure sub compst))
                 (,ipred index)
                 (,atype-array-itype-index-okp array index)
                 (equal val (exec-expr-pure right compst))
                 (,epred val))
            (equal (exec-expr-asg e compst fenv limit)
                   (write-object (value-pointer->designator ptr)
                                 (,atype-array-write-itype array index val)
                                 compst))))
         (event `(defruled ,name
                   ,formula
                   :enable (exec-expr-asg
                            exec-integer
                            ,atype-array-itype-index-okp
                            ,atype-array-write-itype
                            ,atype-array-write-alt-def
                            ,elemtype-when-apred)
                   :prep-lemmas
                   ((defrule lemma1
                      (implies (and (,atype-array-index-okp array index)
                                    (integerp index))
                               (not (< index 0)))
                      :enable ,atype-array-index-okp)
                    (defrule lemma2
                      (implies (and (,apred array)
                                    (integerp index)
                                    (,atype-array-index-okp array index)
                                    (,epred val))
                               (not (errorp
                                     (value-array-write index val array))))
                      :use (:instance ,atype-array-write-alt-def
                            (elem val)))))))
      (mv name event)))

  (define atc-exec-expr-asg-arrsub-rules-gen-loop-itypes ((atype typep)
                                                          (itypes type-listp))
    :guard (and (type-integerp atype)
                (type-integer-listp itypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp itypes)) (mv nil nil))
         ((mv name event) (atc-exec-expr-asg-arrsub-rules-gen atype
                                                              (car itypes)))
         ((mv names events)
          (atc-exec-expr-asg-arrsub-rules-gen-loop-itypes atype (cdr itypes))))
      (mv (cons name names) (cons event events))))

  (define atc-exec-expr-asg-arrsub-rules-gen-loop-atypes ((atypes type-listp)
                                                          (itypes type-listp))
    :guard (and (type-integer-listp atypes)
                (type-integer-listp itypes))
    :returns (mv (names symbol-listp)
                 (events pseudo-event-form-listp))
    :parents nil
    (b* (((when (endp atypes)) (mv nil nil))
         ((mv names events)
          (atc-exec-expr-asg-arrsub-rules-gen-loop-itypes (car atypes) itypes))
         ((mv more-names more-events)
          (atc-exec-expr-asg-arrsub-rules-gen-loop-atypes (cdr atypes) itypes)))
      (mv (append names more-names) (append events more-events))))

  (define atc-exec-expr-asg-arrsub-rules-gen-all ()
    :returns (event pseudo-event-formp)
    :parents nil
    (b* (((mv names events)
          (atc-exec-expr-asg-arrsub-rules-gen-loop-atypes
           *integer-nonbool-nonchar-types*
           *integer-nonbool-nonchar-types*)))
      `(progn
         (defsection atc-exec-expr-asg-arrsub-rules
           :short "Rules for executing assignment expressions to
                   array subscript expressions."
           ,@events
           (defval *atc-exec-expr-asg-arrsub-rules*
             '(,@names
               (:e expr-kind)
               (:e expr-arrsub->arr)
               (:e expr-arrsub->sub)
               (:e expr-binary->op)
               (:e expr-binary->arg1)
               (:e expr-binary->arg2)
               (:e expr-ident->get)
               (:e binop-kind))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(make-event (atc-exec-expr-asg-arrsub-rules-gen-all))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-expr-asg-rules
  :short "Rules for executing assignment expressions."

  (defval *atc-exec-expr-asg-rules*
    (append *atc-exec-expr-asg-ident-rules*
            *atc-exec-expr-asg-arrsub-rules*)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-expr-call-or-asg-rules
  :short "Rules for @(tsee exec-expr-call-or-asg)."

  (defruled exec-expr-call-or-asg-when-call
    (implies (and (syntaxp (quotep e))
                  (equal (expr-kind e) :call)
                  (not (zp limit))
                  (equal val?+compst1
                         (exec-expr-call (expr-call->fun e)
                                         (expr-call->args e)
                                         compst
                                         fenv
                                         (1- limit)))
                  (equal val? (mv-nth 0 val?+compst1))
                  (equal compst1 (mv-nth 1 val?+compst1))
                  (value-optionp val?))
             (equal (exec-expr-call-or-asg e compst fenv limit)
                    compst1))
    :enable exec-expr-call-or-asg)

  (defruled exec-expr-call-or-asg-when-asg
    (implies (and (syntaxp (quotep e))
                  (not (equal (expr-kind e) :call))
                  (not (zp limit))
                  (compustatep compst))
             (equal (exec-expr-call-or-asg e compst fenv limit)
                    (exec-expr-asg e compst fenv (1- limit))))
    :enable exec-expr-call-or-asg)

  (defval *atc-exec-expr-call-or-asg-rules*
    '(exec-expr-call-or-asg-when-call
      exec-expr-call-or-asg-when-asg
      (:e expr-kind)
      (:e expr-call->fun)
      (:e expr-call->args))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-fun-rules
  :short "Rules for @(tsee exec-fun)."
  :long
  (xdoc::topstring
   (xdoc::p
    "The proofs generated by ATC are modularized
     so that there is one theorem per non-recursive target function.
     So we generally do not expand calls of @(tsee exec-fun),
     except in the theorem for the function in question.
     We rely on the fact that the correctness theorems
     for the functions called by the function in question
     come after the following rule in the ACL2 history
     (because they are generated by ATC as part of the generated events),
     and thus take precedence over this rule:
     in other words, given theorems for the called functions,
     this rule is expected to apply only on the function in question,
     i.e. the one whose correctness theorem is being proved.
     Note that these theorems are generated only for non-recursive functions;
     the recursive functions represent loops,
     and their correctness theorems do not involve @(tsee exec-fun)."))

  (defruled exec-fun-open
    (implies (and (not (zp limit))
                  (equal info (fun-env-lookup fun fenv))
                  info
                  (equal scope (init-scope (fun-info->params info) args))
                  (scopep scope)
                  (equal val?+compst1
                         (exec-block-item-list (fun-info->body info)
                                               (push-frame (make-frame
                                                            :function fun
                                                            :scopes (list
                                                                     scope))
                                                           compst)
                                    fenv
                                    (1- limit)))
                  (equal val? (mv-nth 0 val?+compst1))
                  (equal compst1 (mv-nth 1 val?+compst1))
                  (value-optionp val?)
                  (equal (type-of-value-option val?)
                         (tyname-to-type (fun-info->result info))))
             (equal (exec-fun fun args compst fenv limit)
                    (mv val? (pop-frame compst1))))
    :enable exec-fun)

  (defval *atc-exec-fun-rules*
    '(exec-fun-open
      (:e fun-info->params)
      (:e fun-info->result)
      (:e fun-info->body))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-stmt-rules
  :short "Rules for @(tsee exec-stmt)."

  (defruled exec-stmt-when-compound
    (implies (and (syntaxp (quotep s))
                  (equal (stmt-kind s) :compound)
                  (not (zp limit))
                  (equal val?+compst1
                         (exec-block-item-list (stmt-compound->items s)
                                               (enter-scope compst)
                                               fenv
                                               (1- limit)))
                  (equal val? (mv-nth 0 val?+compst1))
                  (equal compst1 (mv-nth 1 val?+compst1))
                  (value-optionp val?))
             (equal (exec-stmt s compst fenv limit)
                    (mv val? (exit-scope compst1))))
    :enable exec-stmt)

  (defruled exec-stmt-when-expr
    (implies (and (syntaxp (quotep s))
                  (equal (stmt-kind s) :expr)
                  (not (zp limit))
                  (equal compst1
                         (exec-expr-call-or-asg (stmt-expr->get s)
                                                compst
                                                fenv
                                                (1- limit)))
                  (compustatep compst1))
             (equal (exec-stmt s compst fenv limit)
                    (mv nil compst1)))
    :enable exec-stmt)

  (defruled exec-stmt-when-if
    (implies (and (syntaxp (quotep s))
                  (equal (stmt-kind s) :if)
                  (not (zp limit))
                  (compustatep compst)
                  (equal test
                         (exec-test (exec-expr-pure (stmt-if->test s) compst)))
                  (booleanp test))
             (equal (exec-stmt s compst fenv limit)
                    (if test
                        (exec-stmt (stmt-if->then s) compst fenv (1- limit))
                      (mv nil compst))))
    :enable exec-stmt)

  (defruled exec-stmt-when-ifelse
    (implies (and (syntaxp (quotep s))
                  (equal (stmt-kind s) :ifelse)
                  (not (zp limit))
                  (equal test
                         (exec-test
                          (exec-expr-pure (stmt-ifelse->test s) compst)))
                  (booleanp test))
             (equal (exec-stmt s compst fenv limit)
                    (if test
                        (exec-stmt (stmt-ifelse->then s) compst fenv (1- limit))
                      (exec-stmt (stmt-ifelse->else s) compst fenv (1- limit)))))
    :enable exec-stmt)

  (defruled exec-stmt-when-while
    (implies (and (syntaxp (quotep s))
                  (equal (stmt-kind s) :while)
                  (not (zp limit)))
             (equal (exec-stmt s compst fenv limit)
                    (exec-stmt-while (stmt-while->test s)
                                     (stmt-while->body s)
                                     compst
                                     fenv
                                     (1- limit))))
    :enable exec-stmt)

  (defruled exec-stmt-when-return
    (implies (and (syntaxp (quotep s))
                  (equal (stmt-kind s) :return)
                  (not (zp limit))
                  (equal e (stmt-return->value s))
                  e
                  (equal val+compst1
                         (exec-expr-call-or-pure e compst fenv (1- limit)))
                  (equal val (mv-nth 0 val+compst1))
                  (equal compst1 (mv-nth 1 val+compst1))
                  (valuep val))
             (equal (exec-stmt s compst fenv limit)
                    (mv val compst1)))
    :enable exec-stmt)

  (defval *atc-exec-stmt-rules*
    '(exec-stmt-when-compound
      exec-stmt-when-expr
      exec-stmt-when-if
      exec-stmt-when-ifelse
      exec-stmt-when-while
      exec-stmt-when-return
      (:e stmt-kind)
      (:e stmt-compound->items)
      (:e stmt-expr->get)
      (:e stmt-if->test)
      (:e stmt-if->then)
      (:e stmt-ifelse->test)
      (:e stmt-ifelse->then)
      (:e stmt-ifelse->else)
      (:e stmt-while->test)
      (:e stmt-while->body)
      (:e stmt-return->value))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-initer-rules
  :short "Rules for @(tsee exec-initer)."

  (defruled exec-initer-when-single
    (implies (and (syntaxp (quotep initer))
                  (equal (initer-kind initer) :single)
                  (not (zp limit))
                  (equal expr (initer-single->get initer))
                  (equal val+compst1
                         (exec-expr-call-or-pure expr compst fenv (1- limit)))
                  (equal val (mv-nth 0 val+compst1))
                  (equal compst1 (mv-nth 1 val+compst1))
                  (valuep val))
             (equal (exec-initer initer compst fenv limit)
                    (mv val compst1)))
    :enable exec-initer)

  (defval *atc-exec-initer-rules*
    '(exec-initer-when-single
      (:e initer-kind)
      (:e initer-single->get))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-block-item-rules
  :short "Rules for @(tsee exec-block-item)."

  (defruled exec-block-item-when-declon
    (implies (and (syntaxp (quotep item))
                  (equal (block-item-kind item) :declon)
                  (not (zp limit))
                  (equal declon (block-item-declon->get item))
                  (equal var+tyname+init
                         (obj-declon-to-ident+tyname+init declon))
                  (equal var (mv-nth 0 var+tyname+init))
                  (equal tyname (mv-nth 1 var+tyname+init))
                  (equal init (mv-nth 2 var+tyname+init))
                  (equal val+compst1
                         (exec-initer init compst fenv (1- limit)))
                  (equal val (mv-nth 0 val+compst1))
                  (equal compst1 (mv-nth 1 val+compst1))
                  (valuep val)
                  (equal (type-of-value val)
                         (tyname-to-type tyname))
                  (equal compst2 (create-var var val compst1))
                  (compustatep compst2))
             (equal (exec-block-item item compst fenv limit)
                    (mv nil compst2)))
    :enable exec-block-item)

  (defruled exec-block-item-when-stmt
    (implies (and (syntaxp (quotep item))
                  (equal (block-item-kind item) :stmt)
                  (not (zp limit)))
             (equal (exec-block-item item compst fenv limit)
                    (exec-stmt (block-item-stmt->get item)
                               compst
                               fenv
                               (1- limit))))
    :enable exec-block-item)

  (defval *atc-exec-block-item-rules*
    '(exec-block-item-when-declon
      exec-block-item-when-stmt
      (:e block-item-kind)
      (:e block-item-declon->get)
      (:e block-item-stmt->get)
      (:e obj-declon-to-ident+tyname+init))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-exec-block-item-list-rules
  :short "Rules for @(tsee exec-block-item-list)."

  (defruled exec-block-item-list-of-nil
    (implies (and (not (zp limit))
                  (compustatep compst))
             (equal (exec-block-item-list nil compst fenv limit)
                    (mv nil compst)))
    :enable exec-block-item-list)

  (defruled exec-block-item-list-when-consp
    (implies (and (syntaxp (quotep items))
                  (consp items)
                  (not (zp limit))
                  (equal val?+compst1
                         (exec-block-item (car items) compst fenv (1- limit)))
                  (equal val? (mv-nth 0 val?+compst1))
                  (value-optionp val?)
                  (equal compst1 (mv-nth 1 val?+compst1)))
             (equal (exec-block-item-list items compst fenv limit)
                    (if val?
                        (mv val? compst1)
                      (exec-block-item-list (cdr items)
                                            compst1
                                            fenv
                                            (1- limit)))))
    :enable exec-block-item-list)

  (defval *atc-exec-block-item-list-rules*
    '(exec-block-item-list-of-nil
      exec-block-item-list-when-consp)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defsection atc-init-scope-rules
  :short "Rules for @(tsee init-scope)."
  :long
  (xdoc::topstring
   (xdoc::p
    "The base case is a call @('(init-scope nil nil)'),
     which is handled by the executable counterpart of @(tsee init-scope).
     For the step case, during symbolic execution we expect that
     there is always the same number of formals and actuals.")
   (xdoc::p
    "We need to enable @(tsee eq) because it arises from
     the translation of @('(obj-declor-case declor :pointer)')
     in one of the hypotheses of the rule."))

  (defruled init-scope-when-consp
    (implies (and (syntaxp (quotep formals))
                  (consp formals)
                  (equal formal (car formals))
                  (param-declonp formal)
                  (valuep val)
                  (equal name+tyname (param-declon-to-ident+tyname formal))
                  (equal name (mv-nth 0 name+tyname))
                  (equal tyname (mv-nth 1 name+tyname))
                  (equal (type-of-value val)
                         (tyname-to-type tyname))
                  (value-listp vals)
                  (equal scope (init-scope (cdr formals) vals))
                  (scopep scope)
                  (not (omap::in name scope)))
             (equal (init-scope formals (cons val vals))
                    (omap::update name val scope)))
    :enable init-scope)

  (defval *atc-init-scope-rules*
    '(init-scope-when-consp
      eq
      (:e init-scope)
      (:e param-declonp)
      (:e param-declon-to-ident+tyname))))