f1r3fly-models 0.1.0

/**
 * Rholang Term Structure
 *
 * The top level is `Par`.
 *
 */
syntax = "proto3";

package rhoapi;

// If you are building for other languages "scalapb.proto"
// can be manually obtained here:
// https://raw.githubusercontent.com/scalapb/ScalaPB/master/protobuf/scalapb/scalapb.proto
// make a scalapb directory in this file's location and place it inside

import "scalapb/scalapb.proto";

option (scalapb.options) = {
  package_name: "coop.rchain.models"
  import: "coop.rchain.models.BitSetBytesMapper.bitSetBytesMapper"
  import: "coop.rchain.models.ParSetTypeMapper.parSetESetTypeMapper"
  import: "coop.rchain.models.ParMapTypeMapper.parMapEMapTypeMapper"
  preserve_unknown_fields: false
};

/**
 * Rholang process
 *
 * For example, `@0!(1) | @2!(3) | for(x <- @0) { Nil }` has two sends
 * and one receive.
 *
 * The Nil process is a `Par` with no sends, receives, etc.
 */
message Par {
  repeated Send sends = 1;
  repeated Receive receives = 2;
  repeated New news = 4;
  repeated Expr exprs = 5;
  repeated Match matches = 6;
  repeated GUnforgeable unforgeables = 7;  // unforgeable names
  repeated Bundle bundles = 11;
  repeated Connective connectives = 8;
  bytes locallyFree = 9
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
  bool connective_used = 10;
}

/**
 * Either rholang code or code built in to the interpreter.
 */
message TaggedContinuation {
  oneof tagged_cont {
    ParWithRandom par_body = 1;
    int64 scala_body_ref = 2;
  }
}

/**
 * Rholang code along with the state of a split random number
 * generator for generating new unforgeable names.
 */
message ParWithRandom {
  Par body = 1 [(scalapb.field).no_box = true];
  bytes randomState = 2
      [(scalapb.field).type = "coop.rchain.crypto.hash.Blake2b512Random"];
}

/**
 * Cost of the performed operations.
 */
message PCost {
  uint64 cost = 1;
}

message ListParWithRandom {
  repeated Par pars = 1;
  bytes randomState = 2
      [(scalapb.field).type = "coop.rchain.crypto.hash.Blake2b512Random"];
}

// While we use vars in both positions, when producing the normalized
// representation we need a discipline to track whether a var is a name or a
// process.
// These are DeBruijn levels
message Var {
  message WildcardMsg {}
  oneof var_instance {
    sint32 bound_var = 1;
    sint32 free_var = 2;
    WildcardMsg wildcard = 3;
  }
}

/**
 * Nothing can be received from a (quoted) bundle with `readFlag = false`.
 * Likeise nothing can be sent to a (quoted) bundle with `writeFlag = false`.
 *
 * If both flags are set to false, bundle allows only for equivalance check.
 */
message Bundle {
  Par body = 1 [(scalapb.field).no_box = true];
  bool writeFlag = 2;  // flag indicating whether bundle is writeable
  bool readFlag = 3;   // flag indicating whether bundle is readable
}

/**
 * A send is written `chan!(data)` or `chan!!(data)` for a persistent send.
 *
 * Upon send, all free variables in data are substituted with their values.
 */
message Send {
  Par chan = 1 [(scalapb.field).no_box = true];
  repeated Par data = 2;
  bool persistent = 3;
  bytes locallyFree = 5
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
  bool connective_used = 6;
}

message ReceiveBind {
  repeated Par patterns = 1;
  Par source = 2 [(scalapb.field).no_box = true];
  Var remainder = 3;
  int32 freeCount = 4;
}

message BindPattern {
  repeated Par patterns = 1;
  Var remainder = 2;
  int32 freeCount = 3;
}

message ListBindPatterns {
  repeated BindPattern patterns = 1;
}

/**
 * A receive is written `for(binds) { body }`
 * i.e. `for(patterns <- source) { body }`
 * or for a persistent recieve: `for(patterns <= source) { body }`.
 *
 * It's an error for free Variable to occur more than once in a pattern.
 */
message Receive {
  repeated ReceiveBind binds = 1;
  Par body = 2 [(scalapb.field).no_box = true];
  bool persistent = 3;
  bool peek = 4;
  int32 bindCount = 5;
  bytes locallyFree = 6
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
  bool connective_used = 7;
}

// Number of variables bound in the new statement.
// For normalized form, p should not contain solely another new.
// Also for normalized form, the first use should be level+0, next use level+1
// up to level+count for the last used variable.
message New {
  // Includes any uris listed below. This makes it easier to substitute or walk
  // a term.
  sint32 bindCount = 1;
  Par p = 2 [(scalapb.field).no_box = true];
  // For normalization, uri-referenced variables come at the end, and in
  // lexicographical order.
  repeated string uri = 3;
  map<string, Par> injections = 4;
  bytes locallyFree = 5
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
}

message MatchCase {
  Par pattern = 1 [(scalapb.field).no_box = true];
  Par source = 2 [(scalapb.field).no_box = true];
  int32 freeCount = 3;
}

message Match {
  Par target = 1 [(scalapb.field).no_box = true];
  repeated MatchCase cases = 2;
  bytes locallyFree = 4
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
  bool connective_used = 5;
}

// Any process may be an operand to an expression.
// Only processes equivalent to a ground process of compatible type will reduce.
message Expr {
  oneof expr_instance {
    bool g_bool = 1;
    sint64 g_int = 2;
    string g_string = 3;
    string g_uri = 4;
    bytes g_byte_array = 25;

    ENot e_not_body = 5;
    ENeg e_neg_body = 6;
    EMult e_mult_body = 7;
    EDiv e_div_body = 8;
    EPlus e_plus_body = 9;
    EMinus e_minus_body = 10;
    ELt e_lt_body = 11;
    ELte e_lte_body = 12;
    EGt e_gt_body = 13;
    EGte e_gte_body = 14;
    EEq e_eq_body = 15;
    ENeq e_neq_body = 16;
    EAnd e_and_body = 17;
    EOr e_or_body = 18;
    EVar e_var_body = 19;

    EList e_list_body = 20;
    ETuple e_tuple_body = 21;
    ESet e_set_body = 22 [(scalapb.field).type = "coop.rchain.models.ParSet"];
    EMap e_map_body = 23 [(scalapb.field).type = "coop.rchain.models.ParMap"];
    EMethod e_method_body = 24;

    EMatches e_matches_body = 27;
    EPercentPercent e_percent_percent_body = 28;  // string interpolation
    EPlusPlus e_plus_plus_body = 29;              // concatenation
    EMinusMinus e_minus_minus_body = 30;          // set difference

    EMod e_mod_body = 31;
  }
}

message EList {
  repeated Par ps = 1;
  bytes locallyFree = 3
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
  bool connective_used = 4;
  Var remainder = 5;
}

message ETuple {
  repeated Par ps = 1;
  bytes locallyFree = 3
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
  bool connective_used = 4;
}

message ESet {
  repeated Par ps = 1;
  bytes locallyFree = 3
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
  bool connective_used = 4;
  Var remainder = 5;
}

message EMap {
  repeated KeyValuePair kvs = 1;
  bytes locallyFree = 3
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
  bool connective_used = 4;
  Var remainder = 5;
}

/**
 * `target.method(arguments)`
 */
message EMethod {
  string methodName = 1;
  Par target = 2 [(scalapb.field).no_box = true];
  repeated Par arguments = 3;
  bytes locallyFree = 5
      [(scalapb.field).type =
           "coop.rchain.models.AlwaysEqual[scala.collection.immutable.BitSet]"];
  bool connective_used = 6;
}

message KeyValuePair {
  Par key = 1 [(scalapb.field).no_box = true];
  Par value = 2 [(scalapb.field).no_box = true];
}

// A variable used as a var should be bound in a process context, not a name
// context. For example:
// `for (@x <- c1; @y <- c2) { z!(x + y) }` is fine, but
// `for (x <- c1; y <- c2) { z!(x + y) }` should raise an error.
message EVar {
  Var v = 1 [(scalapb.field).no_box = true];
}

message ENot {
  Par p = 1 [(scalapb.field).no_box = true];
}

message ENeg {
  Par p = 1 [(scalapb.field).no_box = true];
}

message EMult {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EDiv {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EMod {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EPlus {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EMinus {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message ELt {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message ELte {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EGt {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EGte {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EEq {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message ENeq {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EAnd {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EOr {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message EMatches {
  Par target = 1 [(scalapb.field).no_box = true];
  Par pattern = 2 [(scalapb.field).no_box = true];
}

/**
 * String interpolation
 *
 * `"Hello, {name}" %% {"name": "Bob"}` denotes `"Hello, Bob"`
 */
message EPercentPercent {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

// Concatenation
message EPlusPlus {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

// Set difference
message EMinusMinus {
  Par p1 = 1 [(scalapb.field).no_box = true];
  Par p2 = 2 [(scalapb.field).no_box = true];
}

message Connective {
  oneof connective_instance {
    ConnectiveBody conn_and_body = 1;
    ConnectiveBody conn_or_body = 2;
    Par conn_not_body = 3;
    VarRef var_ref_body = 4;
    bool conn_bool = 5;
    bool conn_int = 6;
    bool conn_string = 7;
    bool conn_uri = 8;
    bool conn_byte_array = 9;
  }
}

message VarRef {
  sint32 index = 1;
  sint32 depth = 2;
}

message ConnectiveBody {
  repeated Par ps = 1;
}

message DeployId {
  bytes sig = 1;
}

message DeployerId {
  bytes publicKey = 1;
}

// Unforgeable names resulting from `new x { ... }`
// These should only occur as the program is being evaluated. There is no way in
// the grammar to construct them.
message GUnforgeable {
  oneof unf_instance {
    GPrivate g_private_body = 1;
    GDeployId g_deploy_id_body = 2;
    GDeployerId g_deployer_id_body = 3;
    GSysAuthToken g_sys_auth_token_body = 4;
  }
}

message GPrivate {
  bytes id = 1;
}

message GDeployId {
  bytes sig = 1;
}

message GDeployerId {
  bytes publicKey = 1;
}

message GSysAuthToken {}