declare updateSparseBytes(setRange) definition as preserving definedness

runtimeverification · Jul 24, 2024 · 01e97d3 · 01e97d3
1 parent 8db0faa
commit 01e97d3
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/sparse-bytes/set-range-lemmas.md b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/sparse-bytes/set-range-lemmas.md
@@ -38,7 +38,8 @@ module SET-RANGE-LEMMAS
         => SBChunk(#bytes(replaceAtBytes(A, Start, Int2Bytes(Width, Value, LE))))
         requires functionSparseBytesWellDefined(setRange(Value), Start, Width)
             andBool Start +Int Width <=Int lengthBytes(A)
-        [simplification, concrete(A)]
+        [simplification, concrete(A), preserves-definedness]
+        // all arguments are checked to be in the required range/of the required size
 
     rule updateSparseBytes(setRange(Value:Int), SBChunk(#empty(A)), Start:Int, Width:Int)
         => SBChunk(#empty(Start))