• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Error-checking
      • Apt
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Prime-field-constraint-systems
        • Proof-support
        • R1cs-subset
        • Semantics
        • Abstract-syntax
        • Well-formedness
          • Definition-list-wfp
          • Definition-wfp
          • Constraint-wfp
          • Constraint-list-wfp
          • System-wfp
        • Abstract-syntax-operations
        • R1cs-bridge
        • Concrete-syntax
        • Prime-field-library-extensions
        • R1cs-library-extensions
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Java
      • C
      • Syntheto
      • Number-theory
      • Cryptography
      • Lists-light
      • File-io-light
      • Json
      • Built-ins
      • Solidity
      • Axe
      • Std-extensions
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Well-formedness

Constraint-list-wfp

Check if a list of constraints is well-formed, with respect to a list of relation definitions.

Signature

(constraint-list-wfp constrs defs) → yes/no

Arguments

constrs — Guard (constraint-listp constrs).

defs — Guard (definition-listp defs).

Returns

yes/no — Type (booleanp yes/no).

A list of constraints is well-formed iff all the constraints are well-formed.

Definitions and Theorems

Function: constraint-list-wfp

(defun constraint-list-wfp (constrs defs)
       (declare (xargs :guard (and (constraint-listp constrs)
                                   (definition-listp defs))))
       (let ((__function__ 'constraint-list-wfp))
            (declare (ignorable __function__))
            (or (endp constrs)
                (and (constraint-wfp (car constrs) defs)
                     (constraint-list-wfp (cdr constrs)
                                          defs)))))

Theorem: booleanp-of-constraint-list-wfp

(defthm booleanp-of-constraint-list-wfp
        (b* ((yes/no (constraint-list-wfp constrs defs)))
            (booleanp yes/no))
        :rule-classes :rewrite)

Theorem: constraint-list-wfp-of-constraint-list-fix-constrs

(defthm constraint-list-wfp-of-constraint-list-fix-constrs
        (equal (constraint-list-wfp (constraint-list-fix constrs)
                                    defs)
               (constraint-list-wfp constrs defs)))

Theorem: constraint-list-wfp-constraint-list-equiv-congruence-on-constrs

(defthm
     constraint-list-wfp-constraint-list-equiv-congruence-on-constrs
     (implies (constraint-list-equiv constrs constrs-equiv)
              (equal (constraint-list-wfp constrs defs)
                     (constraint-list-wfp constrs-equiv defs)))
     :rule-classes :congruence)

Theorem: constraint-list-wfp-of-definition-list-fix-defs

(defthm
     constraint-list-wfp-of-definition-list-fix-defs
     (equal (constraint-list-wfp constrs (definition-list-fix defs))
            (constraint-list-wfp constrs defs)))

Theorem: constraint-list-wfp-definition-list-equiv-congruence-on-defs

(defthm constraint-list-wfp-definition-list-equiv-congruence-on-defs
        (implies (definition-list-equiv defs defs-equiv)
                 (equal (constraint-list-wfp constrs defs)
                        (constraint-list-wfp constrs defs-equiv)))
        :rule-classes :congruence)