Draft: experiments with JSON translation

.github/workflows/rust.yml

@@ -92,6 +92,20 @@ jobs:
             cp ../../rust-toolchain ./
             cd crates
             # We compile each library twice to avoid errors. TODO: investigate why this is needed
+            # context
+            cd context
+            cargo coq-of-rust
+            touch src/lib.rs
+            cargo coq-of-rust --with-json
+            rsync -acv src/ ../../../../CoqOfRust/revm/translations/context/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
+            cd ..
+            # context/interface
+            cd context/interface
+            cargo coq-of-rust
+            touch src/lib.rs
+            cargo coq-of-rust --with-json
+            rsync -acv src/ ../../../../../CoqOfRust/revm/translations/context/interface/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
+            cd ../..
             # interpreter
             cd interpreter
             cargo coq-of-rust
@@ -124,8 +138,8 @@ jobs:
             cd specification
             cargo coq-of-rust
             touch src/lib.rs
-            cargo coq-of-rust
-            rsync -acv src/ ../../../../CoqOfRust/revm/translations/specification/ --include='*/' --include='*.v' --exclude='*'
+            cargo coq-of-rust --with-json
+            rsync -acv src/ ../../../../CoqOfRust/revm/translations/specification/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
             cd ..
             cd ../../..
           endGroup

.gitignore

@@ -29,3 +29,6 @@
 
 # Generated files for the smart contracts
 contracts/generated
+
+# Python
+__pycache__/

CoqOfRust/revm/of_json/common.v

@@ -0,0 +1,9 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import simulations.M.
+
+Module ruint.
+  Module Uint.
+    Definition t (BITS LIMBS : Z) : Set :=
+      Z.
+  End Uint.
+End ruint.

CoqOfRust/revm/of_json/context.py

@@ -0,0 +1,14 @@
+import json
+import of_json as o
+
+crate = "context"
+
+def interface_host():
+    input = json.load(open('../translations/context/interface/host.json'))
+    output = o.get_header([])
+    output += "\n"
+    output += o.pp_top_level_item(*o.find_top_level_item_by_name(crate, input, "SStoreResult"))
+    with open('context/interface/host.v', 'w') as f:
+        f.write(output)
+
+interface_host()

CoqOfRust/revm/of_json/context/interface/host.v

@@ -0,0 +1,26 @@
+(* Generated file. Do not edit. *)
+Require Import CoqOfRust.CoqOfRust.
+Require Import simulations.M.
+
+Module SStoreResult.
+  Record t : Set := {
+    original_value: ruint.Uint.t 256 4;
+    present_value: ruint.Uint.t 256 4;
+    new_value: ruint.Uint.t 256 4;
+  }.
+
+  Definition current_to_value (x: t) : Value.t :=
+    match x with
+    | Build_t original_value present_value new_value =>
+      Value.StructRecord "context::host::SStoreResult" [
+        ("original_value", to_value original_value);
+        ("present_value", to_value present_value);
+        ("new_value", to_value new_value)
+      ]
+    end.
+
+  Global Instance IsLink : Link t := {
+    to_ty := Ty.path "context::host::SStoreResult";
+    to_value := to_value
+  }.
+End SStoreResult.

CoqOfRust/revm/of_json/of_json.py

@@ -0,0 +1,248 @@
+"""
+Utility functions to generate Coq files from the JSON generated by `coq-of-rust`.
+"""
+
+
+from typing import Any, Tuple
+
+
+def find_top_level_item(prefix: list[str], top_level, condition) -> Tuple[list[str], Any] | None:
+    for entry in top_level:
+        item = entry["item"]
+        if condition(item):
+            return (prefix, item)
+        if "Module" in item:
+            module = item["Module"]
+            result = find_top_level_item(prefix + [module["name"]], module["body"], condition)
+            if result:
+                return result
+
+
+def find_top_level_item_by_name(crate: str, top_level, name: str) -> Tuple[list[str], Any]:
+    def item_has_name(item):
+        if isinstance(item, dict):
+            item = next(iter(item.values()))
+            return "name" in item and item["name"] == name
+        return False
+
+    result = find_top_level_item(
+        [crate],
+        top_level,
+        item_has_name,
+    )
+    if result:
+        return result
+    raise Exception("Item not found: " + name)
+
+
+def get_header(imports: list[str]) -> str:
+    return """(* Generated file. Do not edit. *)
+Require Import CoqOfRust.CoqOfRust.
+Require Import simulations.M.
+""" + "".join("Require " + import_ + ".\n" for import_ in imports)
+
+
+def indent(s: str) -> str:
+    return "\n".join(
+        # We do not indent empty lines
+        "  " + line if len(line) > 0 else ""
+        for line in s.split("\n")
+    )
+
+
+def paren(with_paren: bool, s: str) -> str:
+    if with_paren:
+        return "(" + s + ")"
+    return s
+
+
+def pp_path(path) -> str:
+    return ".".join(path)
+
+
+def pp_const(const) -> str:
+    if "Literal" in const:
+        const = const["Literal"]
+        if "Integer" in const:
+            integer = const["Integer"]
+            return str(integer["value"])
+        return "Unknown literal " + str(const)
+    return "Unknown const " + str(const)
+
+
+
+def pp_type(with_paren: bool, item) -> str:
+    if "Var" in item:
+        item = item["Var"]
+        return item["name"]
+    if "Path" in item:
+        item = item["Path"]
+        path = item["path"]
+        if path == ["*const"]:
+            return "Ref.t Pointer.Kind.ConstPointer"
+        if path == ["bool"]:
+            return "bool"
+        return pp_path(path) + ".t"
+    if "Application" in item:
+        item = item["Application"]
+        return paren(
+            with_paren and len(item["consts"]) + len(item["tys"]) > 0,
+            " ".join(
+                [pp_type(True, item["func"])] +
+                [pp_const(const) for const in item["consts"]] +
+                [pp_type(True, ty) for ty in item["tys"]]
+            )
+        )
+    if "Tuple" in item:
+        item = item["Tuple"]
+        return paren(
+            with_paren,
+            " * ".join(pp_type(True, ty) for ty in item["tys"])
+        )
+    return "Unknown type " + str(item)
+
+
+def pp_type_struct_struct(prefix: list[str], item) -> str:
+    def get_ty_params(is_implicit: bool) -> str:
+        if len(item["ty_params"]) != 0:
+            return \
+                ("{" if is_implicit else "(") + \
+                " ".join(item["ty_params"]) + \
+                ": Set" + \
+                ("}" if is_implicit else ")") + \
+                " "
+        else:
+            return ""
+
+    def get_applied_ty() -> str:
+        if len(item["ty_params"]) != 0:
+            return "t" + "".join(" " + ty_param for ty_param in item["ty_params"])
+        else:
+            return "t"
+
+    ty_params_links = "".join("`{Link " + ty_param + "} " for ty_param in item["ty_params"])
+    full_name = "::".join(prefix + [item["name"]])
+    return pp_module(item["name"],
+        "Record t " + get_ty_params(True) + ": Set := {\n" +
+        indent("".join(
+            field[0] + ": " + pp_type(False, field[1]) + ";\n"
+            for field in item["fields"]
+        )) +
+        "}.\n" +
+        ("Arguments Build_t {" + " ".join(["_"] * len(item["ty_params"])) + "}.\n" +
+        "Arguments t : clear implicits.\n"
+        if len(item["ty_params"]) > 0
+        else ""
+        ) +
+        "\n" +
+        f"Definition current_to_value {get_ty_params(True)}(x: {get_applied_ty()}) : Value.t :=\n" +
+        indent(
+            "match x with\n" +
+            "| Build_t" + "".join(" " + field[0] for field in item["fields"]) + " =>\n" +
+            indent(
+                f"Value.StructRecord \"{full_name}\" [\n" +
+                indent(";\n".join(
+                    "(\"" + field[0] + "\", to_value " + field[0] + ")"
+                    for field in item["fields"]
+                )) + "\n" +
+                "]\n"
+            ) +
+            "end.\n"
+        ) +
+        "\n" +
+        "Global Instance IsLink " + get_ty_params(True) + ty_params_links + ": Link " +
+        paren(len(item["ty_params"]) > 0, " ".join(["t"] + item["ty_params"])) +
+        " := {\n" +
+        indent(
+            "to_ty := Ty.path \"" + full_name + "\";\n" +
+            "to_value := to_value\n"
+        ) +
+        "}."
+    )
+
+
+def pp_type_struct_tuple(prefix: list[str], item) -> str:
+    if len(item["ty_params"]) != 0:
+        ty_params = "(" + " ".join(item["ty_params"]) + ": Set) "
+    else:
+        ty_params = ""
+    ty_params_links = "".join("`{Link " + ty_param + "} " for ty_param in item["ty_params"])
+    return pp_module(item["name"],
+        "Inductive t " + ty_params + ": Set :=\n" +
+        "| Make :" +
+        "".join(
+            " " + pp_type(False, field) + " ->"
+            for field in item["fields"]
+        ) +
+        " t" + "".join(" " + ty_param for ty_param in item["ty_params"]) + ".\n" +
+        ("Arguments Make {" + " ".join(["_"] * len(item["ty_params"])) + "}.\n"
+        if len(item["ty_params"]) > 0
+        else ""
+        ) +
+        "\n" +
+        "Global Instance IsLink " + ty_params + ty_params_links + ": Link " +
+        paren(len(item["ty_params"]) > 0, " ".join(["t"] + item["ty_params"])) +
+        " := {\n" +
+        indent(
+            "to_ty := Ty.path \"" + "::".join(prefix + [item["name"]]) + "\";\n" +
+            "to_value '(Make" + "".join(" x" + str(index) for index in range(len(item["fields"]))) + ") :=\n" +
+            indent(
+                "Value.StructTuple \"" + "::".join(prefix + [item["name"]]) + "\" [" +
+                "; ".join("to_value x" + str(index) for index in range(len(item["fields"]))) + "];\n"
+            )
+        ) +
+        "}."
+    )
+
+
+def pp_type_enum(prefix: list[str], item) -> str:
+    name = item["name"]
+    variants = item["variants"]
+
+    if len(item["ty_params"]) != 0:
+        ty_params = "(" + " ".join(item["ty_params"]) + ": Set) "
+        ty_params_args = "".join(" " + ty_param for ty_param in item["ty_params"])
+    else:
+        ty_params = ""
+        ty_params_args = ""
+
+    # Generate the inductive type definition
+    inductive_def = f"Inductive t {ty_params}: Set :=\n"
+    for variant in variants:
+        variant_name = variant["name"]
+        if "Tuple" in variant["item"] and len(variant["item"]["Tuple"]["tys"]) == 0:
+            inductive_def += f"| {variant_name}\n"
+        else:
+            tys = variant["item"]["tys"]
+            inductive_def += f"| {variant_name} : {' -> '.join(pp_type(False, ty) for ty in tys)} -> t{ty_params_args}\n"
+    inductive_def += "."
+
+    # Generate the Arguments line if there are type parameters
+    arguments_line = (f"Arguments {' '.join(variant['name'] for variant in variants)} " +
+                      "{" + " ".join(["_"] * len(item["ty_params"])) + "}.\n"
+                     ) if len(item["ty_params"]) > 0 else ""
+
+    return pp_module(name,
+        inductive_def +
+        arguments_line
+    )
+
+
+def pp_top_level_item(prefix: list[str], item) -> str:
+    if "TypeStructStruct" in item:
+        item = item["TypeStructStruct"]
+        return pp_type_struct_struct(prefix, item)
+    if "TypeStructTuple" in item:
+        item = item["TypeStructTuple"]
+        return pp_type_struct_tuple(prefix, item)
+    if "TypeEnum" in item:
+        item = item["TypeEnum"]
+        return pp_type_enum(prefix, item)
+    return "Unknown item type " + str(item)
+
+
+def pp_module(name: str, content: str) -> str:
+    return \
+        "Module " + name + ".\n" + \
+        indent(content) + "\n" + \
+        "End " + name + "."

CoqOfRust/revm/of_json/specification.py

@@ -0,0 +1,14 @@
+import json
+import of_json as o
+
+crate = "specification"
+
+def hardfork():
+    input = json.load(open('../translations/specification/hardfork.json'))
+    output = o.get_header([])
+    output += "\n"
+    output += o.pp_top_level_item(*o.find_top_level_item_by_name(crate, input, "SpecId"))
+    with open('specification/hardfork.v', 'w') as f:
+        f.write(output)
+
+hardfork()

CoqOfRust/revm/of_json/specification/hardfork.v

@@ -0,0 +1,29 @@
+(* Generated file. Do not edit. *)
+Require Import CoqOfRust.CoqOfRust.
+Require Import simulations.M.
+
+Module SpecId.
+  Inductive t : Set :=
+  | FRONTIER
+  | FRONTIER_THAWING
+  | HOMESTEAD
+  | DAO_FORK
+  | TANGERINE
+  | SPURIOUS_DRAGON
+  | BYZANTIUM
+  | CONSTANTINOPLE
+  | PETERSBURG
+  | ISTANBUL
+  | MUIR_GLACIER
+  | BERLIN
+  | LONDON
+  | ARROW_GLACIER
+  | GRAY_GLACIER
+  | MERGE
+  | SHANGHAI
+  | CANCUN
+  | PRAGUE
+  | OSAKA
+  | LATEST
+  .
+End SpecId.