Upstream symbolic bytes lemmas for CSE

[palinatolmach]

Now that we support symbolic parameters in constructors, we need lemmas to simplify expressions such as `

#dasmOpCode ( b"`\xc0`@R`\x01`\x01`\xf8\x1b\x03`\x80R4\x80\x15a\x00\x1bW`\x00\x80\xfd[P`@Qa\x01^8\x03\x80a\x01^\x839\x81\x01`@\x81\x90Ra\x00:\x91a\x00BV[`\xa0Ra\x00[V[`\x00` \x82\x84\x03\x12\x15a\x00TW`\x00\x80\xfd[PQ\x91\x90PV[`\x80Q`\xa0Q`\xe2a\x00|`\x009`\x00`}\x01R`\x00`E\x01R`\xe2`\x00\xf3\xfe`\x80`@R4\x80\x15`\x0fW`\x00\x80\xfd[P`\x046\x10`<W`\x005`\xe0\x1c\x80c\fUi\x9c\x14`AW\x80c\xa5m\xfeJ\x14`yW\x80c\xc5\xd7\x80.\x14`\x9fW[`\x00\x80\xfd[`g\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`g\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x81V[`g`\x01`\x01`\xf0\x1b\x03\x81V\xfe\xa2dipfsX\"\x12 }\xb9\xc9\xcfL\x8cd\x8e\xba`\xa7\xb9'\x9f\xfc\xba?\x0f\xe6\xe0\x9cDeK\x96\x12}\x19D\xd1=\fdsolcC\x00\x08\x17\x003" +Bytes #buf ( 32 , V0__y:Int ) [ 0 ] , SHANGHAI )

The lemmas should look like this:

    //
    // Alternative memory lookup
    //
    rule [bytes-concat-lookup-left]:
      ( B1:Bytes +Bytes B2:Bytes ) [ I:Int ] => B1 [ I ]
      requires 0 <=Int I andBool I <Int lengthBytes(B1)
      [simplification(40), preserves-definedness]

    rule [bytes-concat-lookup-right]:
      ( B1:Bytes +Bytes B2:Bytes ) [ I:Int ] => B2 [ I -Int lengthBytes(B1) ]
      requires lengthBytes(B1) <=Int I
      [simplification(40), preserves-definedness]

    rule [lookup-as-asWord]:
      B:Bytes [ I:Int ] => #asWord ( #range ( B, I, 1 ) )
      requires 0 <=Int I andBool I <=Int lengthBytes(B)
      [simplification(60)]

Once upstreamed, we can remove this lemmas file from Kontrol test suite.