• 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
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
          • Transformations
          • Language
            • Abstract-syntax
            • Dynamic-semantics
              • Exec
              • Find-fun
              • Init-local
              • Write-vars-values
              • Add-vars-values
              • Add-funs
              • Eoutcome
              • Soutcome
              • Ensure-funscope-disjoint
              • Write-var-value
              • Restrict-vars
              • Add-var-value
              • Funinfo
              • Exec-top-block
              • Values
              • Cstate
                • Cstate-fix
                • Cstatep
                • Cstate-equiv
                • Make-cstate
                • Cstate->local
                • Change-cstate
              • Funinfo+funenv
              • Read-vars-values
              • Read-var-value
              • Funenv
              • Funscope-for-fundefs
              • Exec-path
              • Path-to-var
              • Funinfo+funenv-result
              • Exec-literal
              • Soutcome-result
              • Mode-set-result
              • Literal-evaluation
              • Funscope-result
              • Funinfo-result
              • Funenv-result
              • Eoutcome-result
              • Cstate-result
              • Paths-to-vars
              • Funinfo-for-fundef
              • Lstate
              • Funscope
              • Mode-set
              • Modes
            • Concrete-syntax
            • Static-soundness
            • Static-semantics
            • Errors
          • Yul-json
        • 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
  • Dynamic-semantics

Cstate

Fixtype of computation states.

This is a product type introduced by fty::defprod.

Fields
local — lstate

According to [Yul: Specification of Yul: Formal Specification], this consists of a local state object and a global state object. The latter is generic in generic Yul. For now, for simplicity, we ignore the global state completely, but we plan to add that at some point.

Subtopics

Cstate-fix
Fixing function for cstate structures.
Cstatep
Recognizer for cstate structures.
Cstate-equiv
Basic equivalence relation for cstate structures.
Make-cstate
Basic constructor macro for cstate structures.
Cstate->local
Get the local field from a cstate.
Change-cstate
Modifying constructor for cstate structures.