Inv subst

[andreistefanescu]

fixes #1910

[RyanGlScott]

If I understand correctly, this invariant substitution is always empty for now, but after the changes in #2016, then loop invariant inference will produce a non-empty invariant substitution to apply. Is that correct? If so, it would be worth updating this comment to explicitly state where the invariant substitution comes from (perhaps in #2016).

[kquick]

Yes, this is split out from 2016 to supply the plumbing that will actually be utilized in 2016.

[andreistefanescu]

@RyanGlScott as it turns out, you get a parting gift from me: fixing the CI here. I think this fails because of the simplification changes in What4. I assume fixing this this requires some tinkering with the existing rewrite rules. This need to be fixed regardless of the other open pull requests, as it prevents any further updates to the What4 submodule.

[RyanGlScott]

Indeed, I also suspect that the what4 simplification rules introduced in GaloisInc/what4#252 are responsible for the awslc CI job going into a (seemingly) infinite loop. Most likely, the proof goals now consist of different terms, which causes key rewrite rules not to fire. (See also GaloisInc/crucible#1165, where bumping the what4 submodule on the crucible side caused a What4 term in a test case to take on a very different shape.)

Judging from the failing CI job:

[21:06:03.395] Checking proof obligations EVP_DigestUpdate ...
Error: The operation was canceled.

The infinite loop occurs somewhere in the proof of EVP_DigestUpdate.

[RyanGlScott]

Superseded by #2037.