• 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

Check-function-definition

Check if a function definition (at the top level) is statically well-formed.

Signature

(check-function-definition fundef ctxt) → (mv err? obligs)

Arguments

fundef — Guard (function-definitionp fundef).

ctxt — Guard (contextp ctxt).

Returns

obligs — Type (proof-obligation-listp obligs).

We augment the context with the header and call the more general ACL2 function. Thus, we allow the function to be (singly) recursive.

For now we allow any recursion, but we will extend this code to only allow certain forms, or to generate more explicit termination obligations.

Definitions and Theorems

Function: check-function-definition

(defun check-function-definition (fundef ctxt)
  (declare (xargs :guard (and (function-definitionp fundef)
                              (contextp ctxt))))
  (declare
       (xargs :guard (and (null (context->types ctxt))
                          (null (context->functions ctxt))
                          (omap::emptyp (context->variables ctxt))
                          (null (context->obligation-vars ctxt))
                          (null (context->obligation-hyps ctxt)))))
  (let ((__function__ 'check-function-definition))
    (declare (ignorable __function__))
    (b* ((header (function-definition->header fundef))
         (ctxt (change-context ctxt
                               :functions (list header))))
      (check-function-definition-top/nontop fundef ctxt))))

Theorem: proof-obligation-listp-of-check-function-definition.obligs

(defthm proof-obligation-listp-of-check-function-definition.obligs
  (b* (((mv ?err? ?obligs)
        (check-function-definition fundef ctxt)))
    (proof-obligation-listp obligs))
  :rule-classes :rewrite)

Theorem: check-function-definition-of-function-definition-fix-fundef

(defthm check-function-definition-of-function-definition-fix-fundef
  (equal (check-function-definition (function-definition-fix fundef)
                                    ctxt)
         (check-function-definition fundef ctxt)))

Theorem: check-function-definition-function-definition-equiv-congruence-on-fundef

(defthm
 check-function-definition-function-definition-equiv-congruence-on-fundef
 (implies (function-definition-equiv fundef fundef-equiv)
          (equal (check-function-definition fundef ctxt)
                 (check-function-definition fundef-equiv ctxt)))
 :rule-classes :congruence)

Theorem: check-function-definition-of-context-fix-ctxt

(defthm check-function-definition-of-context-fix-ctxt
  (equal (check-function-definition fundef (context-fix ctxt))
         (check-function-definition fundef ctxt)))

Theorem: check-function-definition-context-equiv-congruence-on-ctxt

(defthm check-function-definition-context-equiv-congruence-on-ctxt
  (implies (context-equiv ctxt ctxt-equiv)
           (equal (check-function-definition fundef ctxt)
                  (check-function-definition fundef ctxt-equiv)))
  :rule-classes :congruence)