• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Error-checking
      • Apt
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Prime-field-constraint-systems
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
        • Primitive-functions
        • Translated-terms
        • Values
        • Evaluation
          • Step-from-trans
          • Call-primitive-function
          • Step-from-init
          • Put-leftmost-nonconst
          • Exec-outcome
          • Stepn
          • Step
          • Terminatingp
          • Get-leftmost-nonconst
          • Exec-call
          • Step*
        • Program-equivalence
        • Functions
        • Packages
        • Programs
        • Interpreter
        • Evaluation-states
      • Prime-fields
      • Java
      • C
      • Syntheto
      • Number-theory
      • Cryptography
      • Lists-light
      • File-io-light
      • Json
      • Built-ins
      • Solidity
      • Axe
      • Std-extensions
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Evaluation

Call-primitive-function

Call a primitive function on some arguments.

Signature

(call-primitive-function name arguments program) → result

Arguments

name — Guard (and (symbol-valuep name) (primitive-function-namep name)).

arguments — Guard (value-listp arguments).

program — Guard (programp program).

Returns

result — Type (value-optionp result).

This is used by step-from-trans when encountering a call of a primitive function.

We dispatch based on the primitive function name. If the number of arguments does not match the arity, we return nil. Otherwise, we return the value resulting from executing the primitive function.

Definitions and Theorems

Function: call-primitive-function

(defun
 call-primitive-function
 (name arguments program)
 (declare (xargs :guard (and (and (symbol-valuep name)
                                  (primitive-function-namep name))
                             (value-listp arguments)
                             (programp program))))
 (let
  ((__function__ 'call-primitive-function))
  (declare (ignorable __function__))
  (cond
    ((symbol-value-equiv name (lift-symbol 'acl2-numberp))
     (and (= (len arguments) 1)
          (eval-acl2-numberp (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'rationalp))
     (and (= (len arguments) 1)
          (eval-rationalp (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'integerp))
     (and (= (len arguments) 1)
          (eval-integerp (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'complex-rationalp))
     (and (= (len arguments) 1)
          (eval-complex-rationalp (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'complex))
     (and (= (len arguments) 2)
          (eval-complex (first arguments)
                        (second arguments))))
    ((symbol-value-equiv name (lift-symbol 'realpart))
     (and (= (len arguments) 1)
          (eval-realpart (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'imagpart))
     (and (= (len arguments) 1)
          (eval-imagpart (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'numerator))
     (and (= (len arguments) 1)
          (eval-numerator (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'denominator))
     (and (= (len arguments) 1)
          (eval-denominator (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'unary--))
     (and (= (len arguments) 1)
          (eval-unary-- (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'unary-/))
     (and (= (len arguments) 1)
          (eval-unary-/ (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'binary-+))
     (and (= (len arguments) 2)
          (eval-binary-+ (first arguments)
                         (second arguments))))
    ((symbol-value-equiv name (lift-symbol 'binary-*))
     (and (= (len arguments) 2)
          (eval-binary-* (first arguments)
                         (second arguments))))
    ((symbol-value-equiv name (lift-symbol '<))
     (and (= (len arguments) 2)
          (eval-< (first arguments)
                  (second arguments))))
    ((symbol-value-equiv name (lift-symbol 'characterp))
     (and (= (len arguments) 1)
          (eval-characterp (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'char-code))
     (and (= (len arguments) 1)
          (eval-char-code (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'code-char))
     (and (= (len arguments) 1)
          (eval-code-char (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'stringp))
     (and (= (len arguments) 1)
          (eval-stringp (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'coerce))
     (and (= (len arguments) 2)
          (eval-coerce (first arguments)
                       (second arguments))))
    ((symbol-value-equiv name (lift-symbol 'symbolp))
     (and (= (len arguments) 1)
          (eval-symbolp (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'symbol-package-name))
     (and (= (len arguments) 1)
          (eval-symbol-package-name (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'symbol-name))
     (and (= (len arguments) 1)
          (eval-symbol-package-name (first arguments))))
    ((symbol-value-equiv name
                         (lift-symbol 'intern-in-package-of-symbol))
     (and (= (len arguments) 2)
          (eval-intern-in-package-of-symbol
               (first arguments)
               (second arguments)
               (program->packages program))))
    ((symbol-value-equiv name (lift-symbol 'consp))
     (and (= (len arguments) 1)
          (eval-consp (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'cons))
     (and (= (len arguments) 2)
          (eval-cons (first arguments)
                     (second arguments))))
    ((symbol-value-equiv name (lift-symbol 'car))
     (and (= (len arguments) 1)
          (eval-car (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'cdr))
     (and (= (len arguments) 1)
          (eval-cdr (first arguments))))
    ((symbol-value-equiv name (lift-symbol 'pkg-imports))
     (and (= (len arguments) 1)
          (eval-pkg-imports (first arguments)
                            (program->packages program))))
    ((symbol-value-equiv name (lift-symbol 'pkg-witness))
     (and (= (len arguments) 1)
          (eval-pkg-witness (first arguments)
                            (program->packages program))))
    ((symbol-value-equiv name (lift-symbol 'equal))
     (and (= (len arguments) 2)
          (eval-equal (first arguments)
                      (second arguments))))
    ((symbol-value-equiv name (lift-symbol 'if))
     (and (= (len arguments) 3)
          (eval-if (first arguments)
                   (second arguments)
                   (third arguments))))
    ((symbol-value-equiv name (lift-symbol 'acl2::bad-atom<=))
     (and (= (len arguments) 2)
          (eval-bad-atom<= (first arguments)
                           (second arguments))))
    (t (impossible)))))

Theorem: value-optionp-of-call-primitive-function

(defthm
     value-optionp-of-call-primitive-function
     (b* ((result (call-primitive-function name arguments program)))
         (value-optionp result))
     :rule-classes :rewrite)

Theorem: call-primitive-function-of-value-list-fix-arguments

(defthm
     call-primitive-function-of-value-list-fix-arguments
     (equal (call-primitive-function name (value-list-fix arguments)
                                     program)
            (call-primitive-function name arguments program)))

Theorem: call-primitive-function-value-list-equiv-congruence-on-arguments

(defthm
 call-primitive-function-value-list-equiv-congruence-on-arguments
 (implies
     (value-list-equiv arguments arguments-equiv)
     (equal (call-primitive-function name arguments program)
            (call-primitive-function name arguments-equiv program)))
 :rule-classes :congruence)

Theorem: call-primitive-function-of-program-fix-program

(defthm
 call-primitive-function-of-program-fix-program
 (equal
      (call-primitive-function name arguments (program-fix program))
      (call-primitive-function name arguments program)))

Theorem: call-primitive-function-program-equiv-congruence-on-program

(defthm
 call-primitive-function-program-equiv-congruence-on-program
 (implies
     (program-equiv program program-equiv)
     (equal (call-primitive-function name arguments program)
            (call-primitive-function name arguments program-equiv)))
 :rule-classes :congruence)