File ‹Data.ML›

(*  Title:      Data.ML
    Author:     Diego Marmsoler
*)

signature SOLIDITY_DATA =
sig
  type data
  val mlookupN: theory -> Symtab.key -> data option
  val mupdateN: Symtab.key -> data -> theory -> theory
  val a_to_b: typ -> typ
  val mk_dt_con_name: string -> string
  val c: typ
  val e: term
  val s: term
  val s': term
  val r: term
  val effect: term
  val finit_map_T: typ
  val call: typ -> term
  val instantiate_b_a: typ -> typ
  val instantiate_b_a2: term -> term
  val instantiate_3: term -> term
  val instantiate_4: term -> term
  val change_types: term -> term
  val change_transfers: typ -> term -> term -> term
  val change_internals: typ -> string list -> term list -> term -> term
  val change_externals: typ -> term -> term -> term
  val mk_inv: term -> term -> term -> term
  val mk_inv_state: term -> term
  val mk_Bind: term -> term -> term
  val mk_init: term * term -> term
  val mk_write: term * term -> term
  val mk_cinit: term * term -> term
  val mk_newStack: term
  val mk_newMemory: term
  val mk_newCalldata: term
  val init_balance: term
  val init_balance_np: term
  val mk_init_storage: term -> term -> term
  val mk_exc: term -> term
  val constructor_binding: Position.T -> binding
  val mono_binding: binding -> binding
  val mk_fallback_t: typ -> typ
  val mk_local_name: Proof.context -> string -> string -> string
  val mk_True: term
  val mk_False: term
  val mk_contract_typ: Proof.context -> string -> typ
  val post_t: term
  val rvalueT: typ
  val exT: typ
  val stateT: typ
  val smonadT: typ
  val mk_external_t: typ -> typ
  val pfun_name: string
  val con_name: string
  val mk_global_name: Proof.context -> string -> string
  val address: sort
  val rT: typ
  val mk_external: typ -> term
  val a: typ
  val solidity_command: ('a -> Toplevel.transition -> Toplevel.transition) ->
      Outer_Syntax.command_keyword ->
        string ->
          (Token.T list -> 'a * Token.T list) -> unit
  val mk_valtype_term: bool option -> term * term -> Name.context -> ((string * typ) * (term * term)) * Name.context
end

structure Solidity_Data: SOLIDITY_DATA =
struct

open Solidity_Util

datatype ptype = Par | Mem | CD

(* Data for constructor *)
type cdata =
  {term: term,                   (* Method constant *)
   name: string,                 (* Method name *)
   binding: binding,             (* Method binding *)
   def: thm,                     (* Definitional theorem *)
   payable: bool,                (* Is the method payable *)
   parlist: (string * typ) list, (* List of value parameters *)
   memlist: (string * typ) list, (* List of memory parameters *)
   mono_name: string,            (* Name of monotonicity property *)
   mono: thm,                    (* Name of monotonicity theorem *)
   dt_const: term}               (* Constructor term for contract datatype *)

(* Data for contract methods *)
type mdata =
  {term: term,                   (* Method constant *)
   name: string,                 (* Method name *)
   binding: binding,             (* Method binding *)
   def: thm,                     (* Definitional theorem *)
   payable: bool,                (* Is the method payable *)
   external: bool,               (* Is the method external *)
   parlist: (string * typ) list, (* List of value parameters *)
   memlist: (string * typ) list, (* List of memory parameters *)
   cdlist: (string * typ) list,  (* List of calldata parameters *)
   mono_name: string,            (* Name of monotonicity property *)
   mono: thm,                    (* Name of monotonicity theorem *)
   dt_const: term}               (* Constructor term for contract datatype *)

(* Data for contract *)
type data =
  {dt_type: typ,                    (* Type of contract datatype *)
   dt_cases: term,                  (* Cases constant for contract datatype *)
   locale: string,                  (* Locale name for contract *)
   members: (term * term) list,     (* Name and type of the member variables *)
   constructor: cdata,              (* Constructor data *)
   methods: (string * mdata) list,  (* Method data indexed by name of the binding *)
   pfun_name: term,                 (* Contract constant *)
   pfun: thm,                       (* Definitional theorem *)
   pinduct: thm}                    (* Induction theorem *)

structure MethodsN = Theory_Data
(
  type T = data Symtab.table
  val empty = Symtab.empty
  val merge = Symtab.merge (K true)
)

val mlookupN = Symtab.lookup o MethodsN.get
fun mupdateN k v = MethodsN.map (Symtab.update (k, v))

fun solidity_command trans command_keyword comment parse =
  Outer_Syntax.command command_keyword comment (parse >> trans);

fun a_to_b (TFree("'a", address)) = TFree("'b", address)
  | a_to_b T = T;

val pfun_name = "call"
fun mk_dt_con_name name = capitalizeFirst name ^ "_m"
val con_name = "constructor";
fun mk_wordT b = \<^Type>‹word b›
fun mk_sumT (a, b) = \<^Type>‹sum a b›;
val stringT = \<^typ>‹String.literal›
val address = \<^sort>‹address›
val typeT = \<^sort>‹type›
val a = TFree("'a", address)
val c = TFree("'c", [])

fun instantiate_b_a t =
  let
    val vars = TVars.make1 ((("'b", 0), address), a);
  in
    Term_Subst.instantiateT vars t
  end;

fun instantiate_b_a2 t =
  let
    val vars = TVars.make1 ((("'b", 0), address), a);
  in
    Term_Subst.instantiate (vars, Vars.empty) t
  end;

fun instantiate_3 t =
  let
    val vars = TVars.make2 ((("'a", 0), typeT), \<^typ>‹bool›) ((("'b", 0), address), TFree("'a", address));
  in
    Term_Subst.instantiate (vars, Vars.empty) t
  end;

val this = Free ("this", a)
val exT = \<^typ>‹ex›;
val e = Free ("e", exT);
val rvalueT = \<^Type>‹rvalue a›;
val stateT = \<^Type>‹state_ext a HOLogic.unitT›
val s = Free ("s", stateT)
val s' = Free ("s'", stateT)
val rT = mk_sumT (HOLogic.mk_prodT (rvalueT, stateT), HOLogic.mk_prodT (exT, stateT));
val r = Free ("r", rT);
val smonadT = \<^Type>‹state_monad rvalueT exT stateT›;

fun call name_ct = Free (pfun_name, \<^Type>‹fun name_ct smonadT›);

fun instantiate_4 t =
  let
    val vars = TVars.make2 ((("'a", 0), typeT), smonadT) ((("'b", 0), address), TFree("'a", address));
  in
    Term_Subst.instantiate (vars, Vars.empty) t
  end;

fun change_type (_,\<^sort>‹address›) = a
  | change_type t = TFree t;

fun change_types x = Term.map_types (fn t => Term.map_type_tfree change_type t) x;

fun change_transfer ct x (Const ("local.transfer_monad", _)) = Const ("local.transfer_monad", (ct --> smonadT) --> smonadT --> smonadT --> smonadT) $ x
  | change_transfer _ _ y = y;
fun change_transfers ct x = Term.map_aterms (change_transfer ct x);

val external = "external";
fun mk_external_t name = (name --> smonadT) --> smonadT;

fun mk_external ct = Free (external, mk_external_t ct)

fun change_external ct x (Free ("external", _)) = mk_external ct $ x
  | change_external _ _ y = y;

fun change_externals ct x = Term.map_aterms (change_external ct x);

fun obtain terms name =
  let
    val x = List.find (fn y => Term.is_Const y andalso Long_Name.base_name (fst (Term.dest_Const y)) = name) terms
  in
    if Option.isSome x then Option.valOf x else error ("aa")
  end

fun mk_internal ct terms y = call ct $ instantiate_b_a2 (obtain terms (mk_dt_con_name y))

fun change_internal ct names terms x =
  if is_Const x andalso Option.isSome (Long_Name.dest_local (fst (dest_Const x))) andalso
    exists (fn x' => x' = Option.valOf (Long_Name.dest_local (fst (dest_Const x)))) names then
    mk_internal ct terms (Option.valOf (Long_Name.dest_local (fst (dest_Const x))))
  else
    x;

fun change_internals ct names terms = Term.map_aterms (change_internal ct names terms);

fun mk_inv r P Q = \<^Const>‹Contract.inv a for r P Q›
fun mk_inv_state i = \<^Const>‹Contract.inv_state a for this i›

val effect = \<^Const>‹State_Monad.effect rvalueT exT stateT›;
val kdataT = \<^Type>‹Stores.kdata a›
val finit_map_T = \<^Type>‹Finite_Map.fmap stringT kdataT›;

fun mk_Bind x y = \<^Const>‹bind rvalueT exT stateT rvalueT for x ‹\<^Const>‹K smonadT rvalueT for y›››;

fun mk_init (x, y) = \<^Const>‹Solidity.init a for y x›;

fun mk_write (x, y) = \<^Const>‹Solidity.write a for y x›;

fun mk_cinit (x, y) = \<^Const>‹Solidity.cinit a for y x›;

val mk_newStack = \<^Const>‹newStack a›

val mk_newMemory = \<^Const>‹newMemory a›

val mk_newCalldata = \<^Const>‹newCalldata a›

val init_balance = \<^Const>‹Solidity.Solidity.init_balance a for ‹Free ("msg_value", mk_wordT \<^typ>‹256›)› this›

val init_balance_np = \<^Const>‹Solidity.Solidity.init_balance_np a for this›

fun mk_init_storage x y = \<^Const>‹Solidity.Contract.initStorage a for this x y›

fun mk_exc x = \<^Const>‹exc rvalueT exT stateT for x›

fun constructor_binding p = Binding.make (con_name, p);

fun mono_binding b = Binding.prefix true "mono" b;

fun mk_fallback_t name = (name --> smonadT) --> a --> smonadT;

fun mk_global_name ctxt x =
  Context.theory_base_name (Proof_Context.theory_of ctxt) ^ "." ^ x;

fun mk_local_name ctxt x y =
  (mk_global_name ctxt x) ^ "." ^ y;

val mk_True =
  let
    val tp = HOLogic.mk_prodT (\<^typ>‹String.literal› --> \<^Type>‹storage_data \<^Type>‹valtype a››, \<^typ>‹nat›)
  in
    \<^Const>‹K \<^typ>‹bool› tp for \<^Const>‹True››
  end

val mk_False =
  let
    val tp = HOLogic.mk_prodT (\<^typ>‹String.literal› --> \<^Type>‹storage_data \<^Type>‹valtype a››, \<^typ>‹nat›)
  in
    \<^Const>‹K \<^typ>‹bool› tp for \<^Const>‹False››
  end

fun mk_contract_typ ctxt name_lc =
  Type (mk_global_name ctxt name_lc, [a]);  

val post_t = \<^Const>‹Contract.post a for this›

fun mk_valtype_term _ (name, \<^term>‹SType.TValue TBool›) ctxt =
    Name.variant "bl" ctxt |>> (fn x => (x, \<^typ>‹bool›))
    |>> ``(fn x => (name, \<^Const>‹Bool a for ‹Free x››))
  | mk_valtype_term _ (name, \<^term>‹SType.TValue TSint›) ctxt = 
    Name.variant "si" ctxt |>> (fn x => (x, \<^typ>‹256 word›))
    |>> ``(fn x => (name, \<^Const>‹Uint a for ‹Free x››))
  | mk_valtype_term _ (name, \<^term>‹SType.TValue TAddress›) ctxt = 
    Name.variant "ad" ctxt |>> (fn x => (x, a))
    |>> ``(fn x => (name, \<^Const>‹Address a for ‹Free x››))
  | mk_valtype_term _ (name, Const (\<^const_name>‹SType.TValue›, _) $ (Const (\<^const_name>‹VType.TBytes›, _) $ _)) ctxt = 
    Name.variant "bt" ctxt |>> (fn x => (x, \<^typ>‹string›))
    |>> ``(fn x => (name, \<^Const>‹Bytes a› $ Free x))
  | mk_valtype_term NONE (_, (Const (\<^const_name>‹SType.TArray›, _) $ _ $ _)) _ = error "unsupported type"
  | mk_valtype_term (SOME memory) (name, (Const (\<^const_name>‹SType.TArray›, _) $ _ $ _)) ctxt= 
    Name.variant "ar" ctxt |>> (fn x => (x, if memory then \<^Type>‹adata \<^Type>‹valtype a›› else \<^Type>‹call_data \<^Type>‹valtype a››))
    |>> ``(fn x => (name, Free x))
  | mk_valtype_term NONE (_, (Const (\<^const_name>‹SType.DArray›, _) $ _)) _ = error "unsupported type"
  | mk_valtype_term (SOME memory) (name, (Const (\<^const_name>‹SType.DArray›, _) $ _)) ctxt = 
    Name.variant "ar" ctxt |>> (fn x => (x, if memory then \<^Type>‹adata \<^Type>‹valtype a›› else \<^Type>‹call_data \<^Type>‹valtype a››))
    |>> ``(fn x => (name, Free x))
  | mk_valtype_term _ _ _ = error "unsupported type"

end