From bbf95c3c01a4a66e823cdf179c4890c681c150d2 Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@runtimeverification.com>
Date: Wed, 28 Aug 2024 17:37:56 +0300
Subject: [PATCH] Add a bigIntDiv hook

---
 mx-semantics/main/biguint/hooks.md | 18 ++++++++++++++++++
 tests/mx/biguint/div.mx            |  7 +++++++
 2 files changed, 25 insertions(+)
 create mode 100644 tests/mx/biguint/div.mx

diff --git a/mx-semantics/main/biguint/hooks.md b/mx-semantics/main/biguint/hooks.md
index 52696fe..2c0110a 100644
--- a/mx-semantics/main/biguint/hooks.md
+++ b/mx-semantics/main/biguint/hooks.md
@@ -3,6 +3,7 @@
 module MX-BIGUINT-HOOKS
     imports BOOL
     imports COMMON-K-CELL
+    imports K-EQUAL-SYNTAX
     imports MX-BIGUINT-CONFIGURATION
     imports MX-COMMON-SYNTAX
 
@@ -58,6 +59,23 @@ module MX-BIGUINT-HOOKS
         <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
         requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
             andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+    rule
+        <k> MX#bigIntDiv(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        /Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+            andBool Ints[Id2] orDefault 0 =/=K 0
 endmodule
 
 ```
diff --git a/tests/mx/biguint/div.mx b/tests/mx/biguint/div.mx
new file mode 100644
index 0000000..50c61eb
--- /dev/null
+++ b/tests/mx/biguint/div.mx
@@ -0,0 +1,7 @@
+push mxIntValue(40);
+call 1 MX#bigIntNew;
+push mxIntValue(500);
+call 1 MX#bigIntNew;
+call 2 MX#bigIntDiv;
+get_big_int;
+check_eq mxIntValue(12)