• 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
          • Syntax-for-tools
          • Atc
            • Atc-implementation
              • Atc-abstract-syntax
              • Atc-pretty-printer
              • Atc-event-and-code-generation
                • Atc-symbolic-computation-states
                • Atc-symbolic-execution-rules
                • Atc-gen-ext-declon-lists
                • Atc-function-and-loop-generation
                • Atc-statement-generation
                • Atc-gen-fileset
                • Atc-gen-everything
                • Atc-gen-obj-declon
                • Atc-gen-fileset-event
                • Atc-tag-tables
                • Atc-expression-generation
                • Atc-generation-contexts
                  • Atc-contextualize
                  • Atc-premise
                    • Atc-premise-fix
                    • Atc-premise-case
                    • Atc-premise-equiv
                    • Atc-premisep
                    • Atc-premise-cvalues
                    • Atc-premise-cvalue
                    • Atc-premise-compustate
                    • Atc-premise-test
                    • Atc-premise-kind
                  • Atc-contextualize-compustate
                  • Atc-context
                  • Atc-context-extend
                  • Irr-atc-context
                  • Atc-premise-list
                • Atc-gen-wf-thm
                • Term-checkers-atc
                • Atc-variable-tables
                • Term-checkers-common
                • Atc-gen-init-fun-env-thm
                • Atc-gen-appconds
                • Read-write-variables
                • Atc-gen-thm-assert-events
                • Test*
                • Atc-gen-prog-const
                • Atc-gen-expr-bool
                • Atc-theorem-generation
                • Atc-tag-generation
                • Atc-gen-expr-pure
                • Atc-function-tables
                • Atc-object-tables
              • Fty-pseudo-term-utilities
              • Atc-term-recognizers
              • Atc-input-processing
              • Atc-shallow-embedding
              • Atc-process-inputs-and-gen-everything
              • Atc-table
              • Atc-fn
              • Atc-pretty-printing-options
              • Atc-types
              • Atc-macro-definition
            • Atc-tutorial
          • Language
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • 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
  • Atc-generation-contexts

Atc-premise

Fixtype of premises.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:compustate → atc-premise-compustate
:cvalue → atc-premise-cvalue
:cvalues → atc-premise-cvalues
:test → atc-premise-test

We include bindings of the computation state. Each such binding consists of a variable for the computation state (stored in compst-var in the code generation code), and a term that must represent a computation state. The meaning is that the variable is bound to the term.

We also include bindings of single variables that hold (ACL2 models of) C values. (Note that a computation state is not, and does not model, a C value.) These also consist of a variable and a term, like the computation state bindings. However, it is useful to differentiate them in this fixtype, so we can support different processing of the different kind of bindings (as in atc-contextualize).

We also include bindings of multiple variables that hold (ACL2 models of) C values. This is similar to the bindings described in the previous paragraph, but involve mv-let instead of let.

We also include terms that are tests of ifs.

Since the terms used in premises are untranslated, we do not have type constraints on them. In the future, we could use a type for untranslated terms, perhaps a shallow/light recognizer analogous to pseudo-event-formp.

We may add more kinds later.

Subtopics

Atc-premise-fix
Fixing function for atc-premise structures.
Atc-premise-case
Case macro for the different kinds of atc-premise structures.
Atc-premise-equiv
Basic equivalence relation for atc-premise structures.
Atc-premisep
Recognizer for atc-premise structures.
Atc-premise-cvalues
Atc-premise-cvalue
Atc-premise-compustate
Atc-premise-test
Atc-premise-kind
Get the kind (tag) of a atc-premise structure.