You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Along the lines of similar work in SAW (GaloisInc/saw-script#1037), and building on the same infrastructure, it may be useful to allow Cryptol users to pass universally-quantified axioms to solvers. Given that we already have a notion of properties, which are implicitly universally quantified, this could look something like:
:proveWith lemma1, lemma2 : goal
where lemma1 and lemma2 are the names of already-specified properties, and goal is a Cryptol expression of the same form as can be currently passed to :prove.
The text was updated successfully, but these errors were encountered:
Along the lines of similar work in SAW (GaloisInc/saw-script#1037), and building on the same infrastructure, it may be useful to allow Cryptol users to pass universally-quantified axioms to solvers. Given that we already have a notion of properties, which are implicitly universally quantified, this could look something like:
where
lemma1
andlemma2
are the names of already-specified properties, andgoal
is a Cryptol expression of the same form as can be currently passed to:prove
.The text was updated successfully, but these errors were encountered: