initial work on extcall

vyperASTScript.sml

@@ -139,7 +139,7 @@ End
 Datatype:
   call_target
   = IntCall identifier
-  | ExtCall identifier (* external call passing Vyper values *)
+  | ExtCall bool identifier (* is_static, method name; target address is first arg *)
   | Send
   (* TODO: external raw call *)
 End

vyperASTSyntax.sig

@@ -75,6 +75,7 @@ signature vyperASTSyntax = sig
   val Acc_tm          : term
   val BlockHash_tm    : term
   val IntCall_tm      : term
+  val ExtCall_tm      : term
   val Send_tm         : term
   val Empty_tm        : term
   val MaxValue_tm     : term
@@ -166,6 +167,7 @@ signature vyperASTSyntax = sig
   val mk_StructLit : term * term list -> term
   val mk_IfExp     : term * term * term -> term
   val mk_IntCall   : term -> term
+  val mk_ExtCall   : term * term -> term
   val mk_Empty     : term -> term
   val mk_MaxValue  : term -> term
   val mk_MinValue  : term -> term

vyperASTSyntax.sml

@@ -88,6 +88,7 @@ structure vyperASTSyntax :> vyperASTSyntax = struct
   val BlockHash_tm    = astk"BlockHash"
   val Acc_tm          = astk"Acc"
   val IntCall_tm      = astk"IntCall"
+  val ExtCall_tm      = astk"ExtCall"
   val Send_tm         = astk"Send"
   val Empty_tm        = astk"Empty"
   val MaxValue_tm     = astk"MaxValue"
@@ -179,6 +180,8 @@ structure vyperASTSyntax :> vyperASTSyntax = struct
     s, mk_list(ls, mk_prod(string_ty, expr_ty))])
   fun mk_IfExp (e1,e2,e3) = list_mk_comb(IfExp_tm, [e1,e2,e3])
   fun mk_IntCall s = mk_comb(IntCall_tm, s)
+  fun mk_ExtCall (is_static, method_name) =
+    list_mk_comb(ExtCall_tm, [is_static, method_name])
   fun mk_Empty t = list_mk_comb(TypeBuiltin_tm, [
     Empty_tm, t, mk_list([], expr_ty)])
   fun mk_MaxValue t = list_mk_comb(TypeBuiltin_tm, [

vyperInterpreterScript.sml

@@ -1612,6 +1612,13 @@ Definition finally_def:
      | (INR e, s) => ignore_bind g (raise e) s
 End
 
+(* Run action but roll back state changes (for staticcall).
+   Only the return value/exception is kept. *)
+Definition with_rollback_def:
+  with_rollback f s : α evaluation_result =
+  case f s of (res, _) => (res, s)
+End
+
 val option_CASE_rator =
   DatatypeSimps.mk_case_rator_thm_tyinfo
     (Option.valOf (TypeBase.read {Thy="option",Tyop="option"}));
@@ -2566,7 +2573,19 @@ Definition evaluate_def:
     transfer_value cx.txn.target toAddr amount;
     return $ Value $ NoneV
   od ∧
-  eval_expr cx (Call (ExtCall _) _) = raise $ Error "TODO: ExtCall" ∧
+  (* ExtCall: external contract call
+   * TODO: Implement cross-contract interpretation once termination measure
+   * is extended to track (address, function) pairs across all sources.
+   * When implemented:
+   * - If is_static=T, wrap the call in with_rollback to discard state changes
+   * - If is_static=F, state changes persist (normal extcall)
+   * Currently stubbed to allow build to succeed. *)
+  eval_expr cx (Call (ExtCall is_static method_name) es) = do
+    check (LENGTH es ≥ 1) "ExtCall needs target";
+    vs <- eval_exprs cx es;
+    toAddr <- lift_option (dest_AddressV $ HD vs) "ExtCall target not AddressV";
+    raise $ Error "ExtCall: cross-contract calls not yet implemented"
+  od ∧
   eval_expr cx (Call (IntCall fn) es) = do
     check (¬MEM fn cx.stk) "recursion";
     ts <- lift_option (get_self_code cx) "IntCall get_self_code";

vyperSmallStepScript.sml

@@ -1,6 +1,6 @@
 Theory vyperSmallStep
 Ancestors
-  arithmetic combin pair list while
+  arithmetic combin pair list While
   vyperMisc vyperInterpreter
 Libs
   cv_transLib
@@ -57,6 +57,7 @@ Datatype:
   | BuiltinK builtin eval_continuation
   | TypeBuiltinK type_builtin type eval_continuation
   | CallSendK eval_continuation
+  | ExtCallK eval_continuation
   | IntCallK (num |-> type_args) identifier ((identifier # type) list) type (stmt list) eval_continuation
   | IntCallK1 (scope list) type_value eval_continuation
   | ExprsK (expr list) eval_continuation
@@ -180,8 +181,10 @@ Definition eval_expr_cps_def:
     (case check (LENGTH es = 2) "Send args" st of
        (INR ex, st) => AK cx9 (ApplyExc ex) st k
      | (INL (), st) => eval_exprs_cps cx9 es st (CallSendK k)) ∧
-  eval_expr_cps cx10 (Call (ExtCall _) _) st k =
-    AK cx10 (ApplyExc (Error "TODO: ExtCall")) st k ∧
+  eval_expr_cps cx10 (Call (ExtCall _ _) es) st k =
+    (case check (LENGTH es ≥ 1) "ExtCall needs target" st of
+       (INR ex, st) => AK cx10 (ApplyExc ex) st k
+     | (INL (), st) => eval_exprs_cps cx10 es st (ExtCallK k)) ∧
   eval_expr_cps cx10 (Call (IntCall fn) es) st k =
     (case do
       check (no_recursion fn cx10.stk) "recursion";
@@ -365,6 +368,7 @@ Definition apply_exc_def:
   apply_exc cx ex st (BuiltinK _ k) = AK cx (ApplyExc ex) st k ∧
   apply_exc cx ex st (TypeBuiltinK _ _ k) = AK cx (ApplyExc ex) st k ∧
   apply_exc cx ex st (CallSendK k) = AK cx (ApplyExc ex) st k ∧
+  apply_exc cx ex st (ExtCallK k) = AK cx (ApplyExc ex) st k ∧
   apply_exc cx ex st (IntCallK _ _ _ _ _ k) = AK cx (ApplyExc ex) st k ∧
   apply_exc cx ex st (IntCallK1 prev rtv k) =
     liftk (cx with stk updated_by TL) (ApplyTv o Value)
@@ -577,6 +581,12 @@ Definition apply_vals_def:
       transfer_value cx.txn.target toAddr amount;
       return $ Value NoneV
     od st) k ∧
+  apply_vals cx vs st (ExtCallK k) =
+    liftk cx ApplyTv (do
+      check (LENGTH vs ≥ 1) "ExtCallK nargs";
+      toAddr <- lift_option (dest_AddressV $ HD vs) "ExtCall target not AddressV";
+      raise $ Error "ExtCall: cross-contract calls not yet implemented"
+    od st) k ∧
   apply_vals cx vs st (IntCallK tenv fn args ret body k) =
     (case do
       env <- lift_option (bind_arguments tenv args vs) "IntCall bind_arguments";
@@ -1135,7 +1145,23 @@ Proof
       \\ drule eval_exprs_length
       \\ gvs[check_def, assert_def] )
     \\ rw[] )
-  \\ conj_tac >- rw[eval_expr_cps_def, evaluate_def, raise_def]
+  (* ExtCall case *)
+  \\ conj_tac >- (
+    rw[eval_expr_cps_def, evaluate_def, ignore_bind_def, bind_def]
+    \\ CASE_TAC \\ gvs[cont_def] \\ reverse CASE_TAC
+    \\ gvs[] \\ first_x_assum drule \\ rw[]
+    \\ CASE_TAC \\ reverse CASE_TAC
+    >- rw[Once OWHILE_THM, stepk_def, apply_exc_def]
+    >> rw[Once OWHILE_THM, stepk_def, apply_vals_def, bind_def,
+          ignore_bind_def, liftk1]
+    \\ qmatch_goalsub_abbrev_tac`check b c d`
+    \\ `check b c d = (INL (), d)`
+    by (
+      rw[check_def, assert_def, Abbr`b`]
+      \\ drule eval_exprs_length
+      \\ gvs[check_def, assert_def] )
+    \\ rw[]
+    \\ CASE_TAC \\ gvs[lift_option_def, raise_def] )
   \\ conj_tac >- (
     rw[eval_expr_cps_def, evaluate_def, ignore_bind_def, bind_def,
        no_recursion_def]

vyperTestLib.sml

@@ -677,6 +677,32 @@ fun d_expression () : term decoder = achoose "expr" [
     field "id" (JSONDecode.map mk_Name string),
     check_ast_type "NameConstant" $
     field "value" (JSONDecode.map mk_lb booltm),
+    (* ExtCall: extcall target.method(args) *)
+    check_ast_type "ExtCall" $
+    JSONDecode.map (fn (method_name, (target_expr, method_args)) =>
+      mk_Call (mk_ExtCall (boolSyntax.F, method_name))
+              (target_expr :: method_args)) $
+    tuple2 (
+      field "value" $ field "func" $ field "attr" stringtm,
+      tuple2 (
+        field "value" $ field "func" $ field "value" $
+          field "args" $ JSONDecode.sub 0 $ delay d_expression,
+        field "value" $ field "args" $ array $ delay d_expression
+      )
+    ),
+    (* StaticCall: staticcall target.method(args) *)
+    check_ast_type "StaticCall" $
+    JSONDecode.map (fn (method_name, (target_expr, method_args)) =>
+      mk_Call (mk_ExtCall (boolSyntax.T, method_name))
+              (target_expr :: method_args)) $
+    tuple2 (
+      field "value" $ field "func" $ field "attr" stringtm,
+      tuple2 (
+        field "value" $ field "func" $ field "value" $
+          field "args" $ JSONDecode.sub 0 $ delay d_expression,
+        field "value" $ field "args" $ array $ delay d_expression
+      )
+    ),
     check_ast_type "Call" $
     JSONDecode.map (fn (i,a) => mk_Call (mk_IntCall i) a) $
     tuple2 (