The Internet Computer Interface Specification

type Principal = Blob

mk_self_authenticating_id : PublicKey -> Principal
mk_self_authenticating_id pk = H(pk) · 0x02

mk_derived_id : Principal -> Blob -> Principal
mk_derived_id p nonce = H(|p| · p · nonce) · 0x03

anonymous_id : Principal
anonymous_id = 0x04

ic_principal : Principal = ""

MethodName = Text

parse_wasm_mod : Blob -> CanisterModule

CallCtxt = {
  canister : CanisterId;
  origin : CallOrigin;
  needs_to_respond : bool;
  deleted : bool;
  available_cycles : Nat;
}
CallId = (abstract)
CallOrigin
  = FromUser {
      request : Request;
    }
  | FromCanister {
      calling_context : CallId;
      callback: Callback
    }
  | FromHeartbeat

Queue = Unordered | Queue { from : System | CanisterId; to : CanisterId }
EntryPoint
  = PublicMethod MethodName Principal Blob
  | Callback Callback Response RefundedCycles
  | Heartbeat

Message
  = CallMessage {
      origin : CallOrigin;
      caller : Principal;
      callee : CanisterId;
      method_name : Text;
      data : Blob;
      transferred_cycles : Nat;
      queue : Queue;
    }
  | FuncMessage {
      call_context : CallId;
      receiver : CanisterId;
      entry_point : EntryPoint;
      queue : Queue;
    }
  | ResponseMessage {
      origin : CallOrigin;
      response : Response;
      refunded_cycles : Nat;
    }

Envelope = {
  content : Request | APIReadRequest;
  sender_pubkey : PublicKey | NoPublicKey;
  sender_sig : Signature | NoSignature;
  sender_delegation: [SignedDelegation]
}

Request
  = CanisterUpdateCall = {
    nonce : Blob;
    ingress_expiry : Nat;
    sender : UserId;
    canister_id : CanisterId;
    method_name : Text;
    data : Blob;
  }

RequestStatus
  = Received
  | Processing
  | Rejected (RejectCode, Text)
  | Replied Blob
  | Done

Path = List(Blob)
APIReadRequest
  = StateRead = {
    nonce : Blob;
    ingress_expiry : Nat;
    sender : UserId;
    paths : List(Path);
  }
  | CanisterQuery = {
    nonce : Blob;
    ingress_expiry : Nat;
    sender : UserId;
    canister_id : CanisterId;
    method_name : Text;
    data : Blob;
  }

Request = Blob
hash_of_map: Request -> Request

PublicKey = Blob
Signature = Blob
verify_signature : PublicKey -> Signature -> Blob -> Bool

SignedDelegation = {
  delegation : {
    pubkey : PublicKey;
    targets : [CanisterId] | Unrestricted;
    senders : [Principal] | Unrestricted;
    expiration : Timestamp
  };
  signature : Signature
}

S = {
  requests : Request ↦ RequestStatus;
  canisters : CanisterId ↦ CanState;
  controllers : CanisterId ↦ Set Principal;
  freezing_threshold : CanisterId ↦ Nat;
  canister_status: CanisterId ↦ CanStatus;
  time : CanisterId ↦ Timestamp;
  balances: CanisterId ↦ Nat;
  certified_data: CanisterId ↦ Blob;
  system_time : Timestamp
  call_contexts : CallId ↦ CallCtxt;
  messages : List Message; // ordered!
  root_key : PublicKey
}
CanState
 = EmptyCanister | {
  wasm_state : WasmState;
  module : CanisterModule;
  raw_module : Blob;
  public_custom_sections: Text ↦ Blob;
  private_custom_sections: Text ↦ Blob;
}
CanStatus
  = Running
  | Stopping (List (CallOrigin, Nat))
  | Stopped

{
  requests = ();
  canisters = ();
  controllers = ();
  freezing_threshold = ();
  time = ();
  balances = ();
  system_time = T;
  call_contexts = ();
  messages = ();
  root_key = PublicKey;
}

verify_envelope({ content = C }, U, T)
  = { p : p is CanisterID } if U = anonymous_id
verify_envelope({ content = C, sender_pubkey = PK, sender_sig = Sig, sender_delegation = DS}, U, T)
  = TS if U = mk_self_authenticating_id E.sender_pubkey
  ∧ (PK', TS) = verify_delegations(DS, PK, T, { p : p is CanisterId }, U)
  ∧ verify_signature PK' Sig ("\x0Aic-request" · hash_of_map(C))

verify_delegations([], PK, T, TS, U) = (PK, TS)
verify_delegations([D] · DS, PK, T, TS, U)
  = verify_delegations(DS, D.pubkey, T, TS ∩ delegation_targets(D), U)
  if verify_signature PK D.signature ("\x1Aic-request-auth-delegation" · hash_of_map(D.delegation))
   ∧ D.delegation.expiration ≥ T
   ∧ U ∈ delegated_senders(D)

delegation_targets(D)
  = if D.targets = Unrestricted
    then { p : p is CanisterId }
    else D.targets

delegated_senders(D)
  = if D.senders = Unrestricted
    then { p : p is Principal }
    else D.senders

is_effective_canister_id(CanisterUpdateCall {canister_id = ic_principal, arg = candid({canister_id = p, …}), …}, p)
is_effective_canister_id(CanisterUpdateCall {canister_id = ic_principal, method = provisional_create_canister_with_cycles, p)
is_effective_canister_id(CanisterUpdateCall {canister_id = p, …}, p), if p ≠ ic_principal

    E.content.canister_id ∈ verify_envelope(E, E.content.sender, S.system_time)
    E.content ∉ requests
    S.system_time <= E.content.ingress_expiry
    is_effective_canister_id(E.content, ECID)
    ( E.content.canister_id = ic_principal
      E.content.arg = candid({canister_id = CanisterId, …})
      E.content.sender ∈ S.controllers[CanisterId]
      E.content.method_name ∈
        { "install_code", "set_controller", "start_canister", "stop_canister",
          "canister_status", "delete_canister" }
    ) ∨ (
      E.content.canister_id ≠ ic_principal
      S.canisters[E.content.canister_id] ≠ EmptyCanister
      Arg = { data = E.content.arg; caller = E.content.sender; method = E.content.method_name; time = S.time[E.content.canister_id] }
      S.canisters[E.content.canister_id].module.inspect_message
        (E.content.method_name, C.wasm_state, Arg, S.balance[E.content.canister_id]) = Return Accept
   )

S with
    requests[E.content] = Received

    S.requests[R] = Received
    Code = SYS_FATAL or Code = SYS_TRANSIENT

S with
    requests[R] = Rejected (Code, Msg)

    S.requests[CanisterUpdateCall R] = Received
    S.system_time <= R.ingress_expiry
    C = S.canisters[R.canister_id]

S with
    requests[CanisterUpdateCall R] = Processing
    messages =
      CallMessage {
        origin = FromUser { request = CanisterUpdateCall R };
        caller = R.sender;
        callee = R.canister_id;
        method_name = R.method_name;
        arg = R.arg;
        transferred_cycles = 0;
        queue = Unordered;
      } · S.messages

    S.messages = Older_messages · CallMessage CM · Younger_messages
    (CM.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ CM.queue)
    S.canister_status[CM.callee] = Stopped or S.canister_status[CM.callee] = Stopping or balances[CM.callee] < freezing_limit(S, CM.callee)

    S.messages = Older_messages · Younger_messages  ·
      ResponseMessage {
          origin = S.call_contexts[CM.call_context].origin
          response = Reject (CANISTER_ERROR, "canister not running");
          refunded_cycles = CM.transferred_cycles;
      }

    S.messages = Older_messages · FuncMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    S.canisters[M.receiver] ≠ EmptyCanister
    Mod = S.canisters[M.receiver].module

    Is_response = M.entry_point == Callback _ _

    Env = {
      time = S.time[M.receiver];
      balance = S.balances[M.receiver]
      freezing_limit = freezing_limit(S, M.receiver);
      certificate = NoCertificate;
      status = S.status[M.receiver];
    }

    Available = S.call_contexts[M.call_contexts].available_cycles
    ( M.entry_point = PublicMethod Name Caller Data
      Arg = { data = Data; caller = Caller }
      (F = M.update_methods[M.method_name](Arg, Env, Available)
      or
      (F = as_update(Mod.query_methods[M.method_name], Arg, Env))
    )
    or
    ( M.entry_point = Callback Callback Response
      F = Mod.callbacks(Callback, Response, Env, Available)
    )
    or
    ( M.entry_point = Heartbeat
      F = Mod.heartbeat(Env)
    )

    R = F(S.canisters[M.receiver].wasm_state)

if
  R = Return res
  Cycles_used ≤ (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE)
  res.cycles_accepted ≤ Available
  New_balance =
      S.balances[M.receiver]
      + res.cycles_accepted
      + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE)
      - Cycles_used
      - ∑ [ MAX_CYCLES_PER_RESPONSE + call.transferred_cycles | call ∈ res.new_calls ]
  New_balance > if Is_response then 0 else freezing_limit(S, CM.callee);
  (res.response = NoResponse) or S.call_contexts[M.call_context].needs_to_respond
then
  S with
    canisters[M.receiver].wasm_state = res.new_state;
    messages =
      Older_messages ·
      Younger_messages ·
      [ CallMessage {
          origin = FromCanister {
            call_context = M.call_context;
            callback = call.callback
          };
          caller = C.callee;
          callee = call.callee;
          method_name = call.method_name;
          arg = call.arg;
          transferred_cycles = call.transferred_cycles
          queue = Queue { from = M.receiver; to = call.callee };
        }
      | call ∈ res.new_calls ] ·
      [ ResponseMessage {
          origin = S.call_contexts[M.call_context].origin
          response = res.response;
          refunded_cycles = Available - res.cycles_accepted;
        }
      | res.response ≠ NoResponse ]

    if res.response = NoResponse:
       call_contexts[M.call_context].available_cycles = Available - res.cycles_accepted
    else
       call_contexts[M.call_context].needs_to_respond = false
       call_contexts[M.call_context].available_cycles = 0

    if res.new_certified_data ≠ NoCertifiedData:
      certified_data[M.receiver] = res.new_certified_data

    balances[M.receiver] = New_balance
else
  S with
    messages = Older_messages · Younger_messages
    balances[M.receiver] =
      S.balances[M.receiver]
      + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE)
      - Cycles_used

as_update(f, arg, env) = λ wasm_state →
  match f(arg, env)(wasm_state) with
    Trap → Trap
    Return res → Return {
      new_state = wasm_state;
      new_calls = [];
      response = res;
      cycles_accepted = 0;
      new_certified_data = NoCertifiedData;
    }

    S.call_contexts[Ctxt_id].needs_to_respond = true
    S.call_contexts[Ctxt_id].origin ≠ FromHeartbeat
    ∀ CallMessage M ∈ S.messages. M.origin.calling_context ≠ Ctxt_id
    ∀ ResponseMessage M ∈ S.messages. M.origin.calling_context ≠ Ctxt_id
    ∀ ctxt_ids.
        S.call_contexts[ctxt_ids].needs_to_respond
        ==> S.call_contexts[ctxt_ids].origin.calling_context ≠ Ctxt_id

S with
    call_contexts[Ctxt_id].needs_to_respond = false
    call_contexts[Ctxt_id].available_cycles = 0
    messages =
      S.messages ·
      ResponseMessage {
        origin = S.call_contexts[Ctxt_id].origin;
        response = Reject (CANISTER_ERROR, "starvation");
        refunded_cycles = S.call_contexts[Ctxt_id].available_cycles
      }

    (
      S.call_contexts[Ctxt_id].needs_to_respond = false
    ) or
    (
      S.call_contexts[Ctxt_id].origin = FromHeartbeat
      ∀ FuncMessage M ∈ S.messages. M.call_context ≠ Ctxt_id
    )
    ∀ CallMessage M ∈ S.messages. M.origin.calling_context ≠ Ctxt_id
    ∀ ResponseMessage M ∈ S.messages. M.origin.calling_context ≠ Ctxt_id
    ∀ ctxt_ids.
        S.call_contexts[ctxt_ids].needs_to_respond = true
        ==> S.call_contexts[ctxt_ids].origin.calling_context ≠ Ctxt_id

S with
    call_contexts[Ctxt_id] = (deleted)

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'create_canister'
    M.arg = candid()
    is_system_assigned CanisterId
    CanisterId ∉ dom S.canisters

S with
    canisters[CanisterId] = EmptyCanister
    time[CanisterId] = CurrentTime
    if A.settings.controllers is not null:
      controllers[CanisterId] = A.settings.controllers
    else:
      controllers[CanisterId] = [M.caller]
    balances[CanisterId] = M.transferred_cycles
    certified_data[CanisterId] = ""
    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = Accepted (candid({canister_id = CanisterId}))
        refunded_cycles = 0
      }
    canister_status[CanisterId] = Running

is_system_assigned : Principal -> Bool

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'update_settings'
    M.arg = candid(A)
    M.caller ∈ S.controllers[A.canister_id]

S with
    if A.settings.controllers is not null:
      controllers[A.canister_id] = A.settings.controllers
    if A.settings.freezing_threshold exists:
      freezing_threshold[A.canister_id] = A.settings.freezing_threshold
    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = Accepted (candid())
        refunded_cycles = M.transferred_cycles
      }

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'canister_status'
    M.arg = candid(A)
    M.caller ∈ S.controllers[A.canister_id]

S with
    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = candid({
          status = S.canister_status[A.canister_id];
          module_hash =
            if S.canisters[A.canister_id] = EmptyCanister
            then null
            else opt (SHA-265(S.canisters[A.canister_id].raw_module));
          controllers = S.controllers[A.canister_id];
          memory_size = Memory_size;
          cycles = S.balance[A.canister_id];
        })
        refunded_cycles = M.transferred_cycles
      }

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'install_code'
    M.arg = candid(A)
    Mod = parse_wasm_mod(A.wasm_module)
      (A.mode = install && S.canisters[A.canister_id] = EmptyCanister)
    or A.mode = reinstall
    M.caller ∈ S.controllers[A.canister_id]
    Arg = {
      data = A.arg;
      caller = M.caller;
    }
    Env = {
      time = S.time[M.receiver];
      balance = S.balances[M.receiver];
      freezing_limit = freezing_limit(S, M.receiver);
      certificate = NoCertificate;
      status = S.status[M.receiver];
    }
    Mod.init(A.canister_id, Arg, Env) = Return New_state

S with
    canisters[A.canister_id] =
      { wasm_state = New_state; module = Mod; raw_module = A.wasm_module }
    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = Accepted (candid())
        refunded_cycles = M.transferred_cycles
      }

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'install_code'
    M.arg = candid(A)
    Mod = parse_wasm_mod(A.wasm_module)

    A.mode = upgrade
    S.canisters[A.canister_id] ≠ EmptyCanister
    M.caller ∈ S.controllers[A.canister_id]
    S.canisters[A.canister_id] = { wasm_state = Old_state; module = Old_module }
    Env = {
      time = S.time[M.receiver];
      balance = S.balances[M.receiver];
      freezing_limit = freezing_limit(S, M.receiver);
      certificate = NoCertificate;
      status = S.status[M.receiver];
    }
    Old_module.pre_upgrade(Old_State, M.caller, Env) = Return Stable_memory
    Arg = {
      data = A.arg;
      caller = M.caller;
    }
    Mod.post_upgrade(A.canister_id, Stable_memory, Arg, Env) = Return New_state

S with
    canisters[A.canister_id] =
      { wasm_state = New_state; module = Mod; raw_module = A.wasm_module }
    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = Accepted (candid())
        refunded_cycles = M.transferred_cycles
      }

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'uninstall_code'
    M.arg = candid(A)
    M.caller ∈ S.controllers[A.canister_id]

S with
    canisters[A.canister_id] = EmptyCanister
    certified_data[A.canister_id] = ""

    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = Accepted (candid())
        refunded_cycles = M.transferred_cycles
      } ·
      [ ResponseMessage {
          origin = Ctxt.origin
          response = Reject (CANISTER_REJECT, 'Canister has been uninstalled')
          refunded_cycles = Ctxt.available_cycles
        }
      | Ctxt_id ↦ Ctxt ∈ S.call_contexts
      , Ctxt.canister = A.canister_id
      , Ctxt.needs_to_respond = true
      ]

      for Ctxt_id ↦ Ctxt ∈ S.call_contexts:
        if Ctxt.canister = A.canister_id:
          call_contexts[Ctxt_id].deleted := true
          call_contexts[Ctxt_id].needs_to_respond := false
          call_contexts[Ctxt_id].available_cycles := 0

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'stop_canister'
    M.arg = candid(A)
    S.canister_status[A.canister_id] = Running
    M.caller ∈ S.controllers[A.canister_id]

S with
    messages = Older_messages · Younger_messages
    S.status[A.canister_id] = Stopping [(M.origin, M.transferred_cycles)]

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'stop_canister'
    M.arg = candid(A)
    S.canister_status[A.canister_id] = Stopping Origins
    M.caller ∈ S.controllers[A.canister_id]

S with
    messages = Older_messages · Younger_messages
    S.status[A.canister_id] = Stopping (Origins · (M.origin, M.transferred_cycles))

    S.canister_status[A.canister_id] = Stopping Origins
    ∀ Ctxt_id. S.call_contexts[Ctxt_id].canister ≠ A.canister_id

    S.canister_status[CanisterId] = Stopped
    S.messages = Messages ·
        [ ResponseMessage {
            origin = O
            response = Accepted (candid())
            refunded_cycles = C
          }
        | (O, C) ∈ Origins
        ]

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'stop_canister'
    M.arg = candid(A)
    S.canister_status[A.canister_id] = Stopped
    M.caller ∈ S.controllers[A.canister_id]

S with
    messages = Older_messages · Younger_messages
    S.messages = Messages ·
        ResponseMessage {
          origin = M.origin
          response = Accepted (candid())
        }

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'start_canister'
    M.arg = candid(A)
    S.status[A.canister_id] = Running or S.status[A.canister_id] = Stopped
    M.caller ∈ S.controllers[A.canister_id]

S with
    S.status[A.canister_id] = Running
    messages = Older_messages · Younger_messages ·
        ResponseMessage{
            origin = M.origin
            response = Accepted (candid())
            refunded_cycles = M.transferred_cycles
        }

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'start_canister'
    M.arg = candid(A)
    S.status[A.canister_id] = Stopping Origins
    M.caller ∈ S.controllers[A.canister_id]

S with
    S.status[A.canister_id] = Running
    messages = Older_messages · Younger_messages ·
        ResponseMessage{
            origin = M.origin
            response = Accepted (candid())
            refunded_cycles = M.transferred_cycles
        } ·
        [ ResponseMessage {
            origin = O
            response = Reject (CANISTER_REJECT, 'Canister has been restarted')
            refunded_cycles = C
          }
        | (O, C) ∈ Origins
        ]

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'delete_canister'
    M.arg = candid(A)
    S.canister_status[A.canister_id] = stopped
    M.caller ∈ S.controllers[A.canister_id]

S with
    canisters[CanisterId] = (deleted)
    controllers[CanisterId] = (deleted)
    canister_status[CanisterId] = (deleted)
    time[CanisterId] = (deleted)
    balances[CanisterId] = (deleted)
    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = Accepted (candid())
        refunded_cycles = M.transferred_cycles
      }

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'deposit_cycles'
    M.arg = candid(A)
    Cycle_cost ≤ S.balances[A.canister_id] + M.transferred_cycles

S with
    balances[CanisterId] =
      S.balances[A.canister_id] + M.transferred_cycles
    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = Accepted (candid())
        refunded_cycles = 0
      }

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'raw_rand'
    M.arg = candid()
    |B| = 32

S with
    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = Accepted (candid(B))
        refunded_cycles = M.transferred_cycles
      }

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'provisional_create_canister_with_cycles'
    M.arg = candid(A)
    is_system_assigned CanisterId
    CanisterId ∉ dom S.canisters

S with
    canisters[CanisterId] = EmptyCanister
    time[CanisterId] = CurrentTime
    controllers[CanisterId] = [M.caller]
    balances[CanisterId] = A.amount
    certified_data[CanisterId] = ""
    messages = Older_messages · Younger_messages ·
      ResponseMessage {
        origin = M.origin
        response = Accepted (candid({canister_id = CanisterId}))
        transferred_cycles = M.transferred_cycles
      }
    canister_status[CanisterId] = Running

    S.messages = Older_messages · CallMessage M · Younger_messages
    (M.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ M.queue)
    M.callee = ic_principal
    M.method_name = 'provisional_top_up_canister'
    M.arg = candid(A)
    A.canister_id ∈ dom S.canisters

S with
    balances[CanisterId] = balances[CanisterId] + A.amount

    S.messages = Older_messages · ResponseMessage RM · Younger_messages
    RM.origin = FromCanister {
        call_context = Ctxt_id
        callback = Callback
      }
    not S.call_contexts[Ctxt_id].deleted

S with
    balances[S.call_contexts[Ctxt_id].canister] =
      balances[S.call_contexts[Ctxt_id].canister] + RM.refunded_cycles
    messages =
      Older_messages ·
      FuncMessage {
        call_context = Ctxt_id2
        receiver = C
        entry_point = Callback Callback FM.response RM.refunded_cycles
        queue = Unordered
      } ·
      Younger_messages

    S.messages = Older_messages · ResponseMessage RM · Younger_messages
    RM.origin = FromCanister {
        call_context = Ctxt_id
        callback = Callback
      }
    S.call_contexts[Ctxt_id].deleted

S with
    balances[S.call_contexts[Ctxt_id].canister] =
      balances[S.call_contexts[Ctxt_id].canister] + RM.refunded_cycles + MAX_CYCLES_PER_RESPONSE
    messages = Older_messages · Younger_messages

    S.requests[M] = Processing
    S.messages = Older_messages · ResponseMessage RM · Younger_messages
    RM.origin = FromUser { request = M }

S with
    messages = Older_messages · Younger_messages
    requests[M] =
      | Replied R   if response = Reply R
      | Rejected R  if response = Reject R

    (S.requests[M] = Replied _) or (S.requests[M] = Rejected _)

S with
    requests[M] = Done

    (S.requests[M] = Replied _) or (S.requests[M] = Rejected _) or (S.requests[M] = Done)
    M.ingress_expiry < S.system_time

S with
    requests[M] = (deleted)

    S.balances[CanisterId] = 0

S with
    canisters[CanisterId] = EmptyCanister
    certified_data[A.canister_id] = ""

    messages = Older_messages · Younger_messages ·
      [ ResponseMessage {
          origin = Ctxt.origin
          response = Reject (CANISTER_REJECT, 'Canister has been uninstalled')
          refunded_cycles = Ctxt.available_cycles
        }
      | Ctxt_id ↦ Ctxt ∈ S.call_contexts
      , Ctxt.canister = A.canister_id
      , Ctxt.needs_to_respond = true
      ]

    for Ctxt_id ↦ Ctxt ∈ S.call_contexts:
      if Ctxt.canister = A.canister_id:
        call_contexts[Ctxt_id].deleted := true
        call_contexts[Ctxt_id].needs_to_respond := false
        call_contexts[Ctxt_id].available_cycles := 0

    T0 = S.time[CanisterId]
    T1 > T0

S with
    time[CanisterId] = T1

    B0 = S.balances[CanisterId]
    0 ≤ B1 < B0

S with
    balances[CanisterId] = B1

    T0 = S.system_time
    T1 > T0

S with
    system_time = T1

  E.content = CanisterQuery Q
  Q.canister_id ∈ verify_envelope(E, Q.sender, S.system_time)
  is_effective_canister_id(E.content, ECID)
  S.system_time <= Q.ingress_expiry
  S.canisters[Q.canister_id] ≠ EmptyCanister
  S.canister_status[Q.canister_id] = Running
  C = S.canisters[Q.canister_id]
  F = C.module.query_methods[Q.method_name]
  Arg = {
    data = Q.arg;
    caller = Q.sender;
  }
  verify_cert(Cert)
  lookup(["canister",Q.canister_id,"certified_data"], Cert) = Found S.certified_data[Q.canister_id]
  lookup(["time"], Cert) = Found S.system_time // or “recent enough”
  Env = {
    time = S.time[Q.receiver];
    balance = S.balances[Q.canister_id];
    freezing_limit = freezing_limit(S, Q.canister_id);
    certificate = Cert;
    status = S.status[Q.receiver];
  }

  E.content = ReadState RS
  TS = verify_envelope(E, RS.sender, S.system_time)
  S.system_time <= RS.ingress_expiry
  ∀ path ∈ RS.paths. may_read_path(S, R.sender, path)
  ∀ ["request_status", Rid] · _ ∈ RS.paths.  ∃ R ∈ S.requests ∧ hash_of_map(R) = Rid ∧ R.canister_id ∈ TS

may_read_path(S, _, ["time"]) = True
may_read_path(S, _, ["request_status", Rid] · _) =
  if ∃ R ∈ S.requests ∧ hash_of_map(R) = Rid
  then RS.sender == R.sender ∧ is_effective_canister_id(R, ECID)
  else True
may_read_path(S, _, ["canister", cid, "module_hash"]) = cid == ECID
may_read_path(S, _, ["canister", cid, "controllers"]) = cid == ECID
may_read_path(S, _, ["canister", cid, "metadata", name]) =
  if name ∈ S.canisters[cid].public_custom_sections
  then cid == ECID
  else if name ∈ S.canisters[cid].private_custom_sections
  then cid == ECID ∧ RS.sender ∈ S.controllers[cid]
  else False
may_read_path(S, _, _) = False

lookup(path, cert) = lookup_in_tree(path, state_tree(S))

state_tree(S) = {
  "time": S.system_time;
  "request_id": { request_id(R): request_status_tree(S) | (R ↦ S) ∈ S.requests };
  "canister":
    { canister_id :
        { "module_hash" : SHA256(C.raw_module) | if C ≠ EmptyCanister } ∪
        { "controllers" : CBOR(S.controllers[canister_id]) } ∪
        { "metadata": { name: blob | (name, blob) ∈ S.canisters[canister_id].public_custom_sections ∪ S.canisters[canister_id].private_custom_sections } }
    | (canister_id, C) ∈ S.canisters };
  "subnet": { subnet_id : { "public_key" : pub } | (subnet_id, subnet_pk) ∈ subnets };
}

request_status_tree(Received) =
  { "status": "received" }
request_status_tree(Processing) =
  { "status": "processing" }
request_status_tree(Rejected (code,msg)) =
  { "status": "rejected"; "reject_code": code; "reject_message": msg }
request_status_tree(Replied arg) =
  { "status": "replied"; "reply": arg }
request_status_tree(Done) =
  { "status": "Done" }

WasmState = {
  store : S; // a store as per WebAssembly spec
  self_id : CanId;
  stable_mem : Blob
}

Closure = {
    fun   : i32,
    env   : i32,
}

Callback = {
  on_reply : Closure;
  on_reject : Closure;
  on_cleanup : Closure | NoClosure;
}

Params = {
  data : NoData | Blob;
  caller : NoCaller | Principal;
  reject_code : 0 | SYS_FATAL | SYS_TRANSIENT | …;
  reject_message : Text;
  sysenv : Env;
  cycles_refundend : Nat;
  method_name : Text;
}
ExecutionState = {
  wasm_state : WasmState;
  params : Params;
  response : NoResponse | Response;
  cycles_accepted : Nat;
  cycles_available : Nat;
  balance : Funds;
  reply_params : { arg : Blob };
  pending_call : MethodCall | NoPendingCall;
  calls : List MethodCall;
  new_certified_data : NoCertifiedData | Blob;
  ingress_filter : Accept | Reject;
}

copy_to_canister<es>(dst : i32, offset : i32, size : i32, data : blob) =
  if offset+size > |data| then Trap
  if dst+size > |es.wasm_state.store.mem| then Trap
  es.wasm_state.store.mem[dst..dst+size] := data[offset..offset+size]

copy_from_canister<es>(src : i32, size : i32) blob =
  if src+size > |es.wasm_state.store.mem| then Trap
  return es.wasm_state.store.mem[src..src+size]

Cycles are represented by 128-bit values so they require 16 bytes of memory.

copy_cycles_to_canister<es>(dst : i32, data : blob) =
 let size = 16;
 if dst+size > |es.wasm_state.store.mem| then Trap
  es.wasm_state.store.mem[dst..dst+size] := data[0..size]

ic0.msg_arg_data_size<es>() : i32 =
  return |es.params.arg|

ic0.msg_arg_data_copy<es>(dst:i32, offset:i32, size:i32) =
  copy_to_canister<es>(dst, offset, size, es.param.arg)

ic0.msg_caller_size() : i32 =
  return |es.params.caller|

ic0.msg_caller_copy(dst:i32, offset:i32, size:i32) : i32 =
  copy_to_canister<es>(dst, offset, size, es.params.caller)

ic0.msg_reject_code<es>() : i32 =
  es.params.reject_code

ic0.msg_reject_msg_size<es>() : i32 =
  return |es.params.reject_msg|

ic0.msg_reject_msg_copy<es>(dst:i32, offset:i32, size:i32) : i32 =
  copy_to_canister<es>(dst, offset, size, es.params.reject_msg)

ic0.msg_reply_data_append<es>(src : i32, size : i32) =
  if es.response ≠ NoResponse then Trap
  es.reply_params.arg := es.reply_params.arg · copy_from_canister<es>(src, size)

ic0.msg_reply<es>() =
  if es.response ≠ NoResponse then Trap
  es.response := Reply (es.reply_params.arg)
  es.cycles_available := 0

ic0.msg_reject<es>(src : i32, size : i32) =
  if es.response ≠ NoResponse then Trap
  es.response := Reject (CANISTER_REJECT, copy_from_canister<es>(src, size))
  es.cycles_available := 0

ic0.msg_cycles_available<es>() : i64 =
  if es.cycles_available >= 2^64 then Trap
  return es.cycles_available

ic0.msg_cycles_available128<es>(dst : i32) =
  let amount = es.cycles_available
  copy_cycles_to_canister<es>(dst, amount.to_little_endian_bytes())

ic0.msg_cycles_refunded<es>() : i64 =
  if es.params.cycles_refunded >= 2^64 then Trap
  return es.params.cycles_refunded

ic0.msg_cycles_refunded128<es>(dst : i32) =
  let amount = es.params.cycles_refunded
  copy_cycles_to_canister<es>(dst, amount.to_little_endian_bytes())

ic0.accept_message<es>() =
  if es.ingress_filter = Accept then Trap
  es.ingress_filter = Accept

ic0.msg_method_name_size<es>() : i32 =
  return |es.method_name|

ic0.msg_method_name_copy<es>(dst : i32, offset : i32, size : i32) : i32 =
  copy_to_canister<es>(dst, offset, size, es.params.method_name)

ic0.msg_cycles_accept<es>(max_amount : i64) : i64 =
  let amount = min(max_amount, es.cycles_available)
  es.cycles_available := es.cycles_available - amount
  es.cycles_accepted := es.cycles_accepted + amount
  es.balance := es.balance + amount
  return amount

ic0.msg_cycles_accept128<es>(max_amount_high : i64, max_amount_low : i64, dst : i32) =
  let max_amount = max_amount_high * 2^64 + max_amount_low
  let amount = min(max_amount, es.cycles_available)
  es.cycles_available := es.cycles_available - amount
  es.cycles_accepted := es.cycles_accepted + amount
  es.balance := es.balance + amount
  copy_cycles_to_canister<es>(dst, amount.to_little_endian_bytes())

ic0.canister_self_size<es>() : i32 =
  return |es.wasm_state.self_id|

ic0.canister_self_copy<es>(dst:i32, offset:i32, size:i32) =
  copy_to_canister<es>(dst, offset, size, es.wasm_state.self_id)

ic0.canister_cycle_balance<es>() : i64 =
  if es.balance >= 2^64 then Trap
  return es.balance

ic0.canister_cycles_balance128<es>(dst : i32) =
  let amount = es.balance
  copy_cycles_to_canister<es>(dst, amount.to_little_endian_bytes())

ic0.canister_status<es>() : i32 =
  match es.params.sysenv.canister_status with
    Running  -> return 1
    Stopping -> return 2
    Stopped  -> return 3

ic0.call_new<es>(
    callee_src  : i32,
    callee_size : i32,
    name_src    : i32,
    name_size   : i32,
    reply_fun   : i32,
    reply_env   : i32,
    reject_fun  : i32,
    reject_env  : i32,
  ) =
  discard_pending_call<es>()

  if es.balance < MAX_CYCLES_PER_RESPONSE then Trap
  es.balance := es.balance - MAX_CYCLES_PER_RESPONSE

  callee := copy_from_canister<es>(callee_src, callee_size);
  method_name := copy_from_canister<es>(name_src, name_size);

  if reply_fun > |es.wasm_state.store.table| then Trap
  if typeof(es.wasm_state.store.table[reply_fun]) ≠ func (anyref, i32) -> () then Trap

  if reject_fun > |es.wasm_state.store.table| then Trap
  if typeof(es.wasm_state.store.table[reject_fun]) ≠ func (anyref, i32) -> () then Trap

  es.pending_call = MethodCall {
    callee = callee;
    method_name = callee;
    arg = "";
    transferred_cycles = 0;
    callback = Callback {
      on_reply = Closure { fun = reply_fun; env = reply_env }
      on_reject = Closure { fun = reject_fun; env = reject_env }
      on_cleanup = NoClosure
    };
  }

ic0.call_data_append<es> (src : i32, size : i32) =
  if es.pending_call = NoPendingCall then Trap
  es.pending_call.arg := es.pending_call.arg · copy_from_canister<es>(src, size)

ic0.call_on_cleanup<es> (fun : i32, env : i32) =
  if fun > |es.wasm_state.store.table| then Trap
  if typeof(es.wasm_state.store.table[fun]) ≠ func (anyref, i32) -> () then Trap
  if es.pending_call = NoPendingCall then Trap
  if es.pending_call.callback.on_cleanup ≠ NoClosure then Trap
  es.pending_call.callback.on_cleanup := Closure { fun = fun; env = env}

ic0.call_cycles_add<es>(amount : i64) =
  if es.pending_call = NoPendingCall then Trap
  if es.balance < amount then Trap

  es.balance := es.balance - amount
  es.pending_call.transferred_cycles := es.pending_call.transferred_cycles + amount

ic0.call_cycles_add128<es>(amount_high : i64, amount_low : i64) =
  let amount = amount_high * 2^64 + amount_low
  if es.pending_call = NoPendingCall then Trap
  if es.balance < amount then Trap

  es.balance := es.balance - amount
  es.pending_call.transferred_cycles := es.pending_call.transferred_cycles + amount

ic0.call_peform<es>() : ( err_code : i32 ) =
  if es.pending_call = NoPendingCall then Trap

  // are we below the threezing threshold?
  // Or maybe the system has other reasons to not perform this
  if es.balance < es.env.freezing_limit or system_cannot_do_this_call_now()
  then
    discard_pending_call<es>()
    return 1
  or
    es.calls := es.calls · es.pending_call
    es.pending_call := NoPendingCall
    return 0

// helper function
discard_pending_call<es>() =
  if es.pending_call ≠ NoPendingCall then
    es.balance := es.balance + MAX_CYCLES_PER_RESPONSE + es.pending_call.transferred_cycles
    es.pending_call := NoPendingCall

ic0.stable_size<es>() : (page_count : i32) =
  if |es.wasm_state.store.mem| > 2^32 then Trap
  page_count := |es.wasm_state.stable_mem| / 64k
  return page_count

ic0.stable_grow<es>(new_pages : i32) : (old_page_count : i32) =
  if |es.wasm_state.store.mem| > 2^32 then Trap
  if arbitrary() then return -1
  else
    old_size := |es.wasm_state.stable_mem| / 64k
    if old_size + new_pages > 2^16 then return -1
    es.wasm_state.stable_mem :=
      es.wasm_state.stable_mem · repeat(0x00, new_pages * 64k)
    return old_size

ic0.stable_write<es>(offset : i32, src : i32, size : i32)
  if |es.wasm_state.store.mem| > 2^32 then Trap
  if src+size > |es.wasm_state.store.mem| then Trap
  if offset+size > |es.wasm_state.stable_mem| then Trap

  es.wasm_state.stable_mem[offset..offset+size] := es.wasm_state.store.mem[src..src+size]

ic0.stable_read<es>(dst : i32, offset : i32, size : i32)
  if |es.wasm_state.store.mem| > 2^32 then Trap
  if offset+size > |es.wasm_state.stable_mem| then Trap
  if dst+size > |es.wasm_state.store.mem| then Trap

  es.wasm_state.store.mem[offset..offset+size] := es.wasm_state.stable.mem[src..src+size]

ic0.stable64_size<es>() : (page_count : i64) =
  return |es.wasm_state.stable_mem| / 64k

ic0.stable64_grow<es>(new_pages : i64) : (old_page_count : i64) =
  if arbitrary()
  then return -1
  else
    old_size := |es.wasm_state.stable_mem| / 64k
    es.wasm_state.stable_mem :=
      es.wasm_state.stable_mem · repeat(0x00, new_pages * 64k)
    return old_size

ic0.stable64_write<es>(offset : i64, src : i64, size : i64)
  if src+size > |es.wasm_state.store.mem| then Trap
  if offset+size > |es.wasm_state.stable_mem| then Trap

  es.wasm_state.stable_mem[offset..offset+size] := es.wasm_state.store.mem[src..src+size]

ic0.stable64_read<es>(dst : i64, offset : i64, size : i64)
  if offset+size > |es.wasm_state.stable_mem| then Trap
  if dst+size > |es.wasm_state.store.mem| then Trap

  es.wasm_state.store.mem[offset..offset+size] := es.wasm_state.stable.mem[src..src+size]

ic0.time<es>() : i32 =
  return es.params.time

ic0.certified_data_set<es>(src: i32, size: i32) =
  es.new_certified_data := es.wasm_state[src..src+size]

ic0.data_certificate_present<es>() : i32 =
  if es.params.sysenv.certificate = NoCertificate
  then return 0
  else return 1

ic0.data_certificate_size<es>() : i32 =
  if es.params.sysenv.certificate = NoCertificate then Trap
  return |es.params.sysenv.certificate|

ic0.data_certificate_copy<es>(dst: i32, offset: i32, size: i32) =
  if es.params.sysenv.certificate = NoCertificate then Trap
  copy_to_canister<es>(dst, offset, size, es.params.sysenv.certificate)

ic0.performance_counter<es>(type : i32) : i64 =
  arbitrary()

ic0.debug_print<es>(src : i32, size : i32) =
  return

ic0.trap<es>(src : i32, size : i32) =
  Trap