From 18bc24e152e3eae4e1d4595dd896dc766be32433 Mon Sep 17 00:00:00 2001 From: bogwar <51327868+bogwar@users.noreply.github.com> Date: Tue, 6 Dec 2022 16:41:06 +0100 Subject: [PATCH 1/3] new release --- spec/changelog.adoc | 6 + spec/ic0.txt | 15 +- spec/index.adoc | 430 ++++++++++++++++++++++++++++++++++---------- 3 files changed, 348 insertions(+), 103 deletions(-) diff --git a/spec/changelog.adoc b/spec/changelog.adoc index c423c3dcd..366abc2f2 100644 --- a/spec/changelog.adoc +++ b/spec/changelog.adoc @@ -1,6 +1,12 @@ [#changelog] == Changelog +[#0_18_9] +=== 0.18.9 (2022-12-06) +* Global timers +* Canister version +* Clarifications for HTTP requests & Bitcoin integration costs + [#0_18_8] === 0.18.8 (2022-11-09) * Updated HTTP request API diff --git a/spec/ic0.txt b/spec/ic0.txt index a37d2f8ff..a553089d3 100644 --- a/spec/ic0.txt +++ b/spec/ic0.txt @@ -28,7 +28,7 @@ ic0.msg_method_name_size : () -> i32; // F ic0.msg_method_name_copy : (dst : i32, offset : i32, size : i32) -> (); // F ic0.accept_message : () -> (); // F -ic0.call_new : // U Ry Rt H +ic0.call_new : // U Ry Rt T ( callee_src : i32, callee_size : i32, name_src : i32, @@ -38,11 +38,11 @@ ic0.call_new : // U reject_fun : i32, reject_env : i32 ) -> (); -ic0.call_on_cleanup : (fun : i32, env : i32) -> (); // U Ry Rt H -ic0.call_data_append : (src : i32, size : i32) -> (); // U Ry Rt H -ic0.call_cycles_add : (amount : i64) -> (); // U Ry Rt H -ic0.call_cycles_add128 : (amount_high : i64, amount_low: i64) -> (); // U Ry Rt H -ic0.call_perform : () -> ( err_code : i32 ); // U Ry Rt H +ic0.call_on_cleanup : (fun : i32, env : i32) -> (); // U Ry Rt T +ic0.call_data_append : (src : i32, size : i32) -> (); // U Ry Rt T +ic0.call_cycles_add : (amount : i64) -> (); // U Ry Rt T +ic0.call_cycles_add128 : (amount_high : i64, amount_low: i64) -> (); // U Ry Rt T +ic0.call_perform : () -> ( err_code : i32 ); // U Ry Rt T ic0.stable_size : () -> (page_count : i32); // * ic0.stable_grow : (new_pages : i32) -> (old_page_count : i32); // * @@ -53,12 +53,13 @@ ic0.stable64_grow : (new_pages : i64) -> (old_page_count : i64); // * ic0.stable64_write : (offset : i64, src : i64, size : i64) -> (); // * ic0.stable64_read : (dst : i64, offset : i64, size : i64) -> (); // * -ic0.certified_data_set : (src: i32, size: i32) -> (); // I G U Ry Rt H +ic0.certified_data_set : (src: i32, size: i32) -> (); // I G U Ry Rt T ic0.data_certificate_present : () -> i32; // * ic0.data_certificate_size : () -> i32; // * ic0.data_certificate_copy : (dst: i32, offset: i32, size: i32) -> (); // * ic0.time : () -> (timestamp : i64); // * +ic0.global_timer_set : (timestamp : i64) -> i64; // I U Ry Rt C T ic0.performance_counter : (counter_type : i32) -> (counter : i64); // * s ic0.debug_print : (src : i32, size : i32) -> (); // * s diff --git a/spec/index.adoc b/spec/index.adoc index 4cb1f6820..b120d2266 100644 --- a/spec/index.adoc +++ b/spec/index.adoc @@ -1,6 +1,6 @@ = The Internet Computer Interface Specification DFINITY Foundation -0.18.8 +0.18.9 // the following are ways to make this document work both in antora and stand alone :example: example$ :partial: partial$ @@ -225,14 +225,14 @@ NOTE: Once the IC frees the resources of a canister, its id, _cycles_ balance, a The canister status can be used to control whether the canister is processing calls: * In status `running`, calls to the canister are processed as normal. -* In status `stopping`, calls to the canister are rejected by the IC, but responses to the canister are processed as normal. -* In status `stopped`, calls to the canister are rejected by the IC, and there are no outstanding responses to call contexts that are not marked as deleted. +* In status `stopping`, calls to the canister are rejected by the IC with reject code `CANISTER_ERROR` (5), but responses to the canister are processed as normal. +* In status `stopped`, calls to the canister are rejected by the IC with reject code `CANISTER_ERROR` (5), and there are no outstanding responses to call contexts that are not marked as deleted. In all cases, calls to the <> are processed, regardless of the state of the managed canister. The controllers of the canister can initiate transitions between these states using <> and <>, and query the state using <> (NB: this call returns additional information, such as the cycle balance of the canister). The canister itself can also query its state using <>. -NOTE: This status is orthogonal to whether a canister is empty or not: an empty canister can be in status `running`. Calls to such a canister are still rejected, but because the canister is empty. +NOTE: This status is orthogonal to whether a canister is empty or not: an empty canister can be in status `running`. Calls to such a canister are still rejected by the IC with an HTTP error, but because the canister is empty. [#signatures] === Signatures @@ -886,6 +886,7 @@ In order for a WebAssembly module to be usable as the code for the canister, it * If it exports a function called `canister_init`, the function must have type `+() -> ()+`. * If it exports a function called `canister_inspect_message`, the function must have type `+() -> ()+`. * If it exports a function called `canister_heartbeat`, the function must have type `+() -> ()+`. +* If it exports a function called `canister_global_timer`, the function must have type `+() -> ()+`. * If it exports any functions called `canister_update ` or `canister_query ` for some `name`, the functions must have type `+() -> ()+`. * It may not export both `canister_update ` and `canister_query ` with the same `name`. * It may not export other methods the names of which start with the prefix `canister_` besides the methods allowed above. @@ -911,6 +912,7 @@ The canister provides entry points which are invoked by the IC under various cir * The canister may export a function with name `canister_post_upgrade` and type `+() -> ()+`. * The canister may export functions with name `canister_inspect_message` with type `+() -> ()+`. * The canister may export a function with name `canister_heartbeat` with type `+() -> ()+`. +* The canister may export a function with name `canister_global_timer` with type `+() -> ()+`. * The canister may export functions with name `canister_update ` and type `+() -> ()+`. * The canister may export functions with name `canister_query ` and type `+() -> ()+`. * The canister table may contain functions of type `+(env : i32) -> ()+` which may be used as callbacks for inter-canister calls. @@ -955,10 +957,20 @@ Eventually, a method will want to send a response, using `ic0.reply` or `ic0.rej For periodic or time-based execution, the WebAssembly module can export a function with name `canister_heartbeat`. The heartbeats scheduling algorithm is implementation-defined. -`canister_heartbeat` is triggered by the IC, and therefore has no arguments, no caller, and cannot reply or reject. +`canister_heartbeat` is triggered by the IC, and therefore has no arguments, no caller, and cannot reply or reject. Still, the function `canister_heartbeat` can initiate new calls. NOTE: While an implementation will likely try to keep the interval between `canister_heartbeat` invocations to within a few seconds, this is not formally part of this specification. +==== Global timer + +For time-based execution, the WebAssembly module can export a function with name `canister_global_timer`. This function is called if the canister has set its global timer (using the System API function `ic0.global_timer_set`) and the current time (as returned by the System API function `ic0.time`) has passed the value of the global timer. + +Once the function `canister_global_timer` is scheduled, the canister's global timer is deactivated. The global timer is also deactivated upon changes to the canister's Wasm module (calling `install_code`, `uninstall_code` methods of the management canister or if the canister runs out of cycles). In particular, the function `canister_global_timer` won't be scheduled again unless the canister sets the global timer again (using the System API function `ic0.global_timer_set`). The global timer scheduling algorithm is implementation-defined. + +`canister_global_timer` is triggered by the IC, and therefore has no arguments, no caller, and cannot reply or reject. Still, the function `canister_global_timer` can initiate new calls. + +NOTE: While an implementation will likely try to keep the interval between the value of the global timer and the time-stamp of the `canister_global_timer` invocation within a few seconds, this is not formally part of this specification. + ==== Callbacks Callbacks are addressed by their table index (as a proxy for a Wasm `funcref`). @@ -987,8 +999,8 @@ The comment after each function lists from where these functions may be invoked: * `C`: from a cleanup callback * `s`: the `(start)` module initialization function * `F`: from `canister_inspect_message` -* `H`: from `canister_heartbeat` -* `*` = `I G U Q Ry Rt C F H` (NB: Not `(start)`) +* `T`: from _system task_ (`canister_heartbeat` or `canister_global_timer`) +* `*` = `I G U Q Ry Rt C F T` (NB: Not `(start)`) If the canister invokes a system call from somewhere else, it will trap. @@ -1113,6 +1125,17 @@ Status `1` indicates running, `2` indicates stopping, and `3` indicates stopped. + Status `3` (stopped) can be observed, for example, in `canister_pre_upgrade` and can be used to prevent accidentally upgrading a canister that is not fully stopped. +[#system-api-canister-version] +=== 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 or settings, i.e., upon every successful management canister call of methods `update_settings`, `install_code`, and `uninstall_code` on that canister and code uninstallation due to that canister running out of cycles. The system can arbitrarily increment the canister version also if the canister's code and settings do not change. + +* `ic0.canister_version : () -> i64` ++ +returns the current canister version. + +During the canister upgrade process, `canister_pre_upgrade` sees the old counter value, and `canister_post_upgrade` sees the new counter value. + [#system-api-call] === Inter-canister method calls @@ -1376,6 +1399,17 @@ The times observed by different canisters are unrelated, and calls from one cani NOTE: While an implementation will likely try to keep the time returned by `ic0.time` close to the real time, this is not formally part of this specification. +[#global-timer] +=== Global timer + +The canister can set a global timer to make the system schedule a call to the exported `canister_global_timer` Wasm method after the specified time. The time must be provided as nanoseconds since 1970-01-01. + +`+ic0.global_timer_set : (timestamp : i64) -> i64+` + +The function returns the previous value of the timer. If no timer is set before invoking the function, then the function returns zero. + +Passing zero as an argument to the function deactivates the timer and thus prevents the system from scheduling calls to the canister's `canister_global_timer` Wasm method. + [#system-api-performance-counter] === Performance counter @@ -1663,29 +1697,36 @@ It is important to note the following for the usage of the `POST` method: For security reasons, only HTTPS connections are allowed (URLs must start with `https://`). The IC uses industry-standard root CA lists to validate certificates of remote web servers. -Each request can specify the maximal expected size for the response from the remote HTTP server. The upper limit on the size of a response defaults to `2MiB` if no maximal size value is specified. -An error will be returned when the response is larger than the maximal size. -The `2MiB` size limit also applies to the value returned by the `transform` function. +The *size* of an HTTP request from the canister or an HTTP response from the remote HTTP server is the total number of bytes representing the names and values of HTTP headers and the HTTP body. The maximal size for the request from the canister is `2MB` (`2,000,000B`). Each request can specify a maximal size for the response from the remote HTTP server. The upper limit on the maximal size for the response is `2MB` (`2,000,000B`) and this value also applies if no maximal size value is specified. +An error will be returned when the request or response is larger than the maximal size. The following parameters should be supplied for the call: -- `url` - the requested URL. The URL may specify a custom port number. -- `max_response_bytes` - optional, specifies the maximal size of the response in bytes. Any value less than or equal to `2MiB` is accepted. The call will be charged based on this parameter. If not provided, the maximum of `2MiB` will be used. +- `url` - the requested URL. The URL must be valid according to https://www.ietf.org/rfc/rfc3986.txt[RFC-3986] and its length must not exceed `8192`. The URL may specify a custom port number. +- `max_response_bytes` - optional, specifies the maximal size of the response in bytes. If provided, the value must not exceed `2MB` (`2,000,000B`). The call will be charged based on this parameter. If not provided, the maximum of `2MB` will be used. - `method` - currently, only GET, HEAD, and POST are supported - `headers` - list of HTTP request headers and their corresponding values - `body` - optional, the content of the request's body - `transform` - an optional record that includes a function that transforms raw responses to sanitized responses, and a byte-encoded context that is provided to the function upon invocation, along with the response to be sanitized. If provided, the calling canister itself must export this function. +Cycles to pay for the call must be explicitly transferred with the call, i.e., they are not deducted from the caller's balance implicitly (e.g., as for inter-canister calls). + The returned response (and the response provided to the `transform` function, if specified) contains the following fields: - `status` - the response status (e.g., 200, 404) - `headers` - list of HTTP response headers and their corresponding values - `body` - the response's body -The `transform` function may, for example, transform the body in any way, add or remove headers, modify headers, etc. -When the transform function was invoked due to a canister HTTP request, the caller's identity is the principal of the management canister. +The `transform` function may, for example, transform the body in any way, add or remove headers, modify headers, etc. The maximal number of bytes representing the response produced by the `transform` function is `2MB` (`2,000,000B`). Note that the number of bytes representing the response produced by the `transform` function includes the serialization overhead of the encoding produced by the canister. + +When the transform function is invoked by the system due to a canister HTTP request, the caller's identity is the principal of the management canister. This information can be used by developers to implement access control mechanism for this function. -NOTE: The identity of the caller for a valid invocation of the `transform` function is `aaaaa-aa`. This information can be used by developers to implement access control mechanism for this function. +The following additional limits apply to HTTP requests and HTTP responses from the remote sever: +- the number of headers must not exceed `64`, +- the number of bytes representing a header name or value must not exceed `8KiB`, and +- the total number of bytes representing the header names and values must not exceed `48KiB`. + +NOTE: Currently, the Internet Computer mainnet only supports URLs that resolve to IPv6 destinations (i.e., the domain has a `AAAA` DNS record) in HTTP requests. [#ic-provisional_create_canister_with_cycles] === IC method `provisional_create_canister_with_cycles` @@ -1715,7 +1756,7 @@ NOTE: The IC Bitcoin API is considered EXPERIMENTAL. Canister developers must be The Bitcoin functionality is exposed via the management canister. Information about Bitcoin can be found in the https://developer.bitcoin.org/devguide/[Bitcoin developer guides]. -Invoking the functions of the Bitcoin API will cost cycles. The concrete costs for each function are yet to be determined. +Invoking the functions of the Bitcoin API will cost cycles. We refer the reader to the [Bitcoin documentation](https://internetcomputer.org/docs/current/developer-docs/integrations/bitcoin/bitcoin-how-it-works) for further relevant information and the [IC pricing page](https://internetcomputer.org/docs/current/developer-docs/deploy/computation-and-storage-costs) for information on pricing for the Bitcoin mainnet and testnet. [#ic-bitcoin_get_utxos] === IC method `bitcoin_get_utxos` @@ -1753,8 +1794,8 @@ For a newly discovered block, a regular Bitcoin (full) node therefore provides a than the Bitcoin component, which implies that it is advisable to set the number of confirmations to a reasonably large value, such as 6, to gain confidence in the correctness of the returned UTXOs. -There is an upper bound of 100,000 UTXOs that can be returned in a single request. For addresses that contain sufficiently large UTXOs, -the partial set of the address' UTXOs are returned along with a page reference. +There is an upper bound of 10,000 UTXOs that can be returned in a single request. For addresses that contain sufficiently many UTXOs, +a partial set of the address's UTXOs are returned along with a page reference. In the second case, a page reference (a series of bytes) must be provided, which instructs the Bitcoin component to collect UTXOs starting from the corresponding "page". @@ -1798,12 +1839,7 @@ If at least one of these checks fails, the call is rejected. If the transaction passes these tests, the transaction is forwarded to the specified Bitcoin network. - -The Bitcoin component periodically forwards the transaction -until the transaction appears in a block appended to the blockchain or the transaction -times out after 24 hours. As soon as it appears in a block or expires, -the Bitcoin component drops the transaction. -It follows that the function does not provide any guarantees that a submitted +Note that the function does not provide any guarantees that a submitted transaction will ever appear in a block. [#ic-bitcoin_get_current_fee_percentiles] @@ -1813,9 +1849,12 @@ The transaction fees in the Bitcoin network change dynamically based on the numb pending transactions. It must be possible for a canister to determine an adequate fee when creating a Bitcoin transaction. -This function returns the 100 fee percentiles, measured in millisatoshi/vbyte (1000 millisatoshi = 1 satoshi), over the last 10,000 transactions in the specified network, i.e., +This function returns fee percentiles, measured in millisatoshi/vbyte (1000 millisatoshi = 1 satoshi), over the last 10,000 transactions in the specified network, i.e., over the transactions in the last approximately 4-10 blocks. +The https://en.wikipedia.org/wiki/Percentile#The_nearest-rank_method[standard nearest-rank estimation method], inclusive, with the addition of a 0th percentile is used. +Concretely, for any i from 1 to 100, the ith percentile is the fee with rank `⌈i * 100⌉`. The 0th percentile is defined as the smallest fee (excluding coinbase transactions). + [#certification] == Certification @@ -2285,12 +2324,15 @@ Arg = Blob; CallerId = Principal; Timestamp = Nat; +CanisterVersion = Nat; Env = { - time : Timestamp + time : Timestamp; + global_timer : Nat; balance : Nat; freezing_limit : Nat; - certificate : NoCertificate | Blob - status : Running | Stopping | Stopped + certificate : NoCertificate | Blob; + status : Running | Stopping | Stopped; + canister_version : CanisterVersion; } RejectCode = Nat @@ -2306,7 +2348,8 @@ MethodCall = { UpdateFunc = WasmState -> Trap { cycles_used : Nat; } | Return { new_state : WasmState; new_calls : List MethodCall; - new_certified_data : NoCertifiedData | Blob + new_certified_data : NoCertifiedData | Blob; + new_global_timer : NoGlobalTimer | Nat; response : NoResponse | Response; cycles_accepted : Nat; cycles_used : Nat; @@ -2315,8 +2358,11 @@ QueryFunc = WasmState -> Trap { cycles_used : Nat; } | Return { response : Response; cycles_used : Nat; } -HeartbeatFunc = WasmState -> Trap { cycles_used : Nat; } | Return { +SystemTaskFunc = WasmState -> Trap { cycles_used : Nat; } | Return { new_state : WasmState; + new_calls : List MethodCall; + new_certified_data : NoCertifiedData | Blob; + new_global_timer : NoGlobalTimer | Nat; cycles_used : Nat; } @@ -2326,19 +2372,25 @@ RefundedCycles = Nat CanisterModule = { init : (CanisterId, Arg, CallerId, Env) -> Trap { cycles_used : Nat; } | Return { new_state : WasmState; + new_certified_data : NoCertifiedData | Blob; + new_global_timer : NoGlobalTimer | Nat; cycles_used : Nat; } pre_upgrade : (WasmState, Principal, Env) -> Trap { cycles_used : Nat; } | Return { stable_memory : StableMemory; + new_certified_data : NoCertifiedData | Blob; cycles_used : Nat; } post_upgrade : (CanisterId, StableMemory, Arg, CallerId, Env) -> Trap { cycles_used : Nat; } | Return { new_state : WasmState; + new_certified_data : NoCertifiedData | Blob; + new_global_timer : NoGlobalTimer | Nat; cycles_used : Nat; } update_methods : MethodName ↦ ((Arg, CallerId, Env, AvailableCycles) -> UpdateFunc) query_methods : MethodName ↦ ((Arg, CallerId, Env) -> QueryFunc) - heartbeat : (Env) -> HeartbeatFunc + heartbeat : (Env) -> SystemTaskFunc + global_timer : (Env) -> SystemTaskFunc callbacks : (Callback, Response, RefundedCycles, Env, AvailableCycles) -> UpdateFunc inspect_message : (MethodName, WasmState, Arg, CallerId, Env) -> Trap { cycles_used : Nat; } | Return { status : Accept | Reject; @@ -2387,7 +2439,7 @@ CallOrigin calling_context : CallId; callback: Callback } - | FromHeartbeat + | FromSystem CallCtxt = { canister : CanisterId; origin : CallOrigin; @@ -2408,6 +2460,7 @@ EntryPoint = PublicMethod MethodName Principal Blob | Callback Callback Response RefundedCycles | Heartbeat + | GlobalTimer Message = CallMessage { @@ -2524,12 +2577,14 @@ CanStatus | Stopping (List (CallOrigin, Nat)) | Stopped S = { - requests : Request ↦ RequestStatus; + requests : Request ↦ (RequestStatus, Principal); canisters : CanisterId ↦ CanState; controllers : CanisterId ↦ Set Principal; freezing_threshold : CanisterId ↦ Nat; canister_status: CanisterId ↦ CanStatus; + canister_version: CanisterId ↦ CanisterVersion; time : CanisterId ↦ Timestamp; + global_timer : CanisterId ↦ Timestamp; balances: CanisterId ↦ Nat; certified_data: CanisterId ↦ Blob; system_time : Timestamp @@ -2556,7 +2611,9 @@ The initial state of the IC is controllers = (); freezing_threshold = (); canister_status = (); + canister_version = (); time = (); + global_timer = (); balances = (); certified_data = (); system_time = T; @@ -2690,10 +2747,12 @@ Conditions:: S.canisters[E.content.canister_id] ≠ EmptyCanister Env = { time = S.time[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); certificate = NoCertificate; status = simple_status(S.canister_status[E.content.canister_id]); + canister_version = S.canister_version[E.content.canister_id]; } 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; cycles_used = Cycles_used;} @@ -2703,7 +2762,7 @@ Conditions:: State after:: .... S with - requests[E.content] = Received + requests[E.content] = (Received, ECID) if E.content.canister_id ≠ ic_principal then balances[E.content.canister_id] = S.balances[E.content.canister_id] - Cycles_used .... @@ -2716,13 +2775,13 @@ The IC may reject a received message for internal reasons (high load, low resour Conditions:: .... - S.requests[R] = Received + S.requests[R] = (Received, ECID) Code = SYS_FATAL or Code = SYS_TRANSIENT .... State after:: .... S with - requests[R] = Rejected (Code, Msg) + requests[R] = (Rejected (Code, Msg), ECID) .... ==== Initiating canister calls @@ -2735,14 +2794,14 @@ The IC does not make any guarantees about the order of incoming messages. Conditions:: .... - S.requests[R] = Received + S.requests[R] = (Received, ECID) S.system_time <= R.ingress_expiry C = S.canisters[R.canister_id] .... State after:: .... S with - requests[R] = Processing + requests[R] = (Processing, ECID) messages = CallMessage { origin = FromUser { request = R }; @@ -2780,7 +2839,7 @@ State after:: ==== Call context creation -Before invoking a heartbeat or a message to a public entry point, a call context is created for bookkeeping purposes. +Before invoking a heartbeat, a global timer, or a message to a public entry point, a call context is created for bookkeeping purposes. For these invocations the canister must be running (so not stopped, or stopping). Additionally, these invocations only happen for "real" canisters, not the IC management canister. @@ -2834,7 +2893,7 @@ Conditions:: .... S.canisters[C] ≠ EmptyCanister S.canister_status[C] = Running - balances[C] ≥ freezing_limit(S, C) + MAX_CYCLES_PER_MESSAGE + S.balances[C] ≥ freezing_limit(S, C) + MAX_CYCLES_PER_MESSAGE Ctxt_id ∉ dom(S.call_contexts) .... + @@ -2852,11 +2911,49 @@ S with · S.messages call_contexts[Ctxt_id] = { canister = C; - origin = FromHeartbeat; + origin = FromSystem; + needs_to_respond = false; + deleted = false; + available_cycles = 0; + } + balances[C] = S.balances[C] - MAX_CYCLES_PER_MESSAGE +.... + +* Call context creation: Global timer ++ +If canister `C` exports a method with name `canister_global_timer`, the global timer of canister `C` is set, and the current time for canister `C` has passed the value of the global timer, the IC will create the corresponding call context and deactivate the global timer. ++ +Conditions:: ++ +.... + 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 + Ctxt_id ∉ dom(S.call_contexts) +.... ++ +State after:: ++ +.... +S with + messages = + FuncMessage { + call_context = Ctxt_id; + receiver = C; + entry_point = GlobalTimer; + queue = Queue { from = System; to = C }; + } + · S.messages + call_contexts[Ctxt_id] = { + canister = C; + origin = FromSystem; needs_to_respond = false; deleted = false; available_cycles = 0; } + global_timer[C] = 0 balances[C] = S.balances[C] - MAX_CYCLES_PER_MESSAGE .... @@ -2880,10 +2977,12 @@ Conditions:: Env = { time = S.time[M.receiver]; + global_timer = S.global_timer[M.receiver]; balance = S.balances[M.receiver] freezing_limit = freezing_limit(S, M.receiver); certificate = NoCertificate; status = simple_status(S.canister_status[M.receiver]); + canister_version = S.canister_version[M.receiver]; } Available = S.call_contexts[M.call_contexts].available_cycles @@ -2896,7 +2995,11 @@ Conditions:: ) or ( M.entry_point = Heartbeat - F = heartbeat_as_update(Mod.heartbeat, Env) + F = system_task_as_update(Mod.heartbeat, Env) + ) + or + ( M.entry_point = GlobalTimer + F = system_task_as_update(Mod.global_timer, Env) ) R = F(S.canisters[M.receiver].wasm_state) @@ -2949,6 +3052,9 @@ then if res.new_certified_data ≠ NoCertifiedData: certified_data[M.receiver] = res.new_certified_data + if res.new_global_timer ≠ NoGlobalTimer: + global_timer[M.receiver] = res.new_global_timer + balances[M.receiver] = New_balance else S with @@ -2978,7 +3084,7 @@ If message execution <>; that would require a (unique) call to `ic0.reply`. Note also that the state changes are persisted even when the IC is set to synthesize a <> reject immediately afterward (which happens when this returns without calling `ic0.reply` or `ic0.reject`, the corresponding call has not been responded to and there are no outstanding callbacks, see <>). -The functions `query_as_update` and `heartbeat_as_update` turns a query function resp the heartbeat into an update function; this is merely a notational trick to simplify the rule: +The functions `query_as_update` and `system_task_as_update` turns a query function 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 @@ -2987,18 +3093,20 @@ query_as_update(f, arg, env) = λ wasm_state → new_state = wasm_state; new_calls = []; new_certified_data = NoCertifiedData; + new_global_timer = NoGlobalTimer; response = res.response; cycles_accepted = 0; cycles_used = res.cycles_used; } -heartbeat_as_update(f, env) = λ wasm_state → +system_task_as_update(f, env) = λ wasm_state → match f(env)(wasm_state) with Trap trap → Trap trap Return res → Return { new_state = res.new_state; - new_calls = []; - new_certified_data = NoCertifiedData; + new_calls = res.new_calls; + new_certified_data = res.new_certified_data; + new_global_timer = res.new_global_timer; response = NoResponse; cycles_accepted = 0; cycles_used = res.cycles_used; @@ -3009,12 +3117,12 @@ Note that by construction, a query function will either trap or return with a re [#rule-starvation] ==== Call context starvation -If the call context is not for heartbeat and there is no call, downstream calling context or response that could possibly fulfill a calling context, then a reject is synthesized. The error message below is _not_ indicative. In particular, if the IC has an idea about _why_ this starved, it can put that in there (e.g. the initial message handler trapped with an out-of-memory access). +If the call context is not for heartbeat or global timer and there is no call, downstream calling context or response that could possibly fulfill a calling context, then a reject is synthesized. The error message below is _not_ indicative. In particular, if the IC has an idea about _why_ this starved, it can put that in there (e.g. the initial message handler trapped with an out-of-memory access). Conditions:: .... S.call_contexts[Ctxt_id].needs_to_respond = true - S.call_contexts[Ctxt_id].origin ≠ FromHeartbeat + S.call_contexts[Ctxt_id].origin ≠ FromSystem ∀ CallMessage {origin = FromCanister O, …} ∈ S.messages. O.calling_context ≠ Ctxt_id ∀ ResponseMessage {origin = FromCanister O, …} ∈ S.messages. O.calling_context ≠ Ctxt_id ∀ _ ↦ {needs_to_respond = true, origin = FromCanister O, …} ∈ S.call_contexts: O.calling_context ≠ Ctxt_id @@ -3035,7 +3143,7 @@ S with ==== Call context removal -If there is no call, downstream calling context, or response that references a call context, and the call context has been replied to or the call context corresponds to a heartbeat that had already been executed, then the call context can be removed. +If there is no call, downstream calling context, or response that references a call context, and the call context has been replied to or the call context corresponds to a heartbeat or global timer that had already been executed, then the call context can be removed. Conditions:: .... @@ -3043,7 +3151,7 @@ Conditions:: S.call_contexts[Ctxt_id].needs_to_respond = false ) or ( - S.call_contexts[Ctxt_id].origin = FromHeartbeat + S.call_contexts[Ctxt_id].origin = FromSystem ∀ FuncMessage M ∈ S.messages. M.call_context ≠ Ctxt_id ) ∀ CallMessage {origin = FromCanister O, …} ∈ S.messages. O.calling_context ≠ Ctxt_id @@ -3082,6 +3190,7 @@ State after:: S with canisters[CanisterId] = EmptyCanister time[CanisterId] = CurrentTime + global_timer[CanisterId] = 0 if A.settings.controllers is not null: controllers[CanisterId] = A.settings.controllers else: @@ -3099,6 +3208,7 @@ S with refunded_cycles = 0 } canister_status[CanisterId] = Running + canister_version[CanisterId] = 0 .... This uses the predicate @@ -3136,6 +3246,7 @@ S with controllers[A.canister_id] = A.settings.controllers 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 messages = Older_messages · Younger_messages · ResponseMessage { origin = M.origin @@ -3201,12 +3312,14 @@ Conditions:: M.caller ∈ S.controllers[A.canister_id] Env = { time = S.time[A.canister_id]; + global_timer = S.global_timer[A.canister_id]; balance = S.balances[A.canister_id]; freezing_limit = freezing_limit(S, A.canister_id); 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; cycles_used = Cycles_used;} + 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;} Cycles_used ≤ S.balances[A.canister_id] dom(Mod.update_methods) ∩ dom(Mod.query_methods) = ∅ @@ -3221,6 +3334,13 @@ S with public_custom_sections = Public_custom_sections; private_custom_sections = Private_custom_sections; } + if New_certified_data ≠ NoCertifiedData: + certified_data[A.canister_id] = New_certified_data + if New_global_timer ≠ NoGlobalTimer: + global_timer[A.canister_id] = New_global_timer + else: + 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 messages = Older_messages · Younger_messages · ResponseMessage { @@ -3254,8 +3374,16 @@ Conditions:: certificate = NoCertificate; status = simple_status(S.canister_status[A.canister_id]); } - Old_module.pre_upgrade(Old_State, M.caller, Env) = Return {stable_memory = Stable_memory; cycles_used = Cycles_used;} - Mod.post_upgrade(A.canister_id, Stable_memory, A.arg, M.caller, Env) = Return {new_state = New_state; cycles_used = Cycles_used';} + Env1 = Env with { + global_timer = S.global_timer[A.canister_id]; + canister_version = S.canister_version[A.canister_id]; + } + 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 { + global_timer = 0; + 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';} Cycles_used + Cycles_used' ≤ S.balances[A.canister_id] dom(Mod.update_methods) ∩ dom(Mod.query_methods) = ∅ .... @@ -3269,6 +3397,15 @@ S with public_custom_sections = Public_custom_sections; private_custom_sections = Private_custom_sections; } + if New_certified_data' ≠ NoCertifiedData: + certified_data[A.canister_id] = New_certified_data' + else if New_certified_data ≠ NoCertifiedData: + certified_data[A.canister_id] = New_certified_data + if New_global_timer ≠ NoGlobalTimer: + global_timer[A.canister_id] = New_global_timer + else: + 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'); messages = Older_messages · Younger_messages · ResponseMessage { @@ -3297,6 +3434,8 @@ State after:: S with canisters[A.canister_id] = EmptyCanister certified_data[A.canister_id] = "" + canister_version[A.canister_id] = S.canister_version[A.canister_id] + 1 + global_timer[A.canister_id] = 0 messages = Older_messages · Younger_messages · ResponseMessage { @@ -3489,7 +3628,9 @@ S with controllers[A.canister_id] = (deleted) freezing_threshold[A.canister_id] = (deleted) canister_status[A.canister_id] = (deleted) + canister_version[A.canister_id] = (deleted) time[A.canister_id] = (deleted) + global_timer[A.canister_id] = (deleted) balances[A.canister_id] = (deleted) certified_data[A.canister_id] = (deleted) messages = Older_messages · Younger_messages · @@ -3569,6 +3710,7 @@ State after:: S with canisters[CanisterId] = EmptyCanister time[CanisterId] = CurrentTime + global_timer[CanisterId] = 0 if A.settings.controllers is not null: controllers[CanisterId] = A.settings.controllers else: @@ -3589,6 +3731,7 @@ S with refunded_cycles = M.transferred_cycles } canister_status[CanisterId] = Running + canister_version[CanisterId] = 0 .... ==== IC Management Canister: Top up canister @@ -3669,15 +3812,15 @@ Conditions:: .... S.messages = Older_messages · ResponseMessage RM · Younger_messages RM.origin = FromUser { request = M } - S.requests[M] = Processing + S.requests[M] = (Processing, ECID) .... State after:: .... S with messages = Older_messages · Younger_messages requests[M] = - | Replied R if M.response = Reply R - | Rejected (c, R) if M.response = Reject (c, R) + | (Replied R, ECID) if M.response = Reply R + | (Rejected (c, R), ECID) if M.response = Reject (c, R) .... NB: The refunded cycles, `RM.refunded_cycles` are, by construction, empty. @@ -3688,12 +3831,12 @@ The IC will keep the data for a completed or rejected request around for a certa Conditions:: .... - (S.requests[M] = Replied _) or (S.requests[M] = Rejected _) + (S.requests[M] = (Replied _, ECID)) or (S.requests[M] = (Rejected _, ECID)) .... State after:: .... S with - requests[M] = Done + requests[M] = (Done, ECID) .... @@ -3701,7 +3844,7 @@ At the same or some later point, the request will be removed from the state of t Conditions:: .... - (S.requests[M] = Replied _) or (S.requests[M] = Rejected _) or (S.requests[M] = Done) + (S.requests[M] = (Replied _, _)) or (S.requests[M] = (Rejected _, _)) or (S.requests[M] = (Done, _)) M.ingress_expiry < S.system_time .... State after:: @@ -3722,7 +3865,9 @@ State after:: .... S with canisters[CanisterId] = EmptyCanister - certified_data[Canister_id] = "" + certified_data[CanisterId] = "" + canister_version[CanisterId] = S.canister_version[CanisterId] + 1 + global_timer[CanisterId] = 0 messages = S.messages · [ ResponseMessage { @@ -3743,7 +3888,7 @@ S with .... -==== Time progressing and cycle consumption +==== Time progressing, cycle consumption, and canister version increments Time progresses. Abstractly, it does so independently for each canister, and in unspecified intervals. @@ -3784,6 +3929,19 @@ S with system_time = T1 .... +Finally, the canister version can be incremented arbitrarily: + +Conditions:: +.... + N0 = S.canister_version[CanisterId] + N1 > N0 +.... +State after:: +.... +S with + canister_version[CanisterId] = N1 +.... + ==== Query call Canister query calls to `/api/v2/canister//query` can be executed directly. They can only be executed against canisters which have a status of `Running` and are also not frozen. @@ -3806,10 +3964,12 @@ Conditions:: lookup(["time"], Cert) = Found S.system_time // or “recent enough” Env = { time = S.time[Q.receiver]; + global_timer = S.global_timer[Q.receiver]; balance = S.balances[Q.canister_id]; freezing_limit = freezing_limit(S, Q.canister_id); certificate = Cert; status = simple_status(S.canister_status[Q.receiver]); + canister_version = S.canister_version[Q.receiver]; } .... Read response:: @@ -3955,7 +4115,9 @@ ExecutionState = { pending_call : MethodCall | NoPendingCall; calls : List MethodCall; new_certified_data : NoCertifiedData | Blob; + new_global_timer : NoGlobalTimer | Nat; ingress_filter : Accept | Reject; + context : I | G | U | Q | Ry | Rt | C | F | T; } .... @@ -3994,7 +4156,9 @@ empty_execution_state = { pending_call = NoPendingCall; calls = []; new_certified_data = NoCertifiedData; + new_global_timer = NoGlobalTimer; ingress_filter = Reject; + context = (undefined); } .... @@ -4005,7 +4169,12 @@ If the WebAssembly module does not export a function called under the name `cani + .... init = λ (self_id, arg, caller, sysenv) → - Return {new_state = { store = initial_wasm_store; self_id = self_id; stable_mem = "" }; cycles_used = 0;} + Return { + new_state = { store = initial_wasm_store; self_id = self_id; stable_mem = "" }; + new_certified_data = NoCertifiedData; + new_global_timer = NoGlobalTimer; + cycles_used = 0; + } .... + Otherwise, if the WebAssembly module exports a function `func` under the name `canister_init`, it is @@ -4016,12 +4185,15 @@ init = λ (self_id, arg, caller, sysenv) → wasm_state = { store = initial_wasm_store; self_id = self_id; stable_mem = "" } params = empty_params with { arg = arg; caller = caller; sysenv } balance = sysenv.balance + context = I } try func() with Trap then Trap {cycles_used = es.cycles_used;} - if es.calls ≠ [] then Trap {cycles_used = es.cycles_used;} - if es.response ≠ NoResponse then Trap {cycles_used = es.cycles_used;} - if es.ingress_filter ≠ Reject then Trap {cycles_used = es.cycles_used;} - Return {new_state = es.wasm_state; cycles_used = es.cycles_used;} + Return { + new_state = es.wasm_state; + new_certified_data = es.new_certified_data; + new_global_timer = es.new_global_timer; + cycles_used = es.cycles_used; + } .... + This formulation checks afterwards that the system calls `call.perform` or `msg.reply` were not invoked; an implementation can of course trap as soon as these system calls are invoked. @@ -4031,7 +4203,7 @@ This formulation checks afterwards that the system calls `call.perform` or `msg. If the WebAssembly module does not export a function called under the name `canister_pre_upgrade`, then it simply returns the stable memory: + .... -pre_upgrade = λ (old_state, caller, sysenv) → Return {stable_memory = old_state.stable_mem; cycles_used = 0;} +pre_upgrade = λ (old_state, caller, sysenv) → Return {stable_memory = old_state.stable_mem; new_certified_data = NoCertifiedData; cycles_used = 0;} .... + Otherwise, if the WebAssembly module exports a function `func` under the name `canister_pre_upgrade`, it is @@ -4042,12 +4214,14 @@ pre_upgrade = λ (old_state, caller, sysenv) → wasm_state = old_state params = { empty_params with caller = caller; sysenv } balance = sysenv.balance + context = G } try func() with Trap then Trap {cycles_used = es.cycles_used;} - if es.calls ≠ [] then Trap {cycles_used = es.cycles_used;} - if es.response ≠ NoResponse then Trap {cycles_used = es.cycles_used;} - if es.ingress_filter ≠ Reject then Trap {cycles_used = es.cycles_used;} - Return {stable_memory = es.wasm_state.stable_mem; cycles_used = es.cycles_used;} + Return { + stable_memory = es.wasm_state.stable_mem; + new_certified_data = es.new_certified_data; + cycles_used = es.cycles_used; + } .... @@ -4057,7 +4231,7 @@ If the WebAssembly module does not export a function called under the name `cani + .... post_upgrade = λ (self_id, stable_mem, arg, caller, sysenv) → - Return {new_state = { store = initial_wasm_store; self_id = self_id; stable_mem = stable_mem }; cycles_used = 0;} + Return {new_state = { store = initial_wasm_store; self_id = self_id; stable_mem = stable_mem }; new_certified_data = NoCertifiedData; new_global_timer = NoGlobalTimer; cycles_used = 0;} .... + Otherwise, if the WebAssembly module exports a function `func` under the name `canister_post_upgrade`, it is @@ -4068,12 +4242,15 @@ post_upgrade = λ (self_id, stable_mem, arg, caller, sysenv) → wasm_state = { store = initial_wasm_store; self_id = self_id; stable_mem = stable_mem } params = { empty_params with arg = arg; caller = caller; sysenv } balance = sysenv.balance + context = I } try func() with Trap then Trap {cycles_used = es.cycles_used;} - if es.calls ≠ [] then Trap {cycles_used = es.cycles_used;} - if es.response ≠ NoResponse then Trap {cycles_used = es.cycles_used;} - if es.ingress_filter ≠ Reject then Trap {cycles_used = es.cycles_used;} - Return {new_state = es.wasm_state; cycles_used = es.cycles_used;} + Return { + new_state = es.wasm_state; + new_certified_data = es.new_certified_data; + new_global_timer = es.new_global_timer; + cycles_used = es.cycles_used; + } .... * The partial map `update_methods` of the `CanisterModule` is defined for all method names `method` for which the WebAssembly program exports a function `func` named `canister_update `, and has value @@ -4085,16 +4262,17 @@ update_methods[method] = λ (arg, caller, sysenv, available) → λ wasm_state params = empty_params with { arg = arg; caller = caller; sysenv } balance = sysenv.balance cycles_available = available; + context = U } try func() with Trap then Trap {cycles_used = es.cycles_used;} - if es.ingress_filter ≠ Reject then Trap {cycles_used = es.cycles_used;} Return { new_state = es.wasm_state; new_calls = es.calls; + new_certified_data = es.new_certified_data; + new_global_timer = es.new_global_timer; response = es.response; cycles_accepted = es.cycles_accepted; cycles_used = es.cycles_used; - new_certified_data = es.new_certified_data; } .... @@ -4106,12 +4284,9 @@ query_methods[method] = λ (arg, caller, sysenv) → λ wasm_state → wasm_state = wasm_state; params = empty_params with { arg = arg; caller = caller; sysenv } balance = sysenv.balance + context = Q } try func() with Trap then Trap {cycles_used = es.cycles_used;} - if es.cycles_accepted ≠ 0 then Trap {cycles_used = es.cycles_used;} - if es.calls ≠ [] then Trap {cycles_used = es.cycles_used;} - if es.ingress_filter ≠ Reject then Trap {cycles_used = es.cycles_used;} - if es.response = NoResponse then Trap {cycles_used = es.cycles_used;} Return { response = es.response; cycles_used = es.cycles_used; @@ -4130,13 +4305,14 @@ heartbeat = λ (sysenv) → λ wasm_state → wasm_state = wasm_state; params = empty_params with { arg = NoArg; caller = NoCaller; sysenv } balance = sysenv.balance + context = T } try func() with Trap then Trap {cycles_used = es.cycles_used;} - if es.cycles_accepted ≠ 0 then Trap {cycles_used = es.cycles_used;} - if es.ingress_filter ≠ Reject then Trap {cycles_used = es.cycles_used;} - if es.response ≠ NoResponse then Trap {cycles_used = es.cycles_used;} Return { new_state = es.wasm_state; + new_calls = es.calls; + new_certified_data = es.certified_data; + new_global_timer = es.new_global_timer; cycles_used = es.cycles_used; } .... @@ -4145,6 +4321,30 @@ otherwise it is heartbeat = λ (sysenv) → λ wasm_state → Trap {cycles_used = 0;} .... +* The function `global_timer` of the `CanisterModule` is defined if the WebAssembly program exports a function `func` named `canister_global_timer`, and has value ++ +.... +global_timer = λ (sysenv) → λ wasm_state → + let es = ref {empty_execution_state with + wasm_state = wasm_state; + params = empty_params with { arg = NoArg; caller = NoCaller; sysenv } + balance = sysenv.balance + context = T + } + try func() with Trap then Trap {cycles_used = es.cycles_used;} + Return { + new_state = es.wasm_state; + new_calls = es.calls; + new_certified_data = es.certified_data; + new_global_timer = es.new_global_timer; + cycles_used = es.cycles_used; + } +.... +otherwise it is +.... +global_timer = λ (sysenv) → λ wasm_state → Trap {cycles_used = 0;} +.... + * The function `callbacks` of the `CanisterModule` is defined as follows + .... @@ -4153,18 +4353,19 @@ callbacks = λ(callbacks, response, refunded_cycles, sysenv, available) → λ w sysenv cycles_refunded = refund_cycles; } - let (fun, env, params) = match response with + let (fun, env, params, context) = match response with Reply data -> (callbacks.on_reply.fun, callbacks.on_reply.env, - { params0 with data}) + { params0 with data}, Ry) Reject (reject_code, reject_message)-> (callbacks.on_reject.fun, callbacks.on_reject.env, - { params0 with reject_code; reject_message}) + { params0 with reject_code; reject_message}, Rt) let es = ref {empty_execution_state with wasm_state = wasm_state; params = params; balance = sysenv.balance; cycles_available = available; + context = context; } try if fun > |es.wasm_state.store.table| then Trap @@ -4175,10 +4376,11 @@ callbacks = λ(callbacks, response, refunded_cycles, sysenv, available) → λ w Return { new_state = es.wasm_state; new_calls = es.calls; + new_certified_data = es.certified_data; + new_global_timer = es.new_global_timer; response = es.response; cycles_accepted = es.cycles_accepted; cycles_used = es.cycles_used; - new_certified_data = es.certified_data; } with Trap if callbacks.on_cleanup = NoClosure then Trap {cycles_used = es.cycles_used;} @@ -4188,15 +4390,14 @@ callbacks = λ(callbacks, response, refunded_cycles, sysenv, available) → λ w let es' = ref { empty_execution_state with wasm_state = wasm_state; + context = C; } try func(callbacks.on_cleanup.env) with Trap then Trap {cycles_used = es.cycles_used + es'.cycles_used;} - if es'.cycles_accepted ≠ 0 then Trap {cycles_used = es.cycles_used + es'.cycles_used;} - if es'.calls ≠ [] then Trap {cycles_used = es.cycles_used + es'.cycles_used;} - if es'.ingress_filter ≠ Reject then Trap {cycles_used = es.cycles_used + es'.cycles_used;} - if es'.response ≠ NoResponse then Trap {cycles_used = es.cycles_used + es'.cycles_used;} Return { new_state = es'.wasm_state; new_calls = []; + new_certified_data = NoCertifiedData; + new_global_timer = es'.new_global_timer; response = NoResponse; cycles_accepted = 0; cycles_used = es.cycles_used + es'.cycles_used; @@ -4228,10 +4429,9 @@ inspect_message = λ (method_name, wasm_state, arg, caller, sysenv) → } balance = sysenv.balance; cycles_available = 0; // ingress requests have no funds + context = F; } try func() with Trap then Trap {cycles_used = es.cycles_used;} - if es.calls ≠ [] then Trap {cycles_used = es.cycles_used;} - if es.response ≠ NoResponse then Trap {cycles_used = es.cycles_used;} Return {status = es.ingress_filter; cycles_used = es.cycles_used;}; .... @@ -4268,67 +4468,85 @@ The pseudo-code below does _not_ explicitly enforce the restrictions of which im .... ic0.msg_arg_data_size() : i32 = + if es.context ∉ {I, U, Q, Ry, F} then Trap {cycles_used = es.cycles_used;} return |es.params.arg| ic0.msg_arg_data_copy(dst:i32, offset:i32, size:i32) = + if es.context ∉ {I, U, Q, Ry, F} then Trap {cycles_used = es.cycles_used;} copy_to_canister(dst, offset, size, es.params.arg) ic0.msg_caller_size() : i32 = + if es.context ∉ {I, G, U, Q, F} then Trap {cycles_used = es.cycles_used;} return |es.params.caller| ic0.msg_caller_copy(dst:i32, offset:i32, size:i32) : i32 = + if es.context ∉ {I, G, U, Q, F} then Trap {cycles_used = es.cycles_used;} copy_to_canister(dst, offset, size, es.params.caller) ic0.msg_reject_code() : i32 = + if es.context ∉ {Ry, Rt} then Trap {cycles_used = es.cycles_used;} es.params.reject_code ic0.msg_reject_msg_size() : i32 = + if es.context ∉ {Rt} then Trap {cycles_used = es.cycles_used;} return |es.params.reject_msg| ic0.msg_reject_msg_copy(dst:i32, offset:i32, size:i32) : i32 = + if es.context ∉ {Rt} then Trap {cycles_used = es.cycles_used;} copy_to_canister(dst, offset, size, es.params.reject_msg) ic0.msg_reply_data_append(src : i32, size : i32) = + if es.context ∉ {U, Q, Ry, Rt} then Trap {cycles_used = es.cycles_used;} if es.response ≠ NoResponse then Trap {cycles_used = es.cycles_used;} es.reply_params.arg := es.reply_params.arg · copy_from_canister(src, size) ic0.msg_reply() = + if es.context ∉ {U, Q, Ry, Rt} then Trap {cycles_used = es.cycles_used;} if es.response ≠ NoResponse then Trap {cycles_used = es.cycles_used;} es.response := Reply (es.reply_params.arg) es.cycles_available := 0 ic0.msg_reject(src : i32, size : i32) = + if es.context ∉ {U, Q, Ry, Rt} then Trap {cycles_used = es.cycles_used;} if es.response ≠ NoResponse then Trap {cycles_used = es.cycles_used;} es.response := Reject (CANISTER_REJECT, copy_from_canister(src, size)) es.cycles_available := 0 ic0.msg_cycles_available() : i64 = + if es.context ∉ {U, 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;} let amount = es.cycles_available copy_cycles_to_canister(dst, amount.to_little_endian_bytes()) ic0.msg_cycles_refunded() : i64 = + if es.context ∉ {Rt, Ry} then Trap {cycles_used = es.cycles_used;} if es.params.cycles_refunded >= 2^64^ then Trap {cycles_used = es.cycles_used;} return es.params.cycles_refunded ic0.msg_cycles_refunded128(dst : i32) = + if es.context ∉ {Rt, Ry} then Trap {cycles_used = es.cycles_used;} let amount = es.params.cycles_refunded copy_cycles_to_canister(dst, amount.to_little_endian_bytes()) ic0.accept_message() = + if es.context ∉ {F} then Trap {cycles_used = es.cycles_used;} if es.ingress_filter = Accept then Trap {cycles_used = es.cycles_used;} es.ingress_filter = Accept ic0.msg_method_name_size() : i32 = + if es.context ∉ {F} then Trap {cycles_used = es.cycles_used;} return |es.method_name| ic0.msg_method_name_copy(dst : i32, offset : i32, size : i32) : i32 = + if es.context ∉ {F} then Trap {cycles_used = es.cycles_used;} copy_to_canister(dst, offset, size, es.params.method_name) ic0.msg_cycles_accept(max_amount : i64) : i64 = + if es.context ∉ {U, 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 @@ -4336,6 +4554,7 @@ ic0.msg_cycles_accept(max_amount : i64) : i64 = 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;} 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 @@ -4363,6 +4582,9 @@ ic0.canister_status() : i32 = Stopping -> return 2 Stopped -> return 3 +ic0.canister_version() : i64 = + return es.params.sysenv.canister_version + ic0.call_new( callee_src : i32, callee_size : i32, @@ -4373,6 +4595,8 @@ ic0.call_new( reject_fun : i32, reject_env : i32, ) = + if es.context ∉ {U, Ry, Rt, T} then Trap {cycles_used = es.cycles_used;} + discard_pending_call() if es.balance < MAX_CYCLES_PER_RESPONSE then Trap {cycles_used = es.cycles_used;} @@ -4400,10 +4624,12 @@ ic0.call_new( } ic0.call_data_append (src : i32, size : i32) = + 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;} es.pending_call.arg := es.pending_call.arg · copy_from_canister(src, size) ic0.call_on_cleanup (fun : i32, env : i32) = + if es.context ∉ {U, Ry, Rt, T} then Trap {cycles_used = es.cycles_used;} if fun > |es.wasm_state.store.table| then Trap {cycles_used = es.cycles_used;} if typeof(es.wasm_state.store.table[fun]) ≠ func (anyref, i32) -> () then Trap {cycles_used = es.cycles_used;} if es.pending_call = NoPendingCall then Trap {cycles_used = es.cycles_used;} @@ -4411,6 +4637,7 @@ ic0.call_on_cleanup (fun : i32, env : i32) = es.pending_call.callback.on_cleanup := Closure { fun = fun; env = env} ic0.call_cycles_add(amount : i64) = + 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;} @@ -4418,6 +4645,7 @@ ic0.call_cycles_add(amount : i64) = es.pending_call.transferred_cycles := es.pending_call.transferred_cycles + amount ic0.call_cycles_add128(amount_high : i64, amount_low : i64) = + if es.context ∉ {U, Ry, Rt, T} then Trap {cycles_used = es.cycles_used;} 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;} @@ -4426,6 +4654,7 @@ ic0.call_cycles_add128(amount_high : i64, amount_low : i64) = es.pending_call.transferred_cycles := es.pending_call.transferred_cycles + amount ic0.call_peform() : ( err_code : i32 ) = + 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;} // are we below the threezing threshold? @@ -4499,9 +4728,18 @@ ic0.stable64_read(dst : i64, offset : i64, size : i64) es.wasm_state.store.mem[offset..offset+size] := es.wasm_state.stable.mem[src..src+size] ic0.time() : i32 = - return es.params.time + return es.params.sysenv.time + +ic0.global_timer_set(timestamp: i64) : i64 = + if es.context ∉ {I, U, Ry, Rt, C, T} then Trap {cycles_used = es.cycles_used;} + let prev_global_timer = es.new_global_timer + es.new_global_timer := timestamp + if prev_global_timer = NoGlobalTimer + then return es.params.sysenv.global_timer + else return prev_global_timer ic0.certified_data_set(src: i32, size: i32) = + if es.context ∉ {I, G, U, Ry, Rt, T} then Trap {cycles_used = es.cycles_used;} es.new_certified_data := es.wasm_state[src..src+size] ic0.data_certificate_present() : i32 = From 7422f79ec37540653fe9cd3b7bccc5615a81cc8d Mon Sep 17 00:00:00 2001 From: bogwar <51327868+bogwar@users.noreply.github.com> Date: Tue, 6 Dec 2022 16:48:19 +0100 Subject: [PATCH 2/3] new release --- spec/ic0.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/ic0.txt b/spec/ic0.txt index a553089d3..454ff815f 100644 --- a/spec/ic0.txt +++ b/spec/ic0.txt @@ -23,6 +23,7 @@ ic0.canister_self_copy : (dst : i32, offset : i32, size : i32) -> (); // * ic0.canister_cycle_balance : () -> i64; // * ic0.canister_cycle_balance128 : (dst : i32) -> (); // * ic0.canister_status : () -> i32; // * +ic0.canister_version : () -> i64; // * ic0.msg_method_name_size : () -> i32; // F ic0.msg_method_name_copy : (dst : i32, offset : i32, size : i32) -> (); // F From 73903a86b2d1e2fc8ea38d33744a87d8fad709d1 Mon Sep 17 00:00:00 2001 From: bogwar <51327868+bogwar@users.noreply.github.com> Date: Tue, 6 Dec 2022 16:48:47 +0100 Subject: [PATCH 3/3] new release --- theories/IC.thy | 394 ++++++++++++++++++++++++++++++++---------------- 1 file changed, 268 insertions(+), 126 deletions(-) diff --git a/theories/IC.thy b/theories/IC.thy index d026c3f3e..ada3a64db 100644 --- a/theories/IC.thy +++ b/theories/IC.thy @@ -175,13 +175,16 @@ type_synonym 'b arg = 'b type_synonym 'p caller_id = 'p type_synonym timestamp = nat +type_synonym canister_version = nat datatype status = Running | Stopping | Stopped record ('b) env = time :: timestamp + global_timer :: nat balance :: nat freezing_limit :: nat certificate :: "'b option" status :: status + canister_version :: canister_version type_synonym reject_code = nat datatype ('b, 's) response = @@ -197,51 +200,66 @@ record ('p, 'canid, 's, 'b, 'c) method_call = record 'x cycles_return = return :: 'x cycles_used :: nat +record ('w, 'b) init_return = + new_state :: 'w + new_certified_data :: "'b option" + new_global_timer :: "nat option" + cycles_used :: nat +record ('sm, 'b) pre_upgrade_return = + stable_memory :: 'sm + new_certified_data :: "'b option" + cycles_used :: nat type_synonym trap_return = "unit cycles_return" record ('w, 'p, 'canid, 's, 'b, 'c) update_return = new_state :: 'w new_calls :: "('p, 'canid, 's, 'b, 'c) method_call list" new_certified_data :: "'b option" + new_global_timer :: "nat option" response :: "('b, 's) response option" cycles_accepted :: nat cycles_used :: nat record ('b, 's) query_return = response :: "('b, 's) response" cycles_used :: nat -record 'w heartbeat_return = +record ('w, 'p, 'canid, 's, 'b, 'c) system_task_return = new_state :: 'w + new_calls :: "('p, 'canid, 's, 'b, 'c) method_call list" + new_certified_data :: "'b option" + new_global_timer :: "nat option" cycles_used :: nat type_synonym ('w, 'p, 'canid, 's, 'b, 'c) update_func = "'w \ trap_return + ('w, 'p, 'canid, 's, 'b, 'c) update_return" type_synonym ('w, 'b, 's) query_func = "'w \ trap_return + ('b, 's) query_return" -type_synonym 'w heartbeat_func = "'w \ trap_return + 'w heartbeat_return" +type_synonym ('w, 'p, 'canid, 's, 'b, 'c) system_task_func = "'w \ trap_return + ('w, 'p, 'canid, 's, 'b, 'c) system_task_return" type_synonym available_cycles = nat type_synonym refunded_cycles = nat datatype inspect_method_result = Accept | Reject record ('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module_rec = - init :: "'canid \ 'b arg \ 'p caller_id \ 'b env \ trap_return + 'w cycles_return" - pre_upgrade :: "'w \ 'p \ 'b env \ trap_return + 'sm cycles_return" - post_upgrade :: "'canid \ 'sm \ 'b arg \ 'p caller_id \ 'b env \ trap_return + 'w cycles_return" + init :: "'canid \ 'b arg \ 'p caller_id \ 'b env \ trap_return + ('w, 'b) init_return" + pre_upgrade :: "'w \ 'p \ 'b env \ trap_return + ('sm, 'b) pre_upgrade_return" + post_upgrade :: "'canid \ 'sm \ 'b arg \ 'p caller_id \ 'b env \ trap_return + ('w, 'b) init_return" update_methods :: "('s method_name, ('b arg \ 'p caller_id \ 'b env \ available_cycles) \ ('w, 'p, 'canid, 's, 'b, 'c) update_func) list_map" query_methods :: "('s method_name, ('b arg \ 'p caller_id \ 'b env) \ ('w, 'b, 's) query_func) list_map" - heartbeat :: "'b env \ 'w heartbeat_func" + heartbeat :: "'b env \ ('w, 'p, 'canid, 's, 'b, 'c) system_task_func" + global_timer :: "'b env \ ('w, 'p, 'canid, 's, 'b, 'c) system_task_func" callbacks :: "('c \ ('b, 's) response \ refunded_cycles \ 'b env \ available_cycles) \ ('w, 'p, 'canid, 's, 'b, 'c) update_func" inspect_message :: "('s method_name \ 'w \ 'b arg \ 'p caller_id \ 'b env) \ trap_return + inspect_method_result cycles_return" typedef ('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module = "{m :: ('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module_rec. list_map_dom (update_methods m) \ list_map_dom (query_methods m) = {}}" by (auto intro: exI[of _ "\init = undefined, pre_upgrade = undefined, post_upgrade = undefined, - update_methods = list_map_empty, query_methods = list_map_empty, heartbeat = undefined, callbacks = undefined, + update_methods = list_map_empty, query_methods = list_map_empty, heartbeat = undefined, global_timer = undefined, callbacks = undefined, inspect_message = undefined\"]) setup_lifting type_definition_canister_module -lift_definition canister_module_init :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ 'canid \ 'b arg \ 'p \ 'b env \ trap_return + 'w cycles_return" is "init" . -lift_definition canister_module_pre_upgrade :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ 'w \ 'p \ 'b env \ trap_return + 'sm cycles_return" is pre_upgrade . -lift_definition canister_module_post_upgrade :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ 'canid \ 'sm \ 'b arg \ 'p \ 'b env \ trap_return + 'w cycles_return" is post_upgrade . +lift_definition canister_module_init :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ 'canid \ 'b arg \ 'p \ 'b env \ trap_return + ('w, 'b) init_return" is "init" . +lift_definition canister_module_pre_upgrade :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ 'w \ 'p \ 'b env \ trap_return + ('sm, 'b) pre_upgrade_return" is pre_upgrade . +lift_definition canister_module_post_upgrade :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ 'canid \ 'sm \ 'b arg \ 'p \ 'b env \ trap_return + ('w, 'b) init_return" is post_upgrade . lift_definition canister_module_update_methods :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ ('s, ('b arg \ 'p \ 'b env \ available_cycles) \ ('w, 'p, 'canid, 's, 'b, 'c) update_func) list_map" is update_methods . lift_definition canister_module_query_methods :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ ('s, ('b arg \ 'p \ 'b env) \ ('w, 'b, 's) query_func) list_map" is query_methods . -lift_definition canister_module_heartbeat :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ 'b env \ 'w heartbeat_func" is heartbeat . +lift_definition canister_module_heartbeat :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ 'b env \ ('w, 'p, 'canid, 's, 'b, 'c) system_task_func" is heartbeat . +lift_definition canister_module_global_timer :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ 'b env \ ('w, 'p, 'canid, 's, 'b, 'c) system_task_func" is global_timer . lift_definition canister_module_callbacks :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ ('c \ ('b, 's) response \ refunded_cycles \ 'b env \ available_cycles) \ ('w, 'p, 'canid, 's, 'b, 'c) update_func" is callbacks . lift_definition canister_module_inspect_message :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ ('s \ 'w \ 'b arg \ 'p \ 'b env) \ trap_return + inspect_method_result cycles_return" is inspect_message . @@ -261,7 +279,7 @@ record ('b, 'p, 'uid, 'canid, 's) request = datatype ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin = From_user "('b, 'p, 'uid, 'canid, 's) request" | From_canister "'cid" "'c" -| From_heartbeat +| From_system record ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt_rep = canister :: 'canid origin :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin" @@ -325,6 +343,7 @@ datatype ('s, 'p, 'b, 'c) entry_point = Public_method "'s method_name" "'p" "'b" | Callback "'c" "('b, 's) response" "refunded_cycles" | Heartbeat +| Global_timer datatype ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) message = Call_message "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin" 'p 'canid 's 'b nat "'canid queue" @@ -381,7 +400,9 @@ record ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic = controllers :: "('canid, 'p set) list_map" freezing_threshold :: "('canid, nat) list_map" canister_status :: "('canid, ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) can_status) list_map" + canister_version :: "('canid, canister_version) list_map" time :: "('canid, timestamp) list_map" + global_timer :: "('canid, nat) list_map" balances :: "('canid, nat) list_map" certified_data :: "('canid, 'b) list_map" system_time :: timestamp @@ -402,7 +423,9 @@ definition initial_ic :: "nat \ 'pk \ ('p, 'uid, 'canid, controllers = list_map_empty, freezing_threshold = list_map_empty, canister_status = list_map_empty, + canister_version = list_map_empty, time = list_map_empty, + global_timer = list_map_empty, balances = list_map_empty, certified_data = list_map_empty, system_time = t, @@ -557,6 +580,7 @@ fun cycles_reserved :: "('s, 'p, 'b, 'c) entry_point \ nat" where "cycles_reserved (entry_point.Public_method _ _ _) = MAX_CYCLES_PER_MESSAGE" | "cycles_reserved (entry_point.Callback _ _ _) = MAX_CYCLES_PER_RESPONSE" | "cycles_reserved (entry_point.Heartbeat) = MAX_CYCLES_PER_MESSAGE" +| "cycles_reserved (entry_point.Global_timer) = MAX_CYCLES_PER_MESSAGE" fun message_cycles :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) message \ nat" where "message_cycles (Call_message orig _ _ _ _ trans_cycles q) = carried_cycles orig + trans_cycles" @@ -638,9 +662,9 @@ definition request_submission_pre :: "('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) enve \ ( request.canister_id req \ ic_principal \ - (case (list_map_get (canisters S) (request.canister_id req), list_map_get (time S) (request.canister_id req), list_map_get (balances S) (request.canister_id req), list_map_get (canister_status S) (request.canister_id req)) of - (Some (Some can), Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S (request.canister_id req), certificate = None, status = simple_status can_status\ in + (case (list_map_get (canisters S) (request.canister_id req), list_map_get (time S) (request.canister_id req), list_map_get (balances S) (request.canister_id req), list_map_get (canister_status S) (request.canister_id req), list_map_get (canister_version S) (request.canister_id req), list_map_get (global_timer S) (request.canister_id req)) of + (Some (Some can), Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S (request.canister_id req), certificate = None, status = simple_status can_status, canister_version = idx\ in (case canister_module_inspect_message (module can) (request.method_name req, wasm_state can, request.arg req, principal_of_uid (request.sender req), env) of Inr ret \ cycles_return.return ret = Accept \ cycles_return.cycles_used ret \ bal | _ \ False) @@ -654,9 +678,9 @@ definition request_submission_post :: "('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) env let req = projl (content E); cid = request.canister_id req; balances = (if cid \ ic_principal then - (case (list_map_get (canisters S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid) of - (Some (Some can), Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status\ in + (case (list_map_get (canisters S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid, list_map_get (canister_version S) (request.canister_id req), list_map_get (global_timer S) (request.canister_id req)) of + (Some (Some can), Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = idx\ in (case canister_module_inspect_message (module can) (request.method_name req, wasm_state can, request.arg req, principal_of_uid (request.sender req), env) of Inr ret \ list_map_set (balances S) cid (bal - cycles_return.cycles_used ret))) else balances S) in @@ -667,9 +691,9 @@ definition request_submission_burned_cycles :: "('b, 'p, 'uid, 'canid, 's, 'pk, let req = projl (content E); cid = request.canister_id req in (if request.canister_id req \ ic_principal then - (case (list_map_get (canisters S) (request.canister_id req), list_map_get (time S) (request.canister_id req), list_map_get (balances S) (request.canister_id req), list_map_get (canister_status S) (request.canister_id req)) of - (Some (Some can), Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S (request.canister_id req), certificate = None, status = simple_status can_status\ in + (case (list_map_get (canisters S) (request.canister_id req), list_map_get (time S) (request.canister_id req), list_map_get (balances S) (request.canister_id req), list_map_get (canister_status S) (request.canister_id req), list_map_get (canister_version S) (request.canister_id req), list_map_get (global_timer S) (request.canister_id req)) of + (Some (Some can), Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S (request.canister_id req), certificate = None, status = simple_status can_status, canister_version = idx\ in (case canister_module_inspect_message (module can) (request.method_name req, wasm_state can, request.arg req, principal_of_uid (request.sender req), env) of Inr ret \ cycles_return.cycles_used ret)) else 0))" @@ -683,9 +707,9 @@ proof - by (auto simp: request_submission_pre_def split: sum.splits) { assume "request.canister_id req \ ic_principal" - then have "(case (list_map_get (canisters S) (request.canister_id req), list_map_get (time S) (request.canister_id req), list_map_get (balances S) (request.canister_id req), list_map_get (canister_status S) (request.canister_id req)) of - (Some (Some can), Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S (request.canister_id req), certificate = None, status = simple_status can_status\ in + then have "(case (list_map_get (canisters S) (request.canister_id req), list_map_get (time S) (request.canister_id req), list_map_get (balances S) (request.canister_id req), list_map_get (canister_status S) (request.canister_id req), list_map_get (canister_version S) (request.canister_id req), list_map_get (global_timer S) (request.canister_id req)) of + (Some (Some can), Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S (request.canister_id req), certificate = None, status = simple_status can_status, canister_version = idx\ in (case canister_module_inspect_message (module can) (request.method_name req, wasm_state can, request.arg req, principal_of_uid (request.sender req), env) of Inr ret \ cycles_return.return ret = Accept \ cycles_return.cycles_used ret \ bal | _ \ False) @@ -706,7 +730,7 @@ lemma request_submission_ic_inv: shows "ic_inv (request_submission_post E ECID S)" using assms by (auto simp: ic_inv_def request_submission_pre_def request_submission_post_def Let_def - split: sum.splits message.splits call_origin.splits) + split: sum.splits message.splits call_origin.splits prod.splits) @@ -868,6 +892,16 @@ lemma call_context_create_ic_inv: (* System transition: Call context creation: Heartbeat [DONE] *) +lift_definition create_call_ctxt_system_task :: "'canid \ ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt" is + "\cee. \canister = cee, origin = From_system, needs_to_respond = False, deleted = False, available_cycles = 0\" + by auto + +lemma create_call_ctxt_system_task_needs_to_respond[simp]: "call_ctxt_needs_to_respond (create_call_ctxt_system_task cee) = False" + by transfer auto + +lemma create_call_ctxt_system_task_carried_cycles[simp]: "call_ctxt_carried_cycles (create_call_ctxt_system_task cee) = 0" + by transfer auto + definition call_context_heartbeat_pre :: "'canid \ 'cid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where "call_context_heartbeat_pre cee ctxt_id S = ( (case list_map_get (canisters S) cee of Some (Some can) \ True | _ \ False) \ @@ -875,21 +909,11 @@ definition call_context_heartbeat_pre :: "'canid \ 'cid \ bal \ ic_freezing_limit S cee + MAX_CYCLES_PER_MESSAGE | _ \ False) \ ctxt_id \ list_map_dom (call_contexts S))" -lift_definition create_call_ctxt_heartbeat :: "'canid \ ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt" is - "\cee. \canister = cee, origin = From_heartbeat, needs_to_respond = False, deleted = False, available_cycles = 0\" - by auto - -lemma create_call_ctxt_heartbeat_needs_to_respond[simp]: "call_ctxt_needs_to_respond (create_call_ctxt_heartbeat cee) = False" - by transfer auto - -lemma create_call_ctxt_heartbeat_carried_cycles[simp]: "call_ctxt_carried_cycles (create_call_ctxt_heartbeat cee) = 0" - by transfer auto - definition call_context_heartbeat_post :: "'canid \ 'cid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where "call_context_heartbeat_post cee ctxt_id S = (case list_map_get (balances S) cee of Some bal \ S\messages := Func_message ctxt_id cee Heartbeat (Queue System cee) # messages S, - call_contexts := list_map_set (call_contexts S) ctxt_id (create_call_ctxt_heartbeat cee), + call_contexts := list_map_set (call_contexts S) ctxt_id (create_call_ctxt_system_task cee), balances := list_map_set (balances S) cee (bal - MAX_CYCLES_PER_MESSAGE)\)" lemma call_context_heartbeat_cycles_inv: @@ -910,17 +934,54 @@ lemma call_context_heartbeat_ic_inv: +(* System transition: Call context creation: Global timer [DONE] *) + +definition call_context_global_timer_pre :: "'canid \ 'cid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where + "call_context_global_timer_pre cee ctxt_id S = ( + (case list_map_get (canisters S) cee of Some (Some can) \ True | _ \ False) \ + list_map_get (canister_status S) cee = Some Running \ + (case (list_map_get (time S) cee, list_map_get (global_timer S) cee) of (Some t, Some timer) \ timer \ 0 \ t \ timer | _ \ False) \ + (case list_map_get (balances S) cee of Some bal \ bal \ ic_freezing_limit S cee + MAX_CYCLES_PER_MESSAGE | _ \ False) \ + ctxt_id \ list_map_dom (call_contexts S))" + +definition call_context_global_timer_post :: "'canid \ 'cid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where + "call_context_global_timer_post cee ctxt_id S = + (case list_map_get (balances S) cee of Some bal \ + S\messages := Func_message ctxt_id cee Global_timer (Queue System cee) # messages S, + call_contexts := list_map_set (call_contexts S) ctxt_id (create_call_ctxt_system_task cee), + global_timer := list_map_set (global_timer S) cee 0, + balances := list_map_set (balances S) cee (bal - MAX_CYCLES_PER_MESSAGE)\)" + +lemma call_context_global_timer_cycles_inv: + assumes "call_context_global_timer_pre cee ctxt_id S" + shows "total_cycles S = total_cycles (call_context_global_timer_post cee ctxt_id S)" + using assms list_map_sum_in_ge[of "balances S" cee, where ?g=id, simplified] + by (auto simp: call_context_global_timer_pre_def call_context_global_timer_post_def total_cycles_def + list_map_sum_in[where ?g=id, simplified] list_map_sum_out split: option.splits) + +lemma call_context_global_timer_ic_inv: + assumes "call_context_global_timer_pre cee ctxt_id S" "ic_inv S" + shows "ic_inv (call_context_global_timer_post cee ctxt_id S)" + using assms + by (auto simp: ic_inv_def call_context_global_timer_pre_def call_context_global_timer_post_def Let_def + split: sum.splits message.splits call_origin.splits option.splits + dest!: in_set_takeD in_set_dropD in_set_updD list_map_range_setD + intro: ic_can_status_inv_mono2) + + + (* System transition: Message execution [DONE] *) fun query_as_update :: "(('b arg \ 'p \ 'b env) \ ('w, 'b, 's) query_func) \ 'b arg \ 'p \ 'b env \ ('w, 'p, 'canid, 's, 'b, 'c) update_func" where "query_as_update (f, a, e) = (\w. case f (a, e) w of Inl t \ Inl t | - Inr res \ Inr \update_return.new_state = w, update_return.new_calls = [], update_return.new_certified_data = None, + Inr res \ Inr \update_return.new_state = w, update_return.new_calls = [], update_return.new_certified_data = None, update_return.new_global_timer = None, update_return.response = Some (query_return.response res), update_return.cycles_accepted = 0, update_return.cycles_used = query_return.cycles_used res\)" -fun heartbeat_as_update :: "('b env \ 'w heartbeat_func) \ 'b env \ ('w, 'p, 'canid, 's, 'b, 'c) update_func" where - "heartbeat_as_update (f, e) = (\w. case f e w of Inl t \ Inl t | - Inr res \ Inr \update_return.new_state = heartbeat_return.new_state res, update_return.new_calls = [], update_return.new_certified_data = None, - update_return.response = None, update_return.cycles_accepted = 0, update_return.cycles_used = heartbeat_return.cycles_used res\)" +fun system_task_as_update :: "('b env \ ('w, 'p, 'canid, 's, 'b, 'c) system_task_func) \ 'b env \ ('w, 'p, 'canid, 's, 'b, 'c) update_func" where + "system_task_as_update (f, e) = (\w. case f e w of Inl t \ Inl t | + Inr res \ Inr \update_return.new_state = system_task_return.new_state res, update_return.new_calls = system_task_return.new_calls res, + update_return.new_certified_data = system_task_return.new_certified_data res, update_return.new_global_timer = system_task_return.new_global_timer res, + update_return.response = None, update_return.cycles_accepted = 0, update_return.cycles_used = system_task_return.cycles_used res\)" fun exec_function :: "('s, 'p, 'b, 'c) entry_point \ 'b env \ nat \ ('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ ('w, 'p, 'canid, 's, 'b, 'c) update_func" where "exec_function (entry_point.Public_method mn c a) e bal m = ( @@ -930,25 +991,26 @@ fun exec_function :: "('s, 'p, 'b, 'c) entry_point \ 'b env \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where "message_execution_pre n S = (n < length (messages S) \ (case messages S ! n of Func_message ctxt_id recv ep q \ (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ (case (list_map_get (canisters S) recv, list_map_get (balances S) recv, list_map_get (canister_status S) recv, - list_map_get (time S) recv, list_map_get (call_contexts S) ctxt_id) of - (Some (Some can), Some bal, Some can_status, Some t, Some ctxt) \ True | _ \ False) + list_map_get (time S) recv, list_map_get (call_contexts S) ctxt_id, list_map_get (canister_version S) recv, list_map_get (global_timer S) recv) of + (Some (Some can), Some bal, Some can_status, Some t, Some ctxt, Some idx, Some timer) \ True | _ \ False) | _ \ False))" definition message_execution_post :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where "message_execution_post n S = (case messages S ! n of Func_message ctxt_id recv ep q \ (case (list_map_get (canisters S) recv, list_map_get (balances S) recv, list_map_get (canister_status S) recv, - list_map_get (time S) recv, list_map_get (call_contexts S) ctxt_id) of - (Some (Some can), Some bal, Some can_status, Some t, Some ctxt) \ ( + list_map_get (time S) recv, list_map_get (call_contexts S) ctxt_id, list_map_get (canister_version S) recv, list_map_get (global_timer S) recv) of + (Some (Some can), Some bal, Some can_status, Some t, Some ctxt, Some idx, Some timer) \ ( let Mod = module can; Is_response = (case ep of Callback _ _ _ \ True | _ \ False); - Env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status\; + Env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status, canister_version = idx\; Available = call_ctxt_available_cycles ctxt; F = exec_function ep Env Available Mod; R = F (wasm_state can); @@ -972,11 +1034,13 @@ definition message_execution_post :: "nat \ ('p, 'uid, 'canid, 'b, ' new_ctxt = (case update_return.response result of None \ call_ctxt_deduct_cycles cycles_accepted_res ctxt | Some _ \ call_ctxt_respond ctxt); - certified_data = (case new_certified_data result of None \ certified_data S - | Some cd \ list_map_set (certified_data S) recv cd) + certified_data = (case update_return.new_certified_data result of None \ certified_data S + | Some cd \ list_map_set (certified_data S) recv cd); + global_timer = (case update_return.new_global_timer result of None \ global_timer S + | Some new_timer \ list_map_set (global_timer S) recv new_timer) in S\canisters := list_map_set (canisters S) recv (Some (can\wasm_state := update_return.new_state result\)), messages := messages, call_contexts := list_map_set (call_contexts S) ctxt_id new_ctxt, - certified_data := certified_data, balances := list_map_set (balances S) recv New_balance\) + certified_data := certified_data, global_timer := global_timer, balances := list_map_set (balances S) recv New_balance\) else S\messages := take n (messages S) @ drop (Suc n) (messages S), balances := list_map_set (balances S) recv ((bal + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE)) - min cyc_used (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE))\)) @@ -985,11 +1049,11 @@ definition message_execution_post :: "nat \ ('p, 'uid, 'canid, 'b, ' definition message_execution_burned_cycles :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where "message_execution_burned_cycles n S = (case messages S ! n of Func_message ctxt_id recv ep q \ (case (list_map_get (canisters S) recv, list_map_get (balances S) recv, list_map_get (canister_status S) recv, - list_map_get (time S) recv, list_map_get (call_contexts S) ctxt_id) of - (Some (Some can), Some bal, Some can_status, Some t, Some ctxt) \ ( + list_map_get (time S) recv, list_map_get (call_contexts S) ctxt_id, list_map_get (canister_version S) recv, list_map_get (global_timer S) recv) of + (Some (Some can), Some bal, Some can_status, Some t, Some ctxt, Some idx, Some timer) \ ( let Mod = module can; Is_response = (case ep of Callback _ _ _ \ True | _ \ False); - Env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status\; + Env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status, canister_version = idx\; Available = call_ctxt_available_cycles ctxt; F = exec_function ep Env Available Mod; R = F (wasm_state can); @@ -1001,23 +1065,25 @@ lemma message_execution_cycles_monotonic: assumes pre: "message_execution_pre n S" shows "total_cycles S = total_cycles (message_execution_post n S) + message_execution_burned_cycles n S" proof - - obtain ctxt_id recv ep q can bal can_status t ctxt where msg: "messages S ! n = Func_message ctxt_id recv ep q" + obtain ctxt_id recv ep q can bal can_status t ctxt idx timer where msg: "messages S ! n = Func_message ctxt_id recv ep q" and prod: "list_map_get (canisters S) recv = Some (Some can)" "list_map_get (balances S) recv = Some bal" "list_map_get (canister_status S) recv = Some can_status" "list_map_get (time S) recv = Some t" "list_map_get (call_contexts S) ctxt_id = Some ctxt" + "list_map_get (canister_version S) recv = Some idx" + "list_map_get (global_timer S) recv = Some timer" using pre by (auto simp: message_execution_pre_def split: message.splits option.splits) define Mod where "Mod = can_state_rec.module can" define Is_response where "Is_response = (case ep of Callback _ _ _ \ True | _ \ False)" - define Env :: "'b env" where "Env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status\" + define Env :: "'b env" where "Env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status, canister_version = idx\" define Available where "Available = call_ctxt_available_cycles ctxt" define F where "F = exec_function ep Env Available Mod" define R where "R = F (wasm_state can)" define cyc_used where "cyc_used = (case R of Inr res \ update_return.cycles_used res | Inl trap \ cycles_return.cycles_used trap)" - obtain cycles_accepted_res new_calls_res where res: "(cycles_accepted_res, new_calls_res) = (case R of Inr res \ (update_return.cycles_accepted res, new_calls res))" - by (cases "(case R of Inr res \ (update_return.cycles_accepted res, new_calls res))") auto + obtain cycles_accepted_res new_calls_res where res: "(cycles_accepted_res, new_calls_res) = (case R of Inr res \ (update_return.cycles_accepted res, update_return.new_calls res))" + by (cases "(case R of Inr res \ (update_return.cycles_accepted res, update_return.new_calls res))") auto define New_balance where "New_balance = bal + cycles_accepted_res + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) - (cyc_used + sum_list (map (\x. MAX_CYCLES_PER_RESPONSE + transferred_cycles x) new_calls_res))" define no_response where "no_response = (case R of Inr result \ update_return.response result = None)" @@ -1068,13 +1134,15 @@ proof - define new_ctxt where "new_ctxt = (case update_return.response result of None \ call_ctxt_deduct_cycles cycles_accepted_res ctxt | Some _ \ call_ctxt_respond ctxt)" - define certified_data where "certified_data = (case new_certified_data result of None \ ic.certified_data S + define certified_data where "certified_data = (case update_return.new_certified_data result of None \ ic.certified_data S | Some cd \ list_map_set (ic.certified_data S) recv cd)" + define global_timer where "global_timer = (case update_return.new_global_timer result of None \ ic.global_timer S + | Some new_timer \ list_map_set (ic.global_timer S) recv new_timer)" define S' where "S' = S\canisters := list_map_set (canisters S) recv (Some (can\wasm_state := update_return.new_state result\)), messages := messages, call_contexts := list_map_set (call_contexts S) ctxt_id new_ctxt, - certified_data := certified_data, balances := list_map_set (balances S) recv New_balance\" + certified_data := certified_data, global_timer := global_timer, balances := list_map_set (balances S) recv New_balance\" have cycles_accepted_res_def: "cycles_accepted_res = update_return.cycles_accepted result" - and new_calls_res_def: "new_calls_res = new_calls result" + and new_calls_res_def: "new_calls_res = update_return.new_calls result" using res by (auto simp: R_Inr) have no_response: "no_response = (update_return.response result = None)" @@ -1085,7 +1153,7 @@ proof - by (simp_all add: message_execution_post_def message_execution_burned_cycles_def Let_def msg prod Mod_def[symmetric] Is_response_def[symmetric] Env_def[symmetric] Available_def[symmetric] F_def[symmetric] R_def[symmetric] cyc_used_def[symmetric] res[symmetric] New_balance_def[symmetric] no_response_def[symmetric] S''_def[symmetric] cond_def[symmetric] - messages_def[symmetric] new_ctxt_def[symmetric] certified_data_def[symmetric] S'_def[symmetric] + messages_def[symmetric] new_ctxt_def[symmetric] certified_data_def[symmetric] global_timer_def[symmetric] S'_def[symmetric] result_def[symmetric] response_messages_def[symmetric] new_call_to_message_def[symmetric] del: min_less_iff_conj split del: if_split) have "message_cycles \ new_call_to_message = (\c. MAX_CYCLES_PER_RESPONSE + transferred_cycles c)" for c :: "(?'p, 'canid, 's, 'b, 'c) method_call" @@ -1114,14 +1182,16 @@ qed lemma message_execution_cases: assumes "message_execution_pre n S" - "\ctxt_id recv ep q can bal can_status t ctxt Mod Is_response Env Available F R cyc_used cycles_accepted_res new_calls_res New_balance no_response result new_call_to_message response_messages msgs new_ctxt cert_data idx. + "\ctxt_id recv ep q can bal can_status t ctxt Mod Is_response Env Available F R cyc_used cycles_accepted_res new_calls_res New_balance no_response result new_call_to_message response_messages msgs new_ctxt cert_data idx timer glob_timer. messages S ! n = Func_message ctxt_id recv ep q \ list_map_get (canisters S) recv = Some (Some can) \ list_map_get (balances S) recv = Some bal \ list_map_get (canister_status S) recv = Some can_status \ list_map_get (time S) recv = Some t \ list_map_get (call_contexts S) ctxt_id = Some ctxt \ + list_map_get (canister_version S) recv = Some idx \ + list_map_get (global_timer S) recv = Some timer \ Mod = module can \ Is_response = (case ep of Callback _ _ _ \ True | _ \ False) \ - Env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status\ \ + Env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status, canister_version = idx\ \ Available = call_ctxt_available_cycles ctxt \ F = exec_function ep Env Available Mod \ R = F (wasm_state can) \ @@ -1145,19 +1215,23 @@ lemma message_execution_cases: new_ctxt = (case update_return.response result of None \ call_ctxt_deduct_cycles cycles_accepted_res ctxt | Some _ \ call_ctxt_respond ctxt) \ - cert_data = (case new_certified_data result of None \ certified_data S + cert_data = (case update_return.new_certified_data result of None \ certified_data S | Some cd \ list_map_set (certified_data S) recv cd) \ + glob_timer = (case update_return.new_global_timer result of None \ global_timer S + | Some new_timer \ list_map_set (global_timer S) recv new_timer) \ P n S (S\canisters := list_map_set (canisters S) recv (Some (can\wasm_state := update_return.new_state result\)), messages := msgs, call_contexts := list_map_set (call_contexts S) ctxt_id new_ctxt, - certified_data := cert_data, balances := list_map_set (balances S) recv New_balance\)" - "\ctxt_id recv ep q can bal can_status t ctxt Mod Is_response Env Available F R cyc_used cycles_accepted_res new_calls_res New_balance no_response idx. + certified_data := cert_data, global_timer := glob_timer, balances := list_map_set (balances S) recv New_balance\)" + "\ctxt_id recv ep q can bal can_status t ctxt Mod Is_response Env Available F R cyc_used cycles_accepted_res new_calls_res New_balance no_response idx timer glob_timer. messages S ! n = Func_message ctxt_id recv ep q \ list_map_get (canisters S) recv = Some (Some can) \ list_map_get (balances S) recv = Some bal \ list_map_get (canister_status S) recv = Some can_status \ list_map_get (time S) recv = Some t \ list_map_get (call_contexts S) ctxt_id = Some ctxt \ + list_map_get (canister_version S) recv = Some idx \ + list_map_get (global_timer S) recv = Some timer \ Mod = module can \ Is_response = (case ep of Callback _ _ _ \ True | _ \ False) \ - Env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status\ \ + Env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status, canister_version = idx\ \ Available = call_ctxt_available_cycles ctxt \ F = exec_function ep Env Available Mod \ R = F (wasm_state can) \ @@ -1177,23 +1251,25 @@ lemma message_execution_cases: - min cyc_used (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE))\)" shows "P n S (message_execution_post n S)" proof - - obtain ctxt_id recv ep q can bal can_status t ctxt where msg: "messages S ! n = Func_message ctxt_id recv ep q" + obtain ctxt_id recv ep q can bal can_status t ctxt idx timer where msg: "messages S ! n = Func_message ctxt_id recv ep q" and prod: "list_map_get (canisters S) recv = Some (Some can)" "list_map_get (balances S) recv = Some bal" "list_map_get (canister_status S) recv = Some can_status" "list_map_get (time S) recv = Some t" "list_map_get (call_contexts S) ctxt_id = Some ctxt" + "list_map_get (canister_version S) recv = Some idx" + "list_map_get (global_timer S) recv = Some timer" using assms(1) by (auto simp: message_execution_pre_def split: message.splits option.splits) define Mod where "Mod = can_state_rec.module can" define Is_response where "Is_response = (case ep of Callback _ _ _ \ True | _ \ False)" - define Env :: "'b env" where "Env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status\" + define Env :: "'b env" where "Env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S recv, certificate = None, status = simple_status can_status, canister_version = idx\" define Available where "Available = call_ctxt_available_cycles ctxt" define F where "F = exec_function ep Env Available Mod" define R where "R = F (wasm_state can)" define cyc_used where "cyc_used = (case R of Inr res \ update_return.cycles_used res | Inl trap \ cycles_return.cycles_used trap)" - obtain cycles_accepted_res new_calls_res where res: "(cycles_accepted_res, new_calls_res) = (case R of Inr res \ (update_return.cycles_accepted res, new_calls res))" - by (cases "(case R of Inr res \ (update_return.cycles_accepted res, new_calls res))") auto + obtain cycles_accepted_res new_calls_res where res: "(cycles_accepted_res, new_calls_res) = (case R of Inr res \ (update_return.cycles_accepted res, update_return.new_calls res))" + by (cases "(case R of Inr res \ (update_return.cycles_accepted res, update_return.new_calls res))") auto define New_balance where "New_balance = bal + cycles_accepted_res + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) - (cyc_used + sum_list (map (\x. MAX_CYCLES_PER_RESPONSE + transferred_cycles x) new_calls_res))" define no_response where "no_response = (case R of Inr result \ update_return.response result = None)" @@ -1230,21 +1306,23 @@ lemma message_execution_cases: define new_ctxt where "new_ctxt = (case update_return.response result of None \ call_ctxt_deduct_cycles cycles_accepted_res ctxt | Some _ \ call_ctxt_respond ctxt)" - define certified_data where "certified_data = (case new_certified_data result of None \ ic.certified_data S + define certified_data where "certified_data = (case update_return.new_certified_data result of None \ ic.certified_data S | Some cd \ list_map_set (ic.certified_data S) recv cd)" + define global_timer where "global_timer = (case update_return.new_global_timer result of None \ ic.global_timer S + | Some new_timer \ list_map_set (ic.global_timer S) recv new_timer)" define S' where "S' = S\canisters := list_map_set (canisters S) recv (Some (can\wasm_state := update_return.new_state result\)), messages := messages, call_contexts := list_map_set (call_contexts S) ctxt_id new_ctxt, - certified_data := certified_data, balances := list_map_set (balances S) recv New_balance\" + certified_data := certified_data, global_timer := global_timer, balances := list_map_set (balances S) recv New_balance\" have msg_exec: "message_execution_post n S = S'" using True by (simp_all add: message_execution_post_def Let_def msg prod Mod_def[symmetric] Is_response_def[symmetric] Env_def[symmetric] Available_def[symmetric] F_def[symmetric] R_def[symmetric] cyc_used_def[symmetric] res[symmetric] New_balance_def[symmetric] no_response_def[symmetric] S''_def[symmetric] cond_def[symmetric] - messages_def[symmetric] new_ctxt_def[symmetric] certified_data_def[symmetric] S'_def[symmetric] + messages_def[symmetric] new_ctxt_def[symmetric] certified_data_def[symmetric] global_timer_def[symmetric] S'_def[symmetric] result_def[symmetric] response_messages_def[symmetric] new_call_to_message_def[symmetric]) show ?thesis using assms(2)[OF msg prod Mod_def Is_response_def Env_def Available_def F_def R_def cyc_used_def res New_balance_def no_response_def _ _ _ _ _ _ result_def - new_call_to_message_def response_messages_def messages_def new_ctxt_def certified_data_def, folded S'_def] True + new_call_to_message_def response_messages_def messages_def new_ctxt_def certified_data_def global_timer_def, folded S'_def] True by (auto simp: cond_def msg_exec) qed qed @@ -1253,7 +1331,7 @@ lemma message_execution_ic_inv: assumes "message_execution_pre n S" "ic_inv S" shows "ic_inv (message_execution_post n S)" proof (rule message_execution_cases[OF assms(1)]) - fix recv msgs ctxt_id new_ctxt cert_data New_balance new_calls_res response_messages ctxt Available cycles_accepted_res no_response idx + fix recv msgs ctxt_id new_ctxt cert_data New_balance new_calls_res response_messages ctxt Available cycles_accepted_res no_response idx glob_timer fix can :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) can_state_rec" fix result :: "('w, 'p, 'canid, 's, 'b, 'c) update_return" fix new_call_to_message :: "('p, 'canid, 's, 'b, 'c) method_call \ ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) message" @@ -1268,7 +1346,7 @@ proof (rule message_execution_cases[OF assms(1)]) "\ isl R" "result = projr R" "new_ctxt = (case update_return.response result of None \ call_ctxt_deduct_cycles cycles_accepted_res ctxt | Some x \ call_ctxt_respond ctxt)" then show "ic_inv (S\canisters := list_map_set (canisters S) recv (Some (can\wasm_state := update_return.new_state result\)), messages := msgs, - call_contexts := list_map_set (call_contexts S) ctxt_id new_ctxt, certified_data := cert_data, balances := list_map_set (balances S) recv New_balance\)" + call_contexts := list_map_set (call_contexts S) ctxt_id new_ctxt, certified_data := cert_data, global_timer := glob_timer, balances := list_map_set (balances S) recv New_balance\)" using assms(2) list_map_get_range[OF ctxt] by (cases R) (force simp: ic_inv_def ic_can_status_inv_def split: message.splits call_origin.splits can_status.splits dest!: in_set_takeD in_set_dropD list_map_range_setD)+ @@ -1289,7 +1367,7 @@ definition call_context_starvation_pre :: "'cid \ ('p, 'uid, 'canid, "call_context_starvation_pre ctxt_id S = (case list_map_get (call_contexts S) ctxt_id of Some call_context \ call_ctxt_needs_to_respond call_context \ - call_ctxt_origin call_context \ From_heartbeat \ + call_ctxt_origin call_context \ From_system \ (\msg \ set (messages S). case msg of Call_message orig _ _ _ _ _ _ \ calling_context orig \ Some ctxt_id | Response_message orig _ _ \ calling_context orig \ Some ctxt_id @@ -1331,7 +1409,7 @@ definition call_context_removal_pre :: "'cid \ ('p, 'uid, 'canid, 'b "call_context_removal_pre ctxt_id S = ( (case list_map_get (call_contexts S) ctxt_id of Some call_context \ (\call_ctxt_needs_to_respond call_context \ - (call_ctxt_origin call_context = From_heartbeat \ + (call_ctxt_origin call_context = From_system \ (\msg \ set (messages S). case msg of Func_message other_ctxt_id _ _ _ \ other_ctxt_id \ ctxt_id | _ \ True))) \ @@ -1383,10 +1461,12 @@ definition ic_canister_creation_pre :: "nat \ 'canid \ n is_system_assigned (principal_of_canid cid) \ cid \ list_map_dom (canisters S) \ cid \ list_map_dom (time S) \ + cid \ list_map_dom (global_timer S) \ cid \ list_map_dom (controllers S) \ cid \ list_map_dom (balances S) \ cid \ list_map_dom (certified_data S) \ - cid \ list_map_dom (canister_status S) + cid \ list_map_dom (canister_status S) \ + cid \ list_map_dom (canister_version S) | _ \ False))" definition ic_canister_creation_post :: "nat \ 'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where @@ -1394,13 +1474,15 @@ definition ic_canister_creation_post :: "nat \ 'canid \ let ctrls = (case candid_parse_controllers a of Some ctrls \ ctrls | _ \ {cer}) in S\canisters := list_map_set (canisters S) cid None, time := list_map_set (time S) cid t, + global_timer := list_map_set (global_timer S) cid 0, controllers := list_map_set (controllers S) cid ctrls, freezing_threshold := list_map_set (freezing_threshold S) cid 2592000, balances := list_map_set (balances S) cid trans_cycles, certified_data := list_map_set (certified_data S) cid empty_blob, messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid (Candid_record (list_map_init [(encode_string ''canister_id'', Candid_blob (blob_of_canid cid))])))) 0], - canister_status := list_map_set (canister_status S) cid Running\)" + canister_status := list_map_set (canister_status S) cid Running, + canister_version := list_map_set (canister_version S) cid 0\)" lemma ic_canister_creation_cycles_inv: assumes "ic_canister_creation_pre n cid t S" @@ -1442,7 +1524,7 @@ definition ic_update_settings_pre :: "nat \ ('p, 'uid, 'canid, 'b, ' cee = ic_principal \ mn = encode_string ''update_settings'' \ (case candid_parse_cid a of Some cid \ - (case list_map_get (controllers S) cid of Some ctrls \ cer \ ctrls + (case (list_map_get (controllers S) cid, list_map_get (canister_version S) cid) of (Some ctrls, Some idx) \ cer \ ctrls | _ \ False) | _ \ False) | _ \ False))" @@ -1451,8 +1533,10 @@ definition ic_update_settings_post :: "nat \ ('p, 'uid, 'canid, 'b, let cid = the (candid_parse_cid a); ctrls = (case candid_parse_controllers a of Some ctrls \ list_map_set (controllers S) cid ctrls | _ \ controllers S); freezing_thres = (case candid_nested_lookup a [encode_string '''settings'', encode_string ''freezing_threshold''] of Some (Candid_nat freeze) \ - list_map_set (freezing_threshold S) cid freeze | _ \ freezing_threshold S) in - S\controllers := ctrls, freezing_threshold := freezing_thres, messages := take n (messages S) @ drop (Suc n) (messages S) @ + list_map_set (freezing_threshold S) cid freeze | _ \ freezing_threshold S); + idx = the (list_map_get (canister_version S) cid) in + S\controllers := ctrls, freezing_threshold := freezing_thres, canister_version := list_map_set (canister_version S) cid (Suc idx), + messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid Candid_empty)) trans_cycles]\)" lemma ic_update_settings_cycles_inv: @@ -1555,13 +1639,13 @@ definition ic_code_installation_pre :: "nat \ ('p, 'uid, 'canid, 'b, (case parse_wasm_mod w of Some m \ parse_public_custom_sections w \ None \ parse_private_custom_sections w \ None \ - (case (list_map_get (controllers S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid) of - (Some ctrls, Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status\ in + (case (list_map_get (controllers S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid, list_map_get (canister_version S) cid, list_map_get (global_timer S) cid) of + (Some ctrls, Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = Suc idx\ in ((mode = encode_string ''install'' \ (case list_map_get (canisters S) cid of Some None \ True | _ \ False)) \ mode = encode_string ''reinstall'') \ cer \ ctrls \ (case canister_module_init m (cid, ar, cer, env) of Inl _ \ False - | Inr ret \ cycles_return.cycles_used ret \ bal) \ + | Inr ret \ init_return.cycles_used ret \ bal) \ list_map_dom (canister_module_update_methods m) \ list_map_dom (canister_module_query_methods m) = {} | _ \ False) | _ \ False) | _ \ False) | _ \ False) | _ \ False))" @@ -1572,12 +1656,16 @@ definition ic_code_installation_post :: "nat \ ('p, 'uid, 'canid, 'b (case (candid_parse_text a [encode_string ''mode''], candid_parse_blob a [encode_string ''wasm_module''], candid_parse_blob a [encode_string ''arg'']) of (Some mode, Some w, Some a) \ (case parse_wasm_mod w of Some m \ - (case (list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid) of - (Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status\; - (new_state, cyc_used) = (case canister_module_init m (cid, a, cer, env) of Inr ret \ (cycles_return.return ret, cycles_return.cycles_used ret)) in + (case (list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid, list_map_get (canister_version S) cid, list_map_get (global_timer S) cid) of + (Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = Suc idx\; + (new_state, new_certified_data, new_global_timer, cyc_used) = (case canister_module_init m (cid, a, cer, env) of Inr ret \ + (init_return.new_state ret, init_return.new_certified_data ret, init_return.new_global_timer ret, init_return.cycles_used ret)) in S\canisters := list_map_set (canisters S) cid (Some \wasm_state = new_state, module = m, raw_module = w, public_custom_sections = the (parse_public_custom_sections w), private_custom_sections = the (parse_private_custom_sections w)\), + certified_data := (case new_certified_data of None \ certified_data S | Some cd \ list_map_set (certified_data S) cid cd), + global_timer := list_map_set (global_timer S) cid (case new_global_timer of None \ 0 | Some new_timer \ new_timer), + canister_version := list_map_set (canister_version S) cid (Suc idx), balances := list_map_set (balances S) cid (bal - cyc_used), messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid Candid_empty)) trans_cycles]\)))))" @@ -1587,10 +1675,10 @@ definition ic_code_installation_burned_cycles :: "nat \ ('p, 'uid, ' (case (candid_parse_blob a [encode_string ''wasm_module''], candid_parse_blob a [encode_string ''arg'']) of (Some w, Some a) \ (case parse_wasm_mod w of Some m \ - (case (list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid) of - (Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status\ in - (case canister_module_init m (cid, a, cer, env) of Inr ret \ cycles_return.cycles_used ret))))))" + (case (list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid, list_map_get (canister_version S) cid, list_map_get (global_timer S) cid) of + (Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = Suc idx\ in + (case canister_module_init m (cid, a, cer, env) of Inr ret \ init_return.cycles_used ret))))))" lemma ic_code_installation_cycles_inv: assumes "ic_code_installation_pre n S" @@ -1615,7 +1703,7 @@ lemma ic_code_installation_ic_inv: assumes "ic_code_installation_pre n S" "ic_inv S" shows "ic_inv (ic_code_installation_post n S)" proof - - obtain orig cer cee mn a trans_cycles q cid mode w ar m ctrls t bal can_status idx where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" + obtain orig cer cee mn a trans_cycles q cid mode w ar m ctrls t bal can_status idx timer where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" and parse: "candid_parse_cid a = Some cid" "candid_parse_text a [encode_string ''mode''] = Some mode" "candid_parse_blob a [encode_string ''wasm_module''] = Some w" @@ -1626,6 +1714,8 @@ proof - "list_map_get (time S) cid = Some t" "list_map_get (balances S) cid = Some bal" "list_map_get (canister_status S) cid = Some can_status" + "list_map_get (canister_version S) cid = Some idx" + "list_map_get (global_timer S) cid = Some timer" using assms by (auto simp: ic_code_installation_pre_def split: message.splits option.splits) show ?thesis @@ -1650,14 +1740,15 @@ definition ic_code_upgrade_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, (case parse_wasm_mod w of Some m \ parse_public_custom_sections w \ None \ parse_private_custom_sections w \ None \ - (case (list_map_get (canisters S) cid, list_map_get (controllers S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid) of - (Some (Some can), Some ctrls, Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status\ in + (case (list_map_get (canisters S) cid, list_map_get (controllers S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid, list_map_get (canister_version S) cid, list_map_get (global_timer S) cid) of + (Some (Some can), Some ctrls, Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env1 = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = idx\; + env2 = \env.time = t, env.global_timer = 0, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = Suc idx\ in mode = encode_string ''upgrade'' \ cer \ ctrls \ - (case canister_module_pre_upgrade (module can) (wasm_state can, cer, env) of Inr pre_ret \ - (case canister_module_post_upgrade m (cid, cycles_return.return pre_ret, ar, cer, env) of Inr post_ret \ - cycles_return.cycles_used pre_ret + cycles_return.cycles_used post_ret \ bal + (case canister_module_pre_upgrade (module can) (wasm_state can, cer, env1) of Inr pre_ret \ + (case canister_module_post_upgrade m (cid, pre_upgrade_return.stable_memory pre_ret, ar, cer, env2) of Inr post_ret \ + pre_upgrade_return.cycles_used pre_ret + init_return.cycles_used post_ret \ bal | _ \ False) | _ \ False) \ list_map_dom (canister_module_update_methods m) \ list_map_dom (canister_module_query_methods m) = {} | _ \ False) | _ \ False) | _ \ False) | _ \ False) @@ -1669,14 +1760,20 @@ definition ic_code_upgrade_post :: "nat \ ('p, 'uid, 'canid, 'b, 'w, (case (candid_parse_text a [encode_string ''mode''], candid_parse_blob a [encode_string ''wasm_module''], candid_parse_blob a [encode_string ''arg'']) of (Some mode, Some w, Some ar) \ (case parse_wasm_mod w of Some m \ - (case (list_map_get (canisters S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid) of - (Some (Some can), Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status\ in - (case canister_module_pre_upgrade (module can) (wasm_state can, cer, env) of Inr pre_ret \ - (case canister_module_post_upgrade m (cid, cycles_return.return pre_ret, ar, cer, env) of Inr post_ret \ - S\canisters := list_map_set (canisters S) cid (Some \wasm_state = cycles_return.return post_ret, module = m, raw_module = w, + (case (list_map_get (canisters S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid, list_map_get (canister_version S) cid, list_map_get (global_timer S) cid) of + (Some (Some can), Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env1 = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = idx\; + env2 = \env.time = t, env.global_timer = 0, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = Suc idx\ in + (case canister_module_pre_upgrade (module can) (wasm_state can, cer, env1) of Inr pre_ret \ + (case canister_module_post_upgrade m (cid, pre_upgrade_return.stable_memory pre_ret, ar, cer, env2) of Inr post_ret \ + S\canisters := list_map_set (canisters S) cid (Some \wasm_state = init_return.new_state post_ret, module = m, raw_module = w, public_custom_sections = the (parse_public_custom_sections w), private_custom_sections = the (parse_private_custom_sections w)\), - balances := list_map_set (balances S) cid (bal - (cycles_return.cycles_used pre_ret + cycles_return.cycles_used post_ret)), + certified_data := (case init_return.new_certified_data post_ret of Some cd' \ list_map_set (certified_data S) cid cd' + | None \ (case pre_upgrade_return.new_certified_data pre_ret of Some cd \ list_map_set (certified_data S) cid cd + | None \ certified_data S)), + global_timer := list_map_set (global_timer S) cid (case init_return.new_global_timer post_ret of None \ 0 | Some new_timer \ new_timer), + canister_version := list_map_set (canister_version S) cid (Suc idx), + balances := list_map_set (balances S) cid (bal - (pre_upgrade_return.cycles_used pre_ret + init_return.cycles_used post_ret)), messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid Candid_empty)) trans_cycles]\)))))))" definition ic_code_upgrade_burned_cycles :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where @@ -1685,12 +1782,13 @@ definition ic_code_upgrade_burned_cycles :: "nat \ ('p, 'uid, 'canid (case (candid_parse_text a [encode_string ''mode''], candid_parse_blob a [encode_string ''wasm_module''], candid_parse_blob a [encode_string ''arg'']) of (Some mode, Some w, Some ar) \ (case parse_wasm_mod w of Some m \ - (case (list_map_get (canisters S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid) of - (Some (Some can), Some t, Some bal, Some can_status) \ - let env = \env.time = t, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status\ in - (case canister_module_pre_upgrade (module can) (wasm_state can, cer, env) of Inr pre_ret \ - (case canister_module_post_upgrade m (cid, cycles_return.return pre_ret, ar, cer, env) of Inr post_ret \ - cycles_return.cycles_used pre_ret + cycles_return.cycles_used post_ret)))))))" + (case (list_map_get (canisters S) cid, list_map_get (time S) cid, list_map_get (balances S) cid, list_map_get (canister_status S) cid, list_map_get (canister_version S) cid, list_map_get (global_timer S) cid) of + (Some (Some can), Some t, Some bal, Some can_status, Some idx, Some timer) \ + let env1 = \env.time = t, env.global_timer = timer, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = idx\; + env2 = \env.time = t, env.global_timer = 0, balance = bal, freezing_limit = ic_freezing_limit S cid, certificate = None, status = simple_status can_status, canister_version = Suc idx\ in + (case canister_module_pre_upgrade (module can) (wasm_state can, cer, env1) of Inr pre_ret \ + (case canister_module_post_upgrade m (cid, pre_upgrade_return.stable_memory pre_ret, ar, cer, env2) of Inr post_ret \ + pre_upgrade_return.cycles_used pre_ret + init_return.cycles_used post_ret)))))))" lemma ic_code_upgrade_cycles_inv: assumes "ic_code_upgrade_pre n S" @@ -1715,7 +1813,7 @@ lemma ic_code_upgrade_ic_inv: assumes "ic_code_upgrade_pre n S" "ic_inv S" shows "ic_inv (ic_code_upgrade_post n S)" proof - - obtain orig cer cee mn a trans_cycles q cid mode w ar m can ctrls t bal can_status idx where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" + obtain orig cer cee mn a trans_cycles q cid mode w ar m can ctrls t bal can_status idx timer where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" and parse: "candid_parse_cid a = Some cid" "candid_parse_text a [encode_string ''mode''] = Some mode" "candid_parse_blob a [encode_string ''wasm_module''] = Some w" @@ -1727,6 +1825,8 @@ proof - "list_map_get (time S) cid = Some t" "list_map_get (balances S) cid = Some bal" "list_map_get (canister_status S) cid = Some can_status" + "list_map_get (canister_version S) cid = Some idx" + "list_map_get (global_timer S) cid = Some timer" using assms by (auto simp: ic_code_upgrade_pre_def split: message.splits option.splits) show ?thesis @@ -1746,7 +1846,7 @@ definition ic_code_uninstallation_pre :: "nat \ ('p, 'uid, 'canid, ' cee = ic_principal \ mn = encode_string ''uninstall_code'' \ (case candid_parse_cid a of Some cid \ - (case list_map_get (controllers S) cid of Some ctrls \ cer \ ctrls + (case (list_map_get (controllers S) cid, list_map_get (canister_version S) cid) of (Some ctrls, Some idx) \ cer \ ctrls | _ \ False) | _ \ False) | _ \ False))" @@ -1757,8 +1857,11 @@ definition ic_code_uninstallation_post :: "nat \ ('p, 'uid, 'canid, if call_ctxt_canister ctxt = cid \ call_ctxt_needs_to_respond ctxt then Some (Response_message (call_ctxt_origin ctxt) (response.Reject CANISTER_REJECT (encode_string ''Canister has been uninstalled'')) (call_ctxt_available_cycles ctxt)) else None); - call_ctxt_to_ctxt = (\ctxt. if call_ctxt_canister ctxt = cid then call_ctxt_delete ctxt else ctxt) in + call_ctxt_to_ctxt = (\ctxt. if call_ctxt_canister ctxt = cid then call_ctxt_delete ctxt else ctxt); + idx = the (list_map_get (canister_version S) cid) in S\canisters := list_map_set (canisters S) cid None, certified_data := list_map_set (certified_data S) cid empty_blob, + canister_version := list_map_set (canister_version S) cid (Suc idx), + global_timer := list_map_set (global_timer S) cid 0, messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid Candid_empty)) trans_cycles] @ List.map_filter call_ctxt_to_msg (list_map_vals (call_contexts S)), call_contexts := list_map_map call_ctxt_to_ctxt (call_contexts S)\))" @@ -2142,7 +2245,9 @@ definition ic_canister_deletion_post :: "nat \ ('p, 'uid, 'canid, 'b controllers := list_map_del (controllers S) cid, freezing_threshold := list_map_del (freezing_threshold S) cid, canister_status := list_map_del (canister_status S) cid, + canister_version := list_map_del (canister_version S) cid, time := list_map_del (time S) cid, + global_timer := list_map_del (global_timer S) cid, balances := list_map_del (balances S) cid, certified_data := list_map_del (certified_data S) cid, messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid Candid_empty)) trans_cycles]\)" @@ -2292,10 +2397,12 @@ definition ic_provisional_canister_creation_pre :: "nat \ 'canid \ cid \ list_map_dom (canisters S) \ cid \ list_map_dom (time S) \ + cid \ list_map_dom (global_timer S) \ cid \ list_map_dom (controllers S) \ cid \ list_map_dom (balances S) \ cid \ list_map_dom (certified_data S) \ - cid \ list_map_dom (canister_status S) + cid \ list_map_dom (canister_status S) \ + cid \ list_map_dom (canister_version S) | _ \ False) | _ \ False))" definition ic_provisional_canister_creation_post :: "nat \ 'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where @@ -2303,13 +2410,15 @@ definition ic_provisional_canister_creation_post :: "nat \ 'canid \< let cyc = the (candid_parse_nat a [encode_string ''amount'']) in S\canisters := list_map_set (canisters S) cid None, time := list_map_set (time S) cid t, + global_timer := list_map_set (global_timer S) cid 0, controllers := list_map_set (controllers S) cid {cer}, freezing_threshold := list_map_set (freezing_threshold S) cid 2592000, balances := list_map_set (balances S) cid cyc, certified_data := list_map_set (certified_data S) cid empty_blob, messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid (Candid_record (list_map_init [(encode_string ''canister_id'', Candid_blob (blob_of_canid cid))])))) trans_cycles], - canister_status := list_map_set (canister_status S) cid Running\)" + canister_status := list_map_set (canister_status S) cid Running, + canister_version := list_map_set (canister_version S) cid 0\)" definition ic_provisional_canister_creation_minted_cycles :: "nat \ 'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where "ic_provisional_canister_creation_minted_cycles n cid t S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ @@ -2602,7 +2711,7 @@ lemma request_cleanup_expired_ic_inv: (* System transition: Canister out of cycles [DONE] *) definition canister_out_of_cycles_pre :: "'canid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "canister_out_of_cycles_pre cid S = (case list_map_get (balances S) cid of Some 0 \ True + "canister_out_of_cycles_pre cid S = (case (list_map_get (balances S) cid, list_map_get (canister_version S) cid) of (Some 0, Some idx) \ True | _ \ False)" definition canister_out_of_cycles_post :: "'canid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where @@ -2611,8 +2720,11 @@ definition canister_out_of_cycles_post :: "'canid \ ('p, 'uid, 'cani if call_ctxt_canister ctxt = cid \ call_ctxt_needs_to_respond ctxt then Some (Response_message (call_ctxt_origin ctxt) (response.Reject CANISTER_REJECT (encode_string ''Canister has been uninstalled'')) (call_ctxt_available_cycles ctxt)) else None); - call_ctxt_to_ctxt = (\ctxt. if call_ctxt_canister ctxt = cid then call_ctxt_delete ctxt else ctxt) in + call_ctxt_to_ctxt = (\ctxt. if call_ctxt_canister ctxt = cid then call_ctxt_delete ctxt else ctxt); + idx = the (list_map_get (canister_version S) cid) in S\canisters := list_map_set (canisters S) cid None, certified_data := list_map_set (certified_data S) cid empty_blob, + canister_version := list_map_set (canister_version S) cid (Suc idx), + global_timer := list_map_set (global_timer S) cid 0, messages := messages S @ List.map_filter call_ctxt_to_msg (list_map_vals (call_contexts S)), call_contexts := list_map_map call_ctxt_to_ctxt (call_contexts S)\)" @@ -2644,7 +2756,7 @@ lemma canister_out_of_cycles_ic_inv: -(* System transition: Time progressing and cycle consumption (canister time) [DONE] *) +(* System transition: Time progressing, cycle consumption, and canister version increments (canister time) [DONE] *) definition canister_time_progress_pre :: "'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where "canister_time_progress_pre cid t1 S = (case list_map_get (time S) cid of Some t0 \ @@ -2670,7 +2782,7 @@ lemma canister_time_progress_ic_inv: -(* System transition: Time progressing and cycle consumption (cycle consumption) [DONE] *) +(* System transition: Time progressing, cycle consumption, and canister version increments (cycle consumption) [DONE] *) definition cycle_consumption_pre :: "'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where "cycle_consumption_pre cid b1 S = (case list_map_get (balances S) cid of Some b0 \ @@ -2701,7 +2813,7 @@ lemma cycle_consumption_ic_inv: -(* System transition: Time progressing and cycle consumption (system time) [DONE] *) +(* System transition: Time progressing, cycle consumption, and canister version increments (system time) [DONE] *) definition system_time_progress_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where "system_time_progress_pre t1 S = (system_time S < t1)" @@ -2725,6 +2837,32 @@ lemma system_time_progress_ic_inv: +(* System transition: Time progressing, cycle consumption, and canister version increments (canister version) [DONE] *) + +definition canister_version_progress_pre :: "'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where + "canister_version_progress_pre cid n1 S = (case list_map_get (canister_version S) cid of Some n0 \ + n0 < n1 + | _ \ False)" + +definition canister_version_progress_post :: "'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where + "canister_version_progress_post cid n1 S = (S\canister_version := list_map_set (canister_version S) cid n1\)" + +lemma canister_version_progress_cycles_inv: + assumes "canister_version_progress_pre cid n1 S" + shows "total_cycles S = total_cycles (canister_version_progress_post cid n1 S)" + by (auto simp: canister_version_progress_post_def total_cycles_def) + +lemma canister_version_progress_ic_inv: + assumes "canister_version_progress_pre cid n1 S" "ic_inv S" + shows "ic_inv (canister_version_progress_post cid n1 S)" + using assms + by (auto simp: ic_inv_def canister_version_progress_pre_def canister_version_progress_post_def Let_def + split: sum.splits message.splits call_origin.splits option.splits if_splits can_status.splits + dest!: in_set_takeD in_set_dropD in_set_updD list_map_range_setD list_map_get_range list_map_range_del + in_set_map_filter_vals) + + + (* State machine *) inductive ic_steps :: "'sig itself \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ @@ -2765,6 +2903,7 @@ inductive ic_steps :: "'sig itself \ ('p, 'uid, 'canid, 'b, 'w, 'sm, | canister_time_progress: "ic_steps sig S0 minted burned S \ canister_time_progress_pre cid t1 S \ ic_steps sig S0 minted burned (canister_time_progress_post cid t1 S)" | cycle_consumption: "ic_steps sig S0 minted burned S \ cycle_consumption_pre cid b1 S \ ic_steps sig S0 minted (burned + cycle_consumption_burned_cycles cid b1 S) (cycle_consumption_post cid b1 S)" | system_time_progress: "ic_steps sig S0 minted burned S \ system_time_progress_pre t1 S \ ic_steps sig S0 minted burned (system_time_progress_post t1 S)" +| canister_version_progress: "ic_steps sig S0 minted burned S \ canister_version_progress_pre cid n1 S \ ic_steps sig S0 minted burned (canister_version_progress_post cid n1 S)" lemma total_cycles: assumes "ic_steps TYPE('sig) S0 minted burned S" @@ -2807,6 +2946,7 @@ lemma total_cycles: using canister_time_progress_cycles_inv apply fastforce using cycle_consumption_cycles_monotonic apply fastforce using system_time_progress_cycles_inv apply fastforce + using canister_version_progress_cycles_inv apply fastforce done lemma ic_inv: @@ -2850,6 +2990,7 @@ lemma ic_inv: using canister_time_progress_ic_inv apply fastforce using cycle_consumption_ic_inv apply fastforce using system_time_progress_ic_inv apply fastforce + using canister_version_progress_ic_inv apply fastforce done end @@ -2889,6 +3030,7 @@ export_code request_submission_pre request_submission_post canister_time_progress_pre canister_time_progress_post cycle_consumption_pre cycle_consumption_post system_time_progress_pre system_time_progress_post + canister_version_progress_pre canister_version_progress_post in Haskell module_name IC file_prefix code end