have Metadata.callResult contain the resulting system state

lindy-labs · Feb 13, 2024 · 71b1ef0 · 71b1ef0
1 parent 34826f8
commit 71b1ef0
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 6 deletions.
diff --git a/Aegis/Libfuncs/Syscall.lean b/Aegis/Libfuncs/Syscall.lean
@@ -66,9 +66,10 @@ def call_contract_syscall : FuncData where
   inputTypes := [.GasBuiltin, .System, .ContractAddress, .Felt252, .Array .Felt252]
   branches := [{ outputTypes := [.GasBuiltin, .System, .Array .Felt252]
                  condition := fun _ (s : Q(System)) (c : Q(ContractAddress))
-                   (f : Q(F)) (d : Q(List F)) _ _ (r : Q(List F)) =>
+                   (f : Q(F)) (d : Q(List F)) _ (s' : Q(System)) (r : Q(List F)) =>
                      let m : Q(Metadata) := .fvar metadataRef
-                     q($r = ($m).callResult $c $f $d $(m).contractAddress $s) },
+                     q($r = (($m).callResult $c $f $d $(m).contractAddress $s).fst
+                       ∧ $s' = (($m).callResult $c $f $d $(m).contractAddress $s).snd) },
                { outputTypes := [.GasBuiltin, .System, .Array .Felt252]
                  condition := fun _ _ _ _ _
                    _ _ _ => q(True) }]  -- TODO can we assume that `s' = s`?

diff --git a/Aegis/Tests/Commands.lean b/Aegis/Tests/Commands.lean
@@ -490,8 +490,9 @@ return([8], [9], [12]); // 12
 test::call_contract_syscall@0([0]: GasBuiltin, [1]: System, [2]: ContractAddress, [3]: felt252, [4]: core::array::Span::<core::felt252>) -> (GasBuiltin, System, core::result::Result::<core::array::Span::<core::felt252>, core::array::Array::<core::felt252>>);"
 
 aegis_spec "test::call_contract_syscall" :=
-  fun m _ s c f d _ _ ρ =>
-  ρ = .inl (m.callResult c f d m.contractAddress s) ∨ ρ.isRight
+  fun m _ s c f d _ s' ρ =>
+  ρ = .inl (m.callResult c f d m.contractAddress s).1
+  ∧ s' = (m.callResult c f d m.contractAddress s).2 ∨ ρ.isRight
 
 aegis_prove "test::call_contract_syscall" :=
   fun m _ s c f d _ _ ρ => by

diff --git a/Aegis/Types.lean b/Aegis/Types.lean
@@ -310,8 +310,10 @@ structure Metadata : Type where
   /-- Contains the contents of the `n`th box for the sierra type `t` -/
   (boxHeap : (t : SierraType) → (n : Nat) → Option t.toType)
   /-- Returns the result for `call_contract_syscall` for a given contract, selector, call data,
-    caller, and system state -/
-  (callResult : (c : ContractAddress) → (f : F) → (d : List F) → (caller : ContractAddress) → System → List F)
+    caller, and system state. The result consists of the actual return value as well as the
+    resulting system state. -/
+  (callResult : (c : ContractAddress) → (f : F) → (d : List F) → (caller : ContractAddress)
+    → System → List F × System)
 
 /-- A structure contining the branch-specific data for a libfunc -/
 structure BranchData (inputTypes : List SierraType) where