GaloisInc / pate

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

Factor out optimization surrounding array operations into What4 #416

Open lcasburn opened 1 month ago

lcasburn commented 1 month ago

For example, we've built simplification rules surrounding arrays to simplify array terms to handle aliasing between updates. This would be better supported within What4 directly. Another example, array copy primitive broken into byte updates.