Added guards for remaining p1cs functions #1783
Conversation
|
Converting If it is important to make it a function, perhaps it should take the prime as an argument and output the appropriate data structure. Then use add-io-pairs to cache the map from prime to data structure for the two current primes, and document how to add a new prime. |
|
^^^ @akitaki79 |
|
Another way to prevent huge constants from showing up in proofs is described in :doc evisc-table. Maybe see also :doc untranslate-patterns. |
|
Another possibility is defining the nullary function in a |
|
Looks good. One thing -- did you try running this on any large R1CS circuits as Eric suggested? If this change from constant to function doesn't actually cause a slowdown, perhaps we could remove the |
| ;; This shows there are no collisions: | ||
| ;; (assert-equal (len *nums-to-strings*) (len (remove-duplicates (strip-cars *nums-to-strings*)))) | ||
| ;;This shows there are no collisions: | ||
| ;;(assert-equal (len *nums-to-strings*) (len (remove-duplicates (strip-cars *nums-to-strings*)))) |
There was a problem hiding this comment.
This comment should be updated to reflect the other changes. Run the assert-equal to make sure it was updated correctly.
The change currently does not "first calculate the constant and then define the function as exactly that constant" (quote from Zulip). As currently structured, it does calculate each constant only once, triggered by |
Co-authored-by: Eric McCarthy <7607035+bendyarm@users.noreply.github.com>
I also converted nums-to-strings from a constant to a function and added some other proofs to admit the guards for
p1cs-coefficient&p1cs-term. These proofs are really inefficient right now, so I will try to get them working faster in the future.