• 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
        • 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
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Evaluation

Step-from-init

Evaluation step from the initial state.

Signature

(step-from-init function arguments) → estate

Arguments

function — Guard (symbol-valuep function).

arguments — Guard (value-listp arguments).

Returns

estate — Type (eval-state-p estate).

In our formalization, an evaluation sequence starts with a call of a named function on some argument values, which together form an initial state (see eval-state). The first evaluation step, which starts from this initial state, is formalized here, given the function symbol and argument values.

This first evaluation step produces the first transitional state of the evaluation sequence. This transitional state consists of a stack with a single frame that contains the empty binding and the ground call of the function symbol on the quoted values.

Definitions and Theorems

Function: step-from-init

(defun step-from-init (function arguments)
 (declare (xargs :guard (and (symbol-valuep function)
                             (value-listp arguments))))
 (let ((__function__ 'step-from-init))
  (declare (ignorable __function__))
  (b*
   ((frame
      (make-frame :term (tterm-call (tfunction-named function)
                                    (tterm-constant-list arguments))
                  :binding nil))
    (stack (list frame)))
   (eval-state-trans stack))))

Theorem: eval-state-p-of-step-from-init

(defthm eval-state-p-of-step-from-init
  (b* ((estate (step-from-init function arguments)))
    (eval-state-p estate))
  :rule-classes :rewrite)

Theorem: step-from-init-of-symbol-value-fix-function

(defthm step-from-init-of-symbol-value-fix-function
  (equal (step-from-init (symbol-value-fix function)
                         arguments)
         (step-from-init function arguments)))

Theorem: step-from-init-symbol-value-equiv-congruence-on-function

(defthm step-from-init-symbol-value-equiv-congruence-on-function
  (implies (symbol-value-equiv function function-equiv)
           (equal (step-from-init function arguments)
                  (step-from-init function-equiv arguments)))
  :rule-classes :congruence)

Theorem: step-from-init-of-value-list-fix-arguments

(defthm step-from-init-of-value-list-fix-arguments
  (equal (step-from-init function (value-list-fix arguments))
         (step-from-init function arguments)))

Theorem: step-from-init-value-list-equiv-congruence-on-arguments

(defthm step-from-init-value-list-equiv-congruence-on-arguments
  (implies (value-list-equiv arguments arguments-equiv)
           (equal (step-from-init function arguments)
                  (step-from-init function arguments-equiv)))
  :rule-classes :congruence)