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

// 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 {}