From 5daf532e6c374ea54e8578c6ecceeeac97633dd3 Mon Sep 17 00:00:00 2001 From: Dimitris Sarlis Date: Wed, 12 Jun 2024 12:14:26 +0000 Subject: [PATCH 1/6] feat: Allow using some of the cycles APIs in replicated queries --- spec/index.md | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/spec/index.md b/spec/index.md index 1a9afcc9..dc84f8fc 100644 --- a/spec/index.md +++ b/spec/index.md @@ -1339,15 +1339,15 @@ The following sections describe various System API functions, also referred to a ic0.msg_reply : () -> (); // U RQ NRQ CQ Ry Rt CRy CRt ic0.msg_reject : (src : i32, size : i32) -> (); // U RQ NRQ CQ Ry Rt CRy CRt - ic0.msg_cycles_available : () -> i64; // U Rt Ry - ic0.msg_cycles_available128 : (dst : i32) -> (); // U Rt Ry + ic0.msg_cycles_available : () -> i64; // U RQ Rt Ry + ic0.msg_cycles_available128 : (dst : i32) -> (); // U RQ Rt Ry ic0.msg_cycles_refunded : () -> i64; // Rt Ry ic0.msg_cycles_refunded128 : (dst : i32) -> (); // Rt Ry - ic0.msg_cycles_accept : (max_amount : i64) -> (amount : i64); // U Rt Ry + ic0.msg_cycles_accept : (max_amount : i64) -> (amount : i64); // U RQ Rt Ry ic0.msg_cycles_accept128 : (max_amount_high : i64, max_amount_low: i64, dst : i32) - -> (); // U Rt Ry + -> (); // U RQ Rt Ry - ic0.cycles_burn128 : (amount_high : i64, amount_low : i64, dst : i32) -> (); // I G U Ry Rt C T + ic0.cycles_burn128 : (amount_high : i64, amount_low : i64, dst : i32) -> (); // I G U RQ Ry Rt C T ic0.canister_self_size : () -> i32; // * ic0.canister_self_copy : (dst : i32, offset : i32, size : i32) -> (); // * @@ -2823,6 +2823,7 @@ The [WebAssembly System API](#system-api) is relatively low-level, and some of i } QueryFunc = WasmState -> Trap { cycles_used : Nat; } | Return { response : Response; + cycles_accepted : Nat; cycles_used : Nat; } CompositeQueryFunc = WasmState -> Trap { cycles_used : Nat; } | Return { @@ -3689,7 +3690,7 @@ Available = S.call_contexts[M.call_contexts].available_cycles ) or ( M.entry_point = PublicMethod Name Caller Arg - F = query_as_update(Mod.query_methods[Name], Arg, Caller, Env) + F = query_as_update(Mod.query_methods[Name], Arg, Caller, Env, Available) New_canister_version = S.canister_version[M.receiver] ) or @@ -6242,16 +6243,18 @@ Finally we can specify the abstract `CanisterModule` that models a concrete WebA - The partial map `query_methods` of the `CanisterModule` is defined for all method names `method` for which the WebAssembly program exports a function `func` named `canister_query `, and has value - query_methods[method] = λ (arg, caller, sysenv) → λ wasm_state → + query_methods[method] = λ (arg, caller, sysenv, available) → λ wasm_state → let es = ref {empty_execution_state with wasm_state = wasm_state; params = empty_params with { arg = arg; caller = caller; sysenv } balance = sysenv.balance + cycles_available = available; context = Q } try func() with Trap then Trap {cycles_used = es.cycles_used;} Return { response = es.response; + cycles_accepted = es.cycles_accepted; cycles_used = es.cycles_used; } @@ -6533,12 +6536,12 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im es.cycles_available := 0 ic0.msg_cycles_available() : i64 = - if es.context ∉ {U, Rt, Ry} then Trap {cycles_used = es.cycles_used;} + if es.context ∉ {U, RQ, Rt, Ry} then Trap {cycles_used = es.cycles_used;} if es.cycles_available >= 2^64 then Trap {cycles_used = es.cycles_used;} return es.cycles_available ic0.msg_cycles_available128(dst : i32) = - if es.context ∉ {U, Rt, Ry} then Trap {cycles_used = es.cycles_used;} + if es.context ∉ {U, RQ, Rt, Ry} then Trap {cycles_used = es.cycles_used;} let amount = es.cycles_available copy_cycles_to_canister(dst, amount.to_little_endian_bytes()) @@ -6553,7 +6556,7 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im copy_cycles_to_canister(dst, amount.to_little_endian_bytes()) ic0.msg_cycles_accept(max_amount : i64) : i64 = - if es.context ∉ {U, Rt, Ry} then Trap {cycles_used = es.cycles_used;} + if es.context ∉ {U, RQ, Rt, Ry} then Trap {cycles_used = es.cycles_used;} let amount = min(max_amount, es.cycles_available) es.cycles_available := es.cycles_available - amount es.cycles_accepted := es.cycles_accepted + amount @@ -6561,7 +6564,7 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im return amount ic0.msg_cycles_accept128(max_amount_high : i64, max_amount_low : i64, dst : i32) = - if es.context ∉ {U, Rt, Ry} then Trap {cycles_used = es.cycles_used;} + if es.context ∉ {U, RQ, Rt, Ry} then Trap {cycles_used = es.cycles_used;} 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 @@ -6570,7 +6573,7 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im copy_cycles_to_canister(dst, amount.to_little_endian_bytes()) ic0.cycles_burn128(amount_high : i64, amount_low : i64, dst : i32) = - if es.context ∉ {I, G, U, Ry, Rt, C, T} then Trap {cycles_used = es.cycles_used;} + if es.context ∉ {I, G, U, RQ, Ry, Rt, C, T} then Trap {cycles_used = es.cycles_used;} let amount = amount_high * 2^64 + amount_low let burned_amount = min( amount, From 0b0510d1737de2484e6a56a9e602ebb0695363ee Mon Sep 17 00:00:00 2001 From: Dimitris Sarlis Date: Wed, 12 Jun 2024 13:02:10 +0000 Subject: [PATCH 2/6] Review comments --- spec/index.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/spec/index.md b/spec/index.md index dc84f8fc..9122efe5 100644 --- a/spec/index.md +++ b/spec/index.md @@ -3690,7 +3690,8 @@ Available = S.call_contexts[M.call_contexts].available_cycles ) or ( M.entry_point = PublicMethod Name Caller Arg - F = query_as_update(Mod.query_methods[Name], Arg, Caller, Env, Available) + F = query_as_update(f, arg, caller, env, available) = λ wasm_state → + match f(arg, caller, env, available)(wasm_state) with New_canister_version = S.canister_version[M.receiver] ) or @@ -3839,7 +3840,7 @@ The functions `query_as_update` and `system_task_as_update` turns a query functi new_certified_data = NoCertifiedData; new_global_timer = NoGlobalTimer; response = res.response; - cycles_accepted = 0; + cycles_accepted = res.cycles_accepted; cycles_used = res.cycles_used; } From a7fc2fdd9f339c62dea1292a2eb9e6feba8e5f5d Mon Sep 17 00:00:00 2001 From: Dimitris Sarlis Date: Wed, 12 Jun 2024 14:05:45 +0000 Subject: [PATCH 3/6] Update --- spec/index.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/spec/index.md b/spec/index.md index 9122efe5..5da7e7e6 100644 --- a/spec/index.md +++ b/spec/index.md @@ -3690,8 +3690,7 @@ Available = S.call_contexts[M.call_contexts].available_cycles ) or ( M.entry_point = PublicMethod Name Caller Arg - F = query_as_update(f, arg, caller, env, available) = λ wasm_state → - match f(arg, caller, env, available)(wasm_state) with + F = query_as_update(Mod.query_methods[Name], Arg, Caller, Env, Available) New_canister_version = S.canister_version[M.receiver] ) or @@ -3831,8 +3830,8 @@ The function `validate_sender_canister_version` checks that `sender_canister_ver The functions `query_as_update` and `system_task_as_update` turns a query function (note that composite query methods cannot be called when executing a message during this transition) resp the heartbeat or global timer into an update function; this is merely a notational trick to simplify the rule: - query_as_update(f, arg, env) = λ wasm_state → - match f(arg, env)(wasm_state) with + query_as_update(f, arg, caller, env, available) = λ wasm_state → + match f(arg, caller, env, available)(wasm_state) with Trap trap → Trap trap Return res → Return { new_state = wasm_state; From 431fc33b61c278f5e8f687305135f6811488568d Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Sun, 23 Jun 2024 21:33:33 +0200 Subject: [PATCH 4/6] indent --- spec/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/index.md b/spec/index.md index 5fba0dc5..356121ab 100644 --- a/spec/index.md +++ b/spec/index.md @@ -3009,7 +3009,7 @@ The [WebAssembly System API](#system-api) is relatively low-level, and some of i status : Accept | Reject; } } - ``` + ``` This high-level interface presents a pure, mathematical model of a canister, and hides the bookkeeping required to provide the System API as seen in Section [Canister interface (System API)](#system-api). From abb77134bdde00c5c1eff62c6bae58842c9c95a0 Mon Sep 17 00:00:00 2001 From: Dimitris Sarlis Date: Mon, 15 Jul 2024 14:31:34 +0000 Subject: [PATCH 5/6] Adjust canister version section --- spec/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/index.md b/spec/index.md index 356121ab..26be4d17 100644 --- a/spec/index.md +++ b/spec/index.md @@ -1618,7 +1618,7 @@ This function allows a canister to find out if it is running, stopping or stoppe ### Canister version

-For each canister, the system maintains a *canister version*. Upon canister creation, it is set to 0, and it is **guaranteed** to be incremented upon every change of the canister's code, settings, running status (Running, Stopping, Stopped), and memory (WASM and stable memory), i.e., upon every successful management canister call of methods `update_settings`, `install_code`, `install_chunked_code`, `uninstall_code`, `start_canister`, and `stop_canister` on that canister, code uninstallation due to that canister running out of cycles, canister's running status transitioning from Stopping to Stopped, and successful execution of update methods, response callbacks, heartbeats, and global timers. The system can arbitrarily increment the canister version also if the canister's code, settings, running status, and memory do not change. +For each canister, the system maintains a *canister version*. Upon canister creation, it is set to 0, and it is **guaranteed** to be incremented upon every change of the canister's code, settings, running status (Running, Stopping, Stopped), and memory (WASM and stable memory), i.e., upon every successful management canister call of methods `update_settings`, `install_code`, `install_chunked_code`, `uninstall_code`, `start_canister`, and `stop_canister` on that canister, code uninstallation due to that canister running out of cycles, canister's running status transitioning from Stopping to Stopped, and successful execution of update methods, response callbacks, heartbeats, global timers and replicated query methods. The system can arbitrarily increment the canister version also if the canister's code, settings, running status, and memory do not change. - `ic0.canister_version : () → i64` From 0ed16014cd894121f338976dc1efa82acef0039c Mon Sep 17 00:00:00 2001 From: Dimitris Sarlis Date: Tue, 16 Jul 2024 11:13:33 +0200 Subject: [PATCH 6/6] Update spec/index.md Co-authored-by: mraszyk <31483726+mraszyk@users.noreply.github.com> --- spec/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/index.md b/spec/index.md index 26be4d17..6c218903 100644 --- a/spec/index.md +++ b/spec/index.md @@ -1618,7 +1618,7 @@ This function allows a canister to find out if it is running, stopping or stoppe ### Canister version

-For each canister, the system maintains a *canister version*. Upon canister creation, it is set to 0, and it is **guaranteed** to be incremented upon every change of the canister's code, settings, running status (Running, Stopping, Stopped), and memory (WASM and stable memory), i.e., upon every successful management canister call of methods `update_settings`, `install_code`, `install_chunked_code`, `uninstall_code`, `start_canister`, and `stop_canister` on that canister, code uninstallation due to that canister running out of cycles, canister's running status transitioning from Stopping to Stopped, and successful execution of update methods, response callbacks, heartbeats, global timers and replicated query methods. The system can arbitrarily increment the canister version also if the canister's code, settings, running status, and memory do not change. +For each canister, the system maintains a *canister version*. Upon canister creation, it is set to 0, and it is **guaranteed** to be incremented upon every change of the canister's code, settings, running status (Running, Stopping, Stopped), cycles balance, and memory (WASM and stable memory), i.e., upon every successful management canister call of methods `update_settings`, `install_code`, `install_chunked_code`, `uninstall_code`, `start_canister`, and `stop_canister` on that canister, code uninstallation due to that canister running out of cycles, canister's running status transitioning from Stopping to Stopped, and successful execution of update methods, replicated query methods, response callbacks, heartbeats, and global timers. The system can arbitrarily increment the canister version also if the canister's code, settings, running status, and memory do not change. - `ic0.canister_version : () → i64`