• 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
          • Constant-propagation
          • Specialize
          • Split-fn
          • Split-fn-when
            • Split-fn-when-implementation
              • Ext-declon-list-try-split-fn-when
              • Transunit-ensemble-split-fn-when
              • Ext-declon-try-split-fn-when
              • Filepath-transunit-map-try-split-fn-when
              • Fundef-try-split-fn-when
              • Transunit-try-split-fn-when
              • Transunit-ensemble-try-split-fn-when
              • Transunit-ensemble-split-fn-when-loop
              • Code-ensemble-split-fn-when
              • Split-fn-when-fn
              • Block-item-list-try-split-fn-when-loop
              • Block-item-list-try-split-fn-when
              • Block-item-triggerp
              • Split-fn-when-event-generation
              • Split-fn-when-input-processing
                • Split-fn-when-process-inputs
          • 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

• Split-fn-when-input-processing

Split-fn-when-process-inputs

Process the inputs.

Signature

(split-fn-when-process-inputs const-old const-new triggers wrld) 
  → 
(mv er? code const-new$ triggers)

Arguments

wrld — Guard (plist-worldp wrld).

Returns

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

code — Type (and (code-ensemblep code) (transunit-ensemble-annop (code-ensemble->transunits code))) .

const-new$ — Type (symbolp const-new$).

triggers — Type (string-listp triggers).

Definitions and Theorems

Function: split-fn-when-process-inputs

(defun split-fn-when-process-inputs
       (const-old const-new triggers wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (b*
  (((reterr) (irr-code-ensemble) nil nil)
   ((unless (symbolp const-old))
    (retmsg$ "~x0 must be a symbol" const-old))
   (code (constant-value const-old wrld))
   ((unless (code-ensemblep code))
    (retmsg$ "~x0 must be a code ensemble."
             const-old))
   (tunits (code-ensemble->transunits code))
   ((unless (transunit-ensemble-annop tunits))
    (retmsg$ "~x0 must be an annotated with validation information."
             const-old))
   ((unless (symbolp const-new))
    (retmsg$ "~x0 must be a symbol" const-new))
   (triggers (if (stringp triggers)
                 (list triggers)
               triggers))
   ((unless (string-listp triggers))
    (retmsg$ "~x0 must be a string or string list"
             triggers))
   ((when (endp triggers))
    (retmsg$ "~x0 must be a list with at least one element"
             triggers)))
  (retok code const-new triggers)))

Theorem: maybe-msgp-of-split-fn-when-process-inputs.er?

(defthm maybe-msgp-of-split-fn-when-process-inputs.er?
  (b* (((mv ?er? ?code ?const-new$ ?triggers)
        (split-fn-when-process-inputs
             const-old const-new triggers wrld)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: return-type-of-split-fn-when-process-inputs.code

(defthm return-type-of-split-fn-when-process-inputs.code
 (b* (((mv ?er? ?code ?const-new$ ?triggers)
       (split-fn-when-process-inputs
            const-old const-new triggers wrld)))
  (and (code-ensemblep code)
       (transunit-ensemble-annop (code-ensemble->transunits code))))
 :rule-classes :rewrite)

Theorem: symbolp-of-split-fn-when-process-inputs.const-new$

(defthm symbolp-of-split-fn-when-process-inputs.const-new$
  (b* (((mv ?er? ?code ?const-new$ ?triggers)
        (split-fn-when-process-inputs
             const-old const-new triggers wrld)))
    (symbolp const-new$))
  :rule-classes :type-prescription)

Theorem: string-listp-of-split-fn-when-process-inputs.triggers

(defthm string-listp-of-split-fn-when-process-inputs.triggers
  (b* (((mv ?er? ?code ?const-new$ ?triggers)
        (split-fn-when-process-inputs
             const-old const-new triggers wrld)))
    (string-listp triggers))
  :rule-classes :rewrite)