• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Pfcs
      • Proof-support
      • Semantics
        • Exec-proof-tree
        • Assertion-list->constr-list
        • Assertion-list->asg-list
        • Eval-expr
        • Eval-expr-list
        • Assignment-wfp
        • Assertion
        • Proof-outcome
        • Proof-list-outcome
        • Assertion-list-from
        • Definition-satp
        • Constraint-satp
        • Assignment
        • System-satp
        • Constraint-list-satp
        • Assertion-list
        • Assignment-list
        • Proof-trees
      • Lifting
      • R1cs-subset
      • Indexed-names
      • Well-formedness
      • Abstract-syntax
      • Concrete-syntax
      • R1cs-bridge
      • Parser-interface
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Riscv
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Semantics

Assertion-list-from

Lift assertion to lists.

Signature

(assertion-list-from asgs constrs) → asrs

Arguments

asgs — Guard (assignment-listp asgs).

constrs — Guard (constraint-listp constrs).

Returns

asrs — Type (assertion-listp asrs).

Definitions and Theorems

Function: assertion-list-from

(defun assertion-list-from (asgs constrs)
  (declare (xargs :guard (and (assignment-listp asgs)
                              (constraint-listp constrs))))
  (declare (xargs :guard (equal (len asgs) (len constrs))))
  (let ((__function__ 'assertion-list-from))
    (declare (ignorable __function__))
    (cond ((endp asgs) nil)
          ((endp constrs) (acl2::impossible))
          (t (cons (assertion (car asgs) (car constrs))
                   (assertion-list-from (cdr asgs)
                                        (cdr constrs)))))))

Theorem: assertion-listp-of-assertion-list-from

(defthm assertion-listp-of-assertion-list-from
  (b* ((asrs (assertion-list-from asgs constrs)))
    (assertion-listp asrs))
  :rule-classes :rewrite)

Theorem: assertion-list->asg-list-of-assertion-list-from

(defthm assertion-list->asg-list-of-assertion-list-from
 (implies
  (equal (len asgs) (len constrs))
  (equal
       (assertion-list->asg-list (assertion-list-from asgs constrs))
       (assignment-list-fix asgs))))

Theorem: assertion-list->constr-list-of-assertion-list-from

(defthm assertion-list->constr-list-of-assertion-list-from
 (implies
  (equal (len asgs) (len constrs))
  (equal
    (assertion-list->constr-list (assertion-list-from asgs constrs))
    (constraint-list-fix constrs))))

Theorem: assertion-list-from-of-assertion-list->asg/constr-list

(defthm assertion-list-from-of-assertion-list->asg/constr-list
 (implies
  (assertion-listp assertions)
  (equal
      (assertion-list-from (assertion-list->asg-list assertions)
                           (assertion-list->constr-list assertions))
      assertions)))

Theorem: len-of-assertion-list-from

(defthm len-of-assertion-list-from
  (equal (len (assertion-list-from asgs constrs))
         (min (len asgs) (len constrs))))

Theorem: assertion-list-from-of-assignment-list-fix-asgs

(defthm assertion-list-from-of-assignment-list-fix-asgs
  (equal (assertion-list-from (assignment-list-fix asgs)
                              constrs)
         (assertion-list-from asgs constrs)))

Theorem: assertion-list-from-assignment-list-equiv-congruence-on-asgs

(defthm assertion-list-from-assignment-list-equiv-congruence-on-asgs
  (implies (assignment-list-equiv asgs asgs-equiv)
           (equal (assertion-list-from asgs constrs)
                  (assertion-list-from asgs-equiv constrs)))
  :rule-classes :congruence)

Theorem: assertion-list-from-of-constraint-list-fix-constrs

(defthm assertion-list-from-of-constraint-list-fix-constrs
  (equal (assertion-list-from asgs (constraint-list-fix constrs))
         (assertion-list-from asgs constrs)))

Theorem: assertion-list-from-constraint-list-equiv-congruence-on-constrs

(defthm
    assertion-list-from-constraint-list-equiv-congruence-on-constrs
  (implies (constraint-list-equiv constrs constrs-equiv)
           (equal (assertion-list-from asgs constrs)
                  (assertion-list-from asgs constrs-equiv)))
  :rule-classes :congruence)