[TODO]: prove a corollary of instrument_sim_safe2 that holds for iexec_star

Question

[TODO]: prove a corollary of instrument_sim_safe2 that holds for iexec_star

stilltracy opened this issue 9 years ago · 2 comments

In order to prove the clause about memory consistency, I wrote down a lemma here. @mansky1 William, would you mind taking a look at it to make sure it's provable?

Answer 1 · 2016-03-06T19:32:05.000Z

The corollary is almost done, except the admit here: we should have been able to apply ss_trans here, however it somehow just failed. @mansky1

Answer 2 · 2016-03-07T00:55:53.000Z

Something went wrong with the type inference in ss_trans, and it was choosing a weird instantiation of VectorClocks.state that would never be applicable. I put in a type annotation that fixed it.