Interesting properties to prove

[hjorthjort]

• (local.get I:Int) (local.set I:Int) is ust identity (no effect)
• (ITYPE.store (i32.const ADDR) (ITYPE.load (i32.const ADDR))) is just identity (no effect)
• A loop invariant: 1+2+...+n = n(n+1)/2
• Soundness of KWasm: Memory byte arrays maintain their invariants
  • Keys-in-range property: All keys K in the map maintain 0 <= K < SIZE * 65536
    • No instruction can store to out of bounds (< 0 or >= SIZE * 65536)
    • No instruction can load from out of bounds
    • Putting them together with an induction proof: an empty memory has keys-in-range, and no statement can cause it to be violated, so it always holds. May require modelling host calls.
  • Values-in-range property: No instruction can modify the memory so that the value in a slot is <1 or > 255
  • Induction proof: an empty memory is valid, and no statement can cause a memory to become invalid, so the semantics never violate the invariant.

Feel free to add more.