Add theoretical motivation section

[smoelius]

No description provided.

[2over12]

This is a bit imprecise to me imo. My major concern is in an SP calculus we could have the information:

{ Q ^ x.y == x.z ^ x.y > 2}
x.foo();
{ Q /\ x.y' == x.y +1 }

We are imagining here that foo checks some state on y and z then increments. But say there is no assert related to x.y' and x.y in the rest of the test then we still get a WP result:

{ Q ^ x.y == x.z ^ x.y > 2}
x.foo();
{ Q }

Since the post condition is essentially trivially satisfied wrt to Q. ie. my more major concern is that (*) drops unasserted effects, which is often the source of a buggy/under-constrained test. ie. in a very rough sense I think verify_untrusted_callback_override_ok is an example of a test that doesnt really uphold (*) since the post condition on the callback is essentially True

On the other hand, state being tested by asserts isnt a bad signal that that portion of the state is interesting. other statements that touch related/the same state are worth attempting to remove

This is a bit pedantic tho, the point remains that there are probably actions that should be/are removed that may not reflect (*)

[smoelius]

Could you please give this another glance when you have a moment?

[2over12]

This makes sense to me! also checked overflows were a nice relevant example

[smoelius]

Thanks a million, @2over12. 🙏