From 81be12cb1967daf6d08fd183aa5a6c245d0cff4e Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Fri, 1 Dec 2023 17:53:03 +0100
Subject: [PATCH] fix box implementation, add tests for it

---
 Aegis/Libfuncs/Box.lean   | 10 +++++-----
 Aegis/Tests/Commands.lean | 37 +++++++++++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 5 deletions(-)

diff --git a/Aegis/Libfuncs/Box.lean b/Aegis/Libfuncs/Box.lean
index 525cb85..24d80d9 100644
--- a/Aegis/Libfuncs/Box.lean
+++ b/Aegis/Libfuncs/Box.lean
@@ -6,13 +6,13 @@ namespace Sierra.FuncData
 
 variable (metadataRef : FVarId)
 
-def box_into (t : SierraType) : FuncData where
+def into_box (t : SierraType) : FuncData where
   inputTypes := [t]
   branches := [{ outputTypes := [.Box t]
                  condition := fun a (ρ : Q(Nat)) =>
                    let m : Q(Metadata) := .fvar metadataRef
                    let lhs : Q(Option ($(t).toType)) := q($(m).boxHeap $t $ρ)
-                   let rhs : Expr := mkAppN (mkConst `Option.some) #[q(Option ($(t).toType)), a]
+                   let rhs := mkAppN (mkConst `Option.some [levelZero]) #[t.toQuote, a]
                    Expr.mkEq q(Option ($(t).toType)) lhs rhs }]
 
 def unbox (t : SierraType) : FuncData where
@@ -21,13 +21,13 @@ def unbox (t : SierraType) : FuncData where
                  condition := fun (a : Q(Nat)) (ρ : Expr) =>
                    let m : Q(Metadata) := .fvar metadataRef
                    let rhs : Q(Option ($(t).toType)) := q($(m).boxHeap $t $a)
-                   let lhs : Expr := mkAppN (mkConst `Option.some) #[q(Option ($(t).toType)), ρ]
+                   let lhs := mkAppN (mkConst `Option.some [levelZero]) #[t.toQuote, ρ]
                    Expr.mkEq q(Option ($(t).toType)) lhs rhs }]
 
 def boxLibfuncs (typeRefs : HashMap Identifier SierraType) : Identifier → Option FuncData
-| .name "box_into" [.identifier ident] _ =>
+| .name "into_box" [.identifier ident] _ =>
   match typeRefs.find? ident with
-  | .some t => box_into metadataRef t
+  | .some t => into_box metadataRef t
   | _ => .none
 | .name "unbox" [.identifier ident] _ =>
   match typeRefs.find? ident with
diff --git a/Aegis/Tests/Commands.lean b/Aegis/Tests/Commands.lean
index af60bdc..78b99b7 100644
--- a/Aegis/Tests/Commands.lean
+++ b/Aegis/Tests/Commands.lean
@@ -128,6 +128,43 @@ aegis_spec "test::u128_const" := fun _ _ => True
 
 aegis_prove "test::u128_const" := fun _ _ _ => True.intro
 
+aegis_load_string "type felt252 = felt252 [storable: true, drop: true, dup: true, zero_sized: false];
+type Box<felt252> = Box<felt252> [storable: true, drop: true, dup: true, zero_sized: false];
+
+libfunc into_box<felt252> = into_box<felt252>;
+
+into_box<felt252>([0]) -> ([1]); // 0
+return([1]); // 1
+
+test::into_box@0([0]: felt252) -> (Box<felt252>);"
+
+aegis_spec "test::into_box" := fun m a ρ =>
+  m.boxHeap .Felt252 ρ = .some a
+
+aegis_prove "test::into_box" := fun _ _ _ _ => by
+  aesop
+
+aegis_load_string "type Box<felt252> = Box<felt252> [storable: true, drop: true, dup: true, zero_sized: false];
+type felt252 = felt252 [storable: true, drop: true, dup: true, zero_sized: false];
+
+libfunc unbox<felt252> = unbox<felt252>;
+libfunc store_temp<felt252> = store_temp<felt252>;
+
+unbox<felt252>([0]) -> ([1]); // 0
+store_temp<felt252>([1]) -> ([1]); // 1
+return([1]); // 2
+
+test::unbox@0([0]: Box<felt252>) -> (felt252);"
+
+aegis_spec "test::unbox" := fun m a ρ =>
+  m.boxHeap .Felt252 a = .some ρ
+
+aegis_prove "test::unbox" := fun m a b => by
+  unfold «spec_test::unbox»
+  rintro ⟨_,h,rfl⟩
+  symm
+  assumption
+
 aegis_load_string "type Unit = Struct<ut@Tuple>;
 type core::bool = Enum<ut@core::bool, Unit, Unit>;