search

AlacrisIO / meta

Internal management of Legicash/Legilogic/Alacris
0 stars 0 forks source link

Verify with Z3 #28

Closed jeapostrophe closed 5 years ago

jeapostrophe commented 5 years ago

If we do not have this initially, then we are "just" a contract language with EPP. We're still useful, but we can't really claim to do much verification. But, to be completely frank, it is possible to run the program and be somewhat useful without this.

AlexKnauth commented 5 years ago

I’m not sure how to approach verifying the assertions in the contract program. I’m following the instructions in the Z3 Theory Generation comment at the top of EmitZ3.hs, but I guess I’m still having trouble understanding the structures of code that would be required for it. For (2) and (3) in that comment, I have to traverse the program verifying assert statements under the assumption of previous assert statements. However, at this point the program is broken up into handlers for the contract, and I’m not sure what counts as “previous” assert statements. Am I looking at this wrong?