From 8a9adc2a57034ad3f863ae7c0fa09378ad025132 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Petar=20Maksimovi=C4=87?=
 <PetarMax@users.noreply.github.com>
Date: Wed, 18 Sep 2024 13:33:02 +0200
Subject: [PATCH] Upstreaming Kontrol slot update lemmas as tests (#2622)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* tests for previous kontrol lemmas

* moving lemmas to slot updates

* reverting some changes

---------

Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com>
---
 tests/specs/functional/slot-updates-spec.k | 54 ++++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/tests/specs/functional/slot-updates-spec.k b/tests/specs/functional/slot-updates-spec.k
index 18edd268d5..5aa76302ef 100644
--- a/tests/specs/functional/slot-updates-spec.k
+++ b/tests/specs/functional/slot-updates-spec.k
@@ -137,4 +137,58 @@ module SLOT-UPDATES-SPEC
            andBool 0 <=Int WORD6 andBool WORD6 <Int 2 ^Int 35
            andBool 0 <=Int WORD7 andBool WORD7 <Int 256
 
+    claim [slot-update-08]:
+      <k> runLemma ( X &Int #asWord ( BA ) ==Int Y:Int ) => doneLemma ( true ) ... </k>
+      requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+      andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+      andBool log2Int (X +Int 1) modInt 8 ==Int 0
+      andBool log2Int(X +Int 1) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32
+      andBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) ==Int Y
+      andBool X ==Int 2 ^Int ( 8 *Int 5 ) -Int 1 // 5 can be replaced by any number between 0 and 32
+
+    claim [slot-update-09]:
+      <k> runLemma ( X &Int #asWord ( BA ) ==Int Y:Int ) => doneLemma ( false ) ... </k>
+      requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+      andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+      andBool log2Int (X +Int 1) modInt 8 ==Int 0
+      andBool log2Int(X +Int 1) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32
+      andBool notBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) ==Int Y
+      andBool X ==Int 2 ^Int ( 8 *Int 5 ) -Int 1 // 5 can be replaced by any number between 0 and 32
+
+    claim [slot-update-10]:
+      <k> runLemma ( X &Int #asWord ( BA ) <Int Y:Int ) => doneLemma ( true ) ... </k>
+      requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+      andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+      andBool log2Int (X +Int 1) modInt 8 ==Int 0
+      andBool log2Int(X +Int 1) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32
+      andBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <Int Y
+      andBool X ==Int 2 ^Int ( 8 *Int 5 ) -Int 1 // 5 can be replaced by any number between 0 and 32
+
+    claim [slot-update-11]:
+      <k> runLemma ( X &Int #asWord ( BA ) <Int Y:Int ) => doneLemma ( false ) ... </k>
+      requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+      andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+      andBool log2Int (X +Int 1) modInt 8 ==Int 0
+      andBool log2Int(X +Int 1) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32
+      andBool notBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <Int Y
+      andBool X ==Int 2 ^Int ( 8 *Int 5 ) -Int 1 // 5 can be replaced by any number between 0 and 32
+
+    claim [slot-update-12]:
+      <k> runLemma ( X &Int #asWord ( BA ) <=Int Y:Int ) => doneLemma ( true ) ... </k>
+      requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+      andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+      andBool log2Int (X +Int 1) modInt 8 ==Int 0
+      andBool log2Int(X +Int 1) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32
+      andBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <=Int Y
+      andBool X ==Int 2 ^Int ( 8 *Int 5 ) -Int 1 // 5 can be replaced by any number between 0 and 32
+
+    claim [slot-update-13]:
+      <k> runLemma ( X &Int #asWord ( BA ) <=Int Y:Int ) => doneLemma ( false ) ... </k>
+      requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(BA))
+      andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+      andBool log2Int (X +Int 1) modInt 8 ==Int 0
+      andBool log2Int(X +Int 1) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32
+      andBool notBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <=Int Y
+      andBool X ==Int 2 ^Int ( 8 *Int 5 ) -Int 1 // 5 can be replaced by any number between 0 and 32
+
 endmodule