search

GaloisInc / pate

Patches Assured up to Trace Equivalence
Other
15 stars 2 forks source link

Unify equivalence condition simplification in the verifier #420

Open thebendavis opened 1 month ago

thebendavis commented 1 month ago

Currently we perform some simplification of equivalence conditions in the verifier itself, as well as some additional simplification/rewriting in the Binary Ninja plugin to improve the presentation for the operator. Unifying all simplification and rewriting logic into a single place would make this easier to reason about and maintain, and performing this unification in the verifier means it could be leveraged by not only the Binary Ninja plugin but also other possible consumers of verifier results.

thebendavis commented 1 month ago

Making simplified equivalence conditions available in the verifier will allow us to make our integration tests less exposed to low-level changes, see discussion in https://github.com/GaloisInc/pate/pull/417#discussion_r1672734608

jim-carciofini commented 1 month ago

If this functionality could be implemented as a well encapsulated component, this might be a good task for me to cut my teeth on Haskel.