• 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
              • Initdeclor-list-wrap-fn-add-wrapper-def
              • Declor-wrap-fn-add-wrapper-def
              • Fundef-wrap-fn-add-wrapper-def
              • Extdecl-wrap-fn-add-wrapper-def
              • Decl-wrap-fn-add-wrapper-def
              • Extdecl-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
          • 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-implementation

Wrap-fn-process-param-declon-list

Check that the parameter list is supported and add parameter names as necessary.

Signature

(wrap-fn-process-param-declon-list 
     params fresh-ident-base blacklist) 
 
  → 
(mv erp blacklist$ params$ idents)

Arguments

params — Guard (param-declon-listp params).

fresh-ident-base — Guard (identp fresh-ident-base).

blacklist — Guard (ident-setp blacklist).

Returns

erp — Type (booleanp erp).

blacklist$ — Type (ident-setp blacklist$).

params$ — Type (param-declon-listp params$).

idents — Type (ident-listp idents).

Definitions and Theorems

Function: wrap-fn-process-param-declon-list

(defun wrap-fn-process-param-declon-list
       (params fresh-ident-base blacklist)
 (declare (xargs :guard (and (param-declon-listp params)
                             (identp fresh-ident-base)
                             (ident-setp blacklist))))
 (b*
  (((reterr) nil nil nil)
   (blacklist (ident-set-fix blacklist))
   (params (param-declon-list-fix params))
   ((when
     (equal
      params
      (list
        (make-param-declon
             :specs (list (decl-spec-typespec (c$::type-spec-void)))
             :declor (param-declor-none)
             :attribs nil))))
    (retok blacklist params nil)))
  (wrap-fn-process-param-declon-list-loop
       params fresh-ident-base blacklist)))

Theorem: booleanp-of-wrap-fn-process-param-declon-list.erp

(defthm booleanp-of-wrap-fn-process-param-declon-list.erp
  (b* (((mv acl2::?erp ?blacklist$ ?params$ ?idents)
        (wrap-fn-process-param-declon-list
             params fresh-ident-base blacklist)))
    (booleanp erp))
  :rule-classes :type-prescription)

Theorem: ident-setp-of-wrap-fn-process-param-declon-list.blacklist$

(defthm ident-setp-of-wrap-fn-process-param-declon-list.blacklist$
  (b* (((mv acl2::?erp ?blacklist$ ?params$ ?idents)
        (wrap-fn-process-param-declon-list
             params fresh-ident-base blacklist)))
    (ident-setp blacklist$))
  :rule-classes :rewrite)

Theorem: param-declon-listp-of-wrap-fn-process-param-declon-list.params$

(defthm
    param-declon-listp-of-wrap-fn-process-param-declon-list.params$
  (b* (((mv acl2::?erp ?blacklist$ ?params$ ?idents)
        (wrap-fn-process-param-declon-list
             params fresh-ident-base blacklist)))
    (param-declon-listp params$))
  :rule-classes :rewrite)

Theorem: ident-listp-of-wrap-fn-process-param-declon-list.idents

(defthm ident-listp-of-wrap-fn-process-param-declon-list.idents
  (b* (((mv acl2::?erp ?blacklist$ ?params$ ?idents)
        (wrap-fn-process-param-declon-list
             params fresh-ident-base blacklist)))
    (ident-listp idents))
  :rule-classes :rewrite)

Theorem: true-listp-of-wrap-fn-process-param-declon-list.idents

(defthm true-listp-of-wrap-fn-process-param-declon-list.idents
  (b* (((mv acl2::?erp ?blacklist$ ?params$ ?idents)
        (wrap-fn-process-param-declon-list
             params fresh-ident-base blacklist)))
    (true-listp idents))
  :rule-classes :type-prescription)

Theorem: wrap-fn-process-param-declon-list-of-param-declon-list-fix-params

(defthm
  wrap-fn-process-param-declon-list-of-param-declon-list-fix-params
 (equal
   (wrap-fn-process-param-declon-list (param-declon-list-fix params)
                                      fresh-ident-base blacklist)
   (wrap-fn-process-param-declon-list
        params fresh-ident-base blacklist)))

Theorem: wrap-fn-process-param-declon-list-param-declon-list-equiv-congruence-on-params

(defthm
 wrap-fn-process-param-declon-list-param-declon-list-equiv-congruence-on-params
 (implies
  (c$::param-declon-list-equiv params params-equiv)
  (equal
    (wrap-fn-process-param-declon-list
         params fresh-ident-base blacklist)
    (wrap-fn-process-param-declon-list params-equiv
                                       fresh-ident-base blacklist)))
 :rule-classes :congruence)

Theorem: wrap-fn-process-param-declon-list-of-ident-fix-fresh-ident-base

(defthm
    wrap-fn-process-param-declon-list-of-ident-fix-fresh-ident-base
  (equal (wrap-fn-process-param-declon-list
              params (ident-fix fresh-ident-base)
              blacklist)
         (wrap-fn-process-param-declon-list
              params fresh-ident-base blacklist)))

Theorem: wrap-fn-process-param-declon-list-ident-equiv-congruence-on-fresh-ident-base

(defthm
 wrap-fn-process-param-declon-list-ident-equiv-congruence-on-fresh-ident-base
 (implies (c$::ident-equiv fresh-ident-base fresh-ident-base-equiv)
          (equal (wrap-fn-process-param-declon-list
                      params fresh-ident-base blacklist)
                 (wrap-fn-process-param-declon-list
                      params
                      fresh-ident-base-equiv blacklist)))
 :rule-classes :congruence)

Theorem: wrap-fn-process-param-declon-list-of-ident-set-fix-blacklist

(defthm wrap-fn-process-param-declon-list-of-ident-set-fix-blacklist
  (equal
       (wrap-fn-process-param-declon-list params fresh-ident-base
                                          (ident-set-fix blacklist))
       (wrap-fn-process-param-declon-list
            params fresh-ident-base blacklist)))

Theorem: wrap-fn-process-param-declon-list-ident-set-equiv-congruence-on-blacklist

(defthm
 wrap-fn-process-param-declon-list-ident-set-equiv-congruence-on-blacklist
 (implies (c$::ident-set-equiv blacklist blacklist-equiv)
          (equal (wrap-fn-process-param-declon-list
                      params fresh-ident-base blacklist)
                 (wrap-fn-process-param-declon-list
                      params
                      fresh-ident-base blacklist-equiv)))
 :rule-classes :congruence)