• 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-header

Check if a function header is statically well-formed.

Signature

(check-function-header header ctxt) → err?

Arguments

header — Guard (function-headerp header).

ctxt — Guard (contextp ctxt).

When checking a function header, no types are being defined, no variables are in scope, and no obligation variables and hypotheses are present. But there may be (other) function headers, which happens when checking mutually recursive functions.

The name must not be the name of an already defined function. Input and output types must be well-formed. Input and output names must be all distinct.

Definitions and Theorems

Function: check-function-header

(defun check-function-header (header ctxt)
 (declare (xargs :guard (and (function-headerp header)
                             (contextp ctxt))))
 (declare
      (xargs :guard (and (null (context->types ctxt))
                         (omap::emptyp (context->variables ctxt))
                         (null (context->obligation-vars ctxt))
                         (null (context->obligation-hyps ctxt)))))
 (let ((__function__ 'check-function-header))
  (declare (ignorable __function__))
  (b*
   (((function-header header) header)
    ((when
         (get-function-definition header.name (context->tops ctxt)))
     (list :function-alread-defined header.name))
    (input-types (typed-variable-list->type-list header.inputs))
    ((when (not (check-type-list input-types ctxt)))
     (list :malformed-input-types
           header.name input-types))
    (output-types (typed-variable-list->type-list header.outputs))
    ((when (not (check-type-list output-types ctxt)))
     (list :malformed-output-types
           header.name output-types))
    (input-output-names
         (append (typed-variable-list->name-list header.inputs)
                 (typed-variable-list->name-list header.outputs)))
    ((unless (no-duplicatesp-equal input-output-names))
     (list :duplicate-input/output-names
           header.name input-output-names)))
   nil)))

Theorem: check-function-header-of-function-header-fix-header

(defthm check-function-header-of-function-header-fix-header
  (equal (check-function-header (function-header-fix header)
                                ctxt)
         (check-function-header header ctxt)))

Theorem: check-function-header-function-header-equiv-congruence-on-header

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

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

(defthm check-function-header-of-context-fix-ctxt
  (equal (check-function-header header (context-fix ctxt))
         (check-function-header header ctxt)))

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

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