links: add generation of Link instances

Author: clarus

.github/workflows/rust.yml

@@ -128,38 +128,38 @@ jobs:
             cd crates
             # move-abstract-stack
             cd move-abstract-stack
-            cargo coq-of-rust
+            cargo coq-of-rust --with-json
             touch src/lib.rs
-            cargo coq-of-rust
-            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_abstract_stack/ --include='*/' --include='*.v' --exclude='*'
+            cargo coq-of-rust --with-json
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_abstract_stack/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
             cd ..
             # move-binary-format
             cd move-binary-format
-            cargo coq-of-rust
+            cargo coq-of-rust --with-json
             touch src/lib.rs
-            cargo coq-of-rust
-            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_binary_format/ --include='*/' --include='*.v' --exclude='*'
+            cargo coq-of-rust --with-json
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_binary_format/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
             cd ..
             # move-bytecode-verifier
             cd move-bytecode-verifier
-            cargo coq-of-rust
+            cargo coq-of-rust --with-json
             touch src/lib.rs
-            cargo coq-of-rust
-            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier/ --include='*/' --include='*.v' --exclude='*'
+            cargo coq-of-rust --with-json
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
             cd ..
             # move-bytecode-verifier-meter
             cd move-bytecode-verifier-meter
-            cargo coq-of-rust
+            cargo coq-of-rust --with-json
             touch src/lib.rs
-            cargo coq-of-rust
-            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier_meter/ --include='*/' --include='*.v' --exclude='*'
+            cargo coq-of-rust --with-json
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_bytecode_verifier_meter/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
             cd ..
             # move-core-types
             cd move-core-types
-            cargo coq-of-rust
+            cargo coq-of-rust --with-json
             touch src/lib.rs
-            cargo coq-of-rust
-            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_core_types/ --include='*/' --include='*.v' --exclude='*'
+            cargo coq-of-rust --with-json
+            rsync -acv src/ ../../../../CoqOfRust/move_sui/translations/move_core_types/ --include='*/' --include='*.v' --include='*.json' --exclude='*'
             cd ..
             cd ../../..
           endGroup

CoqOfRust/blacklist.txt

@@ -17,8 +17,9 @@ core/iter/adapters/flatten.v
 core/net/ip_addr.v
 core/num/int_sqrt.v
 token-2022
+# We ignore the metering for now
+move_sui/simulations/move_bytecode_verifier_meter/lib.v
 # Links that are not working yet
 core/links/cmp.v
-move_sui/links/
-# We ignore the metering for now
-move_sui/simulations/move_bytecode_verifier_meter/lib.v
+links/move_sui/move_binary_format/file_format.v
+links/move_sui/move_bytecode_verifier/type_safety.v

CoqOfRust/links.py

@@ -3,22 +3,29 @@
 """
 
 
-def find_top_level_item(top_level, condition):
+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 item
+            return (prefix, item)
         if item["type"] == "Module":
-            result = find_top_level_item(item["body"], condition)
+            result = find_top_level_item(prefix + [item["name"]], item["body"], condition)
             if result:
                 return result
 
 
-def find_top_level_item_by_name(top_level, name):
-    return find_top_level_item(
+def find_top_level_item_by_name(crate: str, top_level, name: str) -> Tuple[list[str], Any]:
+    result = find_top_level_item(
+        [crate],
         top_level,
         lambda item: "name" in item and item["name"] == name
     )
+    if result:
+        return result
+    raise Exception("Item not found: " + name)
 
 
 def get_header(imports: list[str]) -> str:
@@ -30,8 +37,12 @@ def get_header(imports: list[str]) -> str:
 """
 
 
-def indent(level: int) -> str:
-    return "  " * level
+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:
@@ -51,41 +62,98 @@ def pp_type(with_paren: bool, item) -> str:
         path = item["path"]
         if path == ["*const"]:
             return "Ref.t Pointer.Kind.ConstPointer"
+        if path == ["bool"]:
+            return "bool"
         return pp_path(path) + ".t"
     if item["type"] == "Application":
         return paren(
-            with_paren,
+            with_paren and len(item["tys"]) > 0,
             " ".join(pp_type(True, ty) for ty in [item["func"]] + item["tys"])
         )
     return "Unknown type " + item["type"]
 
 
-def pp_type_struct_struct(level: int, item) -> str:
-    result = "Module " + item["name"] + ".\n"
+def pp_type_struct_struct(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"])
-    result += indent(level + 1) + "Record t " + ty_params + ty_params_links + ": Set := {\n"
-    for field in item["fields"]:
-        result += indent(level + 2) + field[0] + ": " + pp_type(False, field[1]) + ";\n"
-    result += indent(level + 1) + "}.\n"
-    result += indent(level) + "End " + item["name"] + "."
-    return result
+    return pp_module(item["name"],
+        "Record t " + ty_params + ty_params_links + ": 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"
+        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 '(Build_t" + "".join(" " + field[0] for field in item["fields"]) + ") :=\n" +
+            indent(
+                "Value.StructRecord \"" + "::".join(prefix + [item["name"]]) + "\" [\n" +
+                indent(";\n".join(
+                    "(\"" + field[0] + "\", to_value " + field[0] + ")"
+                    for field in item["fields"]
+                )) + "\n" +
+                "];\n"
+            )
+        ) +
+        "}."
+    )
 
 
-def pp_type_struct_tuple(level: int, item) -> str:
-    result = "Module " + item["name"] + ".\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"])
-    result += indent(level + 1) + "Inductive t " + ty_params + ty_params_links + ": Set :=\n"
-    result += \
-        indent(level + 1) + "| Make :" + \
-        "".join(" " + pp_type(False, field) + " ->" for field in item["fields"]) + \
-        " t" + "".join(" " + ty_param for ty_param in item["ty_params"]) + ".\n"
-    result += indent(level) + "End " + item["name"] + "."
-    return result
+    return pp_module(item["name"],
+        "Inductive t " + ty_params + ty_params_links + ": 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_top_level_item(prefix: list[str], item) -> str:
+    if item["type"] == "TypeStructStruct":
+        return pp_type_struct_struct(prefix, item)
+    if item["type"] == "TypeStructTuple":
+        return pp_type_struct_tuple(prefix, item)
+    return "Unknown item type " + item["type"]
+
+
+def pp_module(name: str, content: str) -> str:
+    return \
+        "Module " + name + ".\n" + \
+        indent(content) + "\n" + \
+        "End " + name + "."

CoqOfRust/links/alloc/alloc.py

@@ -0,0 +1,9 @@
+import json
+import links as l
+
+crate = "alloc"
+alloc = json.load(open("alloc/alloc.json"))
+
+print(l.get_header([
+]))
+print(l.pp_top_level_item(*l.find_top_level_item_by_name(crate, alloc, "Global")))

CoqOfRust/links/alloc/alloc.v

@@ -0,0 +1,16 @@
+(* Generated file for the links. Do not edit. *)
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+
+Import Run.
+
+Module Global.
+  Inductive t : Set :=
+  | Make : t.
+
+  Global Instance IsLink : Link t := {
+    to_ty := Ty.path "alloc::alloc::Global";
+    to_value '(Make) :=
+      Value.StructTuple "alloc::alloc::Global" [];
+  }.
+End Global.

CoqOfRust/links/alloc/raw_vec.py

@@ -1,16 +1,14 @@
 import json
 import links as l
 
-input_file = "alloc/raw_vec.json"
-
-with open(input_file) as f:
-    input = json.load(f)
+crate = "alloc"
+raw_vec = json.load(open("alloc/raw_vec.json"))
 
 print(l.get_header([
     "links.core.ptr.unique",
 ]))
-print(l.pp_type_struct_tuple(0, l.find_top_level_item_by_name(input, "Cap")))
+print(l.pp_top_level_item(*l.find_top_level_item_by_name(crate, raw_vec, "Cap")))
 print()
-print(l.pp_type_struct_struct(0, l.find_top_level_item_by_name(input, "RawVecInner")))
+print(l.pp_top_level_item(*l.find_top_level_item_by_name(crate, raw_vec, "RawVecInner")))
 print()
-print(l.pp_type_struct_struct(0, l.find_top_level_item_by_name(input, "RawVec")))
+print(l.pp_top_level_item(*l.find_top_level_item_by_name(crate, raw_vec, "RawVec")))

CoqOfRust/links/alloc/raw_vec.v

@@ -8,6 +8,12 @@ Import Run.
 Module Cap.
   Inductive t : Set :=
   | Make : usize.t -> t.
+
+  Global Instance IsLink : Link t := {
+    to_ty := Ty.path "alloc::raw_vec::Cap";
+    to_value '(Make x0) :=
+      Value.StructTuple "alloc::raw_vec::Cap" [to_value x0];
+  }.
 End Cap.
 
 Module RawVecInner.
@@ -16,11 +22,32 @@ Module RawVecInner.
     cap: alloc.raw_vec.Cap.t;
     alloc: A;
   }.
+  Arguments Build_t {_ _}.
+
+  Global Instance IsLink (A: Set) `{Link A} : Link (t A) := {
+    to_ty := Ty.path "alloc::raw_vec::RawVecInner";
+    to_value '(Build_t ptr cap alloc) :=
+      Value.StructRecord "alloc::raw_vec::RawVecInner" [
+        ("ptr", to_value ptr);
+        ("cap", to_value cap);
+        ("alloc", to_value alloc)
+      ];
+  }.
 End RawVecInner.
 
 Module RawVec.
   Record t (T A: Set) `{Link T} `{Link A} : Set := {
     inner: alloc.raw_vec.RawVecInner.t A;
     _marker: core.marker.PhantomData.t T;
   }.
+  Arguments Build_t {_ _ _ _}.
+
+  Global Instance IsLink (T A: Set) `{Link T} `{Link A} : Link (t T A) := {
+    to_ty := Ty.path "alloc::raw_vec::RawVec";
+    to_value '(Build_t inner _marker) :=
+      Value.StructRecord "alloc::raw_vec::RawVec" [
+        ("inner", to_value inner);
+        ("_marker", to_value _marker)
+      ];
+  }.
 End RawVec.

CoqOfRust/links/alloc/vec.py

@@ -0,0 +1,10 @@
+import json
+import links as l
+
+crate = "alloc"
+vec_mod = json.load(open("alloc/vec/mod.json"))
+
+print(l.get_header([
+    "links.alloc.raw_vec",
+]))
+print(l.pp_top_level_item(*l.find_top_level_item_by_name(crate, vec_mod, "Vec")))

CoqOfRust/links/alloc/vec.v

@@ -0,0 +1,23 @@
+(* Generated file for the links. Do not edit. *)
+Require Import CoqOfRust.CoqOfRust.
+Require Import links.M.
+Require links.alloc.raw_vec.
+
+Import Run.
+
+Module Vec.
+  Record t (T A: Set) `{Link T} `{Link A} : Set := {
+    buf: alloc.raw_vec.RawVec.t T A;
+    len: usize.t;
+  }.
+  Arguments Build_t {_ _ _ _}.
+
+  Global Instance IsLink (T A: Set) `{Link T} `{Link A} : Link (t T A) := {
+    to_ty := Ty.path "alloc::vec::Vec";
+    to_value '(Build_t buf len) :=
+      Value.StructRecord "alloc::vec::Vec" [
+        ("buf", to_value buf);
+        ("len", to_value len)
+      ];
+  }.
+End Vec.