; 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 "symbolic-computation-states")
(include-book "shallow-embedding")
(include-book "execution-rules")

(include-book "tools/rulesets" :dir :system)

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

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

(defrulel true-list-listp-of-append-when-both-true-list-listp
  (implies (and (true-list-listp a)
                (true-list-listp b))
           (true-list-listp (append a b))))

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

(defxdoc+ atc-proof-support
  :parents (atc-implementation)
  :short "Functions and rules to support the proofs generated by ATC."
  :long
  (xdoc::topstring
   (xdoc::p
    "Currently, the generated proofs of function correctness
     are carried out via symbolic execution of the C code.
     The C code is a constant value,
     because we are generating proofs over specific C functions;
     this makes symbolic execution possible.")
   (xdoc::p
    "In order to make these generated proofs more robust,
     we carry them out in a theory that consists exactly of
     (what we believe to be) all and only the needed rules.
     This file defines that theory, which consists of
     some rules introduced elsewhere and some rules introduced in this file.
     This set of rules has been defined by
     not only thinking of what is needed for symbolic execution,
     but also experimenting with several symbolic execution proofs,
     starting with the empty theory and adding rules
     as needed to advance the symbolic execution,
     and also by looking at the C dynamic semantics.
     There is no guarantee (meta proof) that
     these rules will suffice for every use of ATC;
     there is also no guarantee that
     the proof will not be defeated by some ACL2 heuristic in some cases.
     Nonetheless, the proof strategy seems sound and robust,
     and if a generated proof fails
     it should be possible to (prove and) use additional rules.")
   (xdoc::p
    "Besides rules, we also introduce some functions
     that provide a canonical representation of computation states
     that is used during symbolic execution.
     Thus, some of the rules in the symbolic execution theory
     are tailored to the functions that form this canonical representation."))
  :order-subtopics t
  :default-parent t)

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

(defval *atc-other-executable-counterpart-rules*
  :short "List of other executable counterpart rules
          for the proofs generated by ATC."
  '((:e booleanp)
    (:e len)
    (:e natp)
    (:e omap::in)
    (:e scope-list-fix)
    (:e scope-listp)
    (:e scopep)
    (:e tyname)
    (:e obj-adeclor-none)
    (:e valuep)
    (:e value-list-fix)
    (:e zp)
    (:e <<)))

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

(defval *atc-other-definition-rules*
  :short "List of other definition rules for the proofs generated by ATC."
  :long
  (xdoc::topstring
   (xdoc::p
    "These are designated as `other' with respect to the definition rules
     for shifts and other operations that are collected separately.")
   (xdoc::p
    "During symbolic execution, terms appear
     with certain non-recursive functions applied to
     terms that are not constant, but contain constant parts.
     These can be simplified by opening the function definition,
     which ACL2's heuristics (we believe) should never block,
     given that they are not recursive.
     Some are @('exec-...') functions,
     others are functions to manipulate the frame stack,
     etc.")
   (xdoc::p
    "We expand @(tsee condexpr) because it is just a wrapper
     that signifies a conditional expression instead of statement.")
   (xdoc::p
    "It may seem surprising that
     we expand functions like @(tsee sint-dec-const),
     since those correspond to C constructs;
     we certainly do not expand functions like @(tsee add-sint-sint).
     The reason is that functions like @(tsee sint-dec-const)
     are used to represent C constants in ACL2 functions,
     but in the dynamic semantics,
     @(tsee exec-iconst) (which we expand, obviously)
     produces terms of the form @('(sint <quoted-integer>)').
     By expanding @(tsee sint-dec-const) in the ACL2 functions,
     we produce terms of the form @('(sint <quoted-integer>)'),
     which therefore match the ones from @(tsee exec-iconst).")
   (xdoc::p
    "We do not expand any fixtype constructors.
     This is because such expansions would expose
     the internal representational details of the fixtype's values.
     Instead, we want to operate on those as more abstract entities,
     and use deconstructors to obtain their components.
     In fact, as explained elsewhere,
     we enable rules that simplify
     applications of deconstructors to constructors.")
   (xdoc::p
    "We expand @(tsee sint-from-boolean),
     because it is really just an abbreviation.
     In fact, we want to expose its @(tsee if) structure
     in the symbolic execution."))
  '(condexpr
    declar
    assign
    sint-from-boolean
    sint-dec-const
    sint-oct-const
    sint-hex-const
    uint-dec-const
    uint-oct-const
    uint-hex-const
    slong-dec-const
    slong-oct-const
    slong-hex-const
    ulong-dec-const
    ulong-oct-const
    ulong-hex-const
    sllong-dec-const
    sllong-oct-const
    sllong-hex-const
    ullong-dec-const
    ullong-oct-const
    ullong-hex-const))

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

(defsection atc-distributivity-over-if-rewrite-rules
  :short "Rewrite rules about certain functions distributing over @(tsee if)."

  (defruled car-of-if
    (equal (car (if a b c))
           (if a (car b) (car c))))

  (defruled mv-nth-of-if
    (equal (mv-nth n (if a b c))
           (if a (mv-nth n b) (mv-nth n c))))

  (defruled len-of-if
    (equal (len (if a b c))
           (if a (len b) (len c))))

  (defruled errorp-of-if
    (equal (errorp (if a b c))
           (if a (errorp b) (errorp c))))

  (defruled valuep-of-if
    (equal (valuep (if a b c))
           (if a (valuep b) (valuep c))))

  (defruled scharp-of-if
    (equal (scharp (if a b c))
           (if a (scharp b) (scharp c))))

  (defruled ucharp-of-if
    (equal (ucharp (if a b c))
           (if a (ucharp b) (ucharp c))))

  (defruled sshortp-of-if
    (equal (sshortp (if a b c))
           (if a (sshortp b) (sshortp c))))

  (defruled ushortp-of-if
    (equal (ushortp (if a b c))
           (if a (ushortp b) (ushortp c))))

  (defruled sintp-of-if
    (equal (sintp (if a b c))
           (if a (sintp b) (sintp c))))

  (defruled uintp-of-if
    (equal (uintp (if a b c))
           (if a (uintp b) (uintp c))))

  (defruled slongp-of-if
    (equal (slongp (if a b c))
           (if a (slongp b) (slongp c))))

  (defruled ulongp-of-if
    (equal (ulongp (if a b c))
           (if a (ulongp b) (ulongp c))))

  (defruled sllongp-of-if
    (equal (sllongp (if a b c))
           (if a (sllongp b) (sllongp c))))

  (defruled ullongp-of-if
    (equal (ullongp (if a b c))
           (if a (ullongp b) (ullongp c))))

  (defruled booleanp-of-if
    (equal (booleanp (if a b c))
           (if a (booleanp b) (booleanp c))))

  (defruled compustate->frames-of-if
    (equal (compustate->frames (if a b c))
           (if a (compustate->frames b) (compustate->frames c))))

  (defruled scope-fix-of-if
    (equal (scope-fix (if a b c))
           (if a (scope-fix b) (scope-fix c))))

  (defruled value-result-fix-of-if
    (equal (value-result-fix (if a b c))
           (if a (value-result-fix b) (value-result-fix c)))))

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

(defval *atc-distributivity-over-if-rewrite-rules*
  :short "List of rewrite rules about
          certain functions distributing over @(tsee if)."
  '(car-of-if
    mv-nth-of-if
    len-of-if
    errorp-of-if
    valuep-of-if
    scharp-of-if
    ucharp-of-if
    sshortp-of-if
    ushortp-of-if
    sintp-of-if
    uintp-of-if
    slongp-of-if
    ulongp-of-if
    sllongp-of-if
    ullongp-of-if
    booleanp-of-if
    compustate->frames-of-if
    scope-fix-of-if
    value-result-fix-of-if))

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

(defsection atc-identifier-rules
  :short "Rules related to C identifiers."
  :long
  (xdoc::topstring
   (xdoc::p
    "During symbolic execution, C identifiers in the computation state
     always have the form @('(ident <string>)'),
     where @('<string>') is a quoted string constant.
     To keep them in this form, we leave @(tsee ident) disabled.
     Since the symbolic execution
     sometimes applies @(tsee ident-fix) to identifiers,
     we enable @('ident-fix-when-identp') and @('identp-of-ident'),
     so that @(tsee ident-fix) can be rewritten away.
     Sometimes the symbolic execution produces equalities over identifiers:
     we introduce a rule that reduces those to equalities over strings.
     Since the latter equalities involve the string fixer,
     we enable its executable counterpart.
     Similarly, sometimes the symbolic execution produces
     calls of @(tsee <<) over identifiers:
     we introduce a rule that reduces those to @(tsee <<) over strings.")
   (xdoc::p
    "In the course of symbolic execution,
     terms appears of the form @('(exec-fun <ident> ...)'),
     where @('<ident>') is a quoted identifier constant,
     obtained by the C ASTs being executed.
     This @('<ident>') does not have the form @('(ident <string>'));
     we introduce and enable a rule
     to turn @('<ident>') into @('(ident <string>')
     when it appears in @(tsee exec-fun).
     We introduce similar rules for terms of the form
     @('(create-var <ident> ...)'),
     @('(read-var <ident> ...)'),
     @('(write-var <ident> ...)'),
     @('(type-struct <ident>)'), and
     @('(exec-memberp ... <ident> ...)')."))

  (defruled equal-of-ident-and-const
    (implies (and (syntaxp (and (quotep x)
                                (quotep c)))
                  (identp c))
             (equal (equal (ident x) c)
                    (equal (str-fix x)
                           (ident->name c)))))

  (defruled equal-of-ident-and-ident
    (equal (equal (ident x)
                  (ident y))
           (equal (str-fix x)
                  (str-fix y))))

  (defruled <<-of-ident-and-ident
    (equal (<< (ident x)
               (ident y))
           (<< (str-fix x)
               (str-fix y)))
    :enable (<< lexorder ident))

  (defruled exec-fun-of-const-identifier
    (implies (and (syntaxp (quotep fun))
                  (identp fun))
             (equal (exec-fun fun
                              args compst fenv limit)
                    (exec-fun (ident (ident->name fun))
                              args compst fenv limit))))

  (defruled create-var-of-const-identifier
    (implies (and (syntaxp (quotep var))
                  (identp var))
             (equal (create-var var val compst)
                    (create-var (ident (ident->name var)) val compst))))

  (defruled read-var-of-const-identifier
    (implies (and (syntaxp (quotep var))
                  (identp var))
             (equal (read-var var compst)
                    (read-var (ident (ident->name var)) compst))))

  (defruled write-var-of-const-identifier
    (implies (and (syntaxp (quotep var))
                  (identp var))
             (equal (write-var var val compst)
                    (write-var (ident (ident->name var)) val compst))))

  (defruled type-struct-of-const-identifier
    (implies (and (syntaxp (quotep tag))
                  (identp tag))
             (equal (type-struct tag)
                    (type-struct (ident (ident->name tag))))))

  (defruled exec-memberp-of-const-identifier
    (implies (and (syntaxp (quotep mem))
                  (identp mem))
             (equal (exec-memberp val mem compst)
                    (exec-memberp val (ident (ident->name mem)) compst))))

  (defruled exec-arrsub-of-memberp-of-const-identifier
    (implies
     (and (syntaxp (quotep mem))
          (identp mem))
     (equal
      (exec-arrsub-of-memberp str mem sub compst)
      (exec-arrsub-of-memberp str (ident (ident->name mem)) sub compst)))))

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

(defval *atc-identifier-rules*
  :short "List of rules related to C identifiers."
  :long
  (xdoc::topstring
   (xdoc::p
    "See @(see atc-identifier-rules)."))
  '(ident-fix-when-identp
    identp-of-ident
    equal-of-ident-and-const
    equal-of-ident-and-ident
    <<-of-ident-and-ident
    (:e str-fix)
    (:e identp)
    (:e ident->name)
    exec-fun-of-const-identifier
    create-var-of-const-identifier
    read-var-of-const-identifier
    write-var-of-const-identifier
    type-struct-of-const-identifier
    exec-memberp-of-const-identifier
    exec-arrsub-of-memberp-of-const-identifier))

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

(defsection atc-not-rules
  :short "Rules related to @(tsee not)."
  :long
  (xdoc::topstring
   (xdoc::p
    "ATC currently allows the logical negation operator @('!')
     to be represented via not only the @('lognot-<type>') functions,
     but also @(tsee not), with appropriate conversions with booleans as needed.
     That is, an ACL2 target function, from which C code is generate,
     may represent logical negation in two different ways.
     The dynamic semantics of C, during symbolic execution,
     turns expressions with the logical negation operator into one form.
     Thus, we need rules to normalize one of the two forms into the other.")
   (xdoc::p
    "We choose to normalize things to use @(tsee not).
     Thus, we add rules saying that @('(boolean-from-<type> (lognot-<type> x))')
     becomes @('(not (boolean-from-<type> x))').")
   (xdoc::p
    "Because these rules may be applied to terms
     that result from execution and that must be checked not to be errors,
     we also add a rule saying that a call of @(tsee not) is not an error.
     Otherwise, terms of the form @('(errorp (not ...))')
     arise during symbolic execution and cause proofs to fail.")
   (xdoc::p
    "It may be better to change ATC to require
     a unique representation of the logical negation operator,
     and avoid these rules altogether.
     This approach will be considered in the future."))

  (defruled boolean-from-uchar-of-lognot-uchar
    (equal (boolean-from-uchar (lognot-uchar x))
           (not (boolean-from-uchar x)))
    :enable (boolean-from-uchar lognot-uchar))

  (defruled boolean-from-schar-of-lognot-schar
    (equal (boolean-from-schar (lognot-schar x))
           (not (boolean-from-schar x)))
    :enable (boolean-from-schar lognot-schar))

  (defruled boolean-from-ushort-of-lognot-ushort
    (equal (boolean-from-ushort (lognot-ushort x))
           (not (boolean-from-ushort x)))
    :enable (boolean-from-ushort lognot-ushort))

  (defruled boolean-from-sshort-of-lognot-sshort
    (equal (boolean-from-sshort (lognot-sshort x))
           (not (boolean-from-sshort x)))
    :enable (boolean-from-sshort lognot-sshort))

  (defruled boolean-from-uint-of-lognot-uint
    (equal (boolean-from-uint (lognot-uint x))
           (not (boolean-from-uint x)))
    :enable (boolean-from-uint lognot-uint))

  (defruled boolean-from-sint-of-lognot-sint
    (equal (boolean-from-sint (lognot-sint x))
           (not (boolean-from-sint x)))
    :enable (boolean-from-sint lognot-sint))

  (defruled boolean-from-ulong-of-lognot-ulong
    (equal (boolean-from-ulong (lognot-ulong x))
           (not (boolean-from-ulong x)))
    :enable (boolean-from-ulong lognot-ulong))

  (defruled boolean-from-slong-of-lognot-slong
    (equal (boolean-from-slong (lognot-slong x))
           (not (boolean-from-slong x)))
    :enable (boolean-from-slong lognot-slong))

  (defruled boolean-from-ullong-of-lognot-ullong
    (equal (boolean-from-ullong (lognot-ullong x))
           (not (boolean-from-ullong x)))
    :enable (boolean-from-ullong lognot-ullong))

  (defruled boolean-from-sllong-of-lognot-sllong
    (equal (boolean-from-sllong (lognot-sllong x))
           (not (boolean-from-sllong x)))
    :enable (boolean-from-sllong lognot-sllong))

  (defruled not-errorp-of-not
    (not (c::errorp (not x)))))

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

(defval *atc-not-rules*
  :short "List of rules related to @(tsee not)."
  '(boolean-from-uchar-of-lognot-uchar
    boolean-from-schar-of-lognot-schar
    boolean-from-ushort-of-lognot-ushort
    boolean-from-sshort-of-lognot-sshort
    boolean-from-uint-of-lognot-uint
    boolean-from-sint-of-lognot-sint
    boolean-from-ulong-of-lognot-ulong
    boolean-from-slong-of-lognot-slong
    boolean-from-ullong-of-lognot-ullong
    boolean-from-sllong-of-lognot-sllong
    not-errorp-of-not))

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

(defsection atc-integer-size-rules
  :short "Rules related to integer sizes."
  :long
  (xdoc::topstring
   (xdoc::p
    "These are the same as the linear rules,
     but they are rewrite rules."))

  (make-event
   `(defruled uchar-max-vs-sint-max-rewrite
      ,(if (<= (uchar-max) (sint-max))
           '(<= (uchar-max) (sint-max))
         '(> (uchar-max) (sint-max)))))

  (make-event
   `(defruled ushort-max-vs-sint-max-rewrite
      ,(if (<= (ushort-max) (sint-max))
           '(<= (ushort-max) (sint-max))
         '(> (ushort-max) (sint-max)))))

  (make-event
   `(defruled uchar-max-vs-slong-max-rewrite
      ,(if (<= (uchar-max) (slong-max))
           '(<= (uchar-max) (slong-max))
         '(> (uchar-max) (slong-max)))))

  (make-event
   `(defruled ushort-max-vs-slong-max-rewrite
      ,(if (<= (ushort-max) (slong-max))
           '(<= (ushort-max) (slong-max))
         '(> (ushort-max) (slong-max)))))

  (make-event
   `(defruled uint-max-vs-slong-max-rewrite
      ,(if (<= (uint-max) (slong-max))
           '(<= (uint-max) (slong-max))
         '(> (uint-max) (slong-max)))))

  (make-event
   `(defruled uchar-max-vs-sllong-max-rewrite
      ,(if (<= (uchar-max) (sllong-max))
           '(<= (uchar-max) (sllong-max))
         '(> (uchar-max) (sllong-max)))))

  (make-event
   `(defruled ushort-max-vs-sllong-max-rewrite
      ,(if (<= (ushort-max) (sllong-max))
           '(<= (ushort-max) (sllong-max))
         '(> (ushort-max) (sllong-max)))))

  (make-event
   `(defruled uint-max-vs-sllong-max-rewrite
      ,(if (<= (uint-max) (sllong-max))
           '(<= (uint-max) (sllong-max))
         '(> (uint-max) (sllong-max)))))

  (make-event
   `(defruled ulong-max-vs-sllong-max-rewrute
      ,(if (<= (ulong-max) (sllong-max))
           '(<= (ulong-max) (sllong-max))
         '(> (ulong-max) (sllong-max))))))

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

(defval *atc-integer-size-rules*
  :short "List of rules related to integer sizes."
  '(uchar-max-vs-sint-max-rewrite
    ushort-max-vs-sint-max-rewrite
    uchar-max-vs-slong-max-rewrite
    ushort-max-vs-slong-max-rewrite
    uint-max-vs-slong-max-rewrite
    uchar-max-vs-sllong-max-rewrite
    ushort-max-vs-sllong-max-rewrite
    uint-max-vs-sllong-max-rewrite
    ulong-max-vs-sllong-max-rewrute))

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

(defsection atc-other-rewrite-rules
  :short "Other rewrite rules for the proofs generated by ATC."
  :long
  (xdoc::topstring
   (xdoc::p
    "These are designated as `other' with respect to the rewrite rules
     for openers etc., which are collected separately.")
   (xdoc::p
    "During symbolic execution, certain term patterns appear,
     which are amenable to simplification via the following rewrite rules.")
   (xdoc::p
    "The following rules are general
     and should be probably moved to a more general place.
     For now we put them here, disabled.")
   (xdoc::p
    "Some of the following rewrite rules, in combinations with external ones,
     may exhibit backchaining circularities.
     However, it looks like ACL2's ancestor checks
     should avoid actual circularities,
     in effect limiting the application of
     different partial ``arcs'' of the circles in different situations.
     Anyways, this is being flagged here as something to watch for.")
   (xdoc::p
    "The rule @('ifix-when-integerp') serves to simplify away
     occurrences of @(tsee ifix) used in the definition of the shift operations,
     in combination with the return type theorems of
     the @('<type>-integer-value') functions, which return @(tsee integerp).")
   (xdoc::p
    "The rule @('len-of-cons') below
     is a duplicate of @('acl2::len-of-cons')
     from at least two list libraries,
     but this way we avoid having this file depend on those list libraries;
     the theorem is very simple and small,
     so it is not a lot of duplication.")
   (xdoc::p
    "We also have two rules to simplify applications of
     @(tsee boolean-from-sint) to @('(sint 0)') and @('(sint 1)').
     These applications appear during symbolic execution,
     because in C certain ``boolean'' expressions produce those @('int') values,
     and @(tsee boolean-from-sint) is used to turn those into ACL2 booleans,
     which are uses in @(tsee if)s,
     and thus we clearly want to simplify those application
     to @('t') and @('nil'), which further simplifies the @(tsee if)s.")
   (xdoc::p
    "We also have two rules to simplify applications of
     @(tsee lognot-sint) to @('(sint 0)') and @('(sint 1)').
     Terms of this form may arise in the process of simplifying
     C non-strict expressions involving @('&&') and @('||').")
   (xdoc::p
    "We also found it necessary to include rules
     to distribute two specific functions over @(tsee if)s.
     It seems that, in the course of these symbolic execution proofs,
     we will always want to distribute functions over @(tsee if)s.
     This distribution happens at the goal level,
     but not in the rewriter by default.")
   (xdoc::p
    "The two @('not-zp-of-limit-...') rules
     serve to relieve the recurring hypothesis
     that the limit is never 0 during the symbolic execution.
     Initially the limit is a variable, and the first rule applies;
     the hypothesis of this rule is easily discharged by
     the inequality assumption over the initial limit
     in the symbolic execution theorem,
     via ACL2's linear arithmetic.
     The @(tsee syntaxp) hypothesis restricts the application of the rule
     to the case in which the limit is a variable (which is true initially).
     As the symbolic execution proceeds,
     1 gets repeatedly subtracted from the initial limit variable,
     and it appears that ACL2 automatically combines multiple 1s
     into constants larger than 1,
     giving the pattern @('(binary-+ \'<negative-integer> <limit-variable>)').
     This is the pattern in the second rule @('not-zp-of-limit-...'),
     whose hypothesis about the limit variable
     is easily discharged via linear arithmetic."))

  (defruled ifix-when-integerp
    (implies (integerp x)
             (equal (ifix x) x)))

  (defruled not-zp-of-limit-variable
    (implies (and (syntaxp (symbolp limit))
                  (integerp limit)
                  (> limit 0))
             (not (zp limit))))

  (defruled not-zp-of-limit-minus-const
    (implies (and (syntaxp (quotep -c))
                  (integerp -c)
                  (< -c 0)
                  (integerp limit)
                  (> limit (- -c)))
             (not (zp (binary-+ -c limit)))))

  (defruled value-result-fix-when-valuep
    (implies (valuep x)
             (equal (value-result-fix x)
                    x)))

  (defruled not-errorp-when-valuep-rewrite
    (implies (valuep x)
             (not (errorp x)))
    :enable (errorp
             valuep))

  (defruled not-errorp-when-value-listp-rewrite
    (implies (value-listp x)
             (not (errorp x)))
    :enable errorp)

  (defruled not-errorp-when-scopep
    (implies (scopep x)
             (not (errorp x)))
    :enable (errorp scopep))

  (defruled not-errorp-when-scope-listp
    (implies (scope-listp x)
             (not (errorp x)))
    :enable errorp)

  (defruled not-errorp-when-schar-arrayp
    (implies (schar-arrayp x)
             (not (errorp x)))
    :enable (errorp schar-arrayp))

  (defruled not-errorp-when-uchar-arrayp
    (implies (uchar-arrayp x)
             (not (errorp x)))
    :enable (errorp uchar-arrayp))

  (defruled not-errorp-when-sshort-arrayp
    (implies (sshort-arrayp x)
             (not (errorp x)))
    :enable (errorp sshort-arrayp))

  (defruled not-errorp-when-ushort-arrayp
    (implies (ushort-arrayp x)
             (not (errorp x)))
    :enable (errorp ushort-arrayp))

  (defruled not-errorp-when-sint-arrayp
    (implies (sint-arrayp x)
             (not (errorp x)))
    :enable (errorp sint-arrayp))

  (defruled not-errorp-when-uint-arrayp
    (implies (uint-arrayp x)
             (not (errorp x)))
    :enable (errorp uint-arrayp))

  (defruled not-errorp-when-slong-arrayp
    (implies (slong-arrayp x)
             (not (errorp x)))
    :enable (errorp slong-arrayp))

  (defruled not-errorp-when-ulong-arrayp
    (implies (ulong-arrayp x)
             (not (errorp x)))
    :enable (errorp ulong-arrayp))

  (defruled not-errorp-when-sllong-arrayp
    (implies (sllong-arrayp x)
             (not (errorp x)))
    :enable (errorp sllong-arrayp))

  (defruled not-errorp-when-ullong-arrayp
    (implies (ullong-arrayp x)
             (not (errorp x)))
    :enable (errorp ullong-arrayp))

  (defruled not-errorp-when-booleanp
    (implies (booleanp x)
             (not (errorp x)))
    :enable errorp)

  (defruled boolean-from-sint-of-0
    (equal (boolean-from-sint (sint 0)) nil))

  (defruled boolean-from-sint-of-1
    (equal (boolean-from-sint (sint 1)) t))

  (defruled lognot-sint-of-0
    (equal (lognot-sint (sint 0))
           (sint 1)))

  (defruled lognot-sint-of-1
    (equal (lognot-sint (sint 1))
           (sint 0))))

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

(defval *atc-other-rewrite-rules*
  :short "List of rewrite rules proved in @(see atc-other-rewrite-rules)."
  '(ifix-when-integerp
    not-zp-of-limit-variable
    not-zp-of-limit-minus-const
    value-result-fix-when-valuep
    not-errorp-when-valuep-rewrite
    not-errorp-when-value-listp-rewrite
    not-errorp-when-scopep
    not-errorp-when-scope-listp
    not-errorp-when-schar-arrayp
    not-errorp-when-uchar-arrayp
    not-errorp-when-sshort-arrayp
    not-errorp-when-ushort-arrayp
    not-errorp-when-sint-arrayp
    not-errorp-when-uint-arrayp
    not-errorp-when-slong-arrayp
    not-errorp-when-ulong-arrayp
    not-errorp-when-sllong-arrayp
    not-errorp-when-ullong-arrayp
    not-errorp-when-booleanp
    boolean-from-sint-of-0
    boolean-from-sint-of-1
    lognot-sint-of-0
    lognot-sint-of-1))

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

(defval *atc-integer-ops-1-return-rewrite-rules*
  :short "List of rewrite rules for the return types of
          models of C integer operations that involve one C integer type."
  (b* ((ops '(plus minus bitnot lognot)))
    (atc-integer-ops-1-return-names-loop-ops ops
                                             *integer-nonbool-nonchar-types*))

  :prepwork

  ((define atc-integer-ops-1-return-names-loop-types ((op symbolp)
                                                      (types type-listp))
     :guard (and (member-eq op '(plus minus bitnot lognot))
                 (type-integer-listp types))
     :returns (names symbol-listp)
     :parents nil
     (cond
      ((endp types) nil)
      (t (b* ((type (car types))
              (argfixtype (integer-type-to-fixtype type))
              (restype (if (eq op 'lognot) (type-sint) (promote-type type)))
              (resfixtype (integer-type-to-fixtype restype))
              (respred (pack resfixtype 'p)))
           (cons (pack respred '-of- op '- argfixtype)
                 (atc-integer-ops-1-return-names-loop-types op (cdr types)))))))

   (define atc-integer-ops-1-return-names-loop-ops ((ops symbol-listp)
                                                    (types type-listp))
     :guard (and (subsetp-eq ops '(plus minus bitnot lognot))
                 (type-integer-listp types))
     :returns (names symbol-listp)
     :parents nil
     (cond ((endp ops) nil)
           (t (append
               (atc-integer-ops-1-return-names-loop-types (car ops) types)
               (atc-integer-ops-1-return-names-loop-ops (cdr ops) types)))))))

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

(defval *atc-integer-ops-2-return-rewrite-rules*
  :short "List of rewrite rules for the return types of
          models of C integer operations that involve two C integer types."
  (b* ((ops (list 'add 'sub 'mul 'div 'rem
                  'shl 'shr
                  'lt 'gt 'le 'ge 'eq 'ne
                  'bitand 'bitxor 'bitior)))
    (atc-integer-ops-2-return-names-loop-ops ops
                                             *integer-nonbool-nonchar-types*
                                             *integer-nonbool-nonchar-types*))

  :prepwork

  ((define atc-integer-ops-2-return-names-loop-right-types ((op symbolp)
                                                            (ltype typep)
                                                            (rtypes type-listp))
     :guard (and (member-eq op (list 'add 'sub 'mul 'div 'rem
                                     'shl 'shr
                                     'lt 'gt 'le 'ge 'eq 'ne
                                     'bitand 'bitxor 'bitior))
                 (type-integerp ltype)
                 (type-integer-listp rtypes))
     :returns (names symbol-listp)
     :parents nil
     (cond
      ((endp rtypes) nil)
      (t (b* ((rtype (car rtypes))
              (type (cond ((member-eq op '(lt gt le ge eq ne)) (type-sint))
                          ((member-eq op '(shl shr)) (promote-type ltype))
                          (t (uaconvert-types ltype rtype))))
              (lfixtype (integer-type-to-fixtype ltype))
              (rfixtype (integer-type-to-fixtype rtype))
              (fixtype (integer-type-to-fixtype type))
              (pred (pack fixtype 'p)))
           (cons
            (pack pred '-of- op '- lfixtype '- rfixtype)
            (atc-integer-ops-2-return-names-loop-right-types op
                                                             ltype
                                                             (cdr rtypes))))))
     :guard-hints (("Goal" :in-theory (enable type-arithmeticp type-realp))))

   (define atc-integer-ops-2-return-names-loop-left-types ((op symbolp)
                                                           (ltypes type-listp)
                                                           (rtypes type-listp))
     :guard (and (member-eq op (list 'add 'sub 'mul 'div 'rem
                                     'shl 'shr
                                     'lt 'gt 'le 'ge 'eq 'ne
                                     'bitand 'bitxor 'bitior))
                 (type-integer-listp ltypes)
                 (type-integer-listp rtypes))
     :returns (names symbol-listp)
     :parents nil
     (cond ((endp ltypes) nil)
           (t (append
               (atc-integer-ops-2-return-names-loop-right-types op
                                                                (car ltypes)
                                                                rtypes)
               (atc-integer-ops-2-return-names-loop-left-types op
                                                               (cdr ltypes)
                                                               rtypes)))))

   (define atc-integer-ops-2-return-names-loop-ops ((ops symbol-listp)
                                                    (ltypes type-listp)
                                                    (rtypes type-listp))
     :guard (and (subsetp-eq ops (list 'add 'sub 'mul 'div 'rem
                                       'shl 'shr
                                       'lt 'gt 'le 'ge 'eq 'ne
                                       'bitand 'bitxor 'bitior))
                 (type-integer-listp ltypes)
                 (type-integer-listp rtypes))
     :returns (names symbol-listp)
     :parents nil
     (cond ((endp ops) nil)
           (t (append
               (atc-integer-ops-2-return-names-loop-left-types (car ops)
                                                               ltypes
                                                               rtypes)
               (atc-integer-ops-2-return-names-loop-ops (cdr ops)
                                                        ltypes
                                                        rtypes)))))))

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

(defval *atc-integer-convs-return-rewrite-rules*
  :short "List of rewrite rules for the return types of
          models of C integer conversions."
  (atc-integer-convs-return-names-loop-src-types
   *integer-nonbool-nonchar-types*
   *integer-nonbool-nonchar-types*)

  :prepwork

  ((define atc-integer-convs-return-names-loop-dst-types ((stype typep)
                                                          (dtypes type-listp))
     :guard (and (type-integerp stype)
                 (type-integer-listp dtypes))
     :returns (names symbol-listp)
     :parents nil
     (cond
      ((endp dtypes) nil)
      ((equal stype (car dtypes))
       (atc-integer-convs-return-names-loop-dst-types stype
                                                      (cdr dtypes)))
      (t (b* ((sfixtype (integer-type-to-fixtype stype))
              (dfixtype (integer-type-to-fixtype (car dtypes)))
              (pred (pack dfixtype 'p)))
           (cons
            (pack pred '-of- dfixtype '-from- sfixtype)
            (atc-integer-convs-return-names-loop-dst-types stype
                                                           (cdr dtypes)))))))

   (define atc-integer-convs-return-names-loop-src-types ((stypes type-listp)
                                                          (dtypes type-listp))
     :guard (and (type-integer-listp stypes)
                 (type-integer-listp dtypes))
     :returns (names symbol-listp)
     :parents nil
     (cond ((endp stypes) nil)
           (t (append
               (atc-integer-convs-return-names-loop-dst-types (car stypes)
                                                              dtypes)
               (atc-integer-convs-return-names-loop-src-types (cdr stypes)
                                                              dtypes)))))))

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

(defval *atc-array-read-return-rewrite-rules*
  :short "List of rewrite rules for the return types of
          models of C array read operations."
  (atc-array-read-return-names-loop-array-types *integer-nonbool-nonchar-types*
                                                *integer-nonbool-nonchar-types*)

  :prepwork

  ((define atc-array-read-return-names-loop-index-types ((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)))
              (pred (pack afixtype 'p)))
           (cons
            (pack pred '-of- afixtype '-array-read- ifixtype)
            (atc-array-read-return-names-loop-index-types atype
                                                          (cdr itypes)))))))

   (define atc-array-read-return-names-loop-array-types ((atypes type-listp)
                                                         (itypes type-listp))
     :guard (and (type-integer-listp atypes)
                 (type-integer-listp itypes))
     :returns (names symbol-listp)
     :parents nil
     (cond ((endp atypes) nil)
           (t (append
               (atc-array-read-return-names-loop-index-types (car atypes)
                                                             itypes)
               (atc-array-read-return-names-loop-array-types (cdr atypes)
                                                             itypes)))))))

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

(defval *atc-array-write-return-rewrite-rules*
  :short "List of rewrite rules for the return types of
          models of C array write operations."
  (atc-array-write-return-names-loop-array-types
   *integer-nonbool-nonchar-types*
   *integer-nonbool-nonchar-types*)

  :prepwork

  ((define atc-array-write-return-names-loop-index-types ((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)))
              (pred (pack afixtype '-arrayp)))
           (cons
            (pack pred '-of- afixtype '-array-write- ifixtype)
            (atc-array-write-return-names-loop-index-types atype
                                                           (cdr itypes)))))))

   (define atc-array-write-return-names-loop-array-types ((atypes type-listp)
                                                          (itypes type-listp))
     :guard (and (type-integer-listp atypes)
                 (type-integer-listp itypes))
     :returns (names symbol-listp)
     :parents nil
     (cond ((endp atypes) nil)
           (t (append
               (atc-array-write-return-names-loop-index-types (car atypes)
                                                              itypes)
               (atc-array-write-return-names-loop-array-types (cdr atypes)
                                                              itypes)))))))

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

(defval *atc-more-rewrite-rules*
  :short "List of more rewrite rules for the proofs generated by ATC."
  :long
  (xdoc::topstring
   (xdoc::p
    "These are rewrite rules in addition to
     the ones in @(see atc-other-rewrite-rules).
     We definitely need better nomenclature than `more' and `other'."))
  '(booleanp-of-boolean-from-uchar
    booleanp-of-boolean-from-schar
    booleanp-of-boolean-from-ushort
    booleanp-of-boolean-from-sshort
    booleanp-of-boolean-from-uint
    booleanp-of-boolean-from-sint
    booleanp-of-boolean-from-ulong
    booleanp-of-boolean-from-slong
    booleanp-of-boolean-from-ullong
    booleanp-of-boolean-from-sllong
    integerp-of-schar-integer-value
    integerp-of-uchar-integer-value
    integerp-of-sshort-integer-value
    integerp-of-ushort-integer-value
    integerp-of-sint-integer-value
    integerp-of-uint-integer-value
    integerp-of-slong-integer-value
    integerp-of-ulong-integer-value
    integerp-of-sllong-integer-value
    integerp-of-ullong-integer-value
    car-cons
    cdr-cons
    compustate-fix-when-compustatep
    compustatep-of-add-frame
    compustatep-of-enter-scope
    compustatep-of-add-var
    compustatep-of-update-var
    compustatep-of-update-object
    compustatep-when-compustate-resultp-and-not-errorp
    compustate-resultp-of-write-var
    heap-fix-when-heapp
    heapp-of-compustate->heap
    mv-nth-of-cons
    not-errorp-when-compustatep
    omap::in-of-update
    scopep-of-update
    schar-fix-when-scharp
    uchar-fix-when-ucharp
    sshort-fix-when-sshortp
    ushort-fix-when-ushortp
    sint-fix-when-sintp
    uint-fix-when-uintp
    slong-fix-when-slongp
    ulong-fix-when-ulongp
    sllong-fix-when-sllongp
    ullong-fix-when-ullongp
    scharp-of-schar
    ucharp-of-uchar
    sshortp-of-sshort
    ushortp-of-ushort
    sintp-of-sint
    uintp-of-uint
    slongp-of-slong
    ulongp-of-ulong
    sllongp-of-sllong
    ullongp-of-ullong
    value-fix-when-valuep
    value-list-fix-of-cons))

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

(defval *atc-integer-ops-1-type-prescription-rules*
  :short "List of type prescription rules for the
          models of C integer operations that involve one C integer type."
  (b* ((ops '(plus minus bitnot lognot)))
    (atc-integer-ops-1-type-presc-rules-loop-ops
     ops
     *integer-nonbool-nonchar-types*))

  :prepwork

  ((define atc-integer-ops-1-type-presc-rules-loop-types ((op symbolp)
                                                          (types type-listp))
     :guard (and (member-eq op '(plus minus bitnot lognot))
                 (type-integer-listp types))
     :returns (rules true-list-listp)
     :parents nil
     (cond
      ((endp types) nil)
      (t (b* ((type (car types))
              (fixtype (integer-type-to-fixtype type)))
           (cons
            (list :t (pack op '- fixtype))
            (atc-integer-ops-1-type-presc-rules-loop-types op (cdr types)))))))

   (define atc-integer-ops-1-type-presc-rules-loop-ops ((ops symbol-listp)
                                                        (types type-listp))
     :guard (and (subsetp-eq ops '(plus minus bitnot lognot))
                 (type-integer-listp types))
     :returns (rule true-list-listp)
     :parents nil
     (cond
      ((endp ops) nil)
      (t (append
          (atc-integer-ops-1-type-presc-rules-loop-types (car ops) types)
          (atc-integer-ops-1-type-presc-rules-loop-ops (cdr ops) types)))))))

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

(defval *atc-integer-ops-2-type-prescription-rules*
  :short "List of type prescription rules for the
          models of C integer operations that involve two C integer types."
  (b* ((ops (list 'add 'sub 'mul 'div 'rem
                  'shl 'shr
                  'lt 'gt 'le 'ge 'eq 'ne
                  'bitand 'bitxor 'bitior)))
    (atc-integer-ops-2-type-presc-rules-loop-ops
     ops
     *integer-nonbool-nonchar-types*
     *integer-nonbool-nonchar-types*))

  :prepwork

  ((define atc-integer-ops-2-type-presc-rules-loop-right-types
     ((op symbolp)
      (ltype typep)
      (rtypes type-listp))
     :guard (and (member-eq op (list 'add 'sub 'mul 'div 'rem
                                     'shl 'shr
                                     'lt 'gt 'le 'ge 'eq 'ne
                                     'bitand 'bitxor 'bitior))
                 (type-integerp ltype)
                 (type-integer-listp rtypes))
     :returns (rules true-list-listp)
     :parents nil
     (cond
      ((endp rtypes) nil)
      (t (b* ((rtype (car rtypes))
              (lfixtype (integer-type-to-fixtype ltype))
              (rfixtype (integer-type-to-fixtype rtype)))
           (cons
            (list :t (pack op '- lfixtype '- rfixtype))
            (atc-integer-ops-2-type-presc-rules-loop-right-types
             op
             ltype
             (cdr rtypes))))))
     :guard-hints (("Goal" :in-theory (enable type-arithmeticp type-realp))))

   (define atc-integer-ops-2-type-presc-rules-loop-left-types
     ((op symbolp)
      (ltypes type-listp)
      (rtypes type-listp))
     :guard (and (member-eq op (list 'add 'sub 'mul 'div 'rem
                                     'shl 'shr
                                     'lt 'gt 'le 'ge 'eq 'ne
                                     'bitand 'bitxor 'bitior))
                 (type-integer-listp ltypes)
                 (type-integer-listp rtypes))
     :returns (rules true-list-listp)
     :parents nil
     (cond ((endp ltypes) nil)
           (t (append
               (atc-integer-ops-2-type-presc-rules-loop-right-types op
                                                                    (car ltypes)
                                                                    rtypes)
               (atc-integer-ops-2-type-presc-rules-loop-left-types op
                                                                   (cdr ltypes)
                                                                   rtypes)))))

   (define atc-integer-ops-2-type-presc-rules-loop-ops ((ops symbol-listp)
                                                        (ltypes type-listp)
                                                        (rtypes type-listp))
     :guard (and (subsetp-eq ops (list 'add 'sub 'mul 'div 'rem
                                       'shl 'shr
                                       'lt 'gt 'le 'ge 'eq 'ne
                                       'bitand 'bitxor 'bitior))
                 (type-integer-listp ltypes)
                 (type-integer-listp rtypes))
     :returns (rules true-list-listp)
     :parents nil
     (cond ((endp ops) nil)
           (t (append
               (atc-integer-ops-2-type-presc-rules-loop-left-types (car ops)
                                                                   ltypes
                                                                   rtypes)
               (atc-integer-ops-2-type-presc-rules-loop-ops (cdr ops)
                                                            ltypes
                                                            rtypes)))))))

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

(defval *atc-integer-convs-type-prescription-rules*
  :short "List of type prescription rules for the
          models of C integer conversions."
  (atc-integer-convs-type-presc-rules-loop-src-types
   *integer-nonbool-nonchar-types*
   *integer-nonbool-nonchar-types*)

  :prepwork

  ((define atc-integer-convs-type-presc-rules-loop-dst-types
     ((stype typep)
      (dtypes type-listp))
     :guard (and (type-integerp stype)
                 (type-integer-listp dtypes))
     :returns (rules true-list-listp)
     :parents nil
     (cond
      ((endp dtypes) nil)
      ((equal stype (car dtypes))
       (atc-integer-convs-type-presc-rules-loop-dst-types stype
                                                          (cdr dtypes)))
      (t (b* ((sfixtype (integer-type-to-fixtype stype))
              (dfixtype (integer-type-to-fixtype (car dtypes))))
           (cons
            (list :t (pack dfixtype '-from- sfixtype))
            (atc-integer-convs-type-presc-rules-loop-dst-types
             stype
             (cdr dtypes)))))))

   (define atc-integer-convs-type-presc-rules-loop-src-types
     ((stypes type-listp)
      (dtypes type-listp))
     :guard (and (type-integer-listp stypes)
                 (type-integer-listp dtypes))
     :returns (rules true-list-listp)
     :parents nil
     (cond ((endp stypes) nil)
           (t (append
               (atc-integer-convs-type-presc-rules-loop-dst-types (car stypes)
                                                                  dtypes)
               (atc-integer-convs-type-presc-rules-loop-src-types (cdr stypes)
                                                                  dtypes)))))))

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

(defval *atc-array-read-type-prescription-rules*
  :short "List of type prescription rules for the
          models of C array read operations."
  (atc-array-read-type-presc-rules-loop-array-types
   *integer-nonbool-nonchar-types*
   *integer-nonbool-nonchar-types*)

  :prepwork

  ((define atc-array-read-type-presc-rules-loop-index-types
     ((atype typep) (itypes type-listp))
     :guard (and (type-integerp atype)
                 (type-integer-listp itypes))
     :returns (rules true-listp)
     :parents nil
     (cond
      ((endp itypes) nil)
      (t (b* ((afixtype (integer-type-to-fixtype atype))
              (ifixtype (integer-type-to-fixtype (car itypes))))
           (cons
            (list :t (pack afixtype '-array-read- ifixtype))
            (atc-array-read-type-presc-rules-loop-index-types atype
                                                              (cdr itypes)))))))

   (define atc-array-read-type-presc-rules-loop-array-types
     ((atypes type-listp) (itypes type-listp))
     :guard (and (type-integer-listp atypes)
                 (type-integer-listp itypes))
     :returns (rules true-listp)
     :parents nil
     (cond ((endp atypes) nil)
           (t (append
               (atc-array-read-type-presc-rules-loop-index-types (car atypes)
                                                                 itypes)
               (atc-array-read-type-presc-rules-loop-array-types (cdr atypes)
                                                                 itypes)))))))

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

(defval *atc-type-prescription-rules*
  :short "List of type prescription rules for the proofs generated by ATC."
  :long
  (xdoc::topstring
   (xdoc::p
    "In the dynamic semantics, the execution of statements and other entities
     returns @(tsee mv) values, which logically satisfy @(tsee consp);
     the negated application of @(tsee consp) to those execution functions
     comes up in certain subgoals,
     so a simple way to discharge those subgoals
     is to use the type prescription rules for those execution functions.")
   (xdoc::p
    "We also need rules about the constructors of C integer values
     and the C functions that represent C operations and conversions,
     including array read operations."))
  (append
   '((:t exec-expr-call-or-pure)
     (:t exec-fun)
     (:t exec-stmt)
     (:t exec-block-item)
     (:t exec-block-item-list)
     (:t schar)
     (:t uchar)
     (:t sshort)
     (:t ushort)
     (:t sint)
     (:t uint)
     (:t slong)
     (:t ulong)
     (:t sllong)
     (:t ullong))
   *atc-integer-ops-1-type-prescription-rules*
   *atc-integer-ops-2-type-prescription-rules*
   *atc-integer-convs-type-prescription-rules*
   *atc-array-read-type-prescription-rules*))

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

(defval *atc-compound-recognizer-rules*
  :short "List of compound recognizer rules for the proofs generated by ATC."
  :long
  (xdoc::topstring
   (xdoc::p
    "The type prescription rules in @(tsee *atc-type-prescription-rules*)
     cover all the shallowly embedded C expressions except for variables.
     In the scenarios explained in @(tsee *atc-type-prescription-rules*),
     we may need to establish that a variable is not @('nil'),
     which must follow from the guard hypotheses.
     For this, we use the compound recognizer rule below.
     The fact that the type is @(tsee consp) is actually not important;
     what is important is that it does not include @('nil'),
     i.e. it is logically true."))
  '(consp-when-scharp
    consp-when-ucharp
    consp-when-sshortp
    consp-when-ushortp
    consp-when-sintp
    consp-when-uintp
    consp-when-slongp
    consp-when-ulongp
    consp-when-sllongp
    consp-when-ullongp))

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

(defval *atc-all-rules*
  :short "List of all the (generic) rules for the proofs generated by ATC."
  :long
  (xdoc::topstring
   (xdoc::p
    "These are the ones used in all the generated proofs.
     In addition, each proof includes a few additional rules
     that depend on the specific C-representing ACL2 functions involved.
     See @(see atc-implementation)."))
  (append *atc-symbolic-computation-state-rules*
          *atc-tyname-to-type-rules*
          *atc-valuep-rules*
          *atc-value-listp-rules*
          *atc-value-optionp-rules*
          *atc-type-of-value-rules*
          *atc-type-of-value-option-rules*
          *atc-value-array->elemtype-rules*
          *atc-array-length-rules*
          *atc-array-length-write-rules*
          *atc-exec-ident-rules*
          *atc-exec-const-rules*
          *atc-exec-arrsub-rules*
          *atc-exec-unary-rules*
          *atc-exec-cast-rules*
          *atc-exec-binary-strict-pure-rules*
          *atc-exec-test-rules*
          *atc-exec-expr-pure-rules*
          *atc-exec-expr-pure-list-rules*
          *atc-exec-expr-call-rules*
          *atc-exec-expr-call-or-pure-rules*
          *atc-exec-expr-asg-rules*
          *atc-exec-expr-call-or-asg-rules*
          *atc-exec-fun-rules*
          *atc-exec-stmt-rules*
          *atc-exec-initer-rules*
          *atc-exec-block-item-rules*
          *atc-exec-block-item-list-rules*
          *atc-init-scope-rules*
          *atc-other-executable-counterpart-rules*
          *atc-other-definition-rules*
          *atc-distributivity-over-if-rewrite-rules*
          *atc-identifier-rules*
          *atc-not-rules*
          *atc-integer-size-rules*
          *atc-other-rewrite-rules*
          *atc-integer-ops-1-return-rewrite-rules*
          *atc-integer-ops-2-return-rewrite-rules*
          *atc-integer-convs-return-rewrite-rules*
          *atc-array-read-return-rewrite-rules*
          *atc-array-write-return-rewrite-rules*
          *atc-more-rewrite-rules*
          *atc-type-prescription-rules*
          *atc-compound-recognizer-rules*
          *integer-value-disjoint-rules*
          *array-value-disjoint-rules*))

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

; We define a theory for the rules because experiments show that
; a long time is spent by ACL2 translating hints,
; given that *ATC-ALL-RULES* consists of thousands of rules.
; We use this theory in the generated proofs (see generation.lisp).

(deftheory atc-all-rules *atc-all-rules*)