• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • 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
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Static-semantics

Align-let-vars-values

Align bound variables to their expressions.

Signature

(align-let-vars-values vars value) 
  → 
(mv okp var-names var-types values)

Arguments

vars — Guard (typed-variable-listp vars).

value — Guard (expressionp value).

Returns

okp — Type (booleanp okp).

var-names — Type (identifier-listp var-names).

var-types — Type (type-listp var-types).

values — Type (expression-listp values).

A Syntheto binding expression binds a single expression to a list of variables. There must be at least one variable, otherwise it is an error. If there is exactly one variable, the (value of the) expression is bound to it. If there are two or more variables, the expression must return multiple values, whose number must match the number of variables, and these values are bound to the variables, in order.

Statically, we can ``align'' the expression with the variable as follows. When there is an empty list of variables, it is an error. When there is exactly one variable, it aligns with the whole expression. Where there are two or more variables, each aligns with a component of the expression, i.e. with a component expression whose subexpression is the original expression bound to the variable list.

This ACL2 function carries out this ``alignment''. It returns a list of expressions, as many as the variables, each of which corresponds to a variable. It also decomposes the typed variables into names and types. Furthermore, it ensures that there is at least one variable, returning an error indication if that is not the case. This function is called by check-bind-expression; see that function for further details.

Definitions and Theorems

Function: align-let-vars-values-aux

(defun align-let-vars-values-aux (vars index value)
  (declare (xargs :guard (and (typed-variable-listp vars)
                              (natp index)
                              (expressionp value))))
  (let ((__function__ 'align-let-vars-values-aux))
    (declare (ignorable __function__))
    (b* (((when (endp vars)) (mv nil nil nil))
         (var (car vars))
         (name (typed-variable->name var))
         (type (typed-variable->type var))
         (val (make-expression-component :multi value
                                         :index index))
         ((mv names types vals)
          (align-let-vars-values-aux (cdr vars)
                                     (1+ (nfix index))
                                     value)))
      (mv (cons name names)
          (cons type types)
          (cons val vals)))))

Theorem: identifier-listp-of-align-let-vars-values-aux.var-names

(defthm identifier-listp-of-align-let-vars-values-aux.var-names
  (b* (((mv ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values-aux vars index value)))
    (identifier-listp var-names))
  :rule-classes :rewrite)

Theorem: type-listp-of-align-let-vars-values-aux.var-types

(defthm type-listp-of-align-let-vars-values-aux.var-types
  (b* (((mv ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values-aux vars index value)))
    (type-listp var-types))
  :rule-classes :rewrite)

Theorem: expression-listp-of-align-let-vars-values-aux.values

(defthm expression-listp-of-align-let-vars-values-aux.values
  (b* (((mv ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values-aux vars index value)))
    (expression-listp values))
  :rule-classes :rewrite)

Theorem: len-of-align-let-vars-values-aux.names

(defthm len-of-align-let-vars-values-aux.names
  (b* (((mv ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values-aux vars index value)))
    (equal (len var-names) (len vars))))

Theorem: len-of-align-let-vars-values-aux.types

(defthm len-of-align-let-vars-values-aux.types
  (b* (((mv ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values-aux vars index value)))
    (equal (len var-types) (len vars))))

Theorem: len-of-align-let-vars-values-aux.values

(defthm len-of-align-let-vars-values-aux.values
  (b* (((mv ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values-aux vars index value)))
    (equal (len values) (len vars))))

Theorem: align-let-vars-values-aux-of-typed-variable-list-fix-vars

(defthm align-let-vars-values-aux-of-typed-variable-list-fix-vars
  (equal (align-let-vars-values-aux (typed-variable-list-fix vars)
                                    index value)
         (align-let-vars-values-aux vars index value)))

Theorem: align-let-vars-values-aux-typed-variable-list-equiv-congruence-on-vars

(defthm
 align-let-vars-values-aux-typed-variable-list-equiv-congruence-on-vars
 (implies
      (typed-variable-list-equiv vars vars-equiv)
      (equal (align-let-vars-values-aux vars index value)
             (align-let-vars-values-aux vars-equiv index value)))
 :rule-classes :congruence)

Theorem: align-let-vars-values-aux-of-nfix-index

(defthm align-let-vars-values-aux-of-nfix-index
  (equal (align-let-vars-values-aux vars (nfix index)
                                    value)
         (align-let-vars-values-aux vars index value)))

Theorem: align-let-vars-values-aux-nat-equiv-congruence-on-index

(defthm align-let-vars-values-aux-nat-equiv-congruence-on-index
  (implies
       (nat-equiv index index-equiv)
       (equal (align-let-vars-values-aux vars index value)
              (align-let-vars-values-aux vars index-equiv value)))
  :rule-classes :congruence)

Theorem: align-let-vars-values-aux-of-expression-fix-value

(defthm align-let-vars-values-aux-of-expression-fix-value
  (equal
       (align-let-vars-values-aux vars index (expression-fix value))
       (align-let-vars-values-aux vars index value)))

Theorem: align-let-vars-values-aux-expression-equiv-congruence-on-value

(defthm
     align-let-vars-values-aux-expression-equiv-congruence-on-value
  (implies
       (expression-equiv value value-equiv)
       (equal (align-let-vars-values-aux vars index value)
              (align-let-vars-values-aux vars index value-equiv)))
  :rule-classes :congruence)

Function: align-let-vars-values

(defun align-let-vars-values (vars value)
  (declare (xargs :guard (and (typed-variable-listp vars)
                              (expressionp value))))
  (let ((__function__ 'align-let-vars-values))
    (declare (ignorable __function__))
    (cond ((endp vars) (mv nil nil nil nil))
          ((endp (cdr vars))
           (mv t (typed-variable-list->name-list vars)
               (typed-variable-list->type-list vars)
               (list (expression-fix value))))
          (t (b* (((mv names types values)
                   (align-let-vars-values-aux vars 0 value)))
               (mv t names types values))))))

Theorem: booleanp-of-align-let-vars-values.okp

(defthm booleanp-of-align-let-vars-values.okp
  (b* (((mv ?okp ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values vars value)))
    (booleanp okp))
  :rule-classes :rewrite)

Theorem: identifier-listp-of-align-let-vars-values.var-names

(defthm identifier-listp-of-align-let-vars-values.var-names
  (b* (((mv ?okp ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values vars value)))
    (identifier-listp var-names))
  :rule-classes :rewrite)

Theorem: type-listp-of-align-let-vars-values.var-types

(defthm type-listp-of-align-let-vars-values.var-types
  (b* (((mv ?okp ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values vars value)))
    (type-listp var-types))
  :rule-classes :rewrite)

Theorem: expression-listp-of-align-let-vars-values.values

(defthm expression-listp-of-align-let-vars-values.values
  (b* (((mv ?okp ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values vars value)))
    (expression-listp values))
  :rule-classes :rewrite)

Theorem: len-of-align-let-vars-values.names

(defthm len-of-align-let-vars-values.names
  (b* (((mv ?okp ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values vars value)))
    (equal (len var-names) (len vars))))

Theorem: len-of-align-let-vars-values.types

(defthm len-of-align-let-vars-values.types
  (b* (((mv ?okp ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values vars value)))
    (equal (len var-types) (len vars))))

Theorem: len-of-align-let-vars-values.values

(defthm len-of-align-let-vars-values.values
  (b* (((mv ?okp ?var-names
            ?var-types common-lisp::?values)
        (align-let-vars-values vars value)))
    (equal (len values) (len vars))))

Theorem: align-let-vars-values-of-typed-variable-list-fix-vars

(defthm align-let-vars-values-of-typed-variable-list-fix-vars
  (equal (align-let-vars-values (typed-variable-list-fix vars)
                                value)
         (align-let-vars-values vars value)))

Theorem: align-let-vars-values-typed-variable-list-equiv-congruence-on-vars

(defthm
 align-let-vars-values-typed-variable-list-equiv-congruence-on-vars
 (implies (typed-variable-list-equiv vars vars-equiv)
          (equal (align-let-vars-values vars value)
                 (align-let-vars-values vars-equiv value)))
 :rule-classes :congruence)

Theorem: align-let-vars-values-of-expression-fix-value

(defthm align-let-vars-values-of-expression-fix-value
  (equal (align-let-vars-values vars (expression-fix value))
         (align-let-vars-values vars value)))

Theorem: align-let-vars-values-expression-equiv-congruence-on-value

(defthm align-let-vars-values-expression-equiv-congruence-on-value
  (implies (expression-equiv value value-equiv)
           (equal (align-let-vars-values vars value)
                  (align-let-vars-values vars value-equiv)))
  :rule-classes :congruence)