Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Env: translate the Environment trait #90

Closed
Tracked by #87
clarus opened this issue Jun 15, 2023 · 1 comment
Closed
Tracked by #87

Env: translate the Environment trait #90

clarus opened this issue Jun 15, 2023 · 1 comment
Assignees

Comments

@clarus
Copy link
Collaborator

clarus commented Jun 15, 2023

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;

...
@dhilst
Copy link
Collaborator

dhilst commented Jul 3, 2023

The inv_env.v file after the #99 MR, the parameters

image

@dhilst dhilst closed this as completed Jul 3, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants