From ebe1b653d6cef346497e53273cfafaa780de5243 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Mon, 21 Aug 2023 09:57:28 +0200 Subject: [PATCH 01/13] redefine freezing_limit and idle_cycles_burned_rate --- spec/index.md | 274 +++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 224 insertions(+), 50 deletions(-) diff --git a/spec/index.md b/spec/index.md index 5ed81bd6e..7353a4864 100644 --- a/spec/index.md +++ b/spec/index.md @@ -2714,14 +2714,20 @@ Finally, we can describe the state of the IC as a record having the following fi total_num_changes : Nat; recent_changes : [Change]; } + Subnet = { + subnet_id : Principal; + subnet_size : Nat; + } S = { requests : Request ↦ (RequestStatus, Principal); canisters : CanisterId ↦ CanState; controllers : CanisterId ↦ Set Principal; + compute_allocation : CanisterId ↦ Nat; + memory_allocation : CanisterId ↦ Nat; freezing_threshold : CanisterId ↦ Nat; canister_status: CanisterId ↦ CanStatus; canister_version: CanisterId ↦ CanisterVersion; - canister_subnet : CanisterId ↦ Principal; + canister_subnet : CanisterId ↦ Subnet; time : CanisterId ↦ Timestamp; global_timer : CanisterId ↦ Timestamp; balances: CanisterId ↦ Nat; @@ -2761,6 +2767,8 @@ The initial state of the IC is requests = (); canisters = (); controllers = (); + compute_allocation = (); + memory_allocation = (); freezing_threshold = (); canister_status = (); canister_version = (); @@ -2875,9 +2883,11 @@ Requests that have expired are dropped here. Ingress message inspection is applied, and messages that are not accepted by the canister are dropped. -The (unspecified) function `idle_cycles_burned_rate(S, cid)` determines the idle resource consumption rate in cycles per day of the canister with id `cid`, given its current memory footprint, compute and storage cost, and memory and compute allocation. The function `freezing_limit(S, cid)` determines the freezing threshold in cycles of the canister with id `cid`, given its current memory footprint, compute and storage cost, memory and compute allocation, and current `freezing_threshold` setting. The value `freezing_limit(S, cid)` is derived from `idle_cycles_burned_rate(S, cid)` and `freezing_threshold` as follows: +The (unspecified) function `idle_cycles_burned_rate(compute_allocation, memory_allocation, memory_usage, subnet_size)` determines the idle resource consumption rate in cycles per day of a canister given its current compute and memory allocation, memory usage, and subnet size. The function `freezing_limit(compute_allocation, memory_allocation, freezing_threshold, memory_usage, subnet_size)` determines the freezing limit in cycles of a canister given its current compute and memory allocation, freezing threshold in seconds, memory usage, and subnet size. The value `freezing_limit(compute_allocation, memory_allocation, freezing_threshold, memory_usage, subnet_size)` is derived from `idle_cycles_burned_rate(compute_allocation, memory_allocation, memory_usage, subnet_size)` and `freezing_threshold` as follows: + + freezing_limit(compute_allocation, memory_allocation, freezing_threshold, memory_usage, subnet_size) = idle_cycles_burned_rate(compute_allocation, memory_allocation, memory_usage, subnet_size) * freezing_threshold / (24 * 60 * 60) - freezing_limit(S, cid) = idle_cycles_burned_rate(S, cid) * S.freezing_threshold[cid] / (24 * 60 * 60) +The (unspecified) function `memory_usage(wasm_state, raw_module, canister_history)` determines the canister's memory usage in bytes given its Wasm state, raw Wasm binary, and canister history. Submitted request `E : Envelope` @@ -2905,7 +2915,17 @@ is_effective_canister_id(E.content, ECID) controllers = S.controllers[E.content.canister_id]; global_timer = S.global_timer[E.content.canister_id]; balance = S.balances[E.content.canister_id] - freezing_limit = freezing_limit(S, E.content.canister_id); + freezing_limit = freezing_limit( + S.compute_allocation[E.content.canister_id], + S.memory_allocation[E.content.canister_id], + S.freezing_threshold[E.content.canister_id], + memory_usage( + S.canisters[E.content.canister_id].wasm_state, + S.canisters[E.content.canister_id].raw_module, + S.canister_history[E.content.canister_id] + ), + S.canister_subnet[E.content.canister_id].subnet_size, + ); certificate = NoCertificate; status = simple_status(S.canister_status[E.content.canister_id]); canister_version = S.canister_version[E.content.canister_id]; @@ -2999,7 +3019,17 @@ Conditions 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.canister_status[CM.callee] = Stopped or S.canister_status[CM.callee] = Stopping _ or balances[CM.callee] < freezing_limit( + S.compute_allocation[CM.callee], + S.memory_allocation[CM.callee], + S.freezing_threshold[CM.callee], + memory_usage( + S.canisters[CM.callee].wasm_state, + S.canisters[CM.callee].raw_module, + S.canister_history[CM.callee] + ), + S.canister_subnet[CM.callee].subnet_size, +) ``` @@ -3035,7 +3065,17 @@ Conditions S.messages = Older_messages · CallMessage CM · Younger_messages S.canisters[CM.callee] ≠ EmptyCanister S.canister_status[CM.callee] = Running -S.balances[CM.callee] ≥ freezing_limit(S, CM.callee) + MAX_CYCLES_PER_MESSAGE +S.balances[CM.callee] ≥ freezing_limit( + S.compute_allocation[CM.callee], + S.memory_allocation[CM.callee], + S.freezing_threshold[CM.callee], + memory_usage( + S.canisters[CM.callee].wasm_state, + S.canisters[CM.callee].raw_module, + S.canister_history[CM.callee] + ), + S.canister_subnet[CM.callee].subnet_size, +) + MAX_CYCLES_PER_MESSAGE Ctxt_id ∉ dom(S.call_contexts) ``` @@ -3075,7 +3115,17 @@ Conditions S.canisters[C] ≠ EmptyCanister S.canister_status[C] = Running -S.balances[C] ≥ freezing_limit(S, C) + MAX_CYCLES_PER_MESSAGE +S.balances[C] ≥ freezing_limit( + S.compute_allocation[C], + S.memory_allocation[C], + S.freezing_threshold[C], + memory_usage( + S.canisters[C].wasm_state, + S.canisters[C].raw_module, + S.canister_history[C] + ), + S.canister_subnet[C].subnet_size, +) + MAX_CYCLES_PER_MESSAGE Ctxt_id ∉ dom(S.call_contexts) ``` @@ -3116,7 +3166,17 @@ S.canisters[C] ≠ EmptyCanister S.canister_status[C] = Running S.global_timer[C] ≠ 0 S.time[C] ≥ S.global_timer[C] -S.balances[C] ≥ freezing_limit(S, C) + MAX_CYCLES_PER_MESSAGE +S.balances[C] ≥ freezing_limit( + S.compute_allocation[C], + S.memory_allocation[C], + S.freezing_threshold[C], + memory_usage( + S.canisters[C].wasm_state, + S.canisters[C].raw_module, + S.canister_history[C] + ), + S.canister_subnet[C].subnet_size, +) + MAX_CYCLES_PER_MESSAGE Ctxt_id ∉ dom(S.call_contexts) ``` @@ -3170,7 +3230,17 @@ Env = { controllers = S.controllers[M.receiver]; global_timer = S.global_timer[M.receiver]; balance = S.balances[M.receiver] - freezing_limit = freezing_limit(S, M.receiver); + freezing_limit = freezing_limit( + S.compute_allocation[M.receiver], + S.memory_allocation[M.receiver], + S.freezing_threshold[M.receiver], + memory_usage( + S.canisters[M.receiver].wasm_state, + S.canisters[M.receiver].raw_module, + S.canister_history[M.receiver] + ), + S.canister_subnet[M.receiver].subnet_size, + ); certificate = NoCertificate; status = simple_status(S.canister_status[M.receiver]); canister_version = S.canister_version[M.receiver]; @@ -3220,7 +3290,17 @@ if New_balance = (S.balances[M.receiver] + res.cycles_accepted + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE)) - (res.cycles_used + ∑ [ MAX_CYCLES_PER_RESPONSE + call.transferred_cycles | call ∈ res.new_calls ]) - New_balance ≥ if Is_response then 0 else freezing_limit(S, M.receiver); + New_balance ≥ if Is_response then 0 else freezing_limit( + S.compute_allocation[M.receiver], + S.memory_allocation[M.receiver], + S.freezing_threshold[M.receiver], + memory_usage( + res.new_state, + S.canisters[M.receiver].raw_module, + S.canister_history[M.receiver] + ), + S.canister_subnet[M.receiver].subnet_size, + ); (res.response = NoResponse) or S.call_contexts[M.call_context].needs_to_respond then S with @@ -3386,12 +3466,10 @@ S with #### IC Management Canister: Canister creation -The IC chooses an appropriate canister id (referred to as `CanisterId`) and subnet id (referred to as `SubnetId`, `SubnetId ∈ Subnets`, where `Subnets` is the under-specified set of subnet ids on the IC) and instantiates a new (empty) canister identified by `CanisterId` on the subnet identified by `SubnetId`. The *controllers* are set such that the sender of this request is the only controller, unless the `settings` say otherwise. All cycles on this call are now the canister's initial cycles. +The IC chooses an appropriate canister id (referred to as `CanisterId`) and subnet id (referred to as `SubnetId`, `SubnetId ∈ Subnets`, where `Subnets` is the under-specified set of subnet ids on the IC) and instantiates a new (empty) canister identified by `CanisterId` on the subnet identified by `SubnetId` with subnet size denoted by `SubnetSize`. The *controllers* are set such that the sender of this request is the only controller, unless the `settings` say otherwise. All cycles on this call are now the canister's initial cycles. This is also when the System Time of the new canister starts ticking. -The `compute_allocation` and `memory_allocation` settings are ignored in this abstract model of the Internet Computer, as it does not address questions of performance or scheduling. - Conditions ```html @@ -3420,6 +3498,14 @@ S with time[CanisterId] = CurrentTime global_timer[CanisterId] = 0 controllers[CanisterId] = New_controllers + if A.settings.compute_allocation is not null: + compute_allocation = A.settings.compute_allocation + else: + compute_allocation = 0 + if A.settings.memory_allocation is not null: + memory_allocation = A.settings.memory_allocation + else: + memory_allocation = 0 if A.settings.freezing_threshold is not null: freezing_threshold[CanisterId] = A.settings.freezing_threshold else: @@ -3445,7 +3531,10 @@ S with } canister_status[CanisterId] = Running canister_version[CanisterId] = 0 - canister_subnet[CanisterId] = SubnetId + canister_subnet[CanisterId] = Subnet { + subnet_id : SubnetId + subnet_size : SubnetSize + } ``` @@ -3469,8 +3558,6 @@ To avoid clashes with potential user ids or is derived from users or canisters, Only the controllers of the given canister can update the canister settings. -The `compute_allocation` and `memory_allocation` settings are ignored in this abstract model of the Internet Computer, as it does not address questions of performance or scheduling. - Conditions ```html @@ -3506,6 +3593,10 @@ S with }; }; } + if A.settings.compute_allocation is not null: + compute_allocation[A.canister_id] = A.settings.compute_allocation + if A.settings.memory_allocation is not null: + memory_allocation[A.canister_id] = A.settings.memory_allocation if A.settings.freezing_threshold is not null: freezing_threshold[A.canister_id] = A.settings.freezing_threshold canister_version[A.canister_id] = S.canister_version[A.canister_id] + 1 @@ -3557,7 +3648,16 @@ S with memory_size = Memory_size; cycles = S.balances[A.canister_id]; freezing_threshold = S.freezing_threshold[A.canister_id]; - idle_cycles_burned_per_day = idle_cycles_burned_rate(S, A.canister_id); + idle_cycles_burned_per_day = idle_cycles_burned_rate( + S.compute_allocation[A.canister_id], + S.memory_allocation[A.canister_id], + memory_usage( + S.canisters[A.canister_id].wasm_state, + S.canisters[A.canister_id].raw_module, + S.canister_history[A.canister_id] + ), + S.canister_subnet[A.canister_id].subnet_size, + ); }) refunded_cycles = M.transferred_cycles } @@ -3628,13 +3728,33 @@ Env = { controllers = S.controllers[A.canister_id]; global_timer = 0; balance = S.balances[A.canister_id]; - freezing_limit = freezing_limit(S, A.canister_id); + freezing_limit = freezing_limit( + S.compute_allocation[A.canister_id], + S.memory_allocation[A.canister_id], + S.freezing_threshold[A.canister_id], + memory_usage( + S.canisters[A.canister_id].wasm_state, + S.canisters[A.canister_id].raw_module, + S.canister_history[A.canister_id] + ), + S.canister_subnet[A.canister_id].subnet_size, + ); certificate = NoCertificate; status = simple_status(S.canister_status[A.canister_id]); canister_version = S.canister_version[A.canister_id] + 1; } Mod.init(A.canister_id, A.arg, M.caller, Env) = Return {new_state = New_state; new_certified_data = New_certified_data; new_global_timer = New_global_timer; cycles_used = Cycles_used;} -freezing_limit(S, A.canister_id) + Cycles_used ≤ S.balances[A.canister_id] +freezing_limit( + S.compute_allocation[A.canister_id], + S.memory_allocation[A.canister_id], + S.freezing_threshold[A.canister_id], + memory_usage( + New_state, + A.wasm_module, + New_canister_history + ), + S.canister_subnet[A.canister_id].subnet_size, +) + Cycles_used ≤ S.balances[A.canister_id] dom(Mod.update_methods) ∩ dom(Mod.query_methods) = ∅ dom(Mod.update_methods) ∩ dom(Mod.composite_query_methods) = ∅ dom(Mod.query_methods) ∩ dom(Mod.composite_query_methods) = ∅ @@ -3643,6 +3763,18 @@ S.canister_history[A.canister_id] = { total_num_changes = N; recent_changes = H; } +New_canister_history = { + total_num_changes = N + 1; + recent_changes = H · { + timestamp_nanos = S.time[A.canister_id]; + canister_version = S.canister_version[A.canister_id] + 1 + origin = change_origin(M.caller, A.sender_canister_version, M.origin); + details = CodeDeployment { + mode = A.mode; + module_hash = SHA-256(A.wasm_module); + }; + }; +} ``` @@ -3665,18 +3797,7 @@ S with global_timer[A.canister_id] = 0 canister_version[A.canister_id] = S.canister_version[A.canister_id] + 1 balances[A.canister_id] = S.balances[A.canister_id] - Cycles_used - canister_history[A.canister_id] = { - total_num_changes = N + 1; - recent_changes = H · { - timestamp_nanos = S.time[A.canister_id]; - canister_version = S.canister_version[A.canister_id] + 1 - origin = change_origin(M.caller, A.sender_canister_version, M.origin); - details = CodeDeployment { - mode = A.mode; - module_hash = SHA-256(A.wasm_module); - }; - }; - } + canister_history[A.canister_id] = New_canister_history messages = Older_messages · Younger_messages · ResponseMessage { origin = M.origin; @@ -3709,7 +3830,17 @@ Env = { time = S.time[A.canister_id]; controllers = S.controllers[A.canister_id]; balance = S.balances[A.canister_id]; - freezing_limit = freezing_limit(S, A.canister_id); + freezing_limit = freezing_limit( + S.compute_allocation[A.canister_id], + S.memory_allocation[A.canister_id], + S.freezing_threshold[A.canister_id], + memory_usage( + S.canisters[A.canister_id].wasm_state, + S.canisters[A.canister_id].raw_module, + S.canister_history[A.canister_id] + ), + S.canister_subnet[A.canister_id].subnet_size, + ); certificate = NoCertificate; status = simple_status(S.canister_status[A.canister_id]); } @@ -3723,7 +3854,17 @@ Env2 = Env with { canister_version = S.canister_version[A.canister_id] + 1; } Mod.post_upgrade(A.canister_id, Stable_memory, A.arg, M.caller, Env2) = Return {new_state = New_state; new_certified_data = New_certified_data'; new_global_timer = New_global_timer; cycles_used = Cycles_used';} -freezing_limit(S, A.canister_id) + Cycles_used + Cycles_used' ≤ S.balances[A.canister_id] +freezing_limit( + S.compute_allocation[A.canister_id], + S.memory_allocation[A.canister_id], + S.freezing_threshold[A.canister_id], + memory_usage( + New_state, + A.wasm_module, + New_canister_history + ), + S.canister_subnet[A.canister_id].subnet_size, +) + Cycles_used + Cycles_used' ≤ S.balances[A.canister_id] dom(Mod.update_methods) ∩ dom(Mod.query_methods) = ∅ dom(Mod.update_methods) ∩ dom(Mod.composite_query_methods) = ∅ dom(Mod.query_methods) ∩ dom(Mod.composite_query_methods) = ∅ @@ -3731,7 +3872,18 @@ S.canister_history[A.canister_id] = { total_num_changes = N; recent_changes = H; } - +New_canister_history = { + total_num_changes = N + 1; + recent_changes = H · { + timestamp_nanos = S.time[A.canister_id]; + canister_version = S.canister_version[A.canister_id] + 1 + origin = change_origin(M.caller, A.sender_canister_version, M.origin); + details = CodeDeployment { + mode = Upgrade; + module_hash = SHA-256(A.wasm_module); + }; + }; +} ``` State after @@ -3756,18 +3908,7 @@ S with global_timer[A.canister_id] = 0 canister_version[A.canister_id] = S.canister_version[A.canister_id] + 1 balances[A.canister_id] = S.balances[A.canister_id] - (Cycles_used + Cycles_used'); - canister_history[A.canister_id] = { - total_num_changes = N + 1; - recent_changes = H · { - timestamp_nanos = S.time[A.canister_id]; - canister_version = S.canister_version[A.canister_id] + 1 - origin = change_origin(M.caller, A.sender_canister_version, M.origin); - details = CodeDeployment { - mode = Upgrade; - module_hash = SHA-256(A.wasm_module); - }; - }; - } + canister_history[A.canister_id] = New_canister_history messages = Older_messages · Younger_messages · ResponseMessage { origin = M.origin; @@ -4059,6 +4200,8 @@ State after S with canisters[A.canister_id] = (deleted) controllers[A.canister_id] = (deleted) + compute_allocation[A.canister_id] = (deleted) + memory_allocation[A.canister_id] = (deleted) freezing_threshold[A.canister_id] = (deleted) canister_status[A.canister_id] = (deleted) canister_version[A.canister_id] = (deleted) @@ -4177,6 +4320,14 @@ S with time[canister_id] = CurrentTime global_timer[canister_id] = 0 controllers[canister_id] = New_controllers + if A.settings.compute_allocation is not null: + compute_allocation[canister_id] = A.settings.compute_allocation + else: + compute_allocation[canister_id] = 0 + if A.settings.memory_allocation is not null: + memory_allocation[canister_id] = A.settings.memory_allocation + else: + memory_allocation[canister_id] = 0 if A.settings.freezing_threshold is not null: freezing_threshold[canister_id] = A.settings.freezing_threshold else: @@ -4205,7 +4356,10 @@ S with } canister_status[canister_id] = Running canister_version[canister_id] = 0 - canister_subnet[canister_id] = SubnetId + canister_subnet[canister_id] = Subnet { + subnet_id : SubnetId + subnet_size : SubnetSize + } ``` @@ -4555,14 +4709,34 @@ We define an auxiliary method that handles calls from composite query methods by let Env = { time = S.time[Canister_id]; global_timer = S.global_timer[Canister_id]; balance = S.balances[Canister_id]; - freezing_limit = freezing_limit(S, Canister_id); + freezing_limit = freezing_limit( + S.compute_allocation[Canister_id], + S.memory_allocation[Canister_id], + S.freezing_threshold[Canister_id], + memory_usage( + S.canisters[Canister_id].wasm_state, + S.canisters[Canister_id].raw_module, + S.canister_history[Canister_id] + ), + S.canister_subnet[Canister_id].subnet_size, + ); certificate = Cert; status = simple_status(S.canister_status[Canister_id]); canister_version = S.canister_version[Canister_id]; } if S.canisters[Canister_id] ≠ EmptyCanister and S.canister_status[Canister_id] = Running and - S.balances[Canister_id] >= freezing_limit(S, Canister_id) and + S.balances[Canister_id] >= freezing_limit( + S.compute_allocation[Canister_id], + S.memory_allocation[Canister_id], + S.freezing_threshold[Canister_id], + memory_usage( + S.canisters[Canister_id].wasm_state, + S.canisters[Canister_id].raw_module, + S.canister_history[Canister_id] + ), + S.canister_subnet[Canister_id].subnet_size, + ) and (Method_name ∈ dom(Mod.query_methods) or Method_name ∈ dom(Mod.composite_query_methods)) and Cycles >= MAX_CYCLES_PER_MESSAGE then @@ -4587,7 +4761,7 @@ We define an auxiliary method that handles calls from composite query methods by Return (Reject (CANISTER_ERROR, ), Cycles) // max call graph depth exceeded let Calls' · Call · Calls'' = Calls Calls := Calls' · Calls'' - if S.canister_subnet[Canister_id] ≠ S.canister_subnet[Call.callee] + if S.canister_subnet[Canister_id].subnet_id ≠ S.canister_subnet[Call.callee].subnet_id then Return (Reject (CANISTER_ERROR, ), Cycles) // calling to another subnet let (Response', Cycles') = composite_query_helper(S, Cycles, Depth + 1, Root_canister_id, Canister_id, Call.callee, Call.method_name, Call.arg) From 9a28d4f391e4916f3386404db8f8d85785f6ad93 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Mon, 21 Aug 2023 10:42:01 +0200 Subject: [PATCH 02/13] check freezing_limit and memory_usage --- spec/index.md | 255 +++++++++++++++++++++++++++++++++++--------------- 1 file changed, 177 insertions(+), 78 deletions(-) diff --git a/spec/index.md b/spec/index.md index 7353a4864..5940dff3c 100644 --- a/spec/index.md +++ b/spec/index.md @@ -3487,6 +3487,49 @@ if A.settings.controllers is not null: else: New_controllers = [M.caller] +freezing_limit( + New_compute_allocation, + New_memory_allocation, + New_freezing_threshold, + memory_usage( + null, + null, + New_canister_history + ), + SubnetSize, +) ≤ M.transferred_cycles +if A.settings.memory_allocation > 0: + memory_usage( + null, + null, + New_canister_history + ) ≤ A.settings.memory_allocation + +if A.settings.compute_allocation is not null: + New_compute_allocation = A.settings.compute_allocation +else: + New_compute_allocation = 0 +if A.settings.memory_allocation is not null: + New_memory_allocation = A.settings.memory_allocation +else: + New_memory_allocation = 0 +if A.settings.freezing_threshold is not null: + New_freezing_threshold = A.settings.freezing_threshold +else: + New_freezing_threshold = 2592000 + +New_canister_history = { + total_num_changes = 1 + recent_changes = { + timestamp_nanos = CurrentTime + canister_version = 0 + origin = change_origin(M.caller, A.sender_canister_version, M.origin) + details = Creation { + controllers = New_controllers + } + } +} + ``` State after @@ -3498,31 +3541,12 @@ S with time[CanisterId] = CurrentTime global_timer[CanisterId] = 0 controllers[CanisterId] = New_controllers - if A.settings.compute_allocation is not null: - compute_allocation = A.settings.compute_allocation - else: - compute_allocation = 0 - if A.settings.memory_allocation is not null: - memory_allocation = A.settings.memory_allocation - else: - memory_allocation = 0 - if A.settings.freezing_threshold is not null: - freezing_threshold[CanisterId] = A.settings.freezing_threshold - else: - freezing_threshold[CanisterId] = 2592000 + compute_allocation[CanisterId] = New_compute_allocation + memory_allocation[CanisterId] = New_memory_allocation + freezing_threshold[CanisterId] = New_freezing_threshold balances[CanisterId] = M.transferred_cycles certified_data[CanisterId] = "" - canister_history[CanisterId] = { - total_num_changes = 1 - recent_changes = { - timestamp_nanos = CurrentTime - canister_version = 0 - origin = change_origin(M.caller, A.sender_canister_version, M.origin) - details = Creation { - controllers = New_controllers - } - } - } + canister_history[CanisterId] = New_canister_history messages = Older_messages · Younger_messages · ResponseMessage { origin = M.origin @@ -3568,10 +3592,56 @@ M.callee = ic_principal M.method_name = 'update_settings' M.arg = candid(A) M.caller ∈ S.controllers[A.canister_id] + +freezing_limit( + New_compute_allocation, + New_memory_allocation, + New_freezing_threshold, + memory_usage( + S.canisters[A.canister_id].wasm_state, + S.canisters[A.canister_id].raw_module, + New_canister_history + ), + S.canister_subnet[A.canister_id].subnet_size, +) ≤ S.balances[A.canister_id] +if A.settings.memory_allocation > 0: + memory_usage( + S.canisters[A.canister_id].wasm_state, + S.canisters[A.canister_id].raw_module, + New_canister_history + ) ≤ A.settings.memory_allocation + +if A.settings.compute_allocation is not null: + New_compute_allocation = A.settings.compute_allocation +else: + New_compute_allocation = S.compute_allocation[A.canister_id] +if A.settings.memory_allocation is not null: + New_memory_allocation = A.settings.memory_allocation +else: + New_memory_allocation = S.memory_allocation[A.canister_id] +if A.settings.freezing_threshold is not null: + New_freezing_threshold = A.settings.freezing_threshold +else: + New_freezing_threshold = S.freezing_threshold[A.canister_id] + S.canister_history[A.canister_id] = { total_num_changes = N; recent_changes = H; } +if A.settings.controllers is not null: + New_canister_history = { + total_num_changes = N + 1; + recent_changes = H · { + timestamp_nanos = S.time[A.canister_id]; + canister_version = S.canister_version[A.canister_id] + 1; + origin = change_origin(M.caller, A.sender_canister_version, M.origin); + details = ControllersChange { + controllers = A.settings.controllers; + }; + }; + } +else: + New_canister_history = S.canister_history[A.canister_id] ``` @@ -3582,23 +3652,10 @@ State after S with if A.settings.controllers is not null: controllers[A.canister_id] = A.settings.controllers - canister_history[A.canister_id] = { - total_num_changes = N + 1; - recent_changes = H · { - timestamp_nanos = S.time[A.canister_id]; - canister_version = S.canister_version[A.canister_id] + 1; - origin = change_origin(M.caller, A.sender_canister_version, M.origin); - details = ControllersChange { - controllers = A.settings.controllers; - }; - }; - } - if A.settings.compute_allocation is not null: - compute_allocation[A.canister_id] = A.settings.compute_allocation - if A.settings.memory_allocation is not null: - memory_allocation[A.canister_id] = A.settings.memory_allocation - if A.settings.freezing_threshold is not null: - freezing_threshold[A.canister_id] = A.settings.freezing_threshold + canister_history[A.canister_id] = New_canister_history + compute_allocation[A.canister_id] = New_compute_allocation + memory_allocation[A.canister_id] = New_memory_allocation + freezing_threshold[A.canister_id] = New_freezing_threshold canister_version[A.canister_id] = S.canister_version[A.canister_id] + 1 messages = Older_messages · Younger_messages · ResponseMessage { @@ -3723,6 +3780,11 @@ Public_custom_sections = parse_public_custom_sections(A.wasm_module); Private_custom_sections = parse_private_custom_sections(A.wasm_module); (A.mode = install and S.canisters[A.canister_id] = EmptyCanister) or A.mode = reinstall M.caller ∈ S.controllers[A.canister_id] + +dom(Mod.update_methods) ∩ dom(Mod.query_methods) = ∅ +dom(Mod.update_methods) ∩ dom(Mod.composite_query_methods) = ∅ +dom(Mod.query_methods) ∩ dom(Mod.composite_query_methods) = ∅ + Env = { time = S.time[A.canister_id]; controllers = S.controllers[A.canister_id]; @@ -3744,6 +3806,7 @@ Env = { canister_version = S.canister_version[A.canister_id] + 1; } Mod.init(A.canister_id, A.arg, M.caller, Env) = Return {new_state = New_state; new_certified_data = New_certified_data; new_global_timer = New_global_timer; cycles_used = Cycles_used;} + freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], @@ -3755,9 +3818,12 @@ freezing_limit( ), S.canister_subnet[A.canister_id].subnet_size, ) + Cycles_used ≤ S.balances[A.canister_id] -dom(Mod.update_methods) ∩ dom(Mod.query_methods) = ∅ -dom(Mod.update_methods) ∩ dom(Mod.composite_query_methods) = ∅ -dom(Mod.query_methods) ∩ dom(Mod.composite_query_methods) = ∅ +if S.memory_allocation[A.canister_id] > 0: + memory_usage( + New_state, + A.wasm_module, + New_canister_history + ) ≤ S.memory_allocation[A.canister_id] S.canister_history[A.canister_id] = { total_num_changes = N; @@ -3826,6 +3892,11 @@ Private_custom_sections = parse_private_custom_sections(A.wasm_module) A.mode = upgrade M.caller ∈ S.controllers[A.canister_id] S.canisters[A.canister_id] = { wasm_state = Old_state; module = Old_module, …} + +dom(Mod.update_methods) ∩ dom(Mod.query_methods) = ∅ +dom(Mod.update_methods) ∩ dom(Mod.composite_query_methods) = ∅ +dom(Mod.query_methods) ∩ dom(Mod.composite_query_methods) = ∅ + Env = { time = S.time[A.canister_id]; controllers = S.controllers[A.canister_id]; @@ -3854,6 +3925,7 @@ Env2 = Env with { canister_version = S.canister_version[A.canister_id] + 1; } Mod.post_upgrade(A.canister_id, Stable_memory, A.arg, M.caller, Env2) = Return {new_state = New_state; new_certified_data = New_certified_data'; new_global_timer = New_global_timer; cycles_used = Cycles_used';} + freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], @@ -3865,9 +3937,13 @@ freezing_limit( ), S.canister_subnet[A.canister_id].subnet_size, ) + Cycles_used + Cycles_used' ≤ S.balances[A.canister_id] -dom(Mod.update_methods) ∩ dom(Mod.query_methods) = ∅ -dom(Mod.update_methods) ∩ dom(Mod.composite_query_methods) = ∅ -dom(Mod.query_methods) ∩ dom(Mod.composite_query_methods) = ∅ +if S.memory_allocation[A.canister_id] > 0: + memory_usage( + New_state, + A.wasm_module, + New_canister_history + ) ≤ S.memory_allocation[A.canister_id] + S.canister_history[A.canister_id] = { total_num_changes = N; recent_changes = H; @@ -4299,12 +4375,61 @@ M.method_name = 'provisional_create_canister_with_cycles' M.arg = candid(A) is_system_assigned CanisterId CanisterId ∉ dom(S.canisters) -A.specified_id ∉ dom(S.canisters) +if A.specified_id is not null: + A.specified_id ∉ dom(S.canisters) + canister_id = A.specified_id if A.settings.controllers is not null: New_controllers = A.settings.controllers else: New_controllers = [M.caller] +freezing_limit( + New_compute_allocation, + New_memory_allocation, + New_freezing_threshold, + memory_usage( + null, + null, + New_canister_history + ), + SubnetSize +) ≤ New_balance +if A.settings.memory_allocation > 0: + memory_usage( + null, + null, + New_canister_history + ) ≤ A.settings.memory_allocation + +if A.settings.compute_allocation is not null: + New_compute_allocation = A.settings.compute_allocation +else: + New_compute_allocation = 0 +if A.settings.memory_allocation is not null: + New_memory_allocation = A.settings.memory_allocation +else: + New_memory_allocation = 0 +if A.settings.freezing_threshold is not null: + New_freezing_threshold = A.settings.freezing_threshold +else: + New_freezing_threshold = 2592000 +if A.amount is not null: + New_balance = A.amount +else: + New_balance = DEFAULT_PROVISIONAL_CYCLES_BALANCE + +New_canister_history { + total_num_changes = 1 + recent_changes = { + timestamp_nanos = CurrentTime + canister_version = 0 + origin = change_origin(M.caller, A.sender_canister_version, M.origin) + details = Creation { + controllers = New_controllers + } + } +} + ``` State after @@ -4312,42 +4437,16 @@ State after ```html S with - if A.specified_id is not null: - canister_id = A.specified_id - else: - canister_id = CanisterId canisters[canister_id] = EmptyCanister time[canister_id] = CurrentTime global_timer[canister_id] = 0 controllers[canister_id] = New_controllers - if A.settings.compute_allocation is not null: - compute_allocation[canister_id] = A.settings.compute_allocation - else: - compute_allocation[canister_id] = 0 - if A.settings.memory_allocation is not null: - memory_allocation[canister_id] = A.settings.memory_allocation - else: - memory_allocation[canister_id] = 0 - if A.settings.freezing_threshold is not null: - freezing_threshold[canister_id] = A.settings.freezing_threshold - else: - freezing_threshold[canister_id] = 2592000 - if A.amount is not null: - balances[canister_id] = A.amount - else: - balances[canister_id] = DEFAULT_PROVISIONAL_CYCLES_BALANCE + compute_allocation[canister_id] = New_compute_allocation + memory_allocation[canister_id] = New_memory_allocation + freezing_threshold[canister_id] = New_freezing_threshold + balances[canister_id] = New_balance certified_data[canister_id] = "" - canister_history[canister_id] = { - total_num_changes = 1 - recent_changes = { - timestamp_nanos = CurrentTime - canister_version = 0 - origin = change_origin(M.caller, A.sender_canister_version, M.origin) - details = Creation { - controllers = New_controllers - } - } - } + canister_history[canister_id] = New_canister_history messages = Older_messages · Younger_messages · ResponseMessage { origin = M.origin From 8b485b7c29bc608a125ac456fe18f4d541aaff7d Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Mon, 21 Aug 2023 11:21:26 +0200 Subject: [PATCH 03/13] fix --- spec/index.md | 72 +++++++++++++++++++++++++++------------------------ 1 file changed, 38 insertions(+), 34 deletions(-) diff --git a/spec/index.md b/spec/index.md index 5940dff3c..99504ae6b 100644 --- a/spec/index.md +++ b/spec/index.md @@ -3301,6 +3301,7 @@ if ), S.canister_subnet[M.receiver].subnet_size, ); + (S.memory_allocation[M.receiver] = 0) or (memory_usage(res.new_state, S.canisters[M.receiver].raw_module, S.canister_history[M.receiver]) ≤ S.memory_allocation[M.receiver]) (res.response = NoResponse) or S.call_contexts[M.call_context].needs_to_respond then S with @@ -3353,7 +3354,7 @@ else Depending on whether this is a call message and a response messages, we have either set aside `MAX_CYCLES_PER_MESSAGE` or `MAX_CYCLES_PER_RESPONSE`, either in the call context creation rule or the Callback invocation rule. -The cycle consumption of executing this message is modeled via the unspecified `Cycles_used` variable; the variable takes some value between 0 and `MAX_CYCLES_PER_MESSAGE`/`MAX_CYCLES_PER_RESPONSE` (for call execution and response execution, respectively). +The cycle consumption of executing this message is modeled via the unspecified `cycles_used` variable; the variable takes some value between 0 and `MAX_CYCLES_PER_MESSAGE`/`MAX_CYCLES_PER_RESPONSE` (for call execution and response execution, respectively). This transition detects certain behavior that will appear as a trap (and which an implementation may implement by trapping directly in a system call): @@ -3487,17 +3488,18 @@ if A.settings.controllers is not null: else: New_controllers = [M.caller] -freezing_limit( - New_compute_allocation, - New_memory_allocation, - New_freezing_threshold, - memory_usage( - null, - null, - New_canister_history - ), - SubnetSize, -) ≤ M.transferred_cycles +if New_compute_allocation > 0 or New_memory_allocation > 0: + freezing_limit( + New_compute_allocation, + New_memory_allocation, + New_freezing_threshold, + memory_usage( + null, + null, + New_canister_history + ), + SubnetSize, + ) ≤ M.transferred_cycles if A.settings.memory_allocation > 0: memory_usage( null, @@ -3593,17 +3595,18 @@ M.method_name = 'update_settings' M.arg = candid(A) M.caller ∈ S.controllers[A.canister_id] -freezing_limit( - New_compute_allocation, - New_memory_allocation, - New_freezing_threshold, - memory_usage( - S.canisters[A.canister_id].wasm_state, - S.canisters[A.canister_id].raw_module, - New_canister_history - ), - S.canister_subnet[A.canister_id].subnet_size, -) ≤ S.balances[A.canister_id] +if New_compute_allocation > S.compute_allocation[A.canister_id] or New_memory_allocation > S.memory_allocation[A.canister_id]: + freezing_limit( + New_compute_allocation, + New_memory_allocation, + New_freezing_threshold, + memory_usage( + S.canisters[A.canister_id].wasm_state, + S.canisters[A.canister_id].raw_module, + New_canister_history + ), + S.canister_subnet[A.canister_id].subnet_size, + ) ≤ S.balances[A.canister_id] if A.settings.memory_allocation > 0: memory_usage( S.canisters[A.canister_id].wasm_state, @@ -4383,17 +4386,18 @@ if A.settings.controllers is not null: else: New_controllers = [M.caller] -freezing_limit( - New_compute_allocation, - New_memory_allocation, - New_freezing_threshold, - memory_usage( - null, - null, - New_canister_history - ), - SubnetSize -) ≤ New_balance +if New_compute_allocation > 0 or New_memory_allocation > 0: + freezing_limit( + New_compute_allocation, + New_memory_allocation, + New_freezing_threshold, + memory_usage( + null, + null, + New_canister_history + ), + SubnetSize + ) ≤ New_balance if A.settings.memory_allocation > 0: memory_usage( null, From be753d2b9084ccd70615eb3090c34d32a3631c37 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Mon, 21 Aug 2023 11:22:51 +0200 Subject: [PATCH 04/13] typo --- spec/index.md | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/spec/index.md b/spec/index.md index 99504ae6b..d46cc2aa0 100644 --- a/spec/index.md +++ b/spec/index.md @@ -4380,7 +4380,7 @@ is_system_assigned CanisterId CanisterId ∉ dom(S.canisters) if A.specified_id is not null: A.specified_id ∉ dom(S.canisters) - canister_id = A.specified_id + Canister_id = A.specified_id if A.settings.controllers is not null: New_controllers = A.settings.controllers else: @@ -4441,25 +4441,25 @@ State after ```html S with - canisters[canister_id] = EmptyCanister - time[canister_id] = CurrentTime - global_timer[canister_id] = 0 - controllers[canister_id] = New_controllers - compute_allocation[canister_id] = New_compute_allocation - memory_allocation[canister_id] = New_memory_allocation - freezing_threshold[canister_id] = New_freezing_threshold - balances[canister_id] = New_balance - certified_data[canister_id] = "" - canister_history[canister_id] = New_canister_history + canisters[Canister_id] = EmptyCanister + time[Canister_id] = CurrentTime + global_timer[Canister_id] = 0 + controllers[Canister_id] = New_controllers + compute_allocation[Canister_id] = New_compute_allocation + memory_allocation[Canister_id] = New_memory_allocation + freezing_threshold[Canister_id] = New_freezing_threshold + balances[Canister_id] = New_balance + certified_data[Canister_id] = "" + canister_history[Canister_id] = New_canister_history messages = Older_messages · Younger_messages · ResponseMessage { origin = M.origin - response = Reply (candid({canister_id = canister_id})) + response = Reply (candid({canister_id = Canister_id})) refunded_cycles = M.transferred_cycles } - canister_status[canister_id] = Running - canister_version[canister_id] = 0 - canister_subnet[canister_id] = Subnet { + canister_status[Canister_id] = Running + canister_version[Canister_id] = 0 + canister_subnet[Canister_id] = Subnet { subnet_id : SubnetId subnet_size : SubnetSize } From 4b67f20dba41f576278cd1a217449844f0e5ae0d Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Mon, 21 Aug 2023 11:46:39 +0200 Subject: [PATCH 05/13] simplify --- spec/index.md | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/spec/index.md b/spec/index.md index d46cc2aa0..787c298c8 100644 --- a/spec/index.md +++ b/spec/index.md @@ -3500,12 +3500,12 @@ if New_compute_allocation > 0 or New_memory_allocation > 0: ), SubnetSize, ) ≤ M.transferred_cycles -if A.settings.memory_allocation > 0: +if New_memory_allocation > 0: memory_usage( null, null, New_canister_history - ) ≤ A.settings.memory_allocation + ) ≤ New_memory_allocation if A.settings.compute_allocation is not null: New_compute_allocation = A.settings.compute_allocation @@ -3607,12 +3607,12 @@ if New_compute_allocation > S.compute_allocation[A.canister_id] or New_memory_al ), S.canister_subnet[A.canister_id].subnet_size, ) ≤ S.balances[A.canister_id] -if A.settings.memory_allocation > 0: +if New_memory_allocation > 0: memory_usage( S.canisters[A.canister_id].wasm_state, S.canisters[A.canister_id].raw_module, New_canister_history - ) ≤ A.settings.memory_allocation + ) ≤ New_memory_allocation if A.settings.compute_allocation is not null: New_compute_allocation = A.settings.compute_allocation @@ -4379,7 +4379,6 @@ M.arg = candid(A) is_system_assigned CanisterId CanisterId ∉ dom(S.canisters) if A.specified_id is not null: - A.specified_id ∉ dom(S.canisters) Canister_id = A.specified_id if A.settings.controllers is not null: New_controllers = A.settings.controllers @@ -4398,12 +4397,12 @@ if New_compute_allocation > 0 or New_memory_allocation > 0: ), SubnetSize ) ≤ New_balance -if A.settings.memory_allocation > 0: +if New_memory_allocation > 0: memory_usage( null, null, New_canister_history - ) ≤ A.settings.memory_allocation + ) ≤ New_memory_allocation if A.settings.compute_allocation is not null: New_compute_allocation = A.settings.compute_allocation From 9465a59faf811cc28b7258b039aeee3666301563 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Mon, 21 Aug 2023 11:49:39 +0200 Subject: [PATCH 06/13] inspect_message is not invoked on frozen canisters --- spec/index.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/spec/index.md b/spec/index.md index 787c298c8..f93ab6d9b 100644 --- a/spec/index.md +++ b/spec/index.md @@ -2930,8 +2930,20 @@ is_effective_canister_id(E.content, ECID) status = simple_status(S.canister_status[E.content.canister_id]); canister_version = S.canister_version[E.content.canister_id]; } + S.balances[E.content.canister_id] ≥ freezing_limit( + S.compute_allocation[E.content.canister_id], + S.memory_allocation[E.content.canister_id], + S.freezing_threshold[E.content.canister_id], + memory_usage( + S.canisters[E.content.canister_id].wasm_state, + S.canisters[E.content.canister_id].raw_module, + S.canister_history[E.content.canister_id] + ), + S.canister_subnet[E.content.canister_id].subnet_size, + ) S.canisters[E.content.canister_id].module.inspect_message (E.content.method_name, S.canisters[E.content.canister_id].wasm_state, E.content.arg, E.content.sender, Env) = Return {status = Accept;} +) ``` From 5d0f12136c3dfe4ec0cdc017564a21fa47646693 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Mon, 21 Aug 2023 12:38:41 +0200 Subject: [PATCH 07/13] check freezing limit before canister installation --- spec/index.md | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/spec/index.md b/spec/index.md index f93ab6d9b..3a219cbd7 100644 --- a/spec/index.md +++ b/spec/index.md @@ -3822,6 +3822,17 @@ Env = { } Mod.init(A.canister_id, A.arg, M.caller, Env) = Return {new_state = New_state; new_certified_data = New_certified_data; new_global_timer = New_global_timer; cycles_used = Cycles_used;} +freezing_limit( + S.compute_allocation[A.canister_id], + S.memory_allocation[A.canister_id], + S.freezing_threshold[A.canister_id], + memory_usage( + S.canisters[A.canister_id].wasm_state, + S.canisters[A.canister_id].raw_module, + S.canister_history[A.canister_id], + ), + S.canister_subnet[A.canister_id].subnet_size, +) + MAX_CYCLES_PER_MESSAGE ≤ S.balances[A.canister_id] freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], @@ -3941,6 +3952,28 @@ Env2 = Env with { } Mod.post_upgrade(A.canister_id, Stable_memory, A.arg, M.caller, Env2) = Return {new_state = New_state; new_certified_data = New_certified_data'; new_global_timer = New_global_timer; cycles_used = Cycles_used';} +freezing_limit( + S.compute_allocation[A.canister_id], + S.memory_allocation[A.canister_id], + S.freezing_threshold[A.canister_id], + memory_usage( + S.canisters[A.canister_id].wasm_state, + S.canisters[A.canister_id].raw_module, + S.canister_history[A.canister_id], + ), + S.canister_subnet[A.canister_id].subnet_size, +) + MAX_CYCLES_PER_MESSAGE ≤ S.balances[A.canister_id] +freezing_limit( + S.compute_allocation[A.canister_id], + S.memory_allocation[A.canister_id], + S.freezing_threshold[A.canister_id], + memory_usage( + New_state, + A.wasm_module, + New_canister_history + ), + S.canister_subnet[A.canister_id].subnet_size, +) + MAX_CYCLES_PER_MESSAGE ≤ S.balances[A.canister_id] freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], From 06716bba21c786ab618632b83e9ee8b537a49e70 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Wed, 23 Aug 2023 09:20:50 +0200 Subject: [PATCH 08/13] refactor freezing_limit --- spec/index.md | 286 +++++++++++++++++++++----------------------------- 1 file changed, 120 insertions(+), 166 deletions(-) diff --git a/spec/index.md b/spec/index.md index 3a219cbd7..55ea02aec 100644 --- a/spec/index.md +++ b/spec/index.md @@ -2441,7 +2441,11 @@ The [WebAssembly System API](#system-api) is relatively low-level, and some of i controllers : List Principal; global_timer : Nat; balance : Nat; - freezing_limit : Nat; + compute_allocation : Nat; + memory_allocation : Nat; + memory_usage : Nat; + freezing_threshold : Nat; + subnet_size : Nat; certificate : NoCertificate | Blob; status : Running | Stopping | Stopped; canister_version : CanisterVersion; @@ -2887,7 +2891,7 @@ The (unspecified) function `idle_cycles_burned_rate(compute_allocation, memory_a freezing_limit(compute_allocation, memory_allocation, freezing_threshold, memory_usage, subnet_size) = idle_cycles_burned_rate(compute_allocation, memory_allocation, memory_usage, subnet_size) * freezing_threshold / (24 * 60 * 60) -The (unspecified) function `memory_usage(wasm_state, raw_module, canister_history)` determines the canister's memory usage in bytes given its Wasm state, raw Wasm binary, and canister history. +The (unspecified) functions `memory_usage_wasm_state(wasm_state)`, `memory_usage_raw_module(raw_module)`, and `memory_usage_canister_history(canister_history)` determine the canister's memory usage in bytes consumed by its Wasm state, raw Wasm binary, and canister history, respectively. Submitted request `E : Envelope` @@ -2914,18 +2918,13 @@ is_effective_canister_id(E.content, ECID) time = S.time[E.content.canister_id]; controllers = S.controllers[E.content.canister_id]; global_timer = S.global_timer[E.content.canister_id]; - balance = S.balances[E.content.canister_id] - freezing_limit = freezing_limit( - S.compute_allocation[E.content.canister_id], - S.memory_allocation[E.content.canister_id], - S.freezing_threshold[E.content.canister_id], - memory_usage( - S.canisters[E.content.canister_id].wasm_state, - S.canisters[E.content.canister_id].raw_module, - S.canister_history[E.content.canister_id] - ), - S.canister_subnet[E.content.canister_id].subnet_size, - ); + balance = S.balances[E.content.canister_id]; + compute_allocation = S.compute_allocation[E.content.canister_id]; + memory_allocation = S.memory_allocation[E.content.canister_id]; + memory_usage = memory_usage_raw_module(S.canisters[E.content.canister_id].raw_module) + + memory_usage_canister_history(S.canister_history[E.content.canister_id]); + freezing_threshold = S.freezing_threshold[E.content.canister_id]; + subnet_size = S.canister_subnet[E.content.canister_id].subnet_size; certificate = NoCertificate; status = simple_status(S.canister_status[E.content.canister_id]); canister_version = S.canister_version[E.content.canister_id]; @@ -2934,11 +2933,9 @@ is_effective_canister_id(E.content, ECID) S.compute_allocation[E.content.canister_id], S.memory_allocation[E.content.canister_id], S.freezing_threshold[E.content.canister_id], - memory_usage( - S.canisters[E.content.canister_id].wasm_state, - S.canisters[E.content.canister_id].raw_module, - S.canister_history[E.content.canister_id] - ), + memory_usage_wasm_state(S.canisters[E.content.canister_id].wasm_state) + + memory_usage_raw_module(S.canisters[E.content.canister_id].raw_module) + + memory_usage_canister_history(S.canister_history[E.content.canister_id]), S.canister_subnet[E.content.canister_id].subnet_size, ) S.canisters[E.content.canister_id].module.inspect_message @@ -3031,15 +3028,14 @@ Conditions S.messages = Older_messages · CallMessage CM · Younger_messages (CM.queue = Unordered) or (∀ msg ∈ Older_messages. msg.queue ≠ CM.queue) +S.canisters[CM.callee] ≠ EmptyCanister S.canister_status[CM.callee] = Stopped or S.canister_status[CM.callee] = Stopping _ or balances[CM.callee] < freezing_limit( S.compute_allocation[CM.callee], S.memory_allocation[CM.callee], S.freezing_threshold[CM.callee], - memory_usage( - S.canisters[CM.callee].wasm_state, - S.canisters[CM.callee].raw_module, - S.canister_history[CM.callee] - ), + memory_usage_wasm_state(S.canisters[CM.callee].wasm_state) + + memory_usage_raw_module(S.canisters[CM.callee].raw_module) + + memory_usage_canister_history(S.canister_history[CM.callee]), S.canister_subnet[CM.callee].subnet_size, ) @@ -3081,11 +3077,9 @@ S.balances[CM.callee] ≥ freezing_limit( S.compute_allocation[CM.callee], S.memory_allocation[CM.callee], S.freezing_threshold[CM.callee], - memory_usage( - S.canisters[CM.callee].wasm_state, - S.canisters[CM.callee].raw_module, - S.canister_history[CM.callee] - ), + memory_usage_wasm_state(S.canisters[CM.callee].wasm_state) + + memory_usage_raw_module(S.canisters[CM.callee].raw_module) + + memory_usage_canister_history(S.canister_history[CM.callee]), S.canister_subnet[CM.callee].subnet_size, ) + MAX_CYCLES_PER_MESSAGE Ctxt_id ∉ dom(S.call_contexts) @@ -3131,11 +3125,9 @@ S.balances[C] ≥ freezing_limit( S.compute_allocation[C], S.memory_allocation[C], S.freezing_threshold[C], - memory_usage( - S.canisters[C].wasm_state, - S.canisters[C].raw_module, - S.canister_history[C] - ), + memory_usage_wasm_state(S.canisters[C].wasm_state) + + memory_usage_raw_module(S.canisters[C].raw_module) + + memory_usage_canister_history(S.canister_history[C]), S.canister_subnet[C].subnet_size, ) + MAX_CYCLES_PER_MESSAGE Ctxt_id ∉ dom(S.call_contexts) @@ -3182,11 +3174,9 @@ S.balances[C] ≥ freezing_limit( S.compute_allocation[C], S.memory_allocation[C], S.freezing_threshold[C], - memory_usage( - S.canisters[C].wasm_state, - S.canisters[C].raw_module, - S.canister_history[C] - ), + memory_usage_wasm_state(S.canisters[C].wasm_state) + + memory_usage_raw_module(S.canisters[C].raw_module) + + memory_usage_canister_history(S.canister_history[C]), S.canister_subnet[C].subnet_size, ) + MAX_CYCLES_PER_MESSAGE Ctxt_id ∉ dom(S.call_contexts) @@ -3242,17 +3232,12 @@ Env = { controllers = S.controllers[M.receiver]; global_timer = S.global_timer[M.receiver]; balance = S.balances[M.receiver] - freezing_limit = freezing_limit( - S.compute_allocation[M.receiver], - S.memory_allocation[M.receiver], - S.freezing_threshold[M.receiver], - memory_usage( - S.canisters[M.receiver].wasm_state, - S.canisters[M.receiver].raw_module, - S.canister_history[M.receiver] - ), - S.canister_subnet[M.receiver].subnet_size, - ); + compute_allocation = S.compute_allocation[M.receiver]; + memory_allocation = S.memory_allocation[M.receiver]; + memory_usage = memory_usage_raw_module(S.canisters[M.receiver].raw_module) + + memory_usage_canister_history(S.canister_history[M.receiver]); + freezing_threshold = S.freezing_threshold[M.receiver]; + subnet_size = S.canister_subnet[M.receiver].subnet_size; certificate = NoCertificate; status = simple_status(S.canister_status[M.receiver]); canister_version = S.canister_version[M.receiver]; @@ -3306,14 +3291,14 @@ if S.compute_allocation[M.receiver], S.memory_allocation[M.receiver], S.freezing_threshold[M.receiver], - memory_usage( - res.new_state, - S.canisters[M.receiver].raw_module, - S.canister_history[M.receiver] - ), + memory_usage_wasm_state(res.new_state) + + memory_usage_raw_module(S.canisters[M.receiver].raw_module) + + memory_usage_canister_history(S.canister_history[M.receiver]), S.canister_subnet[M.receiver].subnet_size, ); - (S.memory_allocation[M.receiver] = 0) or (memory_usage(res.new_state, S.canisters[M.receiver].raw_module, S.canister_history[M.receiver]) ≤ S.memory_allocation[M.receiver]) + (S.memory_allocation[M.receiver] = 0) or (memory_usage_wasm_state(res.new_state) + + memory_usage_raw_module(S.canisters[M.receiver].raw_module) + + memory_usage_canister_history(S.canister_history[M.receiver]) ≤ S.memory_allocation[M.receiver]) (res.response = NoResponse) or S.call_contexts[M.call_context].needs_to_respond then S with @@ -3505,19 +3490,11 @@ if New_compute_allocation > 0 or New_memory_allocation > 0: New_compute_allocation, New_memory_allocation, New_freezing_threshold, - memory_usage( - null, - null, - New_canister_history - ), + memory_usage_canister_history(New_canister_history), SubnetSize, ) ≤ M.transferred_cycles if New_memory_allocation > 0: - memory_usage( - null, - null, - New_canister_history - ) ≤ New_memory_allocation + memory_usage_canister_history(New_canister_history) ≤ New_memory_allocation if A.settings.compute_allocation is not null: New_compute_allocation = A.settings.compute_allocation @@ -3612,19 +3589,15 @@ if New_compute_allocation > S.compute_allocation[A.canister_id] or New_memory_al New_compute_allocation, New_memory_allocation, New_freezing_threshold, - memory_usage( - S.canisters[A.canister_id].wasm_state, - S.canisters[A.canister_id].raw_module, - New_canister_history - ), + memory_usage_wasm_state(S.canisters[A.canister_id].wasm_state) + + memory_usage_raw_module(S.canisters[A.canister_id].raw_module) + + memory_usage_canister_history(New_canister_history), S.canister_subnet[A.canister_id].subnet_size, ) ≤ S.balances[A.canister_id] if New_memory_allocation > 0: - memory_usage( - S.canisters[A.canister_id].wasm_state, - S.canisters[A.canister_id].raw_module, - New_canister_history - ) ≤ New_memory_allocation + memory_usage_wasm_state(S.canisters[A.canister_id].wasm_state) + + memory_usage_raw_module(S.canisters[A.canister_id].raw_module) + + memory_usage_canister_history(New_canister_history) ≤ New_memory_allocation if A.settings.compute_allocation is not null: New_compute_allocation = A.settings.compute_allocation @@ -3723,11 +3696,10 @@ S with idle_cycles_burned_per_day = idle_cycles_burned_rate( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], - memory_usage( - S.canisters[A.canister_id].wasm_state, - S.canisters[A.canister_id].raw_module, - S.canister_history[A.canister_id] - ), + memory_usage_wasm_state(S.canisters[A.canister_id].wasm_state) + + memory_usage_raw_module(S.canisters[A.canister_id].raw_module) + + memory_usage_canister_history(S.canister_history[A.canister_id]), + S.freezing_threshold[A.canister_id], S.canister_subnet[A.canister_id].subnet_size, ); }) @@ -3805,17 +3777,12 @@ Env = { controllers = S.controllers[A.canister_id]; global_timer = 0; balance = S.balances[A.canister_id]; - freezing_limit = freezing_limit( - S.compute_allocation[A.canister_id], - S.memory_allocation[A.canister_id], - S.freezing_threshold[A.canister_id], - memory_usage( - S.canisters[A.canister_id].wasm_state, - S.canisters[A.canister_id].raw_module, - S.canister_history[A.canister_id] - ), - S.canister_subnet[A.canister_id].subnet_size, - ); + compute_allocation = S.compute_allocation[A.canister_id]; + memory_allocation = S.memory_allocation[A.canister_id]; + memory_usage = memory_usage_raw_module(S.canisters[A.canister_id].raw_module) + + memory_usage_canister_history(S.canister_history[A.canister_id]); + freezing_threshold = S.freezing_threshold[A.canister_id]; + subnet_size = S.canister_subnet[A.canister_id].subnet_size; certificate = NoCertificate; status = simple_status(S.canister_status[A.canister_id]); canister_version = S.canister_version[A.canister_id] + 1; @@ -3826,29 +3793,24 @@ freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], S.freezing_threshold[A.canister_id], - memory_usage( - S.canisters[A.canister_id].wasm_state, - S.canisters[A.canister_id].raw_module, - S.canister_history[A.canister_id], - ), + memory_usage_wasm_state(S.canisters[A.canister_id].wasm_state) + + memory_usage_raw_module(S.canisters[A.canister_id].raw_module) + + memory_usage_canister_history(S.canister_history[A.canister_id]), S.canister_subnet[A.canister_id].subnet_size, ) + MAX_CYCLES_PER_MESSAGE ≤ S.balances[A.canister_id] freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], S.freezing_threshold[A.canister_id], - memory_usage( - New_state, - A.wasm_module, - New_canister_history - ), + memory_usage_wasm_state(New_state) + + memory_usage_raw_module(A.wasm_module) + + memory_usage_canister_history(New_canister_history), S.canister_subnet[A.canister_id].subnet_size, ) + Cycles_used ≤ S.balances[A.canister_id] if S.memory_allocation[A.canister_id] > 0: - memory_usage( - New_state, - A.wasm_module, - New_canister_history + memory_usage_wasm_state(New_state) + + memory_usage_raw_module(A.wasm_module) + + memory_usage_canister_history(New_canister_history), ) ≤ S.memory_allocation[A.canister_id] S.canister_history[A.canister_id] = { @@ -3927,17 +3889,12 @@ Env = { time = S.time[A.canister_id]; controllers = S.controllers[A.canister_id]; balance = S.balances[A.canister_id]; - freezing_limit = freezing_limit( - S.compute_allocation[A.canister_id], - S.memory_allocation[A.canister_id], - S.freezing_threshold[A.canister_id], - memory_usage( - S.canisters[A.canister_id].wasm_state, - S.canisters[A.canister_id].raw_module, - S.canister_history[A.canister_id] - ), - S.canister_subnet[A.canister_id].subnet_size, - ); + compute_allocation = S.compute_allocation[A.canister_id]; + memory_allocation = S.memory_allocation[A.canister_id]; + memory_usage = memory_usage_raw_module(S.canisters[A.canister_id].raw_module) + + memory_usage_canister_history(S.canister_history[A.canister_id]); + freezing_threshold = S.freezing_threshold[A.canister_id]; + subnet_size = S.canister_subnet[A.canister_id].subnet_size; certificate = NoCertificate; status = simple_status(S.canister_status[A.canister_id]); } @@ -3947,6 +3904,7 @@ Env1 = Env with { } Old_module.pre_upgrade(Old_State, M.caller, Env1) = Return {stable_memory = Stable_memory; new_certified_data = New_certified_data; cycles_used = Cycles_used;} Env2 = Env with { + memory_usage = memory_usage_raw_module(A.wasm_module) + memory_usage_canister_history(New_canister_history) global_timer = 0; canister_version = S.canister_version[A.canister_id] + 1; } @@ -3956,41 +3914,33 @@ freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], S.freezing_threshold[A.canister_id], - memory_usage( - S.canisters[A.canister_id].wasm_state, - S.canisters[A.canister_id].raw_module, - S.canister_history[A.canister_id], - ), + memory_usage_wasm_state(S.canisters[A.canister_id].wasm_state) + + memory_usage_raw_module(S.canisters[A.canister_id].raw_module) + + memory_usage_canister_history(S.canister_history[A.canister_id]), S.canister_subnet[A.canister_id].subnet_size, ) + MAX_CYCLES_PER_MESSAGE ≤ S.balances[A.canister_id] freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], S.freezing_threshold[A.canister_id], - memory_usage( - New_state, - A.wasm_module, - New_canister_history - ), + memory_usage_wasm_state(New_state) + + memory_usage_raw_module(A.wasm_module) + + memory_usage_canister_history(New_canister_history), S.canister_subnet[A.canister_id].subnet_size, ) + MAX_CYCLES_PER_MESSAGE ≤ S.balances[A.canister_id] freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], S.freezing_threshold[A.canister_id], - memory_usage( - New_state, - A.wasm_module, - New_canister_history - ), + memory_usage_wasm_state(New_state) + + memory_usage_raw_module(A.wasm_module) + + memory_usage_canister_history(New_canister_history), S.canister_subnet[A.canister_id].subnet_size, ) + Cycles_used + Cycles_used' ≤ S.balances[A.canister_id] if S.memory_allocation[A.canister_id] > 0: - memory_usage( - New_state, - A.wasm_module, - New_canister_history - ) ≤ S.memory_allocation[A.canister_id] + memory_usage_wasm_state(New_state) + + memory_usage_raw_module(A.wasm_module) + + memory_usage_canister_history(New_canister_history) ≤ S.memory_allocation[A.canister_id] S.canister_history[A.canister_id] = { total_num_changes = N; @@ -4435,19 +4385,11 @@ if New_compute_allocation > 0 or New_memory_allocation > 0: New_compute_allocation, New_memory_allocation, New_freezing_threshold, - memory_usage( - null, - null, - New_canister_history - ), + memory_usage_canister_history(New_canister_history), SubnetSize ) ≤ New_balance if New_memory_allocation > 0: - memory_usage( - null, - null, - New_canister_history - ) ≤ New_memory_allocation + memory_usage_canister_history(New_canister_history) ≤ New_memory_allocation if A.settings.compute_allocation is not null: New_compute_allocation = A.settings.compute_allocation @@ -4856,17 +4798,12 @@ We define an auxiliary method that handles calls from composite query methods by let Env = { time = S.time[Canister_id]; global_timer = S.global_timer[Canister_id]; balance = S.balances[Canister_id]; - freezing_limit = freezing_limit( - S.compute_allocation[Canister_id], - S.memory_allocation[Canister_id], - S.freezing_threshold[Canister_id], - memory_usage( - S.canisters[Canister_id].wasm_state, - S.canisters[Canister_id].raw_module, - S.canister_history[Canister_id] - ), - S.canister_subnet[Canister_id].subnet_size, - ); + compute_allocation = S.compute_allocation[Canister_id]; + memory_allocation = S.memory_allocation[Canister_id]; + memory_usage = memory_usage_raw_module(S.canisters[Canister_id].raw_module) + + memory_usage_canister_history(S.canister_history[Canister_id]), + freezing_threshold = S.freezing_threshold[Canister_id]; + subnet_size = S.canister_subnet[Canister_id].subnet_size; certificate = Cert; status = simple_status(S.canister_status[Canister_id]); canister_version = S.canister_version[Canister_id]; @@ -4877,11 +4814,9 @@ We define an auxiliary method that handles calls from composite query methods by S.compute_allocation[Canister_id], S.memory_allocation[Canister_id], S.freezing_threshold[Canister_id], - memory_usage( - S.canisters[Canister_id].wasm_state, - S.canisters[Canister_id].raw_module, - S.canister_history[Canister_id] - ), + memory_usage_wasm_state(S.canisters[Canister_id].wasm_state) + + memory_usage_raw_module(S.canisters[Canister_id].raw_module) + + memory_usage_canister_history(S.canister_history[Canister_id]), S.canister_subnet[Canister_id].subnet_size, ) and (Method_name ∈ dom(Mod.query_methods) or Method_name ∈ dom(Mod.composite_query_methods)) and @@ -5090,6 +5025,7 @@ We can model the execution of WebAssembly functions as stateful functions that h } ExecutionState = { wasm_state : WasmState; + memory_usage : Nat; params : Params; response : NoResponse | Response; cycles_accepted : Nat; @@ -5713,7 +5649,13 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im if es.context ∉ {U, Ry, Rt, T} then Trap {cycles_used = es.cycles_used;} if es.pending_call = NoPendingCall then Trap {cycles_used = es.cycles_used;} if es.balance < amount then Trap {cycles_used = es.cycles_used;} - if es.balance - amount < es.params.sysenv.freezing_limit then Trap {cycles_used = es.cycles_used;} + if es.balance - amount < freezing_limit( + es.params.sysenv.compute_allocation, + es.params.sysenv.memory_allocation, + memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, + es.params.sysenv.freezing_threshold, + es.params.sysenv.subnet_size, + ) then Trap {cycles_used = es.cycles_used;} es.balance := es.balance - amount es.pending_call.transferred_cycles := es.pending_call.transferred_cycles + amount @@ -5723,7 +5665,13 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im let amount = amount_high * 2^64 + amount_low if es.pending_call = NoPendingCall then Trap {cycles_used = es.cycles_used;} if es.balance < amount then Trap {cycles_used = es.cycles_used;} - if es.balance - amount < es.params.sysenv.freezing_limit then Trap {cycles_used = es.cycles_used;} + if es.balance - amount < freezing_limit( + es.params.sysenv.compute_allocation, + es.params.sysenv.memory_allocation, + memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, + es.params.sysenv.freezing_threshold, + es.params.sysenv.subnet_size, + ) then Trap {cycles_used = es.cycles_used;} es.balance := es.balance - amount es.pending_call.transferred_cycles := es.pending_call.transferred_cycles + amount @@ -5734,7 +5682,13 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im // are we below the threezing threshold? // Or maybe the system has other reasons to not perform this - if es.balance < es.params.sysenv.freezing_limit or system_cannot_do_this_call_now() + if es.balance < freezing_limit( + es.params.sysenv.compute_allocation, + es.params.sysenv.memory_allocation, + memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, + es.params.sysenv.freezing_threshold, + es.params.sysenv.subnet_size, + ) or system_cannot_do_this_call_now() then discard_pending_call() return 1 From 0c4dc3546e7d11db3a05a23c6bbaa6ff707ea9f2 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Wed, 23 Aug 2023 10:13:25 +0200 Subject: [PATCH 09/13] update --- spec/index.md | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/spec/index.md b/spec/index.md index 55ea02aec..22bc7a37c 100644 --- a/spec/index.md +++ b/spec/index.md @@ -3919,15 +3919,6 @@ freezing_limit( memory_usage_canister_history(S.canister_history[A.canister_id]), S.canister_subnet[A.canister_id].subnet_size, ) + MAX_CYCLES_PER_MESSAGE ≤ S.balances[A.canister_id] -freezing_limit( - S.compute_allocation[A.canister_id], - S.memory_allocation[A.canister_id], - S.freezing_threshold[A.canister_id], - memory_usage_wasm_state(New_state) + - memory_usage_raw_module(A.wasm_module) + - memory_usage_canister_history(New_canister_history), - S.canister_subnet[A.canister_id].subnet_size, -) + MAX_CYCLES_PER_MESSAGE ≤ S.balances[A.canister_id] freezing_limit( S.compute_allocation[A.canister_id], S.memory_allocation[A.canister_id], @@ -5652,8 +5643,8 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im if es.balance - amount < freezing_limit( es.params.sysenv.compute_allocation, es.params.sysenv.memory_allocation, - memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, es.params.sysenv.freezing_threshold, + memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, es.params.sysenv.subnet_size, ) then Trap {cycles_used = es.cycles_used;} @@ -5668,8 +5659,8 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im if es.balance - amount < freezing_limit( es.params.sysenv.compute_allocation, es.params.sysenv.memory_allocation, - memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, es.params.sysenv.freezing_threshold, + memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, es.params.sysenv.subnet_size, ) then Trap {cycles_used = es.cycles_used;} @@ -5685,8 +5676,8 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im if es.balance < freezing_limit( es.params.sysenv.compute_allocation, es.params.sysenv.memory_allocation, - memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, es.params.sysenv.freezing_threshold, + memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, es.params.sysenv.subnet_size, ) or system_cannot_do_this_call_now() then From 092a347f6d9edbd0af52a1c808c676c236dbcf43 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Wed, 23 Aug 2023 10:14:36 +0200 Subject: [PATCH 10/13] update --- spec/index.md | 1 - 1 file changed, 1 deletion(-) diff --git a/spec/index.md b/spec/index.md index 22bc7a37c..9c87a5e5b 100644 --- a/spec/index.md +++ b/spec/index.md @@ -5016,7 +5016,6 @@ We can model the execution of WebAssembly functions as stateful functions that h } ExecutionState = { wasm_state : WasmState; - memory_usage : Nat; params : Params; response : NoResponse | Response; cycles_accepted : Nat; From c911b70f38e2de6fbbf3338c61c43aff72860aca Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Wed, 23 Aug 2023 10:20:07 +0200 Subject: [PATCH 11/13] clarify --- spec/index.md | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/spec/index.md b/spec/index.md index 9c87a5e5b..829caa32f 100644 --- a/spec/index.md +++ b/spec/index.md @@ -2921,8 +2921,8 @@ is_effective_canister_id(E.content, ECID) balance = S.balances[E.content.canister_id]; compute_allocation = S.compute_allocation[E.content.canister_id]; memory_allocation = S.memory_allocation[E.content.canister_id]; - memory_usage = memory_usage_raw_module(S.canisters[E.content.canister_id].raw_module) + - memory_usage_canister_history(S.canister_history[E.content.canister_id]); + memory_usage_raw_module = memory_usage_raw_module(S.canisters[E.content.canister_id].raw_module); + memory_usage_canister_history = memory_usage_canister_history(S.canister_history[E.content.canister_id]); freezing_threshold = S.freezing_threshold[E.content.canister_id]; subnet_size = S.canister_subnet[E.content.canister_id].subnet_size; certificate = NoCertificate; @@ -3234,8 +3234,8 @@ Env = { balance = S.balances[M.receiver] compute_allocation = S.compute_allocation[M.receiver]; memory_allocation = S.memory_allocation[M.receiver]; - memory_usage = memory_usage_raw_module(S.canisters[M.receiver].raw_module) + - memory_usage_canister_history(S.canister_history[M.receiver]); + memory_usage_raw_module = memory_usage_raw_module(S.canisters[M.receiver].raw_module); + memory_usage_canister_history = memory_usage_canister_history(S.canister_history[M.receiver]); freezing_threshold = S.freezing_threshold[M.receiver]; subnet_size = S.canister_subnet[M.receiver].subnet_size; certificate = NoCertificate; @@ -3779,8 +3779,8 @@ Env = { balance = S.balances[A.canister_id]; compute_allocation = S.compute_allocation[A.canister_id]; memory_allocation = S.memory_allocation[A.canister_id]; - memory_usage = memory_usage_raw_module(S.canisters[A.canister_id].raw_module) + - memory_usage_canister_history(S.canister_history[A.canister_id]); + memory_usage_raw_module = memory_usage_raw_module(S.canisters[A.canister_id].raw_module); + memory_usage_canister_history = memory_usage_canister_history(S.canister_history[A.canister_id]); freezing_threshold = S.freezing_threshold[A.canister_id]; subnet_size = S.canister_subnet[A.canister_id].subnet_size; certificate = NoCertificate; @@ -3891,8 +3891,8 @@ Env = { balance = S.balances[A.canister_id]; compute_allocation = S.compute_allocation[A.canister_id]; memory_allocation = S.memory_allocation[A.canister_id]; - memory_usage = memory_usage_raw_module(S.canisters[A.canister_id].raw_module) + - memory_usage_canister_history(S.canister_history[A.canister_id]); + memory_usage_raw_module = memory_usage_raw_module(S.canisters[A.canister_id].raw_module); + memory_usage_canister_history = memory_usage_canister_history(S.canister_history[A.canister_id]); freezing_threshold = S.freezing_threshold[A.canister_id]; subnet_size = S.canister_subnet[A.canister_id].subnet_size; certificate = NoCertificate; @@ -3904,7 +3904,8 @@ Env1 = Env with { } Old_module.pre_upgrade(Old_State, M.caller, Env1) = Return {stable_memory = Stable_memory; new_certified_data = New_certified_data; cycles_used = Cycles_used;} Env2 = Env with { - memory_usage = memory_usage_raw_module(A.wasm_module) + memory_usage_canister_history(New_canister_history) + memory_usage_raw_module = memory_usage_raw_module(A.wasm_module); + memory_usage_canister_history = memory_usage_canister_history(New_canister_history); global_timer = 0; canister_version = S.canister_version[A.canister_id] + 1; } @@ -4791,8 +4792,8 @@ We define an auxiliary method that handles calls from composite query methods by balance = S.balances[Canister_id]; compute_allocation = S.compute_allocation[Canister_id]; memory_allocation = S.memory_allocation[Canister_id]; - memory_usage = memory_usage_raw_module(S.canisters[Canister_id].raw_module) + - memory_usage_canister_history(S.canister_history[Canister_id]), + memory_usage_raw_module = memory_usage_raw_module(S.canisters[Canister_id].raw_module); + memory_usage_canister_history = memory_usage_canister_history(S.canister_history[Canister_id]); freezing_threshold = S.freezing_threshold[Canister_id]; subnet_size = S.canister_subnet[Canister_id].subnet_size; certificate = Cert; @@ -5643,7 +5644,7 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im es.params.sysenv.compute_allocation, es.params.sysenv.memory_allocation, es.params.sysenv.freezing_threshold, - memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, + memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage_raw_module + es.params.sysenv.memory_usage_canister_history, es.params.sysenv.subnet_size, ) then Trap {cycles_used = es.cycles_used;} @@ -5659,7 +5660,7 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im es.params.sysenv.compute_allocation, es.params.sysenv.memory_allocation, es.params.sysenv.freezing_threshold, - memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, + memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage_raw_module + es.params.sysenv.memory_usage_canister_history, es.params.sysenv.subnet_size, ) then Trap {cycles_used = es.cycles_used;} @@ -5676,7 +5677,7 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im es.params.sysenv.compute_allocation, es.params.sysenv.memory_allocation, es.params.sysenv.freezing_threshold, - memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage, + memory_usage_wasm_state(es.wasm_state) + es.params.sysenv.memory_usage_raw_module + es.params.sysenv.memory_usage_canister_history, es.params.sysenv.subnet_size, ) or system_cannot_do_this_call_now() then From 6d1162b892aedfe790539e3f7833134a8d1348e0 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Wed, 23 Aug 2023 20:42:36 +0200 Subject: [PATCH 12/13] fix Env def --- spec/index.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/spec/index.md b/spec/index.md index 829caa32f..a143569b6 100644 --- a/spec/index.md +++ b/spec/index.md @@ -2443,7 +2443,8 @@ The [WebAssembly System API](#system-api) is relatively low-level, and some of i balance : Nat; compute_allocation : Nat; memory_allocation : Nat; - memory_usage : Nat; + memory_usage_raw_module : Nat; + memory_usage_canister_history : Nat; freezing_threshold : Nat; subnet_size : Nat; certificate : NoCertificate | Blob; From 05e141181f9acd601d22c8172fc164ec582e7925 Mon Sep 17 00:00:00 2001 From: Martin Raszyk Date: Tue, 5 Sep 2023 14:46:03 +0200 Subject: [PATCH 13/13] fix Env for install_code --- spec/index.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/index.md b/spec/index.md index a143569b6..6b442e3c4 100644 --- a/spec/index.md +++ b/spec/index.md @@ -3780,8 +3780,8 @@ Env = { balance = S.balances[A.canister_id]; compute_allocation = S.compute_allocation[A.canister_id]; memory_allocation = S.memory_allocation[A.canister_id]; - memory_usage_raw_module = memory_usage_raw_module(S.canisters[A.canister_id].raw_module); - memory_usage_canister_history = memory_usage_canister_history(S.canister_history[A.canister_id]); + memory_usage_raw_module = memory_usage_raw_module(A.wasm_module); + memory_usage_canister_history = memory_usage_canister_history(New_canister_history); freezing_threshold = S.freezing_threshold[A.canister_id]; subnet_size = S.canister_subnet[A.canister_id].subnet_size; certificate = NoCertificate;