		Search-engine friendly clone of the ACL2 documentation.

Proof-generation-theorems

Exec-congruence-theorems

Congruence theorems about execution.

These are not congruence rules in the ACL2 technical sense, but they are theorems expressing congruence-like properties: given two constructs (before and after a transformation, i.e. old and new), if the executions of their sub-constucts are equivalent, then the executions of the super-constructa are equivalent. Here `equivalent' means the following: if the execution of the old construct does not yield an error, neither does the execution of the new construct, and the two return the same results.

The theorems for identifier expressions (i.e. variables) and constants are a bit different from the others, because those expressions have no sub-expressions. However, the form is fairly similar, given that difference. The theorem for variables has an additional hypothesis about the variable being in the computation state with a certain type, which serves to establish the assertion about the type.

The theorems make use of b* bindings to keep them more readable. The theorems include additional hypotheses, in some cases, to ensure that the constructs in question are amenable to our formal dynamic semantics of C, which currently only covers a subset.

The theorems include hypotheses about the execution of the old construct not yielding an error, and in some cases about the execution of the sub-constructs of the new construct (not the new construct itself) not yielding an error); they also include hypotheses about the sub-constructs yielding the same results. While in some cases the equality of the results of the sub-constructs and the hypotheses that the old construct does not yield an error imply already that the sub-constructs do not yield an error (also see exec-error-theorems), this is not quite the case for (pure) expressions, which return expression values of type c::expr-value. For flexibility, the theorems require the equality, for sub-expressions, not of their full expression values, but just for the values of those expression values (i.e. c::expr-value->value). Thus, we need explicit hypotheses that the expression values are not errors, because they are not readily implied by the equality of the values alone of the expression values. The flexibility is important, for instance, to handle the semantic equality of x + 0 and x, which return different expression values (but the same values), because x is an lvalue while x + 0 is not.

The theorems conclude that the new construct's execution does not yield an error either, and that its results are the same as the old construct's execution's. When these theorems are used in proof generation, the hypotheses about the new sub-constructs not yielding errors and about them returning the same results as the old ones are established via the proofs generated for the sub-constructs; and the conclusions serve for larger constructs, compositionally.

For non-strict constructs, we have multiple theorems, corresponding to which sub-constructs are actually executed.

For the C dynamic semantics execution functions that depend on function environments, we use potentially different function environments for the old vs. new constructs. We always use the same initial computation state for old and new constructs.

Definitions and Theorems

Theorem: expr-ident-congruence

(defthm expr-ident-congruence
 (b* ((expr (c::expr-ident var))
      ((mv old-eval old-compst)
       (c::exec-expr expr compst old-fenv limit))
      ((mv new-eval new-compst)
       (c::exec-expr expr compst new-fenv limit))
      (old-val (c::expr-value->value old-eval))
      (new-val (c::expr-value->value new-eval)))
  (implies (and (not (c::errorp old-eval))
                (c::compustate-has-var-with-type-p var type compst))
           (and (not (c::errorp new-eval))
                (iff old-eval new-eval)
                (equal old-val new-val)
                (equal old-compst new-compst)
                old-eval
                (equal (c::type-of-value old-val)
                       (c::type-fix type))))))

Theorem: expr-const-congruence

(defthm expr-const-congruence
  (b* ((expr (c::expr-const const))
       ((mv old-eval old-compst)
        (c::exec-expr expr compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr expr compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (iconst (c::const-int->get const))
       (type (c::check-iconst iconst)))
    (implies (and (equal (c::const-kind const) :int)
                  (c::typep type)
                  (not (c::errorp old-eval)))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  old-eval
                  (equal (c::type-of-value old-val)
                         type)))))

Theorem: expr-unary-congruence

(defthm expr-unary-congruence
  (b* ((old (c::expr-unary op old-arg))
       (new (c::expr-unary op new-arg))
       ((mv old-arg-eval old-arg-compst)
        (c::exec-expr old-arg compst old-fenv (1- limit)))
       ((mv new-arg-eval new-arg-compst)
        (c::exec-expr new-arg compst new-fenv (1- limit)))
       (old-arg-val (c::expr-value->value old-arg-eval))
       (new-arg-val (c::expr-value->value new-arg-eval))
       ((mv old-eval old-compst)
        (c::exec-expr old compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr new compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (type (c::type-of-value old-arg-val)))
    (implies (and (c::unop-nonpointerp op)
                  (not (c::errorp old-eval))
                  (not (c::errorp new-arg-eval))
                  (iff old-arg-eval new-arg-eval)
                  (equal old-arg-val new-arg-val)
                  (equal old-arg-compst new-arg-compst)
                  (c::type-nonchar-integerp type))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  old-eval
                  (equal (c::type-of-value old-val)
                         (if (equal (c::unop-kind op) :lognot)
                             (c::type-sint)
                           (c::promote-type type)))))))

Theorem: expr-cast-congruence

(defthm expr-cast-congruence
  (b* ((old (c::expr-cast tyname old-arg))
       (new (c::expr-cast tyname new-arg))
       ((mv old-arg-eval old-arg-compst)
        (c::exec-expr old-arg compst old-fenv (1- limit)))
       ((mv new-arg-eval new-arg-compst)
        (c::exec-expr new-arg compst new-fenv (1- limit)))
       (old-arg-val (c::expr-value->value old-arg-eval))
       (new-arg-val (c::expr-value->value new-arg-eval))
       ((mv old-eval old-compst)
        (c::exec-expr old compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr new compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (type (c::type-of-value old-arg-val))
       (type1 (c::tyname-to-type tyname)))
    (implies (and (not (c::errorp old-eval))
                  (not (c::errorp new-arg-eval))
                  (iff old-arg-eval new-arg-eval)
                  (equal old-arg-val new-arg-val)
                  (equal old-arg-compst new-arg-compst)
                  (c::type-nonchar-integerp type)
                  (c::type-nonchar-integerp type1))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  old-eval
                  (equal (c::type-of-value old-val)
                         type1)))))

Theorem: expr-binary-pure-strict-congruence

(defthm expr-binary-pure-strict-congruence
 (b* ((old (c::expr-binary op old-arg1 old-arg2))
      (new (c::expr-binary op new-arg1 new-arg2))
      ((mv old-arg1-eval old-arg1-compst)
       (c::exec-expr old-arg1 compst old-fenv (1- limit)))
      ((mv old-arg2-eval old-arg2-compst)
       (c::exec-expr old-arg2
                     old-arg1-compst old-fenv (1- limit)))
      ((mv new-arg1-eval new-arg1-compst)
       (c::exec-expr new-arg1 compst new-fenv (1- limit)))
      ((mv new-arg2-eval new-arg2-compst)
       (c::exec-expr new-arg2
                     new-arg1-compst new-fenv (1- limit)))
      (old-arg1-val (c::expr-value->value old-arg1-eval))
      (old-arg2-val (c::expr-value->value old-arg2-eval))
      (new-arg1-val (c::expr-value->value new-arg1-eval))
      (new-arg2-val (c::expr-value->value new-arg2-eval))
      ((mv old-eval old-compst)
       (c::exec-expr old compst old-fenv limit))
      ((mv new-eval new-compst)
       (c::exec-expr new compst new-fenv limit))
      (old-val (c::expr-value->value old-eval))
      (new-val (c::expr-value->value new-eval))
      (type1 (c::type-of-value old-arg1-val))
      (type2 (c::type-of-value old-arg2-val)))
  (implies (and (c::binop-purep op)
                (c::binop-strictp op)
                (c::expr-purep new-arg1)
                (c::expr-purep new-arg2)
                (not (c::errorp old-eval))
                (not (c::errorp new-arg1-eval))
                (not (c::errorp new-arg2-eval))
                (iff old-arg1-eval new-arg1-eval)
                (iff old-arg2-eval new-arg2-eval)
                (equal old-arg1-val new-arg1-val)
                (equal old-arg2-val new-arg2-val)
                (equal old-arg1-compst new-arg1-compst)
                (equal old-arg2-compst new-arg2-compst)
                (c::type-nonchar-integerp type1)
                (c::type-nonchar-integerp type2))
           (and (not (c::errorp new-eval))
                (iff old-eval new-eval)
                (equal old-val new-val)
                (equal old-compst new-compst)
                old-eval
                (equal (c::type-of-value old-val)
                       (cond ((member-equal (c::binop-kind op)
                                            '(:mul :div
                                                   :rem :add
                                                   :sub :bitand
                                                   :bitxor :bitior))
                              (c::uaconvert-types type1 type2))
                             ((member-equal (c::binop-kind op)
                                            '(:shl :shr))
                              (c::promote-type type1))
                             (t (c::type-sint))))))))

Theorem: expr-binary-logand-first-congruence

(defthm expr-binary-logand-first-congruence
  (b* ((old (c::expr-binary (c::binop-logand)
                            old-arg1 old-arg2))
       (new (c::expr-binary (c::binop-logand)
                            new-arg1 new-arg2))
       ((mv old-arg1-eval old-arg1-compst)
        (c::exec-expr old-arg1 compst old-fenv (1- limit)))
       ((mv new-arg1-eval new-arg1-compst)
        (c::exec-expr new-arg1 compst new-fenv (1- limit)))
       (old-arg1-val (c::expr-value->value old-arg1-eval))
       (new-arg1-val (c::expr-value->value new-arg1-eval))
       ((mv old-eval old-compst)
        (c::exec-expr old compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr new compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (type1 (c::type-of-value old-arg1-val)))
    (implies (and (not (c::errorp old-eval))
                  (not (c::errorp new-arg1-eval))
                  (iff old-arg1-eval new-arg1-eval)
                  (equal old-arg1-val new-arg1-val)
                  (equal old-arg1-compst new-arg1-compst)
                  (c::type-nonchar-integerp type1)
                  (not (c::test-value old-arg1-val)))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  (equal (c::type-of-value old-val)
                         (c::type-sint))))))

Theorem: expr-binary-logand-second-congruence

(defthm expr-binary-logand-second-congruence
  (b* ((old (c::expr-binary (c::binop-logand)
                            old-arg1 old-arg2))
       (new (c::expr-binary (c::binop-logand)
                            new-arg1 new-arg2))
       ((mv old-arg1-eval old-arg1-compst)
        (c::exec-expr old-arg1 compst old-fenv (1- limit)))
       ((mv old-arg2-eval old-arg2-compst)
        (c::exec-expr old-arg2
                      old-arg1-compst old-fenv (1- limit)))
       ((mv new-arg1-eval new-arg1-compst)
        (c::exec-expr new-arg1 compst new-fenv (1- limit)))
       ((mv new-arg2-eval new-arg2-compst)
        (c::exec-expr new-arg2
                      new-arg1-compst new-fenv (1- limit)))
       (old-arg1-val (c::expr-value->value old-arg1-eval))
       (old-arg2-val (c::expr-value->value old-arg2-eval))
       (new-arg1-val (c::expr-value->value new-arg1-eval))
       (new-arg2-val (c::expr-value->value new-arg2-eval))
       ((mv old-eval old-compst)
        (c::exec-expr old compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr new compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (type1 (c::type-of-value old-arg1-val))
       (type2 (c::type-of-value old-arg2-val)))
    (implies (and (not (c::errorp old-eval))
                  (not (c::errorp new-arg1-eval))
                  (not (c::errorp new-arg2-eval))
                  (iff old-arg1-eval new-arg1-eval)
                  (iff old-arg2-eval new-arg2-eval)
                  (equal old-arg1-val new-arg1-val)
                  (equal old-arg2-val new-arg2-val)
                  (equal old-arg1-compst new-arg1-compst)
                  (equal old-arg2-compst new-arg2-compst)
                  (c::type-nonchar-integerp type1)
                  (c::type-nonchar-integerp type2)
                  (c::test-value old-arg1-val))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  (equal (c::type-of-value old-val)
                         (c::type-sint))))))

Theorem: expr-binary-logor-first-congruence

(defthm expr-binary-logor-first-congruence
  (b* ((old (c::expr-binary (c::binop-logor)
                            old-arg1 old-arg2))
       (new (c::expr-binary (c::binop-logor)
                            new-arg1 new-arg2))
       ((mv old-arg1-eval old-arg1-compst)
        (c::exec-expr old-arg1 compst old-fenv (1- limit)))
       ((mv new-arg1-eval new-arg1-compst)
        (c::exec-expr new-arg1 compst new-fenv (1- limit)))
       (old-arg1-val (c::expr-value->value old-arg1-eval))
       (new-arg1-val (c::expr-value->value new-arg1-eval))
       ((mv old-eval old-compst)
        (c::exec-expr old compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr new compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (type1 (c::type-of-value old-arg1-val)))
    (implies (and (not (c::errorp old-eval))
                  (not (c::errorp new-arg1-eval))
                  (iff old-arg1-eval new-arg1-eval)
                  (equal old-arg1-val new-arg1-val)
                  (equal old-arg1-compst new-arg1-compst)
                  (c::type-nonchar-integerp type1)
                  (c::test-value old-arg1-val))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  (equal (c::type-of-value old-val)
                         (c::type-sint))))))

Theorem: expr-binary-logor-second-congruence

(defthm expr-binary-logor-second-congruence
  (b* ((old (c::expr-binary (c::binop-logor)
                            old-arg1 old-arg2))
       (new (c::expr-binary (c::binop-logor)
                            new-arg1 new-arg2))
       ((mv old-arg1-eval old-arg1-compst)
        (c::exec-expr old-arg1 compst old-fenv (1- limit)))
       ((mv old-arg2-eval old-arg2-compst)
        (c::exec-expr old-arg2
                      old-arg1-compst old-fenv (1- limit)))
       ((mv new-arg1-eval new-arg1-compst)
        (c::exec-expr new-arg1 compst new-fenv (1- limit)))
       ((mv new-arg2-eval new-arg2-compst)
        (c::exec-expr new-arg2
                      new-arg1-compst new-fenv (1- limit)))
       (old-arg1-val (c::expr-value->value old-arg1-eval))
       (old-arg2-val (c::expr-value->value old-arg2-eval))
       (new-arg1-val (c::expr-value->value new-arg1-eval))
       (new-arg2-val (c::expr-value->value new-arg2-eval))
       ((mv old-eval old-compst)
        (c::exec-expr old compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr new compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (type1 (c::type-of-value old-arg1-val))
       (type2 (c::type-of-value old-arg2-val)))
    (implies (and (not (c::errorp old-eval))
                  (not (c::errorp new-arg1-eval))
                  (not (c::errorp new-arg2-eval))
                  (iff old-arg1-eval new-arg1-eval)
                  (iff old-arg2-eval new-arg2-eval)
                  (equal old-arg1-val new-arg1-val)
                  (equal old-arg2-val new-arg2-val)
                  (equal old-arg1-compst new-arg1-compst)
                  (equal old-arg2-compst new-arg2-compst)
                  (c::type-nonchar-integerp type1)
                  (c::type-nonchar-integerp type2)
                  (not (c::test-value old-arg1-val)))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  (equal (c::type-of-value old-val)
                         (c::type-sint))))))

Theorem: expr-binary-asg-congruence

(defthm expr-binary-asg-congruence
  (b* ((old (c::expr-binary (c::binop-asg)
                            (c::expr-ident var)
                            old-arg))
       (new (c::expr-binary (c::binop-asg)
                            (c::expr-ident var)
                            new-arg))
       ((mv old-arg-eval old-arg-compst)
        (c::exec-expr old-arg compst old-fenv (1- limit)))
       ((mv new-arg-eval new-arg-compst)
        (c::exec-expr new-arg compst new-fenv (1- limit)))
       (old-arg-val (c::expr-value->value old-arg-eval))
       (new-arg-val (c::expr-value->value new-arg-eval))
       ((mv old-eval old-compst)
        (c::exec-expr old compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr new compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (val (c::read-object (c::objdesign-of-var var compst)
                            compst))
       (type (c::type-of-value old-arg-val)))
    (implies (and (not (c::errorp val))
                  (not (c::errorp old-eval))
                  (not (c::errorp new-arg-eval))
                  (iff old-arg-eval new-arg-eval)
                  (equal old-arg-val new-arg-val)
                  (equal old-arg-compst new-arg-compst)
                  (c::type-nonchar-integerp type))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  old-eval
                  (equal (c::type-of-value old-val)
                         type)))))

Theorem: expr-cond-true-congruence

(defthm expr-cond-true-congruence
  (b* ((old (c::expr-cond old-test old-then old-else))
       (new (c::expr-cond new-test new-then new-else))
       ((mv old-test-eval old-test-compst)
        (c::exec-expr old-test compst old-fenv (1- limit)))
       ((mv old-then-eval old-then-compst)
        (c::exec-expr old-then
                      old-test-compst old-fenv (1- limit)))
       ((mv new-test-eval new-test-compst)
        (c::exec-expr new-test compst new-fenv (1- limit)))
       ((mv new-then-eval new-then-compst)
        (c::exec-expr new-then
                      new-test-compst new-fenv (1- limit)))
       (old-test-val (c::expr-value->value old-test-eval))
       (old-then-val (c::expr-value->value old-then-eval))
       (new-test-val (c::expr-value->value new-test-eval))
       (new-then-val (c::expr-value->value new-then-eval))
       ((mv old-eval old-compst)
        (c::exec-expr old compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr new compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (type-test (c::type-of-value old-test-val))
       (type-then (c::type-of-value old-then-val)))
    (implies (and (not (c::errorp old-eval))
                  (not (c::errorp new-test-eval))
                  (not (c::errorp new-then-eval))
                  (iff old-test-eval new-test-eval)
                  (iff old-then-eval new-then-eval)
                  (equal old-test-val new-test-val)
                  (equal old-then-val new-then-val)
                  (equal old-test-compst new-test-compst)
                  (equal old-then-compst new-then-compst)
                  (c::type-nonchar-integerp type-test)
                  (c::type-nonchar-integerp type-then)
                  (c::test-value old-test-val))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  (equal (c::type-of-value old-val)
                         type-then)))))

Theorem: expr-cond-false-congruence

(defthm expr-cond-false-congruence
  (b* ((old (c::expr-cond old-test old-then old-else))
       (new (c::expr-cond new-test new-then new-else))
       ((mv old-test-eval old-test-compst)
        (c::exec-expr old-test compst old-fenv (1- limit)))
       ((mv old-else-eval old-else-compst)
        (c::exec-expr old-else
                      old-test-compst old-fenv (1- limit)))
       ((mv new-test-eval new-test-compst)
        (c::exec-expr new-test compst new-fenv (1- limit)))
       ((mv new-else-eval new-else-compst)
        (c::exec-expr new-else
                      new-test-compst new-fenv (1- limit)))
       (old-test-val (c::expr-value->value old-test-eval))
       (old-else-val (c::expr-value->value old-else-eval))
       (new-test-val (c::expr-value->value new-test-eval))
       (new-else-val (c::expr-value->value new-else-eval))
       ((mv old-eval old-compst)
        (c::exec-expr old compst old-fenv limit))
       ((mv new-eval new-compst)
        (c::exec-expr new compst new-fenv limit))
       (old-val (c::expr-value->value old-eval))
       (new-val (c::expr-value->value new-eval))
       (type-test (c::type-of-value old-test-val))
       (type-else (c::type-of-value old-else-val)))
    (implies (and (not (c::errorp old-eval))
                  (not (c::errorp new-test-eval))
                  (not (c::errorp new-else-eval))
                  (iff old-test-eval new-test-eval)
                  (iff old-else-eval new-else-eval)
                  (equal old-test-val new-test-val)
                  (equal old-else-val new-else-val)
                  (equal old-test-compst new-test-compst)
                  (equal old-else-compst new-else-compst)
                  (c::type-nonchar-integerp type-test)
                  (c::type-nonchar-integerp type-else)
                  (not (c::test-value old-test-val)))
             (and (not (c::errorp new-eval))
                  (iff old-eval new-eval)
                  (equal old-val new-val)
                  (equal old-compst new-compst)
                  (equal (c::type-of-value old-val)
                         type-else)))))

Theorem: initer-single-congruence

(defthm initer-single-congruence
  (b* ((old (c::initer-single old-expr))
       (new (c::initer-single new-expr))
       ((mv old-expr-eval old-expr-compst)
        (c::exec-expr old-expr compst old-fenv (1- limit)))
       ((mv new-expr-eval new-expr-compst)
        (c::exec-expr new-expr compst new-fenv (1- limit)))
       (old-expr-val (c::expr-value->value old-expr-eval))
       (new-expr-val (c::expr-value->value new-expr-eval))
       ((mv old-ival old-compst)
        (c::exec-initer old compst old-fenv limit))
       ((mv new-ival new-compst)
        (c::exec-initer new compst new-fenv limit))
       (type (c::type-of-value old-expr-val)))
    (implies (and (not (c::errorp old-ival))
                  (not (c::errorp new-expr-eval))
                  (iff old-expr-eval new-expr-eval)
                  (equal old-expr-val new-expr-val)
                  (equal old-expr-compst new-expr-compst)
                  (c::type-nonchar-integerp type))
             (and (not (c::errorp new-ival))
                  (equal old-ival new-ival)
                  (equal old-compst new-compst)
                  (equal (c::init-type-of-init-value old-ival)
                         (c::init-type-single type))))))

Theorem: stmt-null-congruence

(defthm stmt-null-congruence
  (b* ((old (c::stmt-null))
       (new (c::stmt-null))
       ((mv old-sval old-compst)
        (c::exec-stmt old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-stmt new compst new-fenv limit)))
    (implies (not (c::errorp old-sval))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      (insert nil nil))))))

Theorem: stmt-expr-congruence

(defthm stmt-expr-congruence
  (b* ((old (c::stmt-expr old-expr))
       (new (c::stmt-expr new-expr))
       ((mv old-expr-eval old-expr-compst)
        (c::exec-expr old-expr compst old-fenv (- limit 1)))
       ((mv new-expr-eval new-expr-compst)
        (c::exec-expr new-expr compst new-fenv (- limit 1)))
       (old-expr-val (c::expr-value->value old-expr-eval))
       (new-expr-val (c::expr-value->value new-expr-eval))
       ((mv old-sval old-compst)
        (c::exec-stmt old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-stmt new compst new-fenv limit)))
    (implies (and (not (c::errorp old-sval))
                  (not (c::errorp new-expr-eval))
                  (iff old-expr-eval new-expr-eval)
                  (equal old-expr-val new-expr-val)
                  (equal old-expr-compst new-expr-compst))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      (insert nil nil))))))

Theorem: stmt-return-value-congruence

(defthm stmt-return-value-congruence
  (b* ((old (c::stmt-return old-expr))
       (new (c::stmt-return new-expr))
       ((mv old-expr-eval old-expr-compst)
        (c::exec-expr old-expr compst old-fenv (1- limit)))
       ((mv new-expr-eval new-expr-compst)
        (c::exec-expr new-expr compst new-fenv (1- limit)))
       (old-expr-val (c::expr-value->value old-expr-eval))
       (new-expr-val (c::expr-value->value new-expr-eval))
       ((mv old-sval old-compst)
        (c::exec-stmt old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-stmt new compst new-fenv limit))
       (type (c::type-of-value old-expr-val)))
    (implies (and old-expr
                  new-expr (not (c::errorp old-sval))
                  (not (c::errorp new-expr-eval))
                  (iff old-expr-eval new-expr-eval)
                  (equal old-expr-val new-expr-val)
                  (equal old-expr-compst new-expr-compst)
                  (c::type-nonchar-integerp type))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (equal (c::stmt-value-kind old-sval)
                         :return)
                  (c::stmt-value-return->value? old-sval)
                  (in (c::type-option-of-stmt-value old-sval)
                      (insert type nil))))))

Theorem: stmt-return-novalue-congruence

(defthm stmt-return-novalue-congruence
  (b* ((old (c::stmt-return nil))
       (new (c::stmt-return nil))
       ((mv old-sval old-compst)
        (c::exec-stmt old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-stmt new compst new-fenv limit)))
    (implies (not (c::errorp old-sval))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (equal (c::stmt-value-kind old-sval)
                         :return)
                  (in (c::type-option-of-stmt-value old-sval)
                      (insert (c::type-void) nil))))))

Theorem: stmt-if-true-congruence

(defthm stmt-if-true-congruence
  (b* ((old (c::stmt-if old-test old-then))
       (new (c::stmt-if new-test new-then))
       ((mv old-test-eval old-test-compst)
        (c::exec-expr old-test compst old-fenv (1- limit)))
       ((mv new-test-eval new-test-compst)
        (c::exec-expr new-test compst new-fenv (1- limit)))
       (old-test-val (c::expr-value->value old-test-eval))
       (new-test-val (c::expr-value->value new-test-eval))
       ((mv old-then-sval old-then-compst)
        (c::exec-stmt old-then
                      old-test-compst old-fenv (1- limit)))
       ((mv new-then-sval new-then-compst)
        (c::exec-stmt new-then
                      new-test-compst new-fenv (1- limit)))
       ((mv old-sval old-compst)
        (c::exec-stmt old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-stmt new compst new-fenv limit))
       (type (c::type-of-value old-test-val)))
    (implies (and (not (c::errorp old-sval))
                  (not (c::errorp new-test-eval))
                  (not (c::errorp new-then-sval))
                  (iff old-test-eval new-test-eval)
                  (equal old-test-val new-test-val)
                  (equal old-test-compst new-test-compst)
                  (equal old-then-sval new-then-sval)
                  (equal old-then-compst new-then-compst)
                  (c::test-value old-test-val)
                  (c::type-nonchar-integerp type)
                  (in (c::type-option-of-stmt-value old-then-sval)
                      types))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      types)))))

Theorem: stmt-if-false-congruence

(defthm stmt-if-false-congruence
  (b* ((old (c::stmt-if old-test old-then))
       (new (c::stmt-if new-test new-then))
       ((mv old-test-eval old-test-compst)
        (c::exec-expr old-test compst old-fenv (1- limit)))
       ((mv new-test-eval new-test-compst)
        (c::exec-expr new-test compst new-fenv (1- limit)))
       (old-test-val (c::expr-value->value old-test-eval))
       (new-test-val (c::expr-value->value new-test-eval))
       ((mv old-sval old-compst)
        (c::exec-stmt old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-stmt new compst new-fenv limit))
       (type (c::type-of-value old-test-val)))
    (implies (and (not (c::errorp old-sval))
                  (not (c::errorp new-test-eval))
                  (iff old-test-eval new-test-eval)
                  (equal old-test-val new-test-val)
                  (equal old-test-compst new-test-compst)
                  (not (c::test-value old-test-val))
                  (c::type-nonchar-integerp type))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      (insert nil nil))))))

Theorem: stmt-ifelse-true-congruence

(defthm stmt-ifelse-true-congruence
  (b* ((old (c::stmt-ifelse old-test old-then old-else))
       (new (c::stmt-ifelse new-test new-then new-else))
       ((mv old-test-eval old-test-compst)
        (c::exec-expr old-test compst old-fenv (1- limit)))
       ((mv new-test-eval new-test-compst)
        (c::exec-expr new-test compst new-fenv (1- limit)))
       (old-test-val (c::expr-value->value old-test-eval))
       (new-test-val (c::expr-value->value new-test-eval))
       ((mv old-then-sval old-then-compst)
        (c::exec-stmt old-then
                      old-test-compst old-fenv (1- limit)))
       ((mv new-then-sval new-then-compst)
        (c::exec-stmt new-then
                      new-test-compst new-fenv (1- limit)))
       ((mv old-sval old-compst)
        (c::exec-stmt old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-stmt new compst new-fenv limit))
       (type (c::type-of-value old-test-val)))
    (implies (and (not (c::errorp old-sval))
                  (not (c::errorp new-test-eval))
                  (not (c::errorp new-then-sval))
                  (iff old-test-eval new-test-eval)
                  (equal old-test-val new-test-val)
                  (equal old-test-compst new-test-compst)
                  (equal old-then-sval new-then-sval)
                  (equal old-then-compst new-then-compst)
                  (c::test-value old-test-val)
                  (c::type-nonchar-integerp type)
                  (in (c::type-option-of-stmt-value old-then-sval)
                      types))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      types)))))

Theorem: stmt-ifelse-false-congruence

(defthm stmt-ifelse-false-congruence
  (b* ((old (c::stmt-ifelse old-test old-then old-else))
       (new (c::stmt-ifelse new-test new-then new-else))
       ((mv old-test-eval old-test-compst)
        (c::exec-expr old-test compst old-fenv (1- limit)))
       ((mv new-test-eval new-test-compst)
        (c::exec-expr new-test compst new-fenv (1- limit)))
       (old-test-val (c::expr-value->value old-test-eval))
       (new-test-val (c::expr-value->value new-test-eval))
       ((mv old-else-sval old-else-compst)
        (c::exec-stmt old-else
                      old-test-compst old-fenv (1- limit)))
       ((mv new-else-sval new-else-compst)
        (c::exec-stmt new-else
                      new-test-compst new-fenv (1- limit)))
       ((mv old-sval old-compst)
        (c::exec-stmt old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-stmt new compst new-fenv limit))
       (type (c::type-of-value old-test-val)))
    (implies (and (not (c::errorp old-sval))
                  (not (c::errorp new-test-eval))
                  (not (c::errorp new-else-sval))
                  (iff old-test-eval new-test-eval)
                  (equal old-test-val new-test-val)
                  (equal old-test-compst new-test-compst)
                  (equal old-else-sval new-else-sval)
                  (equal old-else-compst new-else-compst)
                  (not (c::test-value old-test-val))
                  (c::type-nonchar-integerp type)
                  (in (c::type-option-of-stmt-value old-else-sval)
                      types))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      types)))))

Theorem: stmt-compound-congruence

(defthm stmt-compound-congruence
 (b*
  ((old (c::stmt-compound old-items))
   (new (c::stmt-compound new-items))
   (compst1 (c::enter-scope compst))
   ((mv old-items-sval old-items-compst)
    (c::exec-block-item-list old-items compst1 old-fenv (1- limit)))
   ((mv new-items-sval new-items-compst)
    (c::exec-block-item-list new-items compst1 new-fenv (1- limit)))
   ((mv old-sval old-compst)
    (c::exec-stmt old compst old-fenv limit))
   ((mv new-sval new-compst)
    (c::exec-stmt new compst new-fenv limit)))
  (implies (and (not (c::errorp old-sval))
                (equal old-items-sval new-items-sval)
                (equal old-items-compst new-items-compst)
                (in (c::type-option-of-stmt-value old-items-sval)
                    types))
           (and (not (c::errorp new-sval))
                (equal old-sval new-sval)
                (equal old-compst new-compst)
                (in (c::type-option-of-stmt-value old-sval)
                    types)))))

Theorem: declon-declon-congruence

(defthm declon-declon-congruence
  (b* ((declor (c::obj-declor-ident var))
       (old (c::obj-declon (c::scspecseq-none)
                           tyspecs declor old-initer))
       (new (c::obj-declon (c::scspecseq-none)
                           tyspecs declor new-initer))
       ((mv old-init-ival old-init-compst)
        (c::exec-initer old-initer compst old-fenv (1- limit)))
       ((mv new-init-ival new-init-compst)
        (c::exec-initer new-initer compst new-fenv (1- limit)))
       (old-compst (c::exec-obj-declon old compst old-fenv limit))
       (new-compst (c::exec-obj-declon new compst new-fenv limit)))
    (implies (and old-initer
                  new-initer (not (c::errorp old-compst))
                  (equal old-init-ival new-init-ival)
                  (equal old-init-compst new-init-compst))
             (and (not (c::errorp new-compst))
                  (equal old-compst new-compst)))))

Theorem: block-item-stmt-congruence

(defthm block-item-stmt-congruence
  (b* ((old (c::block-item-stmt old-stmt))
       (new (c::block-item-stmt new-stmt))
       ((mv old-stmt-sval old-stmt-compst)
        (c::exec-stmt old-stmt compst old-fenv (1- limit)))
       ((mv new-stmt-sval new-stmt-compst)
        (c::exec-stmt new-stmt compst new-fenv (1- limit)))
       ((mv old-sval old-compst)
        (c::exec-block-item old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-block-item new compst new-fenv limit)))
    (implies (and (not (c::errorp old-sval))
                  (equal old-stmt-sval new-stmt-sval)
                  (equal old-stmt-compst new-stmt-compst)
                  (in (c::type-option-of-stmt-value old-stmt-sval)
                      types))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      types)))))

Theorem: block-item-declon-congruence

(defthm block-item-declon-congruence
  (b*
   ((old (c::block-item-declon old-declon))
    (new (c::block-item-declon new-declon))
    (old-declon-compst
         (c::exec-obj-declon old-declon compst old-fenv (1- limit)))
    (new-declon-compst
         (c::exec-obj-declon new-declon compst new-fenv (1- limit)))
    ((mv old-sval old-compst)
     (c::exec-block-item old compst old-fenv limit))
    ((mv new-sval new-compst)
     (c::exec-block-item new compst new-fenv limit)))
   (implies (and (not (c::errorp old-sval))
                 (equal old-declon-compst new-declon-compst))
            (and (not (c::errorp new-sval))
                 (equal old-sval new-sval)
                 (equal old-compst new-compst)
                 (in (c::type-option-of-stmt-value old-sval)
                     (insert nil nil))))))

Theorem: block-item-list-empty-congruence

(defthm block-item-list-empty-congruence
  (b* ((old nil)
       (new nil)
       ((mv old-sval old-compst)
        (c::exec-block-item-list old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-block-item-list new compst new-fenv limit)))
    (implies (not (c::errorp old-sval))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      (insert nil nil))))))

Theorem: block-item-list-cons-first-congruence

(defthm block-item-list-cons-first-congruence
  (b* ((old (cons old-item old-items))
       (new (cons new-item new-items))
       ((mv old-item-sval old-item-compst)
        (c::exec-block-item old-item compst old-fenv (1- limit)))
       ((mv new-item-sval new-item-compst)
        (c::exec-block-item new-item compst new-fenv (1- limit)))
       ((mv old-sval old-compst)
        (c::exec-block-item-list old compst old-fenv limit))
       ((mv new-sval new-compst)
        (c::exec-block-item-list new compst new-fenv limit)))
    (implies (and (not (c::errorp old-sval))
                  (equal old-item-sval new-item-sval)
                  (equal old-item-compst new-item-compst)
                  (equal (c::stmt-value-kind old-item-sval)
                         :return)
                  (in (c::type-option-of-stmt-value old-item-sval)
                      first-types))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      (union (delete nil first-types)
                             rest-types))))))

Theorem: block-item-list-cons-rest-congruence

(defthm block-item-list-cons-rest-congruence
  (b*
    ((old (cons old-item old-items))
     (new (cons new-item new-items))
     ((mv old-item-sval old-item-compst)
      (c::exec-block-item old-item compst old-fenv (1- limit)))
     ((mv new-item-sval new-item-compst)
      (c::exec-block-item new-item compst new-fenv (1- limit)))
     ((mv old-items-sval old-items-compst)
      (c::exec-block-item-list old-items
                               old-item-compst old-fenv (1- limit)))
     ((mv new-items-sval new-items-compst)
      (c::exec-block-item-list new-items
                               new-item-compst new-fenv (1- limit)))
     ((mv old-sval old-compst)
      (c::exec-block-item-list old compst old-fenv limit))
     ((mv new-sval new-compst)
      (c::exec-block-item-list new compst new-fenv limit)))
    (implies (and (not (c::errorp old-sval))
                  (equal old-item-sval new-item-sval)
                  (equal old-items-sval new-items-sval)
                  (equal old-item-compst new-item-compst)
                  (equal old-items-compst new-items-compst)
                  (equal (c::stmt-value-kind old-item-sval)
                         :none)
                  (in (c::type-option-of-stmt-value old-item-sval)
                      first-types)
                  (in (c::type-option-of-stmt-value old-items-sval)
                      rest-types))
             (and (not (c::errorp new-sval))
                  (equal old-sval new-sval)
                  (equal old-compst new-compst)
                  (in (c::type-option-of-stmt-value old-sval)
                      (union (delete nil first-types)
                             rest-types))))))