add isqrt

vyperASTScript.sml

@@ -134,6 +134,7 @@ Datatype:
   | BlockHash
   | Env env_item
   | Acc account_item
+  | Isqrt
 End
 
 Datatype:

vyperASTSyntax.sig

@@ -74,6 +74,7 @@ signature vyperASTSyntax = sig
   val Env_tm          : term
   val Acc_tm          : term
   val BlockHash_tm    : term
+  val Isqrt_tm        : term
   val IntCall_tm      : term
   val Send_tm         : term
   val Empty_tm        : term
@@ -193,6 +194,7 @@ signature vyperASTSyntax = sig
   val mk_Keccak256 : term -> term
   val mk_AsWeiValue : (term * term) -> term
   val mk_Floor     : term -> term
+  val mk_Isqrt     : term -> term
   val mk_Bop       : term -> term
   val mk_Len       : term -> term
   val mk_MakeArray : term * term * term list -> term

vyperASTSyntax.sml

@@ -87,6 +87,7 @@ structure vyperASTSyntax :> vyperASTSyntax = struct
   val Env_tm          = astk"Env"
   val BlockHash_tm    = astk"BlockHash"
   val Acc_tm          = astk"Acc"
+  val Isqrt_tm        = astk"Isqrt"
   val IntCall_tm      = astk"IntCall"
   val Send_tm         = astk"Send"
   val Empty_tm        = astk"Empty"
@@ -224,6 +225,7 @@ structure vyperASTSyntax :> vyperASTSyntax = struct
   fun mk_Keccak256 t = mk_Builtin Keccak256_tm (mk_list([t], expr_ty))
   fun mk_AsWeiValue (d,t) = mk_Builtin (mk_comb(AsWeiValue_tm, d)) (mk_list([t], expr_ty))
   fun mk_Floor e = mk_Builtin Floor_tm (mk_list([e], expr_ty))
+  fun mk_Isqrt e = mk_Builtin Isqrt_tm (mk_list([e], expr_ty))
   fun mk_Bop b = mk_comb(Bop_tm, b)
   fun mk_Len e = mk_Builtin Len_tm (mk_list([e], expr_ty))
   fun mk_MakeArray (to,b,ls) =

vyperInterpreterScript.sml

@@ -1435,6 +1435,9 @@ Definition evaluate_builtin_def:
   evaluate_builtin cx acc (Acc aop) [BytesV _ bs] =
     (let a = lookup_account (word_of_bytes T (0w:address) bs) acc in
       INL $ evaluate_account_op aop bs a) ∧
+  evaluate_builtin cx _ Isqrt [IntV u i] =
+    (if is_Unsigned u ∧ 0 ≤ i then INL $ IntV u &(num_sqrt (Num i))
+     else INR "Isqrt type") ∧
   evaluate_builtin _ _ _ _ = INR "builtin"
 End
 
@@ -1474,7 +1477,8 @@ Definition builtin_args_length_ok_def:
   builtin_args_length_ok (Bop _) n = (n = 2) ∧
   builtin_args_length_ok (Env _) n = (n = 0) ∧
   builtin_args_length_ok BlockHash n = (n = 1) ∧
-  builtin_args_length_ok (Acc _) n = (n = 1)
+  builtin_args_length_ok (Acc _) n = (n = 1) ∧
+  builtin_args_length_ok Isqrt n = (n = 1)
 End
 
 val () = cv_auto_trans builtin_args_length_ok_def;

vyperMiscScript.sml

@@ -295,3 +295,22 @@ Definition string_to_num_def:
 End
 
 val () = cv_auto_trans string_to_num_def;
+
+(* Integer square root using Newton's method iteration *)
+Definition num_sqrt_aux_def:
+  num_sqrt_aux n r =
+    if r = 0 then 0
+    else let r' = (r + n DIV r) DIV 2 in
+      if r' < r then num_sqrt_aux n r'
+      else r
+Termination
+  WF_REL_TAC `measure SND`
+End
+
+val () = cv_auto_trans num_sqrt_aux_def;
+
+Definition num_sqrt_def:
+  num_sqrt n = if n = 0 then 0 else num_sqrt_aux n n
+End
+
+val () = cv_auto_trans num_sqrt_def;

vyperTestLib.sml

@@ -584,6 +584,15 @@ fun d_expression () : term decoder = achoose "expr" [
       JSONDecode.sub 0 $
       JSONDecode.map mk_Floor (delay d_expression),
     check_ast_type "Call" $
+    check (field "func" $ tuple2 (
+             field "ast_type" string,
+             field "id" string))
+          (equal ("Name", "isqrt"))
+          "not isqrt" $
+      field "args" $
+      JSONDecode.sub 0 $
+      JSONDecode.map mk_Isqrt (delay d_expression),
+    check_ast_type "Call" $
     check (field "func" $ tuple2 (
              field "ast_type" string,
              field "id" string))