From 2ba3cff50988a35cf812ffaf13439da65dd54edb Mon Sep 17 00:00:00 2001
From: utkn <utkns09@gmail.com>
Date: Sat, 9 Nov 2024 15:20:13 +0300
Subject: [PATCH] explicit bigint arithmetic builtins removed

---
 Lampe/Lampe/Builtin/BigInt.lean | 45 ---------------------------------
 Lampe/Lampe/Hoare/Builtins.lean | 36 ++++++++------------------
 2 files changed, 10 insertions(+), 71 deletions(-)

diff --git a/Lampe/Lampe/Builtin/BigInt.lean b/Lampe/Lampe/Builtin/BigInt.lean
index d6615a9..fef51a1 100644
--- a/Lampe/Lampe/Builtin/BigInt.lean
+++ b/Lampe/Lampe/Builtin/BigInt.lean
@@ -1,51 +1,6 @@
 import Lampe.Builtin.Basic
 namespace Lampe.Builtin
 
-/--
-Defines the addition of two bigints `(a b : Int)`.
-The builtin is assumed to return `a + b`.
-
-In Noir, this builtin corresponds to `a + b` for bigints `a`, `b`.
--/
-def bigIntAdd := newPureBuiltin
-  ⟨[.bi, .bi], (.bi)⟩
-  (fun h![a, b]  => ⟨True,
-    fun _ => a + b⟩)
-
-/--
-Defines the subtraction of two bigints `(a b : Int)`.
-The builtin is assumed to return `a - b`.
-
-In Noir, this builtin corresponds to `a - b` for bigints `a`, `b`.
--/
-def bigIntSub := newPureBuiltin
-  ⟨[.bi, .bi], (.bi)⟩
-  (fun h![a, b]  => ⟨True,
-    fun _ => a - b⟩)
-
-/--
-Defines the multiplication of two bigints `(a b : Int)`.
-The builtin is assumed to return `a * b`.
-
-In Noir, this builtin corresponds to `a * b` for bigints `a`, `b`.
--/
-def bigIntMul := newPureBuiltin
-  ⟨[.bi, .bi], (.bi)⟩
-  (fun h![a, b]  => ⟨True,
-    fun _ => a * b⟩)
-
-/--
-Defines the division of two bigints `(a b : Int)`. We make the following assumptions:
-- If `b = 0`, an exception is thrown.
-- Otherwise, the builtin is assumed to return `a / b`.
-
-In Noir, this builtin corresponds to `a / b` for bigints `a`, `b`.
--/
-def bigIntDiv := newPureBuiltin
-  ⟨[.bi, .bi], (.bi)⟩
-  (fun h![a, b]  => ⟨b ≠ 0,
-    fun _ => a / b⟩)
-
 /--
 Defines the conversion of a byte slice `bytes : List (U 8)` in little-endian encoding to a `BigInt`.
 Modulus parameter is ignored.
diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
index 4d575d5..92ecbef 100644
--- a/Lampe/Lampe/Hoare/Builtins.lean
+++ b/Lampe/Lampe/Hoare/Builtins.lean
@@ -113,10 +113,10 @@ theorem div_intro {ha : Builtin.ArithTp tp}: STHoare p Γ ⟦⟧
 theorem rem_intro : STHoare p Γ ⟦⟧
     (.call h![] [tp, tp] tp (.builtin .rem) h![a, b])
     (fun v => Builtin.canDivide a b ∧
-      v = match tp with
-      | .u _ => a % b
-      | .i _ => Builtin.intRem a b
-      | _ => a) := by
+      match tp with
+      | .u _ => v = a % b
+      | .i _ => v = Builtin.intRem a b
+      | _ => False) := by
   unfold STHoare
   intros H st h
   constructor
@@ -138,11 +138,11 @@ theorem rem_intro : STHoare p Γ ⟦⟧
 
 theorem neg_intro : STHoare p Γ ⟦⟧
   (.call h![] [tp, tp] tp (.builtin .neg) h![a, b])
-  (fun v => v = match tp with
-    | .i _ => -a
-    | .field => -a
-    | .bi => -a
-    | _ => a) := by
+  (fun v => match tp with
+    | .i _ => v = -a
+    | .field => v = -a
+    | .bi => v = -a
+    | _ => False) := by
   unfold STHoare
   intros H st h
   constructor
@@ -162,23 +162,7 @@ theorem arrayAsSlice_intro : STHoarePureBuiltin p Γ Builtin.arrayAsSlice (by ta
   apply pureBuiltin_intro_consequence <;> try rfl
   tauto
 
--- BigInt
-
-theorem bigIntAdd_intro : STHoarePureBuiltin p Γ Builtin.bigIntAdd (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
-  tauto
-
-theorem bigIntSub_intro : STHoarePureBuiltin p Γ Builtin.bigIntSub (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
-  tauto
-
-theorem bigIntMul_intro : STHoarePureBuiltin p Γ Builtin.bigIntMul (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
-  tauto
-
-theorem bigIntDiv_intro : STHoarePureBuiltin p Γ Builtin.bigIntDiv (by tauto) h![a, b] (a := ()) := by
-  apply pureBuiltin_intro_consequence <;> tauto
-  tauto
+-- BigInt misc
 
 theorem bigIntFromLeBytes_intro : STHoarePureBuiltin p Γ Builtin.bigIntFromLeBytes (by tauto) h![bs, mbs] (a := ()) := by
   apply pureBuiltin_intro_consequence <;> tauto