Lemmas on Boolean reasoning, set reasoning, map lookup

[PetarMax]

This PR upstreams further lemmas from Lukso/BlockSwap concerning

• Boolean reasoning;
• set reasoning; and
• map lookup.

[PetarMax]

All of the keccak lemmas are indeed problematic (unsound, really), but needed for the engagements. I will remove them from this PR.

[PetarMax]

I'm having some formatting issues here as well with the expected outputs. For example, for the I have additional spacing, different order of constraints (ACTUAL top, EXPECTED bottom):

statusCode: STATUSCODE_FINAL\n\n\n\n\n    \n    \n    rule [BASIC-BLOCK-1-TO-3]:
statusCode: STATUSCODE_FINAL\n\n\n\n\n\n\n    rule [BASIC-BLOCK-1-TO-3]:

[label(BASIC-BLOCK-1-TO-3)]\n    \n    rule [BASIC-BLOCK-3-TO-4]:
[label(BASIC-BLOCK-1-TO-3)]\n\n    rule [BASIC-BLOCK-3-TO-4]:

[label(BASIC-BLOCK-3-TO-4)]\n    \n    rule [BASIC-BLOCK-4-TO-5]:
[label(BASIC-BLOCK-3-TO-4)]\n\n    rule [BASIC-BLOCK-4-TO-5]:

[label(BASIC-BLOCK-4-TO-5)]\n    \n    rule [BASIC-BLOCK-6-TO-8]:
[label(BASIC-BLOCK-4-TO-5)]\n\n    rule [BASIC-BLOCK-6-TO-8]:

andBool ( VV0_n_114b9705:Int <=Int 51816696836262767\n       andBool ( CALLER_ID:Int <Int pow160\n       andBool ( ORIGIN_ID:Int <Int pow160\n       andBool ( NUMBER_CELL:Int <=Int maxSInt256\n       andBool ( VV0_n_114b9705:Int <Int pow256\n               ))))))))))\n
andBool ( CALLER_ID:Int <Int pow160\n       andBool ( ORIGIN_ID:Int <Int pow160\n       andBool ( NUMBER_CELL:Int <=Int maxSInt256\n       andBool ( VV0_n_114b9705:Int <Int pow256\n       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767\n               ))))))))))\n

[label(BASIC-BLOCK-6-TO-8)]\n    \n    rule [BASIC-BLOCK-7-TO-9]:
[label(BASIC-BLOCK-6-TO-8)]\n\n    rule [BASIC-BLOCK-7-TO-9]:

[label(BASIC-BLOCK-7-TO-9)]\n    \n    rule [BASIC-BLOCK-8-TO-10]:
[label(BASIC-BLOCK-7-TO-9)]\n\n    rule [BASIC-BLOCK-8-TO-10]:

[label(BASIC-BLOCK-8-TO-10)]\n    \n    rule [BASIC-BLOCK-9-TO-11]:
[label(BASIC-BLOCK-8-TO-10)]\n\n    rule [BASIC-BLOCK-9-TO-11]: 

* another re-ordering of constraints, too long *

[label(BASIC-BLOCK-9-TO-11)]\n    \n    rule [BASIC-BLOCK-10-TO-12]:
[label(BASIC-BLOCK-9-TO-11)]\n\n    rule [BASIC-BLOCK-10-TO-12]:

[label(BASIC-BLOCK-10-TO-12)]\n    \n    rule [BASIC-BLOCK-11-TO-13]:
[label(BASIC-BLOCK-10-TO-12)]\n\n    rule [BASIC-BLOCK-11-TO-13]:

* another re-ordering of constraints, too long *

I'm confused, because I would think the way things are printed hasn't been affected by the PR...

[PetarMax]

On hold for the moment, waiting for #1866.

[palinatolmach]

@PetarMax now that the blocking booster PR has been merged, shall we be able to merge it?

[PetarMax]

Not yet, the PR is still failing in the booster and passing in the Haskell backend on some tests. I'm trying to figure out what's happening and liaising with @geo2a.

[ehildenb]

I notice that some of these move the concrete to the left and symbolic to the rgiht, and some the other direction. I wonder if there is benefit to always picking one side of the comparison for the concrete and teh other for the symbolic?

I think there are also some rules somewhere which normalize all _>=_ and _>_ to the other operators (_<=_ and _<_), so I wonder if we actually don't need all the duplicate rules? Though I can't find those rules now, so maybe they would need to be added.