Open thebendavis opened 1 month ago
From @danmatichuk
Proposed next steps
Conclusion: 7/8/24
From @danmatichuk
Currently between step 1 and Step 2. Cannot carry domain information from step 1 into step2. There's step missing that we need to address.
At the point we have a non-trivial equivalence domain with pointer that cannot be re-scoped, we can try to assume particular concrete value for link register.
Alternatively, change stub definition to ignore the buffer that we give it. Hardcode some global value and use that in the stubs to ignore the buffer. Dan decided this is the easiest step to take first.
Update 7/10/24:
From @danmatichuk
The verifier now identifies a potential difference in memory but it's not observable, it's trying to put this in the equivalence domain. However, it cannot properly rescope that variable. However, because the difference isn't observable, it doesn't trigger the mechanism to prompt the user for an assertion. Without the assertion we get an error/warning about how the verifier needed to introduce unsoundness to continue.
Without adding equivalence condition, we quickly run into memory separation issues (see #419). We could manually add an assertion (i.e. add an equivalence condition as an assumption) needed to bypass this issue.
However, writing consumer stub first likely enables us to leverage infrastructure that lets user add assertions (i.e. add an equivalence condition as an assumption).
Next step: Add consumer stub that introduces observable event that checks for size mismatch.