formal-land / coq-of-rust Goto Github PK

Translate the file https://github.com/formal-land/coq-of-rust/blob/main/examples-from-rust-book/conversion/converting_to_string.rs

The file https://github.com/paritytech/ink/blob/2eba99ee445a4aee34d0919041388e7e727f7ed8/crates/env/src/api.rs starts with:

use crate::{
    backend::{
        EnvBackend,
        ReturnFlags,
        TypedEnvBackend,
    }

that is translated to:

Module ReturnFlags := crate.backend.ReturnFlags.
Definition ReturnFlags := ReturnFlags.t.

as EnvBackend and TypedEnvBackend are traits and the use of traits is not handled yet.

The goal of this task is to instead inline the use of backend::ReturnFlags so that this type appears fully prefixed where used. This will require introducing an environment of current used types for the translation of top-level items/expressions.

The rationale of this task is to reduce the number of mutual dependencies between sub-modules of a crate, and simplify the re-ordering that we will do later.

We should have a translation option to add lines of Require to require dependencies after compiling a crate (unless if that can be done automatically to discover the dependencies).

The goal of this issue is to have an additional parameter to chose one of two translation modes:

• library mode (axiomatize the definitions)
• code mode (full translation to Coq)

That mode may be set by a command-line parameter or an environment variable. It can be added to the global variable env https://github.com/formal-land/coq-of-rust/blob/main/lib/src/env.rs

In https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_storage_traits.v there is the trait storage.Storable that is translated to:

Module storage.
  Module Storable.
    Class Trait (Self : Set) : Set := {
      encode
        `{H : State.Trait}
        :
        (ref Self) -> (mut_ref T) -> (M (H := H) unit);
      decode
        `{H : State.Trait}
        :
        (mut_ref I) ->
        (M (H := H) (core.result.Result Self parity_scale_codec.error.Error));
    }.

There should also be quantifiers over the type T, as the original code is:

pub trait Storable: Sized {
    /// Convert self to a slice and append it to the destination.
    fn encode<T: scale::Output + ?Sized>(&self, dest: &mut T);

    /// Attempt to deserialize the value from input.
    fn decode<I: scale::Input>(input: &mut I) -> Result<Self, scale::Error>;
}

The goal is to have the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/Env.v type-checking in Coq. This is one of the libraries used to make ink! smart contracts. That would be a good milestone toward translating Rust smart contracts to Coq. Note that there are still other ink! libraries, and these libraries themselves depend on other files.

To translate this file successfully, we take all the Rust features that we do not handle but need to, and make a task on a smaller example. We use the label Ink! env library.

• #88
• #89
• #90
• #95

Generate a version of https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_e2e.v that compiles in Coq. Note that this file depends on https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_env.v that is currently behind handled in the pull request #179 , but it is maybe possible to axiomatize by hand the missing dependencies.

A monadic transformation is necessary to represent the various side-effects, like control-flow primitives (return, break, continue), errors (panic!), and state mutations.

There is already a tentative pull-request to make a monadic transformation of the generated Coq code: #58

This pull-request avoids making an explicit monadic transform through the use of tactics. But the problem is that it limits type inference as we do not have access to the expected return type of an expression inside the tactic. Type inference is quite fragile with what we are doing, as we already rely on type-classes that need a lot inference for example.

A more reliable solution is to make an explicit monadic transformation. This is the goal of this task.

Depends on #90

In https://github.com/paritytech/ink/blob/2eba99ee445a4aee34d0919041388e7e727f7ed8/crates/env/src/api.rs there is the Rust code:

pub fn caller<E>() -> E::AccountId
where
    E: Environment,
{
    <EnvInstance as OnInstance>::on_instance(|instance| {
        TypedEnvBackend::caller::<E>(instance)
    })
}

that we (incorrectly) translate to:

Definition caller
    {E : Set}
    `{Environment.Trait E}
    (_ : unit)
    : M ImplE.AccountId :=
  OnInstance.on_instance (fun instance => TypedEnvBackend.caller instance).

We should:

• remove the (_ : unit) parameter
• translate E::AccountId correctly

Currently, we are adding more and more options to the cargo coq-of-rust command. It would be simpler to group all of them in a JSON configuration file. The goal of this issue is to add such a configuration file, grouping all existing command-line options. There should still be one command-lind option to give the path to this configuration file.

The beginning of https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_env.v starts with:

(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module types.
  Module FromLittleEndian.
    Class Trait
        (Self : Set)
        {Bytes : Set}
        `{core.default.Default.Trait Bytes}
        `{core.convert.AsRef.Trait Bytes}
        `{core.convert.AsMut.Trait Bytes} :
        Set := {
      Bytes := Bytes;
      from_le_bytes : ImplSelf.Bytes -> (M Self);
    }.

Make it compile in Coq, probably plugging/adding the missing traits in the standard library.

The hash.v and convert.v should be moved to the core folder, and exported as core in CoqOfRust.v.

Use the notation (| ... |) to make function calls, as given in #58 For now do not do any monadic transformation, so that:

f(| a, b |)

is just syntactic sugar for:

f a b

In https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_storage_traits.v there is a translation:

  Class Trait
      (Self : Set) {Key : Set}
      {Type : Set}
      `{ink_storage_traits.storage.Storable.Trait Type}
      {PreferredKey : Set}
      `{ink_storage_traits.storage.StorageKey.Trait PreferredKey} :
      Set := {
    Type := Type;
    PreferredKey := PreferredKey;
  }.

containing the forbidden keyword Type. Replace this keyword with something like _Type.

Only public modules/functions/data types should be translated in axiom mode, as the rest will not be used anyways (no private of pub(crate)).

Import the examples from https://doc.rust-lang.org/rust-by-example/index.html To name the examples, follow the same structure as in the source of the book: https://github.com/rust-lang/rust-by-example

This issue depends on #2 that should be done first.

This issue arises from translating parsing_a_string.rs. The current Coq library is intended to organize every functions into a single file in the topological order. It turns out that there could be mutual references between functions, and Coq is not that flexible to support such reference. e.g. std::result::Result::unwrap and std::fmt::Debug.

We should reorganize the file such that it follows the architecture of Rust documentation, e.g. define the type/trait/enum first, and then define the functions associated with this type/trait/enum.

In the current Coq library as well as the translated code, some functions are associated with a crate named _crate. A typical example is the default print function appeared everywhere in the translated snippets.

After investigation, the cause that generates _crate originates in lib/src/path.rs:

pub fn to_valid_coq_name(str: String) -> String {
    let str = str::replace(&str, "$", "_");
    let str = str::replace(&str, "{{root}}", "Root");
    str::replace(&str, "::", ".")
}

Which is easy to see that it would replace anything with a $ sign into an underscore. We have to figure out a way to correctly translate the $crate.

Official reference for $crate: https://doc.rust-lang.org/reference/macros-by-example.html

For now the slices are translated to a single type without parameter, like in https://github.com/formal-land/coq-of-rust/blob/main/coq_translation/default/examples/subtle.v :

  Definition ct_eq
      `{H : State.Trait}
      (self : ref Self)
      (_rhs : ref Slice)
      : M (H := H) subtle.Choice :=

There should be a type parameter to Slice to match the Rust definition.

Have an example folder with foo.rs files together with their foo.v file corresponding to the translation. The cargo test command should check that the .v files are the translation of the corresponding .rs files.

The goal of this task is to translate https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_e2e_macro.v to a file that compiles in Coq.

Add the examples from https://github.com/paritytech/ink/tree/master/integration-tests into the project. A possible solution:

• have a git-submodule to copy their project
• have a shell script to compile their files and re-generate the examples files extracted from their code
• make sure that our configure script for examples try to compile them, unless if they are in the blacklist.

I found a problem when translating the hash.rs example where two arguments are missing in the translated file

We need to fix this in the translation. To reproduce translate examples/trait/hash.rs again, remove it from blacklist.txt and then try to typecheck the generated hash.v

There is an issue where one of the definitions depends on other definitions in the same file and they need to be reordered in Coq translation before we can evaluate the file (Coq cannot call non-evaluated functions for example).

The first idea is to provide a command line flag that enables us to reorder definitions in the files like --reorder moduleX,definition_a,definition_b,definition_c,...

Another idea is to have a configuration file where we can define the right order

  {
      "reorder": {
        "moduleX": ["definition_a", "definition_b", "definition_c"]
      },
      ...
  } 

Understand where the:

Definition _ : unit := run (tt).

come from in the translation and remove them/translate them correctly, depending on the issue.

Translate the file https://github.com/formal-land/coq-of-rust/blob/main/examples-from-rust-book/cargo/concurrent_tests.rs

This file should go quite fast, as I think that we ignore the tests in the translation to Coq.

In the file https://github.com/formal-land/coq-of-rust/blob/main/examples/traits/traits_parms.rs we have a trait:

trait SomeTrait {
    type SomeType: Foo + Bar + Tar;

    fn some_fn();
}

with the fields:

• SomeType that is a type,
• some_fn that is a value.

that is translated to https://github.com/formal-land/coq-of-rust/blob/main/coq_translation/examples/traits/traits_parms.v

For now we only have a notation to access to some_fn:

  Global Instance AssociatedFunction_some_fn :
    Notation.DoubleColon Self "some_fn" := {
    Notation.double_colon := some_fn;
  }.

The goal of this issue is to add a similar notation for SomeType. One challenge is that we need to generalize Notation.DoubleColon so that it can return a type in addition to a value. Maybe adding something like:

Class DoubleColonType {Kind : Type} (type : Kind) (name : string) : Set := {
  double_colon_type : Set;
}.

that is similar to what we had:

Class DoubleColon {Kind : Type} (type : Kind) (name : string) {T : Set} :
  Set := {
  double_colon : T;
}.

to access to value fields. We would also need to find a new notation for double_colon_type, proposition:

Notation "e1 ::type[ e2 ]" := (Notation.double_colon_type e1 e2)
  (at level 0).

With traits, it is sometimes unclear what type parameter is referring to. Instead of using explicit ordered type parameters, we should use implicit named types parameters with curly braces.

Successfully translate the type definition:

struct PhantomTuple<A, B>(A, PhantomData<B>);

in https://github.com/formal-land/coq-of-rust/blob/main/examples/generics/generics_phantom_type.rs For now it gets translated to:

Record t : Set := { _ : A; _ : core.marker.PhantomData B;}.

to the type parameters A and B are missing.

Translate the file https://github.com/formal-land/coq-of-rust/blob/main/examples-from-rust-book/conversion/parsing_a_string.rs

Translate the file https://github.com/formal-land/coq-of-rust/blob/main/examples-from-rust-book/attributes/dead_code.rs

Translate in axiom mode the https://docs.rs/scale-encode/latest/scale_encode/ library. As a first step, we can add a snapshot of the translation of the library into our CI system for a specific release version, even if the generated file does not compile in Coq.

Note: some code is already defined in the Draft pull-request #58 and can be re-used.

Define a bare monad like:

Module M.
  Inductive t (A : Set) : Set :=
  | Pure : A -> t A
  | Bind B : t B -> (B -> t A) -> t A.
  Arguments Pure {_}.
  Arguments Bind {_ _}.
End M.

with a notation let* for M.Bind.

Use this monad to make a monadic translation of the code. This will necessitate adding an M to all the return types of functions:

Definition f (s : string) : bool :=
  ...

becomes:

Definition f (s : string) : M bool :=
  ...

and this will necessitate to name all the intermediate values for the monadic translation:

f(| a, g(| b |) |)

becomes:

let* 𝑣_1 := g(| b |) in
f(| a, 𝑣_1 |)

for example. Note that we use a Unicode character 𝑣 to limit name collisions (unless if this character is also used in Rust, but that should be rare).

Make sure that the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_storage_traits.v compiles in Coq. This is one of the lowest file in the hierarchy of dependencies for the ERC-20 smart contract.

• use the axiom mode to translate the library

Find a way to define the type Cow in CoqOfRust/std/borrow.v. The difficulty is the as keyword:

pub enum Cow<'a, B>
where
    B: 'a + ToOwned + ?Sized,
{
    Borrowed(&'a B),
    Owned(<B as ToOwned>::Owned),
}

Translate the file https://github.com/formal-land/coq-of-rust/blob/main/examples-from-rust-book/conversion/try_from_and_try_into.rs

In https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_storage_traits.v there is a translation:

  Global Instance Method_key `{H : State.Trait} `(Trait)
    : Notation.Dot "key" := {
    Notation.dot (self : ref Self) :=
      (Pure Self::["KEY"]
      : M (H := H) ink_primitives.key.Key);
  }.

with an explicit definition instead of an axiom as this is a library file. Make this definition an axiom.

Translate the file https://github.com/formal-land/coq-of-rust/blob/main/examples-from-rust-book/conversion/into.rs

Translate the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_macro.v to a Coq file that compiles. Add replacement rules if needed in https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/update_after_translation.py

In https://github.com/paritytech/ink/blob/2eba99ee445a4aee34d0919041388e7e727f7ed8/crates/env/src/types.rs there is the definition of the trait Environment:

pub trait Environment {
    /// The maximum number of supported event topics provided by the runtime.
    ///
    /// The value must match the maximum number of supported event topics of the used
    /// runtime.
    const MAX_EVENT_TOPICS: usize;

    /// The account id type.
    type AccountId: 'static
        + scale::Codec
        + CodecAsType
        + Clone
        + PartialEq
        + Eq
        + Ord
        + AsRef<[u8]>
        + AsMut<[u8]>;
        
...

It is translated for now as:

Module Environment.
  Class Trait (Self : Set) : Set := {
    MAX_EVENT_TOPICS : usize;
    AccountId : Set;

...

in https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/Env.v

Instead, we want to have types that are "synonym fields" (with := instead of :), and all the types being given as parameters together with the type-class information:

Module Environment.
  Class Trait (Self : Set) {AccountId : Set}
      `{scale.Codec AccountId}
      `{CodecAsType AccountId}
      `{Clone AccountId}
      ...
      : Set := {
    MAX_EVENT_TOPICS : usize;
    AccountId := AccountId;

...

Adding a special operator for the while loops in the monad, translate the file https://github.com/formal-land/coq-of-rust/blob/main/examples/flow_of_control/while.rs to a type-checking Coq file https://github.com/formal-land/coq-of-rust/blob/main/coq_translation/examples/flow_of_control/while.v

There is some non-termination effect in the monad M to help for that task.

For now, in https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/CoqOfRust.v , the definition of the monad is:

Module M.
  Parameter M : Set -> Set.
  Parameter Pure : forall {a : Set}, a -> M a.
  Parameter bind : forall {a b : Set}, M a -> (a -> M b) -> M b.

Use the definition from the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/experiments/MonadExperiments.v instead. To use definitions from this file, either do a copy&paste or import these definitions from a separate file.

Many technical difficulties might appear when doing this integration.

Should use name of struct instead of self

Rust code:

Current Coq translation:

Have a beginning of code to translate the type definitions, that is to say fill these lines:

The translation should go to a simple AST and be printed without trying to compile in Coq (basic printing so that we can see something). We will see later how to sort the type definitions, ...

For now there are a few warnings in the compilation of Coq files, that can blur the CI output/that we should fix as these are warnings. Warnings from the _std library are fixed in #117 but there are more warnings in the files generated by the coq-of-rust command. The goal of this issue is to also fix them.

In addition, I do not know if this is possible, but the CI should check that there are no warnings emitted for the Coq command to compile the files.

Translate the file https://github.com/formal-land/coq-of-rust/blob/main/examples-from-rust-book/conversion/from.rs

Very often, a definition is duplicated into the same module. For example, in https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_macro.v there is:

Parameter generate : forall `{H : State.Trait},
    proc_macro2.TokenStream ->
    proc_macro2.TokenStream ->
    M (H := H) proc_macro2.TokenStream.

that is repeated 4 times. This also happens with whole modules or type definitions.

The goal of this issue is to remove such duplicated definitions.

Our monad M used for the monadic translation of Rust requires an additional parameter State.Trait that allows choosing the shape of the state at proof time. The goal of this issue is to add this parameter everywhere.

For example, we should generate:

  Definition fmt
      `{State.Trait}
      (self : ref Self)
      (f : mut_ref core.fmt.Formatter)
      : M core.fmt.Result :=
  ...

instead of:

  Definition fmt
      `{State.Trait}
      (self : ref Self)
      (f : mut_ref core.fmt.Formatter)
      : M core.fmt.Result :=
  ...

That additional parameter should also propagate to other places where monadic functions are used, for example in the signatures of traits.

This issue is a follow-up of #105

The trait core.cmp.PartialEq.Trait has one necessary type parameter and one implicit. Currently, when this trait is implemented we get:

Global Instance I : core.cmp.PartialEq.Trait Self := {
  core.cmp.PartialEq.eq `{H : State.Trait} := eq;
}.

but we should have with the implicit type parameter at None:

Global Instance I : core.cmp.PartialEq.Trait Self None := {
  core.cmp.PartialEq.eq `{H : State.Trait} := eq;
}.

In the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/ink/ink_primitives.v , the translation:

Definition MessageResult : Set := core.result.Result T ink_primitives.LangError.

has a type parameter T that is not introduced, like:

Definition MessageResult (T : Set) : Set := core.result.Result T ink_primitives.LangError.

The goal of this task is to correctly handle the polymorphic parameters.