add orDefault lemmas

[dwightguth]

Previously we were missing some lemmas for lookup or default that were present for lookup. We add some lemmas here to the MAP-SYMBOLIC module so that reasoning about the orDefault version of lookup can work correctly.

[dwightguth]

@ehildenb what tests would you suggest for this PR?

[ehildenb]

@dwightguth add tests to k-distribution/tests/regression-new/map-symbolic. You should make sure that each lemma here is exercised by some test. Do not specify the RHS of the tests (similar to how the existing tests work), instead use the exact output of the proof run and compare to a golden file. This is a more robust way tto measure "did the exact simplifications I wanted to apply actually apply?"

[ehildenb]

We should add a tests which have the in_keys predicate in the side-condition:

claim <k> lookup( M:Map [ X <- 1 ] [ Y ] orDefault 0 ) => . </k> requires COND1 andBool COND2

Where COND1 ranges over [X ==K Y, X =/=K Y], and COND2 ranges over [Y in_keys(M), notBool Y in_keys(M)].

As it stands, we only have one test that exercises the orDefault behavior, and only with a single-element map.

[dwightguth]

I can add these tests, and will, but I wanted to note that, in fact, test 51 also exercises several of the default cases.

[ehildenb]

If we instead just have (y |-> 4) [ x] orDefault 0 directly, the output will be exactly 0, which is a bit stronger of a test than this one.

But if we add the other 4 tests I mentioned then we should be covering the behaviors of orDefault.

[dwightguth]

I added the tests you requested, but I want to note that none of them actually simplify to 0. The only one that ought in theory to be simplifiable to 0 is the one where X =/= Y and Y is not in M. But the simplification rules I added aren't actually powerful enough to determine that that means the lookup ought to be simplifiable to 0. We can always add more simplification rules later to do so, but I would prefer to add the minimum amount necessary to bring orDefault up to parity with regular lookup while also being sufficient to solve the issue I was having in the C semantics. The lemmas don't need to be complete; we can add more when we discover more things we want to be able to prove.

[ehildenb]

One small generalization of this rule, which should enable both this simpliifcation and many others (as well as actually exercising some of the new tests), without being considered an "extension" of the previous lemmass because there is no analogue in the previous lemmsa for this:

Suggested change

	rule .Map [ _ ] orDefault D => D [simplification]
	rule M [ K ] orDefault D => D requires notBool K in_keys(M) [simplification]

This would let it simplify out more, at the expense of triggering more frequent in_keys(...) checks.

[dwightguth]

Per discussion with Everett over slack we decided to leave this lemma as-is for now since it's current form suffices for the C semantics example I was working with. We can revisit Everett's suggestion if we discover terms that we want to simplify that these lemmas are not powerful enough to handle.