• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
        • Process-syntheto-toplevel-fn
        • Translation
        • Language
          • Static-semantics
            • Check-expression-fns
            • Subtypep
            • Match-type
            • Check-product-update-expression
            • Get-builtin-function-in/out/pre-post
            • Check-sum-update-expression
            • Check-sum-field-expression
            • Check-strict-binary-expression
            • Check-lt/le/gt/ge-expression
            • Check-eq/ne-expression
            • Check-div/rem-expression
            • Check-add/sub/mul-expression
            • Align-let-vars-values
            • Check-iff-expression
            • Check-function-definition-top/nontop
            • Check-sum-construct-expression
            • Check-rem-expression
            • Check-mul-expression
            • Check-sub-expression
            • Check-div-expression
            • Check-add-expression
            • Check-ne-expression
            • Check-lt-expression
            • Check-le-expression
            • Check-gt-expression
            • Check-ge-expression
            • Check-eq-expression
            • Check-function-specifier
            • Type-result
            • Check-product-construct-expression
            • Supremum-type
            • Check-call-expression
            • Check-product-field-expression
            • Check-function-definer
            • Make-subproof-obligations
            • Get-function-in/out/pre/post
            • Check-sum-test-expression
            • Match-field
            • Decompose-expression
            • Match-to-target
            • Check-unary-expression
            • Max-supertype
            • Match-type-list
            • Check-minus-expression
            • Check-type-definition
            • Check-not-expression
            • Check-type-product
            • Match-field-list
            • Check-type-subset
            • Check-type-definition-in-recursion
            • Align-let-vars-values-aux
            • Non-trivial-proof-obligation
            • Check-type-recursion
            • Check-function-specification
            • Check-toplevel
            • Supremum-type-list
            • Check-component-expression
            • Check-branch-list
            • Check-function-recursion
            • Check-function-definition
            • Binding
            • Check-function-header
            • Check-function-definition-list
            • Check-type-definition-list-in-recursion
            • Check-theorem
            • Check-nonstrict-binary-expression
            • Context-add-variables
            • Decompose-expression-aux
            • Check-alternative
            • Check-multi-expression
            • Check-type-sum
            • Check-type
            • Check-alternative-list
            • Context-add-condition
            • Check-type-definer
            • Check-transform
            • Check-variable
            • Check-transform-args
            • Check-toplevel-list
            • Context-add-condition-list
            • Check-if/when/unless-expression
            • Initializers-to-variable-substitution
            • Context-add-binding
            • Check-function-header-list
            • Context-add-toplevel
            • Ensure-single-type
            • Max-supertypes
            • Check-bind-expression
            • Check-type-list
            • Check-literal
            • Literal-type
            • Check-expression-list
            • Variable-context
            • Check-cond-expression
            • Check-branch
            • Args-without-defaults
            • Check-expression
            • *builtin-function-names*
            • Function-called-in
          • Abstract-syntax
          • Outcome
          • Abstract-syntax-operations
          • Outcome-list
          • Outcomes
        • Process-syntheto-toplevel
        • Shallow-embedding
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Static-semantics

Check-product-update-expression

Check if a product update expression is statically well-formed.

Signature

(check-product-update-expression tname target target-result 
                                 fields fields-result expr ctxt) 
 
  → 
result

Arguments

tname — Guard (identifierp tname).

target — Guard (expressionp target).

target-result — Guard (type-resultp target-result).

fields — Guard (initializer-listp fields).

fields-result — Guard (type-resultp fields-result).

expr — Guard (expressionp expr).

ctxt — Guard (contextp ctxt).

Returns

result — Type (type-resultp result).

The type of the target expression must be a deined product type, or a subtype of a defined product type: we calculate the maximal supertype of the expression's type, and ensure that it is a defined product type; since product types are not subtypes, calculating the maximal supertype cannot ``skip'' a product type.

We match the initializers to the fields of the product type, returning an error if there is any mismatch. Unlike a product construction expression, there may be unmatched fields: in general, a product update expression changes only some of the fields.

If the product type has an invariant, we generate a proof obligation saying that the new product type value satisfies the invariant. This formula is obtained by substituting, in the invariant, the updated field names with the updating expressions, and the non-updated field names with corresponding product field expressions.

Definitions and Theorems

Function: check-product-update-expression

(defun check-product-update-expression
       (tname target target-result
              fields fields-result expr ctxt)
 (declare (xargs :guard (and (identifierp tname)
                             (expressionp target)
                             (type-resultp target-result)
                             (initializer-listp fields)
                             (type-resultp fields-result)
                             (expressionp expr)
                             (contextp ctxt))))
 (declare
    (xargs :guard (type-result-case fields-result
                                    :err t
                                    :ok (= (len fields-result.types)
                                           (len fields)))))
 (let ((__function__ 'check-product-update-expression))
  (declare (ignorable __function__))
  (type-result-case
   target-result
   :err (type-result-err target-result.info)
   :ok
   (type-result-case
    fields-result :err
    (type-result-err fields-result.info)
    :ok
    (b*
     ((type (ensure-single-type target-result.types))
      ((when (not type))
       (type-result-err (list :multi-valued-field-target
                              (expression-fix target)
                              target-result.types)))
      (type (max-supertype type (context->tops ctxt)))
      ((when (not type))
       (type-result-err (list :no-max-supertype type)))
      (tprod (get-type-product type (context->tops ctxt)))
      ((when (not tprod))
       (type-result-err (list :product-update-type-mismatch type)))
      (target-fields (type-product->fields tprod))
      ((mv okp obligs unmatched-fields)
       (match-field-list fields
                         fields-result.types target-fields ctxt))
      ((when (not okp))
       (type-result-err (list :field-type-mismatch
                              type (initializer-list-fix fields)
                              unmatched-fields)))
      (inv (type-product->invariant tprod))
      (inv-oblig?
       (if inv
        (b*
         ((subst-new (initializers-to-variable-substitution fields))
          (names (field-list->name-list unmatched-fields))
          (subst-old
           (omap::from-lists
                names
                (expression-product-field-list tname target names)))
          (subst (omap::update* subst-new subst-old)))
         (non-trivial-proof-obligation
              (context->obligation-vars ctxt)
              (context->obligation-hyps ctxt)
              (subst-expression subst inv)
              expr))
        nil)))
     (make-type-result-ok
          :types (list type)
          :obligations (append fields-result.obligations
                               obligs inv-oblig?)))))))

Theorem: type-resultp-of-check-product-update-expression

(defthm type-resultp-of-check-product-update-expression
  (b* ((result (check-product-update-expression
                    tname target target-result
                    fields fields-result expr ctxt)))
    (type-resultp result))
  :rule-classes :rewrite)

Theorem: check-product-update-expression-of-identifier-fix-tname

(defthm check-product-update-expression-of-identifier-fix-tname
 (equal
  (check-product-update-expression (identifier-fix tname)
                                   target target-result
                                   fields fields-result expr ctxt)
  (check-product-update-expression tname target target-result
                                   fields fields-result expr ctxt)))

Theorem: check-product-update-expression-identifier-equiv-congruence-on-tname

(defthm
 check-product-update-expression-identifier-equiv-congruence-on-tname
 (implies
  (identifier-equiv tname tname-equiv)
  (equal
    (check-product-update-expression tname target target-result
                                     fields fields-result expr ctxt)
    (check-product-update-expression
         tname-equiv target target-result
         fields fields-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-product-update-expression-of-expression-fix-target

(defthm check-product-update-expression-of-expression-fix-target
 (equal
  (check-product-update-expression tname (expression-fix target)
                                   target-result
                                   fields fields-result expr ctxt)
  (check-product-update-expression tname target target-result
                                   fields fields-result expr ctxt)))

Theorem: check-product-update-expression-expression-equiv-congruence-on-target

(defthm
 check-product-update-expression-expression-equiv-congruence-on-target
 (implies
  (expression-equiv target target-equiv)
  (equal
    (check-product-update-expression tname target target-result
                                     fields fields-result expr ctxt)
    (check-product-update-expression
         tname target-equiv target-result
         fields fields-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-product-update-expression-of-type-result-fix-target-result

(defthm
   check-product-update-expression-of-type-result-fix-target-result
 (equal
  (check-product-update-expression
       tname
       target (type-result-fix target-result)
       fields fields-result expr ctxt)
  (check-product-update-expression tname target target-result
                                   fields fields-result expr ctxt)))

Theorem: check-product-update-expression-type-result-equiv-congruence-on-target-result

(defthm
 check-product-update-expression-type-result-equiv-congruence-on-target-result
 (implies
  (type-result-equiv target-result target-result-equiv)
  (equal
    (check-product-update-expression tname target target-result
                                     fields fields-result expr ctxt)
    (check-product-update-expression
         tname target target-result-equiv
         fields fields-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-product-update-expression-of-initializer-list-fix-fields

(defthm
     check-product-update-expression-of-initializer-list-fix-fields
 (equal
  (check-product-update-expression tname target target-result
                                   (initializer-list-fix fields)
                                   fields-result expr ctxt)
  (check-product-update-expression tname target target-result
                                   fields fields-result expr ctxt)))

Theorem: check-product-update-expression-initializer-list-equiv-congruence-on-fields

(defthm
 check-product-update-expression-initializer-list-equiv-congruence-on-fields
 (implies
  (initializer-list-equiv fields fields-equiv)
  (equal
    (check-product-update-expression tname target target-result
                                     fields fields-result expr ctxt)
    (check-product-update-expression
         tname target target-result
         fields-equiv fields-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-product-update-expression-of-type-result-fix-fields-result

(defthm
   check-product-update-expression-of-type-result-fix-fields-result
 (equal
  (check-product-update-expression
       tname target target-result
       fields (type-result-fix fields-result)
       expr ctxt)
  (check-product-update-expression tname target target-result
                                   fields fields-result expr ctxt)))

Theorem: check-product-update-expression-type-result-equiv-congruence-on-fields-result

(defthm
 check-product-update-expression-type-result-equiv-congruence-on-fields-result
 (implies
  (type-result-equiv fields-result fields-result-equiv)
  (equal
    (check-product-update-expression tname target target-result
                                     fields fields-result expr ctxt)
    (check-product-update-expression
         tname target target-result
         fields fields-result-equiv expr ctxt)))
 :rule-classes :congruence)

Theorem: check-product-update-expression-of-expression-fix-expr

(defthm check-product-update-expression-of-expression-fix-expr
 (equal
  (check-product-update-expression
       tname target target-result fields
       fields-result (expression-fix expr)
       ctxt)
  (check-product-update-expression tname target target-result
                                   fields fields-result expr ctxt)))

Theorem: check-product-update-expression-expression-equiv-congruence-on-expr

(defthm
 check-product-update-expression-expression-equiv-congruence-on-expr
 (implies
  (expression-equiv expr expr-equiv)
  (equal
    (check-product-update-expression tname target target-result
                                     fields fields-result expr ctxt)
    (check-product-update-expression
         tname target target-result
         fields fields-result expr-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-product-update-expression-of-context-fix-ctxt

(defthm check-product-update-expression-of-context-fix-ctxt
 (equal
  (check-product-update-expression
       tname target target-result fields
       fields-result expr (context-fix ctxt))
  (check-product-update-expression tname target target-result
                                   fields fields-result expr ctxt)))

Theorem: check-product-update-expression-context-equiv-congruence-on-ctxt

(defthm
   check-product-update-expression-context-equiv-congruence-on-ctxt
 (implies
  (context-equiv ctxt ctxt-equiv)
  (equal
    (check-product-update-expression tname target target-result
                                     fields fields-result expr ctxt)
    (check-product-update-expression
         tname target target-result
         fields fields-result expr ctxt-equiv)))
 :rule-classes :congruence)