Interesting properties to prove

• (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.

The issue names no files, tests, or entry points. Start by locating the KWasm memory semantics and any host-call model, then formalize the keys-in-range and values-in-range invariants and prove them by induction. Done means the listed soundness properties are established, including the effect of host calls.