• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
            • Exec
            • Find-fun
            • Init-local
            • Write-vars-values
            • Add-vars-values
            • Add-funs
            • Eoutcome
            • Soutcome
              • Soutcome-fix
              • Soutcome-equiv
              • Make-soutcome
              • Soutcome->cstate
              • Change-soutcome
              • Soutcome->mode
              • Soutcomep
            • Ensure-funscope-disjoint
            • Write-var-value
            • Restrict-vars
            • Add-var-value
            • Funinfo
            • Exec-top-block
            • Values
            • 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
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Dynamic-semantics

Soutcome

Fixtype of statement outcomes.

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

Fields
cstate — cstate
mode — mode

According to [Yul: Specification of Yul: Formal Specification], the execution of a statement results in not only possibly updated global and local states, but also a mode. [Yul: Specification of Yul: Formal Specification] does not have an explicit name for this notion, which in our formalization consists of a computation state and a mode. We call this a statement outcome.

Subtopics

Soutcome-fix
Fixing function for soutcome structures.
Soutcome-equiv
Basic equivalence relation for soutcome structures.
Make-soutcome
Basic constructor macro for soutcome structures.
Soutcome->cstate
Get the cstate field from a soutcome.
Change-soutcome
Modifying constructor for soutcome structures.
Soutcome->mode
Get the mode field from a soutcome.
Soutcomep
Recognizer for soutcome structures.