In the rules for lenient_wp (and wp_sem_ctx) it would be good to unify all the numeric conversions using a representation relation. So instead of premises like
N.of_nat n ↦[wms][Wasm_int.N_of_uint i32m k + off] bits v
lenient_wp .. [BI_const (VAL_int32 k); BI_load n]
we could have
N_repr_nat nN n -∗
N_repr_uint kN kI -∗
nN ↦[wms][kN + off] bits v -∗
lenient_wp .. [BI_const (VAL_int32 kI); BI_load n]
Then we can prove easy facts about the representation relations agreeing with conversion functions going either direction and being congruences w.r.t. algebraic operations.
The beginnings of this appear in theories/iris/util.v where there is a relation N_repr : N -> i32 -> Prop and some lemmas about it. It's used pretty extensively in the proofs about the allocator.
In the rules for lenient_wp (and wp_sem_ctx) it would be good to unify all the numeric conversions using a representation relation. So instead of premises like
we could have
Then we can prove easy facts about the representation relations agreeing with conversion functions going either direction and being congruences w.r.t. algebraic operations.
The beginnings of this appear in
theories/iris/util.vwhere there is a relationN_repr : N -> i32 -> Propand some lemmas about it. It's used pretty extensively in the proofs about the allocator.