• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
            • Sr1cs-constraintp
            • R1cs-polynomialp
            • R1cs-constraintp
            • R1cs-monomialp
            • Sr1cs-definitionp
            • R1cs-systemp
            • Sr1cs-systemp
            • Sr1cs-definition-listp
            • Sr1cs-constraint-listp
            • R1cs-constraint-listp
          • Semantics
          • Abstract-syntax
          • Well-formedness
          • 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
  • Prime-field-constraint-systems

R1cs-subset

R1CS subset of PFCSes.

PFCSes generalize R1CSes; a subset of PFCSes corresponds to R1CSes. Here we characterize that subset.

We provide two related characterizations. One is that of a PFCS that is an R1CS, i.e. it has no definitions and all the constraints are in R1CS form. Another is that of a PFCS that has definitions, but all its equality constraints are in R1CS form, and all its relation applications have constants or variables as arguments. The latter kind of PFCS can be regarded as a structured R1CS: the constraints are all in R1CS form in the end, but they may be organized hierarchically, via defined relations. We use the prefix sr1cs for predicates that define these structured R1CSes.

Our characterization of R1CS monomials, polynomials, and equality constraints is a natural one, but not necessarily the only one possible. In particular, PFCS expressions are trees, and there are many tree shapes that represent linear polynomials, besides the left-associated ones that we use here.

Subtopics

Sr1cs-constraintp
Check if a PFCS constraint is a structured R1CS constraint.
R1cs-polynomialp
Check if a PFCS expression is an R1CS polynomial.
R1cs-constraintp
Check if a PFCS constraint is an R1CS constraint.
R1cs-monomialp
Check if a PFCS expression is an R1CS monomial.
Sr1cs-definitionp
Check if a PFCS definition consists of strcutred R1CS constraints.
R1cs-systemp
Check if a PFCS is an R1CS.
Sr1cs-systemp
Check if a PFCS system consits of structured R1CS constraints.
Sr1cs-definition-listp
Check if a list of PFCS definitions consist of structured R1CS constraints.
Sr1cs-constraint-listp
Check if a list of PFCS constraints consists of structured R1CS constraints.
R1cs-constraint-listp
Check if a list of PFCS constraints consists of R1CS constraints.