• 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-construct-expression

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

Signature

(check-product-construct-expression 
     type inits inits-result expr ctxt) 
 
  → 
result

Arguments

type — Guard (identifierp type).

inits — Guard (initializer-listp inits).

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

expr — Guard (expressionp expr).

ctxt — Guard (contextp ctxt).

Returns

result — Type (type-resultp result).

The identifier must be the name of a product type in the context. We match the field types calculated for the initializers with the field types of the product type. If the product type has an invariant, we also generate a proof obligation saying that the initializers satisfy the invariant. The type of the expression is the product type.

Definitions and Theorems

Function: check-product-construct-expression

(defun check-product-construct-expression
       (type inits inits-result expr ctxt)
 (declare (xargs :guard (and (identifierp type)
                             (initializer-listp inits)
                             (type-resultp inits-result)
                             (expressionp expr)
                             (contextp ctxt))))
 (declare
     (xargs :guard (type-result-case inits-result
                                     :err t
                                     :ok (= (len inits-result.types)
                                            (len inits)))))
 (let ((__function__ 'check-product-construct-expression))
  (declare (ignorable __function__))
  (type-result-case
   inits-result
   :err (type-result-err inits-result.info)
   :ok
   (b*
    ((product (get-type-product (type-defined type)
                                (context->tops ctxt)))
     ((when (not product))
      (type-result-err
       (list
           :product-construct-type-mismatch (identifier-fix type))))
     (fields (type-product->fields product))
     ((mv okp obligs unmatched-fields)
      (match-field-list inits inits-result.types fields ctxt))
     ((when (not okp))
      (type-result-err (list :field-type-mismatch
                             (identifier-fix type)
                             (initializer-list-fix inits)
                             fields)))
     ((when (consp unmatched-fields))
      (type-result-err (list :unmatched-fields (identifier-fix type)
                             (initializer-list-fix inits)
                             fields)))
     (inv (type-product->invariant product))
     (inv-oblig?
       (if inv
         (b* ((subst (initializers-to-variable-substitution inits)))
           (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-defined type))
         :obligations (append inits-result.obligations
                              obligs inv-oblig?))))))

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

(defthm type-resultp-of-check-product-construct-expression
  (b* ((result (check-product-construct-expression
                    type inits inits-result expr ctxt)))
    (type-resultp result))
  :rule-classes :rewrite)

Theorem: check-product-construct-expression-of-identifier-fix-type

(defthm check-product-construct-expression-of-identifier-fix-type
 (equal
   (check-product-construct-expression (identifier-fix type)
                                       inits inits-result expr ctxt)
   (check-product-construct-expression
        type inits inits-result expr ctxt)))

Theorem: check-product-construct-expression-identifier-equiv-congruence-on-type

(defthm
 check-product-construct-expression-identifier-equiv-congruence-on-type
 (implies (identifier-equiv type type-equiv)
          (equal (check-product-construct-expression
                      type inits inits-result expr ctxt)
                 (check-product-construct-expression
                      type-equiv
                      inits inits-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-product-construct-expression-of-initializer-list-fix-inits

(defthm
   check-product-construct-expression-of-initializer-list-fix-inits
  (equal (check-product-construct-expression
              type (initializer-list-fix inits)
              inits-result expr ctxt)
         (check-product-construct-expression
              type inits inits-result expr ctxt)))

Theorem: check-product-construct-expression-initializer-list-equiv-congruence-on-inits

(defthm
 check-product-construct-expression-initializer-list-equiv-congruence-on-inits
 (implies (initializer-list-equiv inits inits-equiv)
          (equal (check-product-construct-expression
                      type inits inits-result expr ctxt)
                 (check-product-construct-expression
                      type
                      inits-equiv inits-result expr ctxt)))
 :rule-classes :congruence)

Theorem: check-product-construct-expression-of-type-result-fix-inits-result

(defthm
 check-product-construct-expression-of-type-result-fix-inits-result
 (equal (check-product-construct-expression
             type
             inits (type-result-fix inits-result)
             expr ctxt)
        (check-product-construct-expression
             type inits inits-result expr ctxt)))

Theorem: check-product-construct-expression-type-result-equiv-congruence-on-inits-result

(defthm
 check-product-construct-expression-type-result-equiv-congruence-on-inits-result
 (implies (type-result-equiv inits-result inits-result-equiv)
          (equal (check-product-construct-expression
                      type inits inits-result expr ctxt)
                 (check-product-construct-expression
                      type
                      inits inits-result-equiv expr ctxt)))
 :rule-classes :congruence)

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

(defthm check-product-construct-expression-of-expression-fix-expr
  (equal (check-product-construct-expression
              type
              inits inits-result (expression-fix expr)
              ctxt)
         (check-product-construct-expression
              type inits inits-result expr ctxt)))

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

(defthm
 check-product-construct-expression-expression-equiv-congruence-on-expr
 (implies (expression-equiv expr expr-equiv)
          (equal (check-product-construct-expression
                      type inits inits-result expr ctxt)
                 (check-product-construct-expression
                      type
                      inits inits-result expr-equiv ctxt)))
 :rule-classes :congruence)

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

(defthm check-product-construct-expression-of-context-fix-ctxt
  (equal (check-product-construct-expression
              type inits
              inits-result expr (context-fix ctxt))
         (check-product-construct-expression
              type inits inits-result expr ctxt)))

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

(defthm
 check-product-construct-expression-context-equiv-congruence-on-ctxt
 (implies (context-equiv ctxt ctxt-equiv)
          (equal (check-product-construct-expression
                      type inits inits-result expr ctxt)
                 (check-product-construct-expression
                      type
                      inits inits-result expr ctxt-equiv)))
 :rule-classes :congruence)