• 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
        • Soft
        • C
          • Syntax-for-tools
          • Atc
            • Atc-implementation
              • Atc-abstract-syntax
              • Atc-pretty-printer
              • Atc-event-and-code-generation
                • Atc-symbolic-computation-states
                • Atc-symbolic-execution-rules
                • Atc-gen-ext-declon-lists
                • Atc-function-and-loop-generation
                • Atc-statement-generation
                  • Stmt-gin
                  • Atc-gen-term-type-formula
                  • Atc-gen-stmt
                  • Stmt-gout
                  • Atc-gen-expr
                  • Atc-gen-block-item-var-asg
                  • Atc-gen-return-stmt
                  • Atc-gen-mbt-block-items
                  • Atc-gen-if/ifelse-stmt
                  • Atc-gen-cfun-call-stmt
                  • Atc-gen-block-item-struct-scalar-asg
                  • Atc-gen-block-item-struct-array-asg
                  • Atc-gen-block-item-list-append
                  • Atc-gen-block-item-integer-asg
                  • Atc-gen-block-item-declon
                  • Atc-gen-block-item-array-asg
                  • Atc-gen-loop-stmt
                  • Atc-gen-block-item-list-cons
                  • Atc-uterm-to-components
                  • Atc-gen-block-item-stmt
                    • Lstmt-gin
                    • Atc-gen-block-item-list-one
                    • Atc-gen-block-item-var-decl
                    • Atc-gen-block-item-asg
                    • Atc-gen-call-result-and-endstate
                    • Lstmt-gout
                    • Atc-ensure-formals-not-lost
                    • Atc-gen-block-item-list-none
                    • Atc-var-assignablep
                    • Atc-gen-uterm-result-and-type-formula
                    • Atc-remove-extobj-args
                    • Atc-affecting-term-for-let-p
                    • Atc-vars-assignablep
                    • Atc-make-lets-of-uterms
                    • Atc-symbolp-list
                    • Atc-make-mv-nth-terms
                    • Atc-make-mv-lets-of-uterms
                    • Atc-update-var-term-alist
                    • Irr-stmt-gout
                    • Irr-lstmt-gout
                  • Atc-gen-fileset
                  • Atc-gen-everything
                  • Atc-gen-obj-declon
                  • Atc-gen-fileset-event
                  • Atc-tag-tables
                  • Atc-expression-generation
                  • Atc-generation-contexts
                  • Atc-gen-wf-thm
                  • Term-checkers-atc
                  • Atc-variable-tables
                  • Term-checkers-common
                  • Atc-gen-init-fun-env-thm
                  • Atc-gen-appconds
                  • Read-write-variables
                  • Atc-gen-thm-assert-events
                  • Test*
                  • Atc-gen-prog-const
                  • Atc-gen-expr-bool
                  • Atc-theorem-generation
                  • Atc-tag-generation
                  • Atc-gen-expr-pure
                  • Atc-function-tables
                  • Atc-object-tables
                • Fty-pseudo-term-utilities
                • Atc-term-recognizers
                • Atc-input-processing
                • Atc-shallow-embedding
                • Atc-process-inputs-and-gen-everything
                • Atc-table
                • Atc-fn
                • Atc-pretty-printing-options
                • Atc-types
                • Atc-macro-definition
              • Atc-tutorial
            • Language
            • Representation
            • Transformation-tools
            • Insertion-sort
            • Pack
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Riscv
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Atc-statement-generation

    Atc-gen-block-item-stmt

    Generate a C block item that consists of a given statement.

    Signature
    (atc-gen-block-item-stmt stmt stmt-limit stmt-events stmt-thm 
                             uterm? type result new-compst gin state) 
     
      → 
    (mv item item-limit item-events item-thm thm-index names-to-avoid)
    Arguments
    stmt — Guard (stmtp stmt).
    stmt-limit — Guard (pseudo-termp stmt-limit).
    stmt-events — Guard (pseudo-event-form-listp stmt-events).
    stmt-thm — Guard (symbolp stmt-thm).
    uterm? — An untranslated term.
    type — Guard (typep type).
    result — An untranslated term.
    new-compst — An untranslated term.
    gin — Guard (stmt-ginp gin).
    Returns
    item — Type (block-itemp item).
    item-limit — Type (pseudo-termp item-limit).
    item-events — Type (pseudo-event-form-listp item-events), given (pseudo-event-form-listp stmt-events).
    item-thm — Type (symbolp item-thm).
    thm-index — Type (posp thm-index).
    names-to-avoid — Type (symbol-listp names-to-avoid).

    This is used to lift generated statements to generated block items. Besdies the block item, we also generate a theorem saying that exec-block-item applied to the quoted block item yields an mv pair consisting of a result term (or nil) and a possibly updated computation state; these are the same as the ones for the statement theorem.

    If uterm? is not nil, we also generate, as part of the theorem, an assertion that the term returns a value, or values, of the expected type(s). Callers pass a non-nil uterm? when the blok item corresponds to a full ACL2 term (e.g. a conditional); while they pass nil otherwise (e.g. for an assignment).

    The limit for the block item is 1 more than the limit for the statement, because we need 1 to go from exec-block-item to the :stmt case and exec-stmt.

    Definitions and Theorems

    Function: atc-gen-block-item-stmt

    (defun atc-gen-block-item-stmt
           (stmt stmt-limit stmt-events stmt-thm
                 uterm? type result new-compst gin state)
     (declare (xargs :stobjs (state)))
     (declare (xargs :guard (and (stmtp stmt)
                                 (pseudo-termp stmt-limit)
                                 (pseudo-event-form-listp stmt-events)
                                 (symbolp stmt-thm)
                                 (typep type)
                                 (stmt-ginp gin))))
     (let ((__function__ 'atc-gen-block-item-stmt))
      (declare (ignorable __function__))
      (b*
       (((stmt-gin gin) gin)
        (wrld (w state))
        (item (block-item-stmt stmt))
        (item-limit (pseudo-term-fncall 'binary-+
                                        (list (pseudo-term-quote 1)
                                              stmt-limit)))
        (name (pack gin.fn '-correct- gin.thm-index))
        (thm-index (1+ gin.thm-index))
        ((mv name names-to-avoid)
         (fresh-logical-name-with-$s-suffix
              name nil gin.names-to-avoid wrld))
        (exec-formula
         (cons
             'equal
             (cons (cons 'exec-block-item
                         (cons (cons 'quote (cons item 'nil))
                               (cons gin.compst-var
                                     (cons gin.fenv-var
                                           (cons gin.limit-var 'nil)))))
                   (cons (cons 'mv
                               (cons result (cons new-compst 'nil)))
                         'nil))))
        (exec-formula
             (atc-contextualize exec-formula gin.context
                                gin.fn gin.fn-guard gin.compst-var
                                gin.limit-var item-limit t wrld))
        (formula
         (if uterm?
          (b*
           (((mv type-formula &)
             (atc-gen-term-type-formula
                  uterm? type
                  gin.affect gin.inscope gin.prec-tags))
            (type-formula
                 (atc-contextualize type-formula gin.context gin.fn
                                    gin.fn-guard nil nil nil nil wrld)))
           (cons 'and
                 (cons exec-formula (cons type-formula 'nil))))
          exec-formula))
        (hints
         (cons
          (cons
           '"Goal"
           (cons
            ':in-theory
            (cons
             (cons
              'quote
              (cons
               (cons
                'exec-block-item-when-stmt
                (cons
                 '(:e block-item-kind)
                 (cons
                  'not-zp-of-limit-variable
                  (cons
                   '(:e block-item-stmt->get)
                   (cons
                    stmt-thm
                    '(uchar-array-length-of-uchar-array-write
                         schar-array-length-of-schar-array-write
                         ushort-array-length-of-ushort-array-write
                         sshort-array-length-of-sshort-array-write
                         uint-array-length-of-uint-array-write
                         sint-array-length-of-sint-array-write
                         ulong-array-length-of-ulong-array-write
                         slong-array-length-of-slong-array-write
                         ullong-array-length-of-ullong-array-write
                         sllong-array-length-of-sllong-array-write))))))
               'nil))
             'nil)))
          'nil))
        ((mv event &)
         (evmac-generate-defthm name
                                :formula formula
                                :hints hints
                                :enable nil)))
       (mv item item-limit
           (append stmt-events (list event))
           name thm-index names-to-avoid))))

    Theorem: block-itemp-of-atc-gen-block-item-stmt.item

    (defthm block-itemp-of-atc-gen-block-item-stmt.item
      (b*
       (((mv ?item ?item-limit ?item-events
             ?item-thm ?thm-index ?names-to-avoid)
         (atc-gen-block-item-stmt stmt
                                  stmt-limit stmt-events stmt-thm uterm?
                                  type result new-compst gin state)))
       (block-itemp item))
      :rule-classes :rewrite)

    Theorem: pseudo-termp-of-atc-gen-block-item-stmt.item-limit

    (defthm pseudo-termp-of-atc-gen-block-item-stmt.item-limit
      (b*
       (((mv ?item ?item-limit ?item-events
             ?item-thm ?thm-index ?names-to-avoid)
         (atc-gen-block-item-stmt stmt
                                  stmt-limit stmt-events stmt-thm uterm?
                                  type result new-compst gin state)))
       (pseudo-termp item-limit))
      :rule-classes :rewrite)

    Theorem: pseudo-event-form-listp-of-atc-gen-block-item-stmt.item-events

    (defthm
         pseudo-event-form-listp-of-atc-gen-block-item-stmt.item-events
     (implies
      (pseudo-event-form-listp stmt-events)
      (b*
       (((mv ?item ?item-limit ?item-events
             ?item-thm ?thm-index ?names-to-avoid)
         (atc-gen-block-item-stmt stmt
                                  stmt-limit stmt-events stmt-thm uterm?
                                  type result new-compst gin state)))
       (pseudo-event-form-listp item-events)))
     :rule-classes :rewrite)

    Theorem: symbolp-of-atc-gen-block-item-stmt.item-thm

    (defthm symbolp-of-atc-gen-block-item-stmt.item-thm
      (b*
       (((mv ?item ?item-limit ?item-events
             ?item-thm ?thm-index ?names-to-avoid)
         (atc-gen-block-item-stmt stmt
                                  stmt-limit stmt-events stmt-thm uterm?
                                  type result new-compst gin state)))
       (symbolp item-thm))
      :rule-classes :rewrite)

    Theorem: posp-of-atc-gen-block-item-stmt.thm-index

    (defthm posp-of-atc-gen-block-item-stmt.thm-index
      (b*
       (((mv ?item ?item-limit ?item-events
             ?item-thm ?thm-index ?names-to-avoid)
         (atc-gen-block-item-stmt stmt
                                  stmt-limit stmt-events stmt-thm uterm?
                                  type result new-compst gin state)))
       (posp thm-index))
      :rule-classes (:rewrite :type-prescription))

    Theorem: symbol-listp-of-atc-gen-block-item-stmt.names-to-avoid

    (defthm symbol-listp-of-atc-gen-block-item-stmt.names-to-avoid
      (b*
       (((mv ?item ?item-limit ?item-events
             ?item-thm ?thm-index ?names-to-avoid)
         (atc-gen-block-item-stmt stmt
                                  stmt-limit stmt-events stmt-thm uterm?
                                  type result new-compst gin state)))
       (symbol-listp names-to-avoid))
      :rule-classes :rewrite)