Removes Injectivity Assumptions on Inhale - #409
Conversation
|
Before merging this, I would also like to run it with verifiedSCION |
Makes sense. I've just opened this PR to detect possible issues before the Viper release. Might make sense to run your experiments sooner than later in case we need to defer the Viper release |
8a0a790 to
74adad8
Compare
|
I believe it makes sense to merge these changes before I start looking at enabling the consistency checks. I am now running tests locally on the verified scion repository. @ArquintL should we disable the dense_sparse_matrix tests? Or did you find a way to make them pass the injectivity tests? |
This reverts commit dbfdcd2.
ArquintL
changed the title
|
@ArquintL should we close this PR? Right now, it seems unlikely that it will be merged. Regarding the changes to the encoding, if you think it is worth keeping, maybe we can open a PR for that already |
|
The only changes to me seems to be that I use
|
Quantifying the footprint over len(loc) alone is not enough. Permission is then inhaled for `idx < len(loc)`, and to use it at the statically known indices the prover has to re-derive `len(loc) == n` from the embedding invariant `len(loc) == n || loc == nil`. It cannot, because nothing rules out the nil case, so `acc(&a)` for `var a@ [12]int` stopped reporting a failed injectivity check and started reporting "Permission to a might not suffice" instead. `Ref[loc] != nil` is implied by the quantifier -- all locations of the nil array are null and Viper does not permit holding permission to null -- but that derivation is never triggered where it is needed, so state it explicitly, as PR #409 does. Measured over the regression suite with the injectivity check enabled (DefaultAssumeInjectivityOnInhale = false), out of 1195 tests: no encoding change 62 failures len(loc) bound only 44 failures len(loc) bound + non-nil 10 failures with no test failing that did not already fail without the encoding change. Two of the remaining ten need Boogie, which is absent from the machine these numbers were taken on. The other eight are quantified permissions over stored pointers -- (m.values)[i][j], b.valuesMap[i], m[s], s.nodes[i] -- where injectivity means pairwise distinctness of the pointers and has to be specified by hand; they are not encoding gaps. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ESqeR8oFbRH3HB7D92eiEb
2 participants
Fixes #427