search

NethermindEth / horus-checker

Horus, a formal verification tool for StarkNet smart contracts.
https://nethermind.io/horus/
Other
71 stars 7 forks source link

Fix combination of subgoals #175

Closed aemartinez closed 1 year ago

aemartinez commented 1 year ago

@Julek

Hi guys! I just realized probably no one is aware of this branch (it was part of the work I did when investigating issues with the toy amm). This fixes a bug in the subgoal combination after applying tactics.

To be clear: This branch still assumes the semantics of subgoals is a disjunction, but it fixes a bug that produced an unsound verdict when one of the subgoals returns unknown. For example, if we have two subgoals: g1 -> Unsat, g2 -> Unknown, the current version returns Unsat, which is not sound because g2 might be Sat. The fixed version returns Unkown if there is at least one Unkown and there is no Sat.

Also, this is not really an issue for the current version of Horus because the tactics we are using do not produce more than one goal. But it will be a headache if you introduce more tactics in the future.

langfield commented 1 year ago

Cool! Thanks!

langfield commented 1 year ago

@aemartinez Is it all right if I rebase this so we can merge it?

aemartinez commented 1 year ago

Yes! I just wanted to bring it to your eyes and let you decide what to do. If there's any question I can help with let me know!