search

bennn / rosette-contract

Proving away contracts with Rosette
Other
2 stars 0 forks source link

Don't verify flat contracts #4

Open bennn opened 7 years ago

bennn commented 7 years ago

Idea from @AlexKnauth,

We currently replace -> contracts with a verified range with ->i contracts that check (in their range) that all inputs are within the current-bitwidth Rosette used to verify the range.

Checking these inputs in the range is probably more expensive than the original flat contract, for instance in (-> positive? positive? positive?).

So maybe, if the range is a flat contract we should just let it alone & instead focus on verifying higher-order range contracts.

bennn commented 7 years ago

Maybe instead, use a chaperone that's sensitive to the value of current-bitwidth. That should be cheaper that using ->i.

AlexKnauth commented 7 years ago

Wouldn't that just be re-implementing some of ->i's functionality?

bennn commented 7 years ago

I don't mind re-implementing parts of ->i, as long as this library only needs a small part and doing so makes things run faster.

Anyway, I think I need something lower-level than -> and ->i to do contract-stronger. At runtime, the library needs to get the preconditions of 2 arrow contracts and see if one implies the other. I don't think -> and ->i let you get just the precondition from a contract.