processFlows.sqnc

/*
 * ------------------
 * Token Declarations
 * ------------------
 *
 * Note that `token`s define formats that should be persisted in transitions.
 * Fields can be of type Role, File, Literal, a specific literal, a token type
 * or a union of any of these
 */

token InitiatedCert {
  hydrogen_owner: Role,
  energy_owner: Role,
  regulator: Role,
  hydrogen_quantity_wh: Literal,
  commitment: Literal,
}

token IssuedCert {
  hydrogen_owner: Role,
  energy_owner: Role,
  regulator: Role,
  embodied_co2: Literal,
}

token RevokedCert {
  hydrogen_owner: Role,
  energy_owner: Role,
  regulator: Role,
  reason: File,
}

/*
 * ---------------------
 * Function Declarations
 * ---------------------
 *
 * Note that `fn`s define process flow restrictions and consist of a set of
 * inputs, a set of outputs and a set of additional conditions.
 * public `fn` will be published as a process flow (`fn`s can also be private)
 */

pub fn initiate_cert || => |output: InitiatedCert| where {
  output.hydrogen_owner == sender,
  output.energy_owner != sender,
  output.regulator != sender,
}

pub fn issue_cert |input: InitiatedCert| => |output: IssuedCert| where {
  output == input,
  input.hydrogen_owner == output.hydrogen_owner,
  input.energy_owner == output.energy_owner,
  input.regulator == output.regulator,
  input.energy_owner != output.regulator,
  output.hydrogen_owner != sender,
  output.regulator != sender,
  output.energy_owner == sender,
}

pub fn revoke_cert |input: IssuedCert| => |output: RevokedCert| where {
  output == input,
  input.hydrogen_owner == output.hydrogen_owner,
  input.energy_owner == output.energy_owner,
  input.regulator == output.regulator,
  output.energy_owner != sender,
  output.hydrogen_owner != sender,
  output.regulator == sender,
  output.reason: File
}