		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-expr-when-asg-arrsub-rules

Rules for executing assignment expressions to array subscript expressions.

Definitions and Theorems

Theorem: exec-expr-when-asg-arrsub-when-schar-arrayp

(defthm exec-expr-when-asg-arrsub-when-schar-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-schar))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (schar-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (schar-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (scharp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (schar-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-schar-arrayp-for-modular-proofs

(defthm
     exec-expr-when-asg-arrsub-when-schar-arrayp-for-modular-proofs
  (implies
       (and (equal (expr-kind expr) :binary)
            (equal (binop-kind (expr-binary->op expr))
                   :asg)
            (equal left (expr-binary->arg1 expr))
            (equal right (expr-binary->arg2 expr))
            (equal (expr-kind left) :arrsub)
            (equal arr (expr-arrsub->arr left))
            (equal sub (expr-arrsub->sub left))
            (equal (expr-kind arr) :ident)
            (expr-purep right)
            (integerp limit)
            (>= limit
                (1+ (max (1+ (expr-pure-limit sub))
                         (expr-pure-limit right))))
            (expr-purep sub)
            (equal arr-eval (exec-expr-pure arr compst))
            (expr-valuep arr-eval)
            (equal ptr-eval
                   (apconvert-expr-value arr-eval))
            (expr-valuep ptr-eval)
            (equal ptr (expr-value->value ptr-eval))
            (value-case ptr :pointer)
            (value-pointer-validp ptr)
            (equal (value-pointer->reftype ptr)
                   (type-schar))
            (equal array
                   (read-object (value-pointer->designator ptr)
                                compst))
            (schar-arrayp array)
            (equal sub-eval (exec-expr-pure sub compst))
            (expr-valuep sub-eval)
            (equal index-eval
                   (apconvert-expr-value sub-eval))
            (expr-valuep index-eval)
            (equal index (expr-value->value index-eval))
            (cintegerp index)
            (schar-array-index-okp array index)
            (equal right-eval
                   (exec-expr-pure right compst))
            (expr-valuep right-eval)
            (equal eval (apconvert-expr-value right-eval))
            (expr-valuep eval)
            (equal val (expr-value->value eval))
            (scharp val)
            (equal compst1
                   (write-object (value-pointer->designator ptr)
                                 (schar-array-write array index val)
                                 compst))
            (compustatep compst1))
       (equal (exec-expr expr compst fenv limit)
              (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-uchar-arrayp

(defthm exec-expr-when-asg-arrsub-when-uchar-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-uchar))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (uchar-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (uchar-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (ucharp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (uchar-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-uchar-arrayp-for-modular-proofs

(defthm
     exec-expr-when-asg-arrsub-when-uchar-arrayp-for-modular-proofs
  (implies
       (and (equal (expr-kind expr) :binary)
            (equal (binop-kind (expr-binary->op expr))
                   :asg)
            (equal left (expr-binary->arg1 expr))
            (equal right (expr-binary->arg2 expr))
            (equal (expr-kind left) :arrsub)
            (equal arr (expr-arrsub->arr left))
            (equal sub (expr-arrsub->sub left))
            (equal (expr-kind arr) :ident)
            (expr-purep right)
            (integerp limit)
            (>= limit
                (1+ (max (1+ (expr-pure-limit sub))
                         (expr-pure-limit right))))
            (expr-purep sub)
            (equal arr-eval (exec-expr-pure arr compst))
            (expr-valuep arr-eval)
            (equal ptr-eval
                   (apconvert-expr-value arr-eval))
            (expr-valuep ptr-eval)
            (equal ptr (expr-value->value ptr-eval))
            (value-case ptr :pointer)
            (value-pointer-validp ptr)
            (equal (value-pointer->reftype ptr)
                   (type-uchar))
            (equal array
                   (read-object (value-pointer->designator ptr)
                                compst))
            (uchar-arrayp array)
            (equal sub-eval (exec-expr-pure sub compst))
            (expr-valuep sub-eval)
            (equal index-eval
                   (apconvert-expr-value sub-eval))
            (expr-valuep index-eval)
            (equal index (expr-value->value index-eval))
            (cintegerp index)
            (uchar-array-index-okp array index)
            (equal right-eval
                   (exec-expr-pure right compst))
            (expr-valuep right-eval)
            (equal eval (apconvert-expr-value right-eval))
            (expr-valuep eval)
            (equal val (expr-value->value eval))
            (ucharp val)
            (equal compst1
                   (write-object (value-pointer->designator ptr)
                                 (uchar-array-write array index val)
                                 compst))
            (compustatep compst1))
       (equal (exec-expr expr compst fenv limit)
              (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-sshort-arrayp

(defthm exec-expr-when-asg-arrsub-when-sshort-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-sshort))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (sshort-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (sshort-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (sshortp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (sshort-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-sshort-arrayp-for-modular-proofs

(defthm
    exec-expr-when-asg-arrsub-when-sshort-arrayp-for-modular-proofs
 (implies
      (and (equal (expr-kind expr) :binary)
           (equal (binop-kind (expr-binary->op expr))
                  :asg)
           (equal left (expr-binary->arg1 expr))
           (equal right (expr-binary->arg2 expr))
           (equal (expr-kind left) :arrsub)
           (equal arr (expr-arrsub->arr left))
           (equal sub (expr-arrsub->sub left))
           (equal (expr-kind arr) :ident)
           (expr-purep right)
           (integerp limit)
           (>= limit
               (1+ (max (1+ (expr-pure-limit sub))
                        (expr-pure-limit right))))
           (expr-purep sub)
           (equal arr-eval (exec-expr-pure arr compst))
           (expr-valuep arr-eval)
           (equal ptr-eval
                  (apconvert-expr-value arr-eval))
           (expr-valuep ptr-eval)
           (equal ptr (expr-value->value ptr-eval))
           (value-case ptr :pointer)
           (value-pointer-validp ptr)
           (equal (value-pointer->reftype ptr)
                  (type-sshort))
           (equal array
                  (read-object (value-pointer->designator ptr)
                               compst))
           (sshort-arrayp array)
           (equal sub-eval (exec-expr-pure sub compst))
           (expr-valuep sub-eval)
           (equal index-eval
                  (apconvert-expr-value sub-eval))
           (expr-valuep index-eval)
           (equal index (expr-value->value index-eval))
           (cintegerp index)
           (sshort-array-index-okp array index)
           (equal right-eval
                  (exec-expr-pure right compst))
           (expr-valuep right-eval)
           (equal eval (apconvert-expr-value right-eval))
           (expr-valuep eval)
           (equal val (expr-value->value eval))
           (sshortp val)
           (equal compst1
                  (write-object (value-pointer->designator ptr)
                                (sshort-array-write array index val)
                                compst))
           (compustatep compst1))
      (equal (exec-expr expr compst fenv limit)
             (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-ushort-arrayp

(defthm exec-expr-when-asg-arrsub-when-ushort-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-ushort))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (ushort-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (ushort-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (ushortp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (ushort-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-ushort-arrayp-for-modular-proofs

(defthm
    exec-expr-when-asg-arrsub-when-ushort-arrayp-for-modular-proofs
 (implies
      (and (equal (expr-kind expr) :binary)
           (equal (binop-kind (expr-binary->op expr))
                  :asg)
           (equal left (expr-binary->arg1 expr))
           (equal right (expr-binary->arg2 expr))
           (equal (expr-kind left) :arrsub)
           (equal arr (expr-arrsub->arr left))
           (equal sub (expr-arrsub->sub left))
           (equal (expr-kind arr) :ident)
           (expr-purep right)
           (integerp limit)
           (>= limit
               (1+ (max (1+ (expr-pure-limit sub))
                        (expr-pure-limit right))))
           (expr-purep sub)
           (equal arr-eval (exec-expr-pure arr compst))
           (expr-valuep arr-eval)
           (equal ptr-eval
                  (apconvert-expr-value arr-eval))
           (expr-valuep ptr-eval)
           (equal ptr (expr-value->value ptr-eval))
           (value-case ptr :pointer)
           (value-pointer-validp ptr)
           (equal (value-pointer->reftype ptr)
                  (type-ushort))
           (equal array
                  (read-object (value-pointer->designator ptr)
                               compst))
           (ushort-arrayp array)
           (equal sub-eval (exec-expr-pure sub compst))
           (expr-valuep sub-eval)
           (equal index-eval
                  (apconvert-expr-value sub-eval))
           (expr-valuep index-eval)
           (equal index (expr-value->value index-eval))
           (cintegerp index)
           (ushort-array-index-okp array index)
           (equal right-eval
                  (exec-expr-pure right compst))
           (expr-valuep right-eval)
           (equal eval (apconvert-expr-value right-eval))
           (expr-valuep eval)
           (equal val (expr-value->value eval))
           (ushortp val)
           (equal compst1
                  (write-object (value-pointer->designator ptr)
                                (ushort-array-write array index val)
                                compst))
           (compustatep compst1))
      (equal (exec-expr expr compst fenv limit)
             (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-sint-arrayp

(defthm exec-expr-when-asg-arrsub-when-sint-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-sint))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (sint-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (sint-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (sintp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (sint-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-sint-arrayp-for-modular-proofs

(defthm
      exec-expr-when-asg-arrsub-when-sint-arrayp-for-modular-proofs
  (implies
       (and (equal (expr-kind expr) :binary)
            (equal (binop-kind (expr-binary->op expr))
                   :asg)
            (equal left (expr-binary->arg1 expr))
            (equal right (expr-binary->arg2 expr))
            (equal (expr-kind left) :arrsub)
            (equal arr (expr-arrsub->arr left))
            (equal sub (expr-arrsub->sub left))
            (equal (expr-kind arr) :ident)
            (expr-purep right)
            (integerp limit)
            (>= limit
                (1+ (max (1+ (expr-pure-limit sub))
                         (expr-pure-limit right))))
            (expr-purep sub)
            (equal arr-eval (exec-expr-pure arr compst))
            (expr-valuep arr-eval)
            (equal ptr-eval
                   (apconvert-expr-value arr-eval))
            (expr-valuep ptr-eval)
            (equal ptr (expr-value->value ptr-eval))
            (value-case ptr :pointer)
            (value-pointer-validp ptr)
            (equal (value-pointer->reftype ptr)
                   (type-sint))
            (equal array
                   (read-object (value-pointer->designator ptr)
                                compst))
            (sint-arrayp array)
            (equal sub-eval (exec-expr-pure sub compst))
            (expr-valuep sub-eval)
            (equal index-eval
                   (apconvert-expr-value sub-eval))
            (expr-valuep index-eval)
            (equal index (expr-value->value index-eval))
            (cintegerp index)
            (sint-array-index-okp array index)
            (equal right-eval
                   (exec-expr-pure right compst))
            (expr-valuep right-eval)
            (equal eval (apconvert-expr-value right-eval))
            (expr-valuep eval)
            (equal val (expr-value->value eval))
            (sintp val)
            (equal compst1
                   (write-object (value-pointer->designator ptr)
                                 (sint-array-write array index val)
                                 compst))
            (compustatep compst1))
       (equal (exec-expr expr compst fenv limit)
              (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-uint-arrayp

(defthm exec-expr-when-asg-arrsub-when-uint-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-uint))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (uint-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (uint-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (uintp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (uint-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-uint-arrayp-for-modular-proofs

(defthm
      exec-expr-when-asg-arrsub-when-uint-arrayp-for-modular-proofs
  (implies
       (and (equal (expr-kind expr) :binary)
            (equal (binop-kind (expr-binary->op expr))
                   :asg)
            (equal left (expr-binary->arg1 expr))
            (equal right (expr-binary->arg2 expr))
            (equal (expr-kind left) :arrsub)
            (equal arr (expr-arrsub->arr left))
            (equal sub (expr-arrsub->sub left))
            (equal (expr-kind arr) :ident)
            (expr-purep right)
            (integerp limit)
            (>= limit
                (1+ (max (1+ (expr-pure-limit sub))
                         (expr-pure-limit right))))
            (expr-purep sub)
            (equal arr-eval (exec-expr-pure arr compst))
            (expr-valuep arr-eval)
            (equal ptr-eval
                   (apconvert-expr-value arr-eval))
            (expr-valuep ptr-eval)
            (equal ptr (expr-value->value ptr-eval))
            (value-case ptr :pointer)
            (value-pointer-validp ptr)
            (equal (value-pointer->reftype ptr)
                   (type-uint))
            (equal array
                   (read-object (value-pointer->designator ptr)
                                compst))
            (uint-arrayp array)
            (equal sub-eval (exec-expr-pure sub compst))
            (expr-valuep sub-eval)
            (equal index-eval
                   (apconvert-expr-value sub-eval))
            (expr-valuep index-eval)
            (equal index (expr-value->value index-eval))
            (cintegerp index)
            (uint-array-index-okp array index)
            (equal right-eval
                   (exec-expr-pure right compst))
            (expr-valuep right-eval)
            (equal eval (apconvert-expr-value right-eval))
            (expr-valuep eval)
            (equal val (expr-value->value eval))
            (uintp val)
            (equal compst1
                   (write-object (value-pointer->designator ptr)
                                 (uint-array-write array index val)
                                 compst))
            (compustatep compst1))
       (equal (exec-expr expr compst fenv limit)
              (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-slong-arrayp

(defthm exec-expr-when-asg-arrsub-when-slong-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-slong))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (slong-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (slong-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (slongp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (slong-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-slong-arrayp-for-modular-proofs

(defthm
     exec-expr-when-asg-arrsub-when-slong-arrayp-for-modular-proofs
  (implies
       (and (equal (expr-kind expr) :binary)
            (equal (binop-kind (expr-binary->op expr))
                   :asg)
            (equal left (expr-binary->arg1 expr))
            (equal right (expr-binary->arg2 expr))
            (equal (expr-kind left) :arrsub)
            (equal arr (expr-arrsub->arr left))
            (equal sub (expr-arrsub->sub left))
            (equal (expr-kind arr) :ident)
            (expr-purep right)
            (integerp limit)
            (>= limit
                (1+ (max (1+ (expr-pure-limit sub))
                         (expr-pure-limit right))))
            (expr-purep sub)
            (equal arr-eval (exec-expr-pure arr compst))
            (expr-valuep arr-eval)
            (equal ptr-eval
                   (apconvert-expr-value arr-eval))
            (expr-valuep ptr-eval)
            (equal ptr (expr-value->value ptr-eval))
            (value-case ptr :pointer)
            (value-pointer-validp ptr)
            (equal (value-pointer->reftype ptr)
                   (type-slong))
            (equal array
                   (read-object (value-pointer->designator ptr)
                                compst))
            (slong-arrayp array)
            (equal sub-eval (exec-expr-pure sub compst))
            (expr-valuep sub-eval)
            (equal index-eval
                   (apconvert-expr-value sub-eval))
            (expr-valuep index-eval)
            (equal index (expr-value->value index-eval))
            (cintegerp index)
            (slong-array-index-okp array index)
            (equal right-eval
                   (exec-expr-pure right compst))
            (expr-valuep right-eval)
            (equal eval (apconvert-expr-value right-eval))
            (expr-valuep eval)
            (equal val (expr-value->value eval))
            (slongp val)
            (equal compst1
                   (write-object (value-pointer->designator ptr)
                                 (slong-array-write array index val)
                                 compst))
            (compustatep compst1))
       (equal (exec-expr expr compst fenv limit)
              (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-ulong-arrayp

(defthm exec-expr-when-asg-arrsub-when-ulong-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-ulong))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (ulong-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (ulong-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (ulongp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (ulong-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-ulong-arrayp-for-modular-proofs

(defthm
     exec-expr-when-asg-arrsub-when-ulong-arrayp-for-modular-proofs
  (implies
       (and (equal (expr-kind expr) :binary)
            (equal (binop-kind (expr-binary->op expr))
                   :asg)
            (equal left (expr-binary->arg1 expr))
            (equal right (expr-binary->arg2 expr))
            (equal (expr-kind left) :arrsub)
            (equal arr (expr-arrsub->arr left))
            (equal sub (expr-arrsub->sub left))
            (equal (expr-kind arr) :ident)
            (expr-purep right)
            (integerp limit)
            (>= limit
                (1+ (max (1+ (expr-pure-limit sub))
                         (expr-pure-limit right))))
            (expr-purep sub)
            (equal arr-eval (exec-expr-pure arr compst))
            (expr-valuep arr-eval)
            (equal ptr-eval
                   (apconvert-expr-value arr-eval))
            (expr-valuep ptr-eval)
            (equal ptr (expr-value->value ptr-eval))
            (value-case ptr :pointer)
            (value-pointer-validp ptr)
            (equal (value-pointer->reftype ptr)
                   (type-ulong))
            (equal array
                   (read-object (value-pointer->designator ptr)
                                compst))
            (ulong-arrayp array)
            (equal sub-eval (exec-expr-pure sub compst))
            (expr-valuep sub-eval)
            (equal index-eval
                   (apconvert-expr-value sub-eval))
            (expr-valuep index-eval)
            (equal index (expr-value->value index-eval))
            (cintegerp index)
            (ulong-array-index-okp array index)
            (equal right-eval
                   (exec-expr-pure right compst))
            (expr-valuep right-eval)
            (equal eval (apconvert-expr-value right-eval))
            (expr-valuep eval)
            (equal val (expr-value->value eval))
            (ulongp val)
            (equal compst1
                   (write-object (value-pointer->designator ptr)
                                 (ulong-array-write array index val)
                                 compst))
            (compustatep compst1))
       (equal (exec-expr expr compst fenv limit)
              (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-sllong-arrayp

(defthm exec-expr-when-asg-arrsub-when-sllong-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-sllong))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (sllong-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (sllong-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (sllongp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (sllong-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-sllong-arrayp-for-modular-proofs

(defthm
    exec-expr-when-asg-arrsub-when-sllong-arrayp-for-modular-proofs
 (implies
      (and (equal (expr-kind expr) :binary)
           (equal (binop-kind (expr-binary->op expr))
                  :asg)
           (equal left (expr-binary->arg1 expr))
           (equal right (expr-binary->arg2 expr))
           (equal (expr-kind left) :arrsub)
           (equal arr (expr-arrsub->arr left))
           (equal sub (expr-arrsub->sub left))
           (equal (expr-kind arr) :ident)
           (expr-purep right)
           (integerp limit)
           (>= limit
               (1+ (max (1+ (expr-pure-limit sub))
                        (expr-pure-limit right))))
           (expr-purep sub)
           (equal arr-eval (exec-expr-pure arr compst))
           (expr-valuep arr-eval)
           (equal ptr-eval
                  (apconvert-expr-value arr-eval))
           (expr-valuep ptr-eval)
           (equal ptr (expr-value->value ptr-eval))
           (value-case ptr :pointer)
           (value-pointer-validp ptr)
           (equal (value-pointer->reftype ptr)
                  (type-sllong))
           (equal array
                  (read-object (value-pointer->designator ptr)
                               compst))
           (sllong-arrayp array)
           (equal sub-eval (exec-expr-pure sub compst))
           (expr-valuep sub-eval)
           (equal index-eval
                  (apconvert-expr-value sub-eval))
           (expr-valuep index-eval)
           (equal index (expr-value->value index-eval))
           (cintegerp index)
           (sllong-array-index-okp array index)
           (equal right-eval
                  (exec-expr-pure right compst))
           (expr-valuep right-eval)
           (equal eval (apconvert-expr-value right-eval))
           (expr-valuep eval)
           (equal val (expr-value->value eval))
           (sllongp val)
           (equal compst1
                  (write-object (value-pointer->designator ptr)
                                (sllong-array-write array index val)
                                compst))
           (compustatep compst1))
      (equal (exec-expr expr compst fenv limit)
             (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-ullong-arrayp

(defthm exec-expr-when-asg-arrsub-when-ullong-arrayp
 (implies
  (and
    (equal (expr-kind expr) :binary)
    (equal (binop-kind (expr-binary->op expr))
           :asg)
    (equal left (expr-binary->arg1 expr))
    (equal right (expr-binary->arg2 expr))
    (equal (expr-kind left) :arrsub)
    (equal arr (expr-arrsub->arr left))
    (equal sub (expr-arrsub->sub left))
    (equal (expr-kind arr) :ident)
    (equal var (expr-ident->get arr))
    (expr-purep right)
    (integerp limit)
    (>= limit
        (1+ (max (1+ (expr-pure-limit sub))
                 (expr-pure-limit right))))
    (expr-purep sub)
    (equal arr-val (read-var var compst))
    (valuep arr-val)
    (equal eptr
           (apconvert-expr-value
                (expr-value arr-val (objdesign-of-var var compst))))
    (expr-valuep eptr)
    (equal ptr (expr-value->value eptr))
    (value-case ptr :pointer)
    (value-pointer-validp ptr)
    (equal (value-pointer->reftype ptr)
           (type-ullong))
    (equal array
           (read-object (value-pointer->designator ptr)
                        compst))
    (ullong-arrayp array)
    (equal eindex (exec-expr-pure sub compst))
    (expr-valuep eindex)
    (equal eindex1 (apconvert-expr-value eindex))
    (expr-valuep eindex1)
    (equal index (expr-value->value eindex1))
    (cintegerp index)
    (ullong-array-index-okp array index)
    (equal eval (exec-expr-pure right compst))
    (expr-valuep eval)
    (equal eval1 (apconvert-expr-value eval))
    (expr-valuep eval1)
    (equal val (expr-value->value eval1))
    (ullongp val)
    (equal compst1
           (write-object (value-pointer->designator ptr)
                         (ullong-array-write array index val)
                         compst))
    (compustatep compst1))
  (equal (exec-expr expr compst fenv limit)
         (mv (expr-value val nil) compst1))))

Theorem: exec-expr-when-asg-arrsub-when-ullong-arrayp-for-modular-proofs

(defthm
    exec-expr-when-asg-arrsub-when-ullong-arrayp-for-modular-proofs
 (implies
      (and (equal (expr-kind expr) :binary)
           (equal (binop-kind (expr-binary->op expr))
                  :asg)
           (equal left (expr-binary->arg1 expr))
           (equal right (expr-binary->arg2 expr))
           (equal (expr-kind left) :arrsub)
           (equal arr (expr-arrsub->arr left))
           (equal sub (expr-arrsub->sub left))
           (equal (expr-kind arr) :ident)
           (expr-purep right)
           (integerp limit)
           (>= limit
               (1+ (max (1+ (expr-pure-limit sub))
                        (expr-pure-limit right))))
           (expr-purep sub)
           (equal arr-eval (exec-expr-pure arr compst))
           (expr-valuep arr-eval)
           (equal ptr-eval
                  (apconvert-expr-value arr-eval))
           (expr-valuep ptr-eval)
           (equal ptr (expr-value->value ptr-eval))
           (value-case ptr :pointer)
           (value-pointer-validp ptr)
           (equal (value-pointer->reftype ptr)
                  (type-ullong))
           (equal array
                  (read-object (value-pointer->designator ptr)
                               compst))
           (ullong-arrayp array)
           (equal sub-eval (exec-expr-pure sub compst))
           (expr-valuep sub-eval)
           (equal index-eval
                  (apconvert-expr-value sub-eval))
           (expr-valuep index-eval)
           (equal index (expr-value->value index-eval))
           (cintegerp index)
           (ullong-array-index-okp array index)
           (equal right-eval
                  (exec-expr-pure right compst))
           (expr-valuep right-eval)
           (equal eval (apconvert-expr-value right-eval))
           (expr-valuep eval)
           (equal val (expr-value->value eval))
           (ullongp val)
           (equal compst1
                  (write-object (value-pointer->designator ptr)
                                (ullong-array-write array index val)
                                compst))
           (compustatep compst1))
      (equal (exec-expr expr compst fenv limit)
             (mv (expr-value val nil) compst1))))