• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
      • C
        • Syntax-for-tools
        • Atc
        • Transformation-tools
          • Simpadd0
          • Proof-generation
          • Split-gso
          • Wrap-fn
            • Wrap-fn-implementation
              • Init-declor-list-wrap-fn-add-wrapper-def
              • Declor-wrap-fn-add-wrapper-def
              • Ext-declon-wrap-fn-add-wrapper-def
              • Fundef-wrap-fn-add-wrapper-def
              • Declon-wrap-fn-add-wrapper-def
              • Ext-declon-list-wrap-fn
              • Wrap-fn-process-param-declon-list-loop
              • Filepath-transunit-map-wrap-fn
              • Wrap-fn-process-param-declon-list
              • Transunit-wrap-fn
              • Transunit-ensemble-wrap-fn
              • Code-ensemble-wrap-fn
              • Code-ensemble-wrap-fn-multiple
              • Declor-wrap-fn-make-wrapper
              • Dirdeclor-wrap-fn-make-wrapper
              • Wrap-fn-input-processing
              • Wrap-fn-event-generation
                • Wrap-fn-gen-everything
                • Wrap-fn-process-inputs-and-gen-everything
                • Wrap-fn-fn
                • Wrap-fn-macro-definition
          • Constant-propagation
          • Specialize
          • Split-fn
          • Split-fn-when
          • Split-all-gso
          • Copy-fn
          • Variables-in-computation-states
          • Rename
          • Utilities
          • Proof-generation-theorems
          • Input-processing
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Wrap-fn-event-generation

Wrap-fn-gen-everything

Generate all the events.

Signature

(wrap-fn-gen-everything code const-new targets) 
  → 
(mv er? event)

Arguments

code — Guard (code-ensemblep code).

const-new — Guard (symbolp const-new).

targets — Guard (ident-ident-option-mapp targets).

Returns

er? — Type (maybe-msgp er?).

event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: wrap-fn-gen-everything

(defun wrap-fn-gen-everything (code const-new targets)
  (declare (xargs :guard (and (code-ensemblep code)
                              (symbolp const-new)
                              (ident-ident-option-mapp targets))))
  (declare (xargs :guard (code-ensemble-annop code)))
  (b*
   (((reterr) '(_))
    (const-new (mbe :logic (acl2::symbol-fix const-new)
                    :exec const-new))
    ((erp code)
     (code-ensemble-wrap-fn-multiple code targets))
    (defconst-event (cons 'defconst
                          (cons const-new
                                (cons (cons 'quote (cons code 'nil))
                                      'nil)))))
   (retok defconst-event)))

Theorem: maybe-msgp-of-wrap-fn-gen-everything.er?

(defthm maybe-msgp-of-wrap-fn-gen-everything.er?
  (b* (((mv ?er? acl2::?event)
        (wrap-fn-gen-everything code const-new targets)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-wrap-fn-gen-everything.event

(defthm pseudo-event-formp-of-wrap-fn-gen-everything.event
  (b* (((mv ?er? acl2::?event)
        (wrap-fn-gen-everything code const-new targets)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Theorem: wrap-fn-gen-everything-of-code-ensemble-fix-code

(defthm wrap-fn-gen-everything-of-code-ensemble-fix-code
  (equal (wrap-fn-gen-everything (c$::code-ensemble-fix code)
                                 const-new targets)
         (wrap-fn-gen-everything code const-new targets)))

Theorem: wrap-fn-gen-everything-code-ensemble-equiv-congruence-on-code

(defthm
      wrap-fn-gen-everything-code-ensemble-equiv-congruence-on-code
 (implies
      (c$::code-ensemble-equiv code code-equiv)
      (equal (wrap-fn-gen-everything code const-new targets)
             (wrap-fn-gen-everything code-equiv const-new targets)))
 :rule-classes :congruence)

Theorem: wrap-fn-gen-everything-of-symbol-fix-const-new

(defthm wrap-fn-gen-everything-of-symbol-fix-const-new
  (equal (wrap-fn-gen-everything code (acl2::symbol-fix const-new)
                                 targets)
         (wrap-fn-gen-everything code const-new targets)))

Theorem: wrap-fn-gen-everything-symbol-equiv-congruence-on-const-new

(defthm wrap-fn-gen-everything-symbol-equiv-congruence-on-const-new
 (implies
      (acl2::symbol-equiv const-new const-new-equiv)
      (equal (wrap-fn-gen-everything code const-new targets)
             (wrap-fn-gen-everything code const-new-equiv targets)))
 :rule-classes :congruence)

Theorem: wrap-fn-gen-everything-of-ident-ident-option-map-fix-targets

(defthm wrap-fn-gen-everything-of-ident-ident-option-map-fix-targets
  (equal
       (wrap-fn-gen-everything code const-new
                               (ident-ident-option-map-fix targets))
       (wrap-fn-gen-everything code const-new targets)))

Theorem: wrap-fn-gen-everything-ident-ident-option-map-equiv-congruence-on-targets

(defthm
 wrap-fn-gen-everything-ident-ident-option-map-equiv-congruence-on-targets
 (implies
      (ident-ident-option-map-equiv targets targets-equiv)
      (equal (wrap-fn-gen-everything code const-new targets)
             (wrap-fn-gen-everything code const-new targets-equiv)))
 :rule-classes :congruence)