GaloisInc / pycryptol

pycryptol: Use Cryptol with Python
BSD 3-Clause "New" or "Revised" License
9 stars 1 forks source link

Allow richer Python values for property arguments #9

Open acfoltzer opened 9 years ago

acfoltzer commented 9 years ago

Currently, _CryptolModule.{check, exhaust, sat, prove} all take a string argument representing the property to check. It should be possible to pass in Python values to these functions, as long as those Python values originated from Cryptol in the first place. So if you have:

module Foo where

bar : [32] -> Bit
property bar x = x == x

On the Python side you ought to be able to have something like:

Foo = Cryptol().load_module("Foo.cry")
Foo.prove(Foo.bar)
acfoltzer commented 9 years ago

We'll need to keep track of some syntactic representation of the value for this to work.