From d265c2c6f2dd0ffa4767d25fec002d9d28525291 Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Fri, 28 Jul 2023 13:16:14 +0200 Subject: [PATCH 01/12] rephrase description of create_canister method (#207) --- spec/index.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/spec/index.md b/spec/index.md index 652c1f632..ebc4f3e49 100644 --- a/spec/index.md +++ b/spec/index.md @@ -1776,7 +1776,9 @@ The optional `settings` parameter can be used to set the following settings: - `controllers` (`vec principal`) - A list of principals. Must be between 0 and 10 in size. This value is assigned to the *controllers* attribute of the canister. + A list of at most 10 principals. The principals in this list become the *controllers* of the canister. + Note that the caller of the `create_canister` call is not a controller of the canister + unless it is a member of the `controllers` list. Default value: A list containing only the caller of the `create_canister` call. From 5a8c93f8cd316ddc9890ff04153b5412f863b267 Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Fri, 28 Jul 2023 13:18:58 +0200 Subject: [PATCH 02/12] update ecdsa_public_key specs (#208) --- spec/index.md | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/spec/index.md b/spec/index.md index ebc4f3e49..23af818c8 100644 --- a/spec/index.md +++ b/spec/index.md @@ -1934,14 +1934,12 @@ This method takes no input and returns 32 pseudo-random bytes to the caller. The ### IC method `ecdsa_public_key` {#ic-ecdsa_public_key} -This method returns a [SEC1](https://www.secg.org/sec1-v2.pdf) encoded ECDSA public key for the given canister using the given derivation path. If the `canister_id` is unspecified, it will default to the canister id of the caller. The `derivation_path` is a vector of variable length byte strings. Each byte string may be of arbitrary length, including empty. The total number of strings in `derivation_path` can be at most 255. The `key_id` is a struct specifying both a curve and a name. The availability of a particular `key_id` depends on implementation. +This method returns a [SEC1](https://www.secg.org/sec1-v2.pdf) encoded ECDSA public key for the given canister using the given derivation path. If the `canister_id` is unspecified, it will default to the canister id of the caller. The `derivation_path` is a vector of variable length byte strings. Each byte string may be of arbitrary length, including empty. The total number of byte strings in the `derivation_path` must be at most 255. The `key_id` is a struct specifying both a curve and a name. The availability of a particular `key_id` depends on implementation. -For curve `secp256k1`, the public key is derived using a generalization of BIP32 (see [ia.cr/2021/1330, Appendix D](https://ia.cr/2021/1330)). To derive (non-hardened) [BIP-0032](https://github.com/bitcoin/bips/blob/master/bip-0032.mediawiki)-compatible public keys, each byte string (`blob`) in the `derivation_path` must be a 4-byte big-endian encoding of an unsigned integer less than 231. +For curve `secp256k1`, the public key is derived using a generalization of BIP32 (see [ia.cr/2021/1330, Appendix D](https://ia.cr/2021/1330)). To derive (non-hardened) [BIP32](https://github.com/bitcoin/bips/blob/master/bip-0032.mediawiki)-compatible public keys, each byte string (`blob`) in the `derivation_path` must be a 4-byte big-endian encoding of an unsigned integer less than 231. If the `derivation_path` contains a byte string that is not a 4-byte big-endian encoding of an unsigned integer less than 231, then a derived public key will be returned, but that key derivation process will not be compatible with the [BIP32](https://github.com/bitcoin/bips/blob/master/bip-0032.mediawiki) standard. The return result is an extended public key consisting of an ECDSA `public_key`, encoded in [SEC1](https://www.secg.org/sec1-v2.pdf) compressed form, and a `chain_code`, which can be used to deterministically derive child keys of the `public_key`. -This call requires that the ECDSA feature is enabled, and the `canister_id` meets the requirement of a canister id. Otherwise it will be rejected. - ### IC method `sign_with_ecdsa` {#ic-sign_with_ecdsa} This method returns a new [ECDSA](https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.186-4.pdf) signature of the given `message_hash` that can be separately verified against a derived ECDSA public key. This public key can be obtained by calling `ecdsa_public_key` with the caller's `canister_id`, and the same `derivation_path` and `key_id` used here. From 3f62116689942167744270a883542b468111f6da Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Fri, 28 Jul 2023 13:25:06 +0200 Subject: [PATCH 03/12] drop formal model in Isabelle/HOL (#206) --- .github/workflows/isabelle.yml | 23 - README.md | 20 - theories/IC.thy | 3098 -------------------------------- theories/ROOT | 8 - 4 files changed, 3149 deletions(-) delete mode 100644 .github/workflows/isabelle.yml delete mode 100644 theories/IC.thy delete mode 100644 theories/ROOT diff --git a/.github/workflows/isabelle.yml b/.github/workflows/isabelle.yml deleted file mode 100644 index 2b2a018d6..000000000 --- a/.github/workflows/isabelle.yml +++ /dev/null @@ -1,23 +0,0 @@ -name: Build on Ubuntu -on: - push: - paths: - - 'theories/**' - -jobs: - isabelle: - runs-on: ubuntu-latest - steps: - - name: Check out the repo - uses: actions/checkout@v2 - - name: Run Isabelle with Docker - uses: addnab/docker-run-action@v3 - with: - image: martin2718/isabelle - options: -v ${{ github.workspace }}:/interface-spec - run: Isabelle/bin/isabelle build -e -v -D /interface-spec/theories/ - - name: Haskell Code - uses: actions/upload-artifact@v2 - with: - name: haskell-code - path: ${{ github.workspace }}/theories/code diff --git a/README.md b/README.md index e8eeef12b..fdb11a137 100644 --- a/README.md +++ b/README.md @@ -31,26 +31,6 @@ The `master` branch contains finished designs, but is not directly scheduled for implementation. It lists version version number `∞`. The reference implementation on this branch typically does _not_ fully implement the spec. This branch should always be “ahead” of all the release branches. -## Formal Model - -We are developing a formal model of Interface Spec in the interactive theorem prover [Isabelle/HOL](https://isabelle.in.tum.de/). -The formal development is included in the directory `theories/`. - -To setup the environment, follow the standard [instructions](https://isabelle.in.tum.de/installation.html) for Isabelle/HOL. -Additionally, you may want to setup `isabelle` as an alias for the path `bin/isabelle` in your local Isabelle directory. - -To browse the formal model, open Isabelle/jEdit: -``` -isabelle jedit theories/IC.thy -``` -from the root directory of this repository. - -To build the formal model and export Haskell code from the formal model, run -``` -isabelle build -e -v -D theories/ -``` -in the root directory of this repository. The exported Haskell code can then be found under `theories/code/`. - ## Contributing This repository accepts external contributions, conditioned on acceptance of the [Contributor Lincense Agreement](https://github.com/dfinity/cla/). diff --git a/theories/IC.thy b/theories/IC.thy deleted file mode 100644 index f760e71e8..000000000 --- a/theories/IC.thy +++ /dev/null @@ -1,3098 +0,0 @@ -theory IC - imports "HOL-Library.AList" -begin - -(* General helper lemmas *) - -lemma in_set_updD: "x \ set (xs[n := z]) \ x \ set xs \ x = z" - by (meson insert_iff set_update_subset_insert subsetD) - -(* Partial maps *) - -typedef ('a, 'b) list_map = "{f :: ('a \ 'b) list. distinct (map fst f)}" - by (auto intro: exI[of _ "[]"]) - -setup_lifting type_definition_list_map - -lift_bnf (dead 'k, set: 'v) list_map [wits: "[] :: ('k \ 'v) list"] for map: map rel: rel - by auto - -hide_const (open) map set rel - -lift_definition list_map_dom :: "('a, 'b) list_map \ 'a set" is - "set \ map fst" . - -lift_definition list_map_vals :: "('a, 'b) list_map \ 'b list" is - "map snd" . - -lift_definition list_map_range :: "('a, 'b) list_map \ 'b set" is - "set \ map snd" . - -lemma in_set_map_filter_vals: "z \ set (List.map_filter g (list_map_vals f)) \ \w \ list_map_range f. g w = Some z" - by transfer (force simp: List.map_filter_def) - -lift_definition list_map_sum_vals :: "('b \ nat) \ ('a, 'b) list_map \ nat" is - "\g. sum_list \ (map (g \ snd))" . - -lift_definition list_map_get :: "('a, 'b) list_map \ 'a \ 'b option" is - "map_of" . - -lemma list_map_get_dom[dest]: "x \ list_map_dom f \ list_map_get f x = None \ False" - by transfer auto - -lemma list_map_get_range: "list_map_get f x = Some y \ y \ list_map_range f" - by transfer force - -lift_definition list_map_set :: "('a, 'b) list_map \ 'a \ 'b \ ('a, 'b) list_map" is - "\f x y. AList.update x y f" - by (rule distinct_update) - -lemma list_map_get_set: "list_map_get (list_map_set f x y) z = (if x = z then Some y else list_map_get f z)" - by transfer (auto simp add: update_Some_unfold update_conv) - -lemma list_map_dom_set[simp]: "list_map_dom (list_map_set f x y) = list_map_dom f \ {x}" - by transfer (auto simp add: dom_update) - -lemma list_map_range_setD: "z \ list_map_range (list_map_set f x y) \ z \ list_map_range f \ z = y" - apply transfer - apply auto - apply (metis distinct_update image_iff map_of_eq_Some_iff snd_eqD update_Some_unfold) - done - -lift_definition list_map_del :: "('a, 'b) list_map \ 'a \ ('a, 'b) list_map" is - "\f x. AList.delete x f" - by (rule distinct_delete) - -lemma list_map_get_del: "list_map_get (list_map_del f x) z = (if x = z then None else list_map_get f z)" - by transfer (auto simp add: delete_conv') - -lemma list_map_dom_del[simp]: "list_map_dom (list_map_del f x) = list_map_dom f - {x}" - by transfer (simp add: delete_keys) - -lemma list_map_range_del: "z \ list_map_range (list_map_del f x) \ z \ list_map_range f" - apply transfer - apply auto - apply (metis Some_eq_map_of_iff delete_notin_dom distinct_delete fst_eqD imageI map_of_delete snd_eqD) - done - -lift_definition list_map_empty :: "('a, 'b) list_map" is "[]" - by auto - -lemma list_map_get_empty[simp]: "list_map_get list_map_empty x = None" - by transfer auto - -lemma list_map_empty_dom[simp]: "list_map_dom list_map_empty = {}" - by transfer auto - -lemma list_map_empty_range[simp]: "list_map_range list_map_empty = {}" - by transfer auto - -lift_definition list_map_init :: "('a \ 'b) list \ ('a, 'b) list_map" is - "\xys. AList.updates (map fst xys) (map snd xys) []" - using distinct_updates - by force - -lift_definition list_map_map :: "('b \ 'c) \ ('a, 'b) list_map \ ('a, 'c) list_map" is - "\f xs. map (\(k, v). (k, f v)) xs" - by (auto simp: comp_def case_prod_beta) - -lemma list_map_dom_map_map[simp]: "list_map_dom (list_map_map g f) = list_map_dom f" - by transfer force - -lemma list_map_range_map_map[simp]: "list_map_range (list_map_map g f) = g ` list_map_range f" - by transfer force - -lemma list_map_sum_vals_split: "(\ctxt. ctxt \ list_map_range xs \ f (g ctxt) \ f ctxt) \ list_map_sum_vals f xs = - list_map_sum_vals id - (list_map_map (\ctxt. if P ctxt then f ctxt - f (g ctxt) else 0) xs) + - list_map_sum_vals f - (list_map_map (\ctxt. if P ctxt then g ctxt else ctxt) xs)" - apply (transfer fixing: f g P) - subgoal for xs - by (induction xs) auto - done - -lemma list_map_sum_vals_filter: - assumes "\b. b \ list_map_range xs \ P b = None \ f b = 0" "\b y. b \ list_map_range xs \ P b = Some y \ f b = g y" - shows "list_map_sum_vals id (list_map_map f xs) = sum_list (map g (List.map_filter P (list_map_vals xs)))" - using assms - apply (transfer fixing: f g P) - subgoal for xs - by (induction xs) (auto simp: List.map_filter_def) - done - -lemma list_map_sum_in_ge_aux: - fixes g :: "'a \ nat" - shows "distinct (map fst f) \ map_of f x = Some y \ g y \ sum_list (map g (map snd f))" - by (induction f) (auto split: if_splits) - -lemma list_map_sum_in_ge: "list_map_get f x = Some y \ list_map_sum_vals g f \ g y" - apply transfer - using list_map_sum_in_ge_aux[OF _ map_of_is_SomeI] - by fastforce - -lemma list_map_sum_in_aux: fixes g :: "'a \ nat" - shows "distinct (map fst f) \ map_of f x = Some y \ - sum_list (map (g \ snd) (AList.update x y' f)) = sum_list (map (g \ snd) f) + g y' - g y" - apply (induction f) - apply auto[1] - subgoal for a f - using list_map_sum_in_ge_aux[OF _ map_of_is_SomeI, of f x y g] - by auto - done - -lemma list_map_sum_in: "list_map_get f x = Some y \ list_map_sum_vals g (list_map_set f x y') = list_map_sum_vals g f + g y' - g y" - apply transfer - using list_map_sum_in_aux - by fastforce - -lemma list_map_sum_out_aux: - "x \ set (map fst f) \ sum_list (map (g \ snd) (AList.update x y f)) = sum_list (map (g \ snd) f) + g y" - by (induction f) (auto simp: add.assoc) - -lemma list_map_sum_out: "x \ list_map_dom f \ list_map_sum_vals g (list_map_set f x y) = list_map_sum_vals g f + g y" - apply transfer - using list_map_sum_out_aux - by fastforce - -lemma list_map_del_sum_aux: - fixes g :: "'a \ nat" - shows "distinct (map fst f) \ map_of f x = Some y \ sum_list (map (g \ snd) f) = sum_list (map (g \ snd) (AList.delete x f)) + g y" - by (induction f) auto - -lemma list_map_del_sum: "list_map_get f x = Some y \ list_map_sum_vals g f = list_map_sum_vals g (list_map_del f x) + g y" - apply transfer - using list_map_del_sum_aux - by fastforce - -(* Abstract behaviour *) - -(* Abstract canisters *) - -type_synonym 's method_name = 's - -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 = - Reply "'b" -| Reject reject_code 's -record ('p, 'canid, 's, 'b, 'c) method_call = - callee :: 'canid - method_name :: "'s method_name" - arg :: 'b - transferred_cycles :: nat - callback :: 'c - -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, '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, '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, '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, '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, 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, '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, '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 . - -lift_definition dispatch_method :: "'s \ ('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module \ - ((('b arg \ 'p \ 'b env \ available_cycles) \ ('w, 'p, 'canid, 's, 'b, 'c) update_func) + (('b arg \ 'p \ 'b env) \ ('w, 'b, 's) query_func)) option" is - "\f m. case list_map_get (update_methods m) f of Some f' \ Some (Inl f') | None \ (case list_map_get (query_methods m) f of Some f' \ Some (Inr f') | None \ None)" . - -(* Call contexts *) - -record ('b, 'p, 'uid, 'canid, 's) request = - nonce :: 'b - ingress_expiry :: nat - sender :: 'uid - canister_id :: 'canid - method_name :: 's - arg :: 'b -datatype ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin = - From_user "('b, 'p, 'uid, 'canid, 's) request" -| From_canister "'cid" "'c" -| 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" - needs_to_respond :: bool - deleted :: bool - available_cycles :: nat - -typedef ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt = "{ctxt :: ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt_rep. - (deleted ctxt \ \needs_to_respond ctxt) \ (\needs_to_respond ctxt \ available_cycles ctxt = 0)}" - by (auto intro: exI[of _ "\canister = undefined, origin = undefined, needs_to_respond = True, deleted = False, available_cycles = 0\"]) - -setup_lifting type_definition_call_ctxt - -lift_definition call_ctxt_canister :: "('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt \ 'canid" is "canister" . -lift_definition call_ctxt_origin :: "('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt \ ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin" is "origin" . -lift_definition call_ctxt_needs_to_respond :: "('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt \ bool" is needs_to_respond . -lift_definition call_ctxt_deleted :: "('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt \ bool" is deleted . -lift_definition call_ctxt_available_cycles :: "('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt \ nat" is available_cycles . - -lemma call_ctxt_not_needs_to_respond_available_cycles: "\call_ctxt_needs_to_respond x2 \ call_ctxt_available_cycles x2 = 0" - by transfer auto - -lift_definition call_ctxt_respond :: "('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt \ ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt" is - "\ctxt. ctxt\needs_to_respond := False, available_cycles := 0\" - by auto - -lemma call_ctxt_respond_canister[simp]: "call_ctxt_canister (call_ctxt_respond ctxt) = call_ctxt_canister ctxt" - by transfer auto - -lemma call_ctxt_respond_origin[simp]: "call_ctxt_origin (call_ctxt_respond ctxt) = call_ctxt_origin ctxt" - by transfer auto - -lemma call_ctxt_respond_needs_to_respond[dest]: "call_ctxt_needs_to_respond (call_ctxt_respond ctxt) \ False" - by transfer auto - -lemma call_ctxt_respond_available_cycles[simp]: "call_ctxt_available_cycles (call_ctxt_respond ctxt) = 0" - by transfer auto - -lift_definition call_ctxt_deduct_cycles :: "nat \ ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt \ ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt" is - "\n ctxt. ctxt\available_cycles := available_cycles ctxt - n\" - by auto - -lemma call_ctxt_deduct_cycles_canister[simp]: "call_ctxt_canister (call_ctxt_deduct_cycles n ctxt) = call_ctxt_canister ctxt" - by transfer auto - -lemma call_ctxt_deduct_cycles_origin[simp]: "call_ctxt_origin (call_ctxt_deduct_cycles n ctxt) = call_ctxt_origin ctxt" - by transfer auto - -lemma call_ctxt_deduct_cycles_needs_to_respond[simp]: "call_ctxt_needs_to_respond (call_ctxt_deduct_cycles n ctxt) = call_ctxt_needs_to_respond ctxt" - by transfer auto - -lemma call_ctxt_deduct_cycles_available_cycles[simp]: "call_ctxt_available_cycles (call_ctxt_deduct_cycles n ctxt) = call_ctxt_available_cycles ctxt - n" - by transfer auto - -lift_definition call_ctxt_delete :: "('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt \ ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt" is - "\ctxt. ctxt\deleted := True, needs_to_respond := False, available_cycles := 0\" - by auto - -lemma call_ctxt_delete_canister[simp]: "call_ctxt_canister (call_ctxt_delete ctxt) = call_ctxt_canister ctxt" - by transfer auto - -lemma call_ctxt_delete_needs_to_respond[simp]: "call_ctxt_needs_to_respond (call_ctxt_delete ctxt) = False" - by transfer auto - -(* Calls and Messages *) - -datatype 'canid queue_origin = System | Canister 'canid -datatype 'canid queue = Unordered | Queue "'canid queue_origin" 'canid -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" -| Func_message 'cid 'canid "('s, 'p, 'b, 'c) entry_point" "'canid queue" -| Response_message "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin" "('b, 's) response" nat - -(* API requests *) - -type_synonym 'b path = "'b list" -record ('b, 'uid) StateRead = - nonce :: 'b - ingress_expiry :: nat - sender :: 'uid - paths :: "'b path list" -record ('b, 'uid, 'canid, 's) CanisterQuery = - nonce :: 'b - ingress_expiry :: nat - sender :: 'uid - canister_id :: 'canid - method_name :: 's - arg :: 'b -type_synonym ('b, 'uid, 'canid, 's) APIReadRequest = "('b, 'uid) StateRead + ('b, 'uid, 'canid, 's) CanisterQuery" - -record ('p, 'canid, 'pk, 'sig) delegation = - pubkey :: 'pk - targets :: "'canid list option" - senders :: "'p list option" - expiration :: timestamp -record ('p, 'canid, 'pk, 'sig) signed_delegation = - delegation :: "('p, 'canid, 'pk, 'sig) delegation" - signature :: "'sig" - -record ('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) envelope = - content :: "('b, 'p, 'uid, 'canid, 's) request + ('b, 'uid, 'canid, 's) APIReadRequest" - sender_pubkey :: "'pk option" - sender_sig :: "'sig option" - sender_delegation :: "('p, 'canid, 'pk, 'sig) delegation list" - -datatype ('b, 's) request_status = Received | Processing | Rejected reject_code 's | Replied 'b | Done - -(* The system state *) - -record ('p, 'canid, 'b, 'w, 'sm, 'c, 's) can_state_rec = - wasm_state :: 'w - module :: "('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module" - raw_module :: 'b - public_custom_sections :: "('s, 'b) list_map" - private_custom_sections :: "('s, 'b) list_map" -type_synonym ('p, 'canid, 'b, 'w, 'sm, 'c, 's) can_state = "('p, 'canid, 'b, 'w, 'sm, 'c, 's) can_state_rec option" -datatype ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) can_status = Running | Stopping "(('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin \ nat) list" | Stopped -record ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic = - requests :: "(('b, 'p, 'uid, 'canid, 's) request, ('b, 's) request_status) list_map" - canisters :: "('canid, ('p, 'canid, 'b, 'w, 'sm, 'c, 's) can_state) list_map" - 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 - call_contexts :: "('cid, ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt) list_map" - messages :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) message list" - root_key :: 'pk - -fun simple_status :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) can_status \ status" where - "simple_status can_status.Running = status.Running" -| "simple_status (can_status.Stopping _) = status.Stopping" -| "simple_status can_status.Stopped = status.Stopped" - -(* Initial state *) - -definition initial_ic :: "nat \ 'pk \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where - "initial_ic t pk = \requests = list_map_empty, - canisters = list_map_empty, - 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, - call_contexts = list_map_empty, - messages = [], - root_key = pk\" - -(* Invariants *) - -definition ic_can_status_inv :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) can_status set \ 'cid set \ bool" where - "ic_can_status_inv st c = (\can_status \ st. - case can_status of Stopping os \ \(orig, cycles) \ set os. (case orig of - From_canister ctxt_id _ \ ctxt_id \ c - | _ \ True) - | _ \ True)" - -lemma ic_can_status_inv_mono1: "ic_can_status_inv x y \ - z \ x \ {can_status.Running, can_status.Stopped} \ - ic_can_status_inv z y" - by (fastforce simp: ic_can_status_inv_def split: can_status.splits call_origin.splits) - -lemma ic_can_status_inv_mono2: "ic_can_status_inv x y \ - y \ z \ - ic_can_status_inv x z" - by (force simp: ic_can_status_inv_def split: can_status.splits call_origin.splits) - -lemma ic_can_status_inv_stopping: "ic_can_status_inv x y \ - (\ctxt_id c. os = From_canister ctxt_id c \ ctxt_id \ y) \ - z \ x \ {can_status.Stopping [(os, cyc)]} \ - ic_can_status_inv z y" - by (fastforce simp: ic_can_status_inv_def split: can_status.splits call_origin.splits) - -lemma ic_can_status_inv_stopping_app: "ic_can_status_inv x y \ - can_status.Stopping w \ x \ - (\ctxt_id c. os = From_canister ctxt_id c \ ctxt_id \ y) \ - z \ x \ {can_status.Stopping (w @ [(os, cyc)])} \ - ic_can_status_inv z y" - by (force simp: ic_can_status_inv_def split: can_status.splits call_origin.splits dest!: subsetD[where ?A=z]) - -lemma ic_can_status_inv_del: "ic_can_status_inv x z \ - (\os other_ctxt_id c cyc. Stopping os \ x \ (From_canister other_ctxt_id c, cyc) \ set os \ ctxt_id \ other_ctxt_id) \ - ic_can_status_inv x (z - {ctxt_id})" - by (fastforce simp: ic_can_status_inv_def split: can_status.splits call_origin.splits) - -definition ic_inv_call_ctxt_stopped :: "('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt set \ - ('canid, ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) can_status) list_map \ bool" where - "ic_inv_call_ctxt_stopped ctxts can_status = (\ctxt \ ctxts. list_map_get can_status (call_ctxt_canister ctxt) \ Some Stopped)" - -lemma ic_inv_call_ctxt_stopped_mono1: - assumes "ic_inv_call_ctxt_stopped (list_map_range ctxts) can_status" - shows "ic_inv_call_ctxt_stopped (list_map_range (list_map_del ctxts ctxt_id)) can_status" - using assms - by (auto simp: ic_inv_call_ctxt_stopped_def list_map_range_del) - -lemma ic_inv_call_ctxt_stopped_mono2: - assumes "ic_inv_call_ctxt_stopped ctxts can_status" - shows "ic_inv_call_ctxt_stopped ctxts (list_map_del can_status can_id)" - using assms - by (auto simp: ic_inv_call_ctxt_stopped_def list_map_get_del) - -lemma ic_inv_stopped_ctxt_stopped_set_running: - assumes "ic_inv_call_ctxt_stopped ctxts can_status" - shows "ic_inv_call_ctxt_stopped ctxts (list_map_set can_status cid Running)" - using assms - by (auto simp: ic_inv_call_ctxt_stopped_def list_map_get_set) - -lemma ic_inv_call_ctxt_stopped_set_stopping: - assumes "ic_inv_call_ctxt_stopped ctxts can_status" - shows "ic_inv_call_ctxt_stopped ctxts (list_map_set can_status can_id (Stopping os))" - using assms - by (auto simp: ic_inv_call_ctxt_stopped_def list_map_get_set) - -lemma ic_inv_call_ctxt_stopped_set_stopped: - assumes "ic_inv_call_ctxt_stopped ctxts can_status" - "\ctxt. ctxt \ ctxts \ call_ctxt_canister ctxt \ cid" - shows "ic_inv_call_ctxt_stopped ctxts (list_map_set can_status cid Stopped)" - using assms - by (auto simp: ic_inv_call_ctxt_stopped_def list_map_get_set) - -lemma ic_inv_call_ctxt_stopped_set_respond: - assumes "ic_inv_call_ctxt_stopped (list_map_range ctxts) can_status" "ctxt \ list_map_range ctxts" - shows "ic_inv_call_ctxt_stopped (list_map_range (list_map_set ctxts ctxt_id (call_ctxt_respond ctxt))) can_status" - using assms - by (auto simp: ic_inv_call_ctxt_stopped_def dest!: list_map_range_setD) - -lemma ic_inv_call_ctxt_stopped_map_map: - assumes "ic_inv_call_ctxt_stopped (list_map_range ctxts) can_status" - shows "ic_inv_call_ctxt_stopped (list_map_range (list_map_map (\ctxt. if call_ctxt_canister ctxt = cid then call_ctxt_delete ctxt else ctxt) ctxts)) can_status" - using assms - by (auto simp: ic_inv_call_ctxt_stopped_def) - -definition ic_inv :: "('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_inv S = ((\msg \ set (messages S). case msg of - Call_message (From_canister ctxt_id _) _ _ _ _ _ _ \ ctxt_id \ list_map_dom (call_contexts S) - | Response_message (From_canister ctxt_id _) _ _ \ ctxt_id \ list_map_dom (call_contexts S) - | _ \ True) \ - (\ctxt \ list_map_range (call_contexts S). call_ctxt_needs_to_respond ctxt \ - (case call_ctxt_origin ctxt of From_canister ctxt_id _ \ ctxt_id \ list_map_dom (call_contexts S) - | _ \ True)) \ - ic_can_status_inv (list_map_range (canister_status S)) (list_map_dom (call_contexts S)) \ - ic_inv_call_ctxt_stopped (list_map_range (call_contexts S)) (canister_status S))" - -lemma ic_initial_inv: "ic_inv (initial_ic t pk)" - by (auto simp: ic_inv_def ic_can_status_inv_def ic_inv_call_ctxt_stopped_def initial_ic_def split: call_origin.splits) - -(* Candid *) - -datatype ('s, 'b, 'p) candid = - Candid_nat nat - | Candid_text 's - | Candid_blob (candid_unwrap_blob: 'b) - | Candid_opt "('s, 'b, 'p) candid" - | Candid_vec "('s, 'b, 'p) candid list" - | Candid_record "('s, ('s, 'b, 'p) candid) list_map" - | Candid_null - | Candid_empty - -fun candid_is_blob :: "('s, 'b, 'p) candid \ bool" where - "candid_is_blob (Candid_blob b) = True" -| "candid_is_blob _ = False" - -fun candid_lookup :: "('s, 'b, 'p) candid \ 's \ ('s, 'b, 'p) candid option" where - "candid_lookup (Candid_record m) s = list_map_get m s" -| "candid_lookup _ _ = None" - -(* State transitions *) - -context fixes - CANISTER_ERROR :: reject_code - and CANISTER_REJECT :: reject_code - and SYS_FATAL :: reject_code - and SYS_TRANSIENT :: reject_code - and MAX_CYCLES_PER_MESSAGE :: nat - and MAX_CYCLES_PER_RESPONSE :: nat - and MAX_CANISTER_BALANCE :: nat - and ic_idle_cycles_burned_rate :: "('p :: linorder, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ 'canid \ nat" - and blob_length :: "'b \ nat" - and sha_256 :: "'b \ 'b" - and ic_principal :: 'canid - and blob_of_candid :: "('s, 'b, 'p) candid \ 'b" - and parse_candid :: "'b \ ('s, 'b, 'p) candid option" - and parse_principal :: "'b \ 'p option" - and blob_of_principal :: "'p \ 'b" - and empty_blob :: 'b - and is_system_assigned :: "'p \ bool" - and encode_string :: "string \ 's" - and principal_of_uid :: "'uid \ 'p" - and principal_of_canid :: "'canid \ 'p" - and canid_of_principal :: "'p \ 'canid option" - and parse_wasm_mod :: "'b \ ('p, 'canid, 'b, 'w, 'sm, 'c, 's) canister_module option" - and parse_public_custom_sections :: "'b \ ('s, 'b) list_map option" - and parse_private_custom_sections :: "'b \ ('s, 'b) list_map option" - and verify_envelope :: "('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) envelope \ 'p \ nat \ 'p set" (* TODO *) - and principal_list_of_set :: "'p set \ 'p list" -begin - -(* Type conversion functions *) - -definition canid_of_blob :: "'b \ 'canid option" where - "canid_of_blob b = (case parse_principal b of Some p \ canid_of_principal p | _ \ None)" - -definition blob_of_canid :: "'canid \ 'b" where - "blob_of_canid = blob_of_principal \ principal_of_canid" - -(* Candid helper functions *) - -definition candid_nested_lookup :: "'b \ 's list \ ('s, 'b, 'p) candid option" where - "candid_nested_lookup b = foldl (\c s. case c of Some c' \ candid_lookup c' s | _ \ None) (parse_candid b)" - -definition candid_parse_nat :: "'b \ 's list \ nat option" where - "candid_parse_nat b s = (case candid_nested_lookup b s of Some (Candid_nat n') \ Some n' | _ \ None)" - -definition candid_parse_text :: "'b \ 's list \ 's option" where - "candid_parse_text b s = (case candid_nested_lookup b s of Some (Candid_text t') \ Some t' | _ \ None)" - -definition candid_parse_blob :: "'b \ 's list \ 'b option" where - "candid_parse_blob b s = (case candid_nested_lookup b s of Some (Candid_blob b') \ Some b' | _ \ None)" - -definition candid_parse_cid :: "'b \ 'canid option" where - "candid_parse_cid b = (case candid_parse_blob b [encode_string ''canister_id''] of Some b' \ canid_of_blob b' | _ \ None)" - -definition candid_parse_controllers :: "'b \ 'p set option" where - "candid_parse_controllers b = (case candid_nested_lookup b [encode_string ''settings'', encode_string ''controllers''] of Some (Candid_vec xs) \ - if (\c'' \ set xs. candid_is_blob c'' \ parse_principal (candid_unwrap_blob c'') \ None) then - Some (the ` parse_principal ` candid_unwrap_blob ` set xs) - else None | _ \ None)" - -fun candid_of_status :: "status \ ('s, 'b, 'p) candid" where - "candid_of_status status.Running = Candid_text (encode_string ''Running'')" -| "candid_of_status status.Stopping = Candid_text (encode_string ''Stopping'')" -| "candid_of_status status.Stopped = Candid_text (encode_string ''Stopped'')" - -(* Cycles *) - -fun carried_cycles :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin \ nat" where - "carried_cycles (From_canister _ _) = MAX_CYCLES_PER_RESPONSE" -| "carried_cycles _ = 0" - -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" -| "message_cycles (Func_message _ _ ep _) = cycles_reserved ep" -| "message_cycles (Response_message orig _ ref_cycles) = carried_cycles orig + ref_cycles" - -fun status_cycles :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) can_status \ nat" where - "status_cycles (Stopping os) = sum_list (map (carried_cycles \ fst) os) + sum_list (map snd os)" -| "status_cycles _ = 0" - -lift_definition call_ctxt_carried_cycles :: "('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt \ nat" is - "\ctxt. (if needs_to_respond ctxt - then available_cycles ctxt + carried_cycles (origin ctxt) - else 0)" . - -lemma call_ctxt_respond_carried_cycles[simp]: "call_ctxt_carried_cycles (call_ctxt_respond ctxt) = 0" - by transfer auto - -lemma call_ctxt_carried_cycles: "call_ctxt_carried_cycles ctxt = (if call_ctxt_needs_to_respond ctxt - then call_ctxt_available_cycles ctxt + carried_cycles (call_ctxt_origin ctxt) else 0)" - by transfer auto - -lemma call_ctxt_delete_carried_cycles[simp]: "call_ctxt_carried_cycles (call_ctxt_delete ctxt) = 0" - by transfer auto - -definition total_cycles :: "('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where - "total_cycles ic = ( - let cycles_in_balances = list_map_sum_vals id (balances ic) in - let cycles_in_messages = sum_list (map message_cycles (messages ic)) in - let cycles_in_contexts = list_map_sum_vals call_ctxt_carried_cycles (call_contexts ic) in - let cycles_in_statuses = list_map_sum_vals status_cycles (canister_status ic) in - cycles_in_balances + cycles_in_messages + cycles_in_contexts + cycles_in_statuses)" - -(* Accessor functions *) - -fun calling_context :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin \ 'cid option" where - "calling_context (From_canister c _) = Some c" -| "calling_context _ = None" - -fun message_queue :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) message \ 'canid queue option" where - "message_queue (Call_message _ _ _ _ _ _ q) = Some q" -| "message_queue (Func_message _ _ _ q) = Some q" -| "message_queue _ = None" - -(* Effective canister IDs *) - -definition is_effective_canister_id :: "('b, 'p, 'uid, 'canid, 's) request \ 'p \ bool" where - "is_effective_canister_id r p = (if request.canister_id r = ic_principal then - request.method_name r = encode_string ''provisional_create_canister_with_cycles'' \ - (case candid_parse_cid (request.arg r) of Some cid \ principal_of_canid cid = p | _ \ False) - else principal_of_canid (request.canister_id r) = p)" - - - -(* System transition: API Request submission [DONE] *) - -definition ic_freezing_limit :: "('p :: linorder, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ 'canid \ nat" where - "ic_freezing_limit S cid = ic_idle_cycles_burned_rate S cid * (the (list_map_get (freezing_threshold S) cid)) div (24 * 60 * 60)" - -definition request_submission_pre :: "('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) envelope \ 'p \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "request_submission_pre E ECID S = (case content E of Inl req \ - principal_of_canid (request.canister_id req) \ verify_envelope E (principal_of_uid (request.sender req)) (system_time S) \ - req \ list_map_dom (requests S) \ - system_time S \ request.ingress_expiry req \ - is_effective_canister_id req ECID \ - ( - ( - request.canister_id req = ic_principal \ - (case candid_parse_cid (request.arg req) of Some cid \ - (case list_map_get (controllers S) cid of Some ctrls \ - principal_of_uid (request.sender req) \ ctrls \ - request.method_name req \ {encode_string ''install_code'', encode_string ''uninstall_code'', encode_string ''update_settings'', - encode_string ''start_canister'', encode_string ''stop_canister'', - encode_string ''canister_status'', encode_string ''delete_canister'', - encode_string ''provisional_create_canister_with_cycles'', encode_string ''provisional_top_up_canister''} - | _ \ False) - | _ \ False) - ) - \ - ( - 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), 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) - | _ \ False) - ) - ) - | _ \ False)" - -definition request_submission_post :: "('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) envelope \ 'p \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where - "request_submission_post E ECID S = ( - 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, 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 - S\requests := list_map_set (requests S) req Received, balances := balances\)" - -definition request_submission_burned_cycles :: "('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) envelope \ 'p \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where - "request_submission_burned_cycles E ECID S = ( - 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), 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))" - -lemma request_submission_cycles_inv: - assumes "request_submission_pre E ECID S" - shows "total_cycles S = total_cycles (request_submission_post E ECID S) + request_submission_burned_cycles E ECID S" -proof - - obtain req where req_def: "content E = Inl req" - using assms - 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), 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) - | _ \ False)" - using assms - by (auto simp: request_submission_pre_def req_def split: option.splits sum.splits prod.splits) - then have ?thesis - using list_map_sum_in_ge[where ?f="balances S" and ?g=id and ?x="request.canister_id req"] - by (auto simp: request_submission_pre_def request_submission_post_def request_submission_burned_cycles_def total_cycles_def req_def list_map_sum_in[where ?f="balances S"] - split: option.splits sum.splits) - } - then show ?thesis - by (auto simp: request_submission_pre_def request_submission_post_def request_submission_burned_cycles_def total_cycles_def req_def) -qed - -lemma request_submission_ic_inv: - assumes "request_submission_pre E ECID S" "ic_inv S" - 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 prod.splits) - - - -(* System transition: Request rejection [DONE] *) - -definition request_rejection_pre :: "('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) envelope \ ('b, 'p, 'uid, 'canid, 's) request \ reject_code \ 's \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "request_rejection_pre E req code msg S = (list_map_get (requests S) req = Some Received \ (code = SYS_FATAL \ code = SYS_TRANSIENT))" - -definition request_rejection_post :: "('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) envelope \ ('b, 'p, 'uid, 'canid, 's) request \ reject_code \ 's \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where - "request_rejection_post E req code msg S = S\requests := list_map_set (requests S) req (Rejected code msg)\" - -lemma request_rejection_cycles_inv: - assumes "request_rejection_pre E req code msg S" - shows "total_cycles S = total_cycles (request_rejection_post E req code msg S)" - by (auto simp: request_rejection_pre_def request_rejection_post_def total_cycles_def) - -lemma request_rejection_ic_inv: - assumes "request_rejection_pre E req code msg S" "ic_inv S" - shows "ic_inv (request_rejection_post E req code msg S)" - using assms - by (auto simp: ic_inv_def request_rejection_pre_def request_rejection_post_def Let_def - split: sum.splits message.splits call_origin.splits) - - - -(* System transition: Initiating canister calls [DONE] *) - -definition initiate_canister_call_pre :: "('b, 'p, 'uid, 'canid, 's) request \ - ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "initiate_canister_call_pre req S = (list_map_get (requests S) req = Some Received \ - system_time S \ request.ingress_expiry req \ - request.canister_id req \ list_map_dom (canisters S))" - -definition initiate_canister_call_post :: "('b, 'p, 'uid, 'canid, 's) request \ - ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ - ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where - "initiate_canister_call_post req S = - S\requests := list_map_set (requests S) req Processing, messages := - Call_message (From_user req) (principal_of_uid (request.sender req)) (request.canister_id req) (request.method_name req) - (request.arg req) 0 Unordered # messages S\" - -lemma initiate_canister_call_cycles_inv: - assumes "initiate_canister_call_pre R S" - shows "total_cycles S = total_cycles (initiate_canister_call_post R S)" - by (auto simp: initiate_canister_call_pre_def initiate_canister_call_post_def total_cycles_def) - -lemma initiate_canister_call_ic_inv: - assumes "initiate_canister_call_pre R S" "ic_inv S" - shows "ic_inv (initiate_canister_call_post R S)" - using assms - by (auto simp: ic_inv_def initiate_canister_call_pre_def initiate_canister_call_post_def Let_def - split: sum.splits message.splits call_origin.splits) - - - -(* System transition: Calls to stopped/stopping/frozen canisters are rejected [DONE] *) - -definition call_reject_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "call_reject_pre n S = (n < length (messages S) \ (case messages S ! n of - Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - (case list_map_get (canister_status S) cee of Some Stopped \ True - | Some (Stopping l) \ True - | _ \ (case list_map_get (balances S) cee of Some bal \ bal < ic_freezing_limit S cee | _ \ False)) - | _ \ False))" - -definition call_reject_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 - "call_reject_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - S\messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (response.Reject CANISTER_ERROR (encode_string ''canister not running'')) trans_cycles]\)" - -lemma call_reject_cycles_inv: - assumes "call_reject_pre n S" - shows "total_cycles S = total_cycles (call_reject_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: call_reject_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: call_reject_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: call_reject_pre_def call_reject_post_def total_cycles_def Let_def msgs split: message.splits option.splits) -qed - -lemma call_reject_ic_inv: - assumes "call_reject_pre n S" "ic_inv S" - shows "ic_inv (call_reject_post n S)" - using assms - by (auto simp: ic_inv_def call_reject_pre_def call_reject_post_def Let_def - split: sum.splits message.splits call_origin.splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"]) - - - -(* System transition: Call context creation: Public entry points [DONE] *) - -definition call_context_create_pre :: "nat \ 'cid - \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "call_context_create_pre n ctxt_id S = (n < length (messages S) \ (case messages S ! n of - Call_message orig cer cee mn a trans_cycles q \ - (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 (balances S) cee of Some bal \ bal \ ic_freezing_limit S cee + MAX_CYCLES_PER_MESSAGE | None \ False) \ - ctxt_id \ list_map_dom (call_contexts S) - | _ \ False))" - -lift_definition create_call_ctxt :: "'canid \ ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) call_origin \ nat \ - ('p, 'uid, 'canid, 'b, 's, 'c, 'cid) call_ctxt" is - "\cee orig trans_cycles. \canister = cee, origin = orig, needs_to_respond = True, deleted = False, available_cycles = trans_cycles\" - by auto - -lemma create_call_ctxt_canister[simp]: "call_ctxt_canister (create_call_ctxt cee orig trans_cycles) = cee" - by transfer auto - -lemma create_call_ctxt_origin[simp]: "call_ctxt_origin (create_call_ctxt cee orig trans_cycles) = orig" - by transfer auto - -lemma create_call_ctxt_carried_cycles[simp]: "call_ctxt_carried_cycles (create_call_ctxt cee orig trans_cycles) = carried_cycles orig + trans_cycles" - by transfer auto - -definition call_context_create_post :: "nat \ '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_create_post n ctxt_id S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - case list_map_get (balances S) cee of Some bal \ - S\messages := list_update (messages S) n (Func_message ctxt_id cee (Public_method mn cer a) q), - call_contexts := list_map_set (call_contexts S) ctxt_id (create_call_ctxt cee orig trans_cycles), - balances := list_map_set (balances S) cee (bal - MAX_CYCLES_PER_MESSAGE)\)" - -lemma call_context_create_cycles_inv: - assumes "call_context_create_pre n ctxt_id S" - shows "total_cycles S = total_cycles (call_context_create_post n ctxt_id S)" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: call_context_create_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ m # younger) ! n = m" - and msgs_upd: "(older @ Call_message orig cer cee mn a trans_cycles q # younger)[n := m] = older @ m # younger" for m - using id_take_nth_drop[of n "messages S"] upd_conv_take_nth_drop[of n "messages S"] assms - by (auto simp: call_context_create_pre_def msg older_def younger_def nth_append) - show ?thesis - using assms list_map_sum_in_ge[of "balances S" cee, where ?g=id] - by (auto simp: call_context_create_pre_def call_context_create_post_def total_cycles_def - list_map_sum_in[where ?g=id, simplified] list_map_sum_out msgs msgs_upd split: option.splits) -qed - -lemma call_context_create_ic_inv: - assumes "call_context_create_pre n ctxt_id S" "ic_inv S" - shows "ic_inv (call_context_create_post n ctxt_id S)" - using assms - by (auto simp: ic_inv_def ic_inv_call_ctxt_stopped_def call_context_create_pre_def call_context_create_post_def Let_def - split: sum.splits message.splits call_origin.splits option.splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"] in_set_updD list_map_range_setD - intro: ic_can_status_inv_mono2) - - - -(* 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_canister[simp]: "call_ctxt_canister (create_call_ctxt_system_task cee) = cee" - by transfer 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) \ - list_map_get (canister_status S) cee = Some Running \ - (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_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_system_task cee), - balances := list_map_set (balances S) cee (bal - MAX_CYCLES_PER_MESSAGE)\)" - -lemma call_context_heartbeat_cycles_inv: - assumes "call_context_heartbeat_pre cee ctxt_id S" - shows "total_cycles S = total_cycles (call_context_heartbeat_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_heartbeat_pre_def call_context_heartbeat_post_def total_cycles_def - list_map_sum_in[where ?g=id, simplified] list_map_sum_out split: option.splits) - -lemma call_context_heartbeat_ic_inv: - assumes "call_context_heartbeat_pre cee ctxt_id S" "ic_inv S" - shows "ic_inv (call_context_heartbeat_post cee ctxt_id S)" - using assms - by (auto simp: ic_inv_def ic_inv_call_ctxt_stopped_def call_context_heartbeat_pre_def call_context_heartbeat_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: 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 ic_inv_call_ctxt_stopped_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, 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 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 = ( - case dispatch_method mn m of Some (Inl upd) \ upd (a, c, e, bal) - | Some (Inr query) \ query_as_update (query, a, c, e) - | None \ undefined - )" -| "exec_function (entry_point.Callback c resp ref_cycles) e bal m = - canister_module_callbacks m (c, resp, ref_cycles, e, bal)" -| "exec_function (entry_point.Heartbeat) e bal m = system_task_as_update ((canister_module_heartbeat m), e)" -| "exec_function (entry_point.Global_timer) e bal m = system_task_as_update ((canister_module_global_timer m), e)" - -definition message_execution_pre :: "nat \ ('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, 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, 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, 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); - cyc_used = (case R of Inr res \ update_return.cycles_used res | Inl trap \ cycles_return.cycles_used trap); - (cycles_accepted_res, new_calls_res) = (case R of Inr res \ (update_return.cycles_accepted res, update_return.new_calls res)); - 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)); - no_response = (case R of Inr result \ update_return.response result = None) in - if \isl R \ cyc_used \ (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - cycles_accepted_res \ Available \ - cyc_used + sum_list (map (\x. MAX_CYCLES_PER_RESPONSE + transferred_cycles x) new_calls_res) \ - bal + cycles_accepted_res + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - New_balance \ (if Is_response then 0 else ic_freezing_limit S recv) \ - (no_response \ call_ctxt_needs_to_respond ctxt) then - (let result = projr R; - new_call_to_message = (\call. Call_message (From_canister ctxt_id (method_call.callback call)) (principal_of_canid recv) - (method_call.callee call) (method_call.method_name call) (method_call.arg call) (method_call.transferred_cycles call) (Queue (Canister recv) (method_call.callee call))); - response_messages = (case update_return.response result of None \ [] - | Some resp \ [Response_message (call_ctxt_origin ctxt) resp (Available - cycles_accepted_res)]); - messages = take n (messages S) @ drop (Suc n) (messages S) @ map new_call_to_message new_calls_res @ response_messages; - 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 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, 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))\)) - | _ \ undefined)" - -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, 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, 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); - cyc_used = (case R of Inr res \ update_return.cycles_used res | Inl trap \ cycles_return.cycles_used trap) in - min cyc_used (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) - )))" - -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 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, 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, 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)" - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Func_message ctxt_id recv ep q # younger" - "take n older = older" "drop (Suc n) older = []" - "take (n - length older) ws = []" "drop (Suc n - length older) (w # ws) = ws" - for w and ws :: "('b, 'p, 'uid, 'canid, 's, 'c, 'cid) message list" - using id_take_nth_drop[of n "messages S"] pre - by (auto simp: message_execution_pre_def msg older_def younger_def) - note lm = list_map_sum_in[OF prod(2), where ?g=id, simplified] list_map_sum_in_ge[OF prod(2), where ?g=id, simplified] - list_map_sum_in[OF prod(5), where ?g=call_ctxt_carried_cycles] list_map_sum_in_ge[OF prod(5), where ?g=call_ctxt_carried_cycles] - define S'' where "S'' = 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))\" - define cond where "cond = (\isl R \ cyc_used \ (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - cycles_accepted_res \ Available \ - cyc_used + sum_list (map (\x. MAX_CYCLES_PER_RESPONSE + transferred_cycles x) new_calls_res) \ - bal + cycles_accepted_res + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - New_balance \ (if Is_response then 0 else ic_freezing_limit S recv) \ - (no_response \ call_ctxt_needs_to_respond ctxt))" - have reserved: "(if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) = cycles_reserved ep" - by (auto simp: Is_response_def split: entry_point.splits) - show ?thesis - proof (cases cond) - case False - have "message_execution_post n S = S''" - "message_execution_burned_cycles n S = min cyc_used (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE)" - using False - 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] del: min_less_iff_conj split del: if_split) - then show ?thesis - using lm(2) - by (auto simp: total_cycles_def S''_def msgs lm(1) reserved) - next - case True - define result where "result = projr R" - have R_Inr: "R = Inr result" - using True - by (auto simp: cond_def result_def split: option.splits) - define response_messages where "response_messages = (case update_return.response result of None \ [] - | Some resp \ [Response_message (call_ctxt_origin ctxt) resp (Available - cycles_accepted_res)])" - define new_call_to_message :: "(?'p, 'canid, 's, 'b, 'c) method_call \ ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) message" where - "new_call_to_message = (\call. Call_message (From_canister ctxt_id (callback call)) (principal_of_canid recv) - (callee call) (method_call.method_name call) (method_call.arg call) (transferred_cycles call) (Queue (Canister recv) (callee call)))" - define messages where "messages = take n (ic.messages S) @ drop (Suc n) (ic.messages S) @ map new_call_to_message new_calls_res @ response_messages" - 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 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, 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 = update_return.new_calls result" - using res - by (auto simp: R_Inr) - have no_response: "no_response = (update_return.response result = None)" - by (auto simp: no_response_def R_Inr) - have msg_exec: "message_execution_post n S = S'" - and lost: "message_execution_burned_cycles n S = min cyc_used (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE)" - using True - 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] 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" - by (auto simp: new_call_to_message_def) - then have A1: "sum_list (map (message_cycles \ new_call_to_message) new_calls_res) = (\x\new_calls_res. MAX_CYCLES_PER_RESPONSE + transferred_cycles x)" - by auto - have A2: "sum_list (map local.message_cycles response_messages) = (case update_return.response result of None \ 0 - | _ \ carried_cycles (call_ctxt_origin ctxt) + (call_ctxt_available_cycles ctxt - update_return.cycles_accepted result))" - by (auto simp: response_messages_def Available_def cycles_accepted_res_def split: option.splits) - have A3: "call_ctxt_carried_cycles new_ctxt = (case update_return.response result of Some _ \ 0 - | _ \ if call_ctxt_needs_to_respond ctxt then carried_cycles (call_ctxt_origin ctxt) + (call_ctxt_available_cycles ctxt - update_return.cycles_accepted result) else 0)" - by (auto simp: new_ctxt_def Available_def cycles_accepted_res_def call_ctxt_carried_cycles split: option.splits) - have A4: "call_ctxt_carried_cycles ctxt = (if call_ctxt_needs_to_respond ctxt then carried_cycles (call_ctxt_origin ctxt) + call_ctxt_available_cycles ctxt else 0)" - using call_ctxt_carried_cycles - by auto - have reserve: "cycles_reserved ep = (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE)" - by (auto simp: Is_response_def split: entry_point.splits) - have messages_msgs: "messages = older @ younger @ map new_call_to_message new_calls_res @ response_messages" - by (auto simp: messages_def older_def younger_def) - show ?thesis - using lm(2,4) True call_ctxt_not_needs_to_respond_available_cycles[of ctxt] - by (auto simp: cond_def msg_exec S'_def total_cycles_def lm(1,3) msgs messages_msgs A1 A2 A3 A4 New_balance_def - reserve cycles_accepted_res_def no_response_def R_Inr lost Available_def split: option.splits) - qed -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 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, 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) \ - cyc_used = (case R of Inr res \ update_return.cycles_used res | Inl trap \ cycles_return.cycles_used trap) \ - (cycles_accepted_res, new_calls_res) = (case R of Inr res \ (update_return.cycles_accepted res, update_return.new_calls res)) \ - 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)) \ - no_response = (case R of Inr result \ update_return.response result = None) \ - \isl R \ cyc_used \ (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - cycles_accepted_res \ Available \ - cyc_used + sum_list (map (\x. MAX_CYCLES_PER_RESPONSE + transferred_cycles x) new_calls_res) \ - bal + cycles_accepted_res + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - New_balance \ (if Is_response then 0 else ic_freezing_limit S recv) \ - (no_response \ call_ctxt_needs_to_respond ctxt) \ - result = projr R \ - new_call_to_message = (\call. Call_message (From_canister ctxt_id (method_call.callback call)) (principal_of_canid recv) - (method_call.callee call) (method_call.method_name call) (method_call.arg call) (method_call.transferred_cycles call) (Queue (Canister recv) (method_call.callee call))) \ - response_messages = (case update_return.response result of None \ [] - | Some resp \ [Response_message (call_ctxt_origin ctxt) resp (Available - cycles_accepted_res)]) \ - msgs = take n (messages S) @ drop (Suc n) (messages S) @ map new_call_to_message new_calls_res @ response_messages \ - 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 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, 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, 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) \ - cyc_used = (case R of Inr res \ update_return.cycles_used res | Inl trap \ cycles_return.cycles_used trap) \ - (cycles_accepted_res, new_calls_res) = (case R of Inr res \ (update_return.cycles_accepted res, update_return.new_calls res)) \ - 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)) \ - no_response = (case R of Inr result \ update_return.response result = None) \ - \(\isl R \ cyc_used \ (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - cycles_accepted_res \ Available \ - cyc_used + sum_list (map (\x. MAX_CYCLES_PER_RESPONSE + transferred_cycles x) new_calls_res) \ - bal + cycles_accepted_res + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - New_balance \ (if Is_response then 0 else ic_freezing_limit S recv) \ - (no_response \ call_ctxt_needs_to_respond ctxt)) \ - P n S (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))\)" - shows "P n S (message_execution_post n S)" - proof - - 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, 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, 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)" - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - define S'' where "S'' = 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))\" - define cond where "cond = (\isl R \ cyc_used \ (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - cycles_accepted_res \ Available \ - cyc_used + sum_list (map (\x. MAX_CYCLES_PER_RESPONSE + transferred_cycles x) new_calls_res) \ - bal + cycles_accepted_res + (if Is_response then MAX_CYCLES_PER_RESPONSE else MAX_CYCLES_PER_MESSAGE) \ - New_balance \ (if Is_response then 0 else ic_freezing_limit S recv) \ - (no_response \ call_ctxt_needs_to_respond ctxt))" - show ?thesis - proof (cases cond) - case False - have "message_execution_post n S = S''" - using False - 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]) - then show ?thesis - using assms(3)[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, folded cond_def S''_def] False - by auto - next - case True - define result where "result = projr R" - define response_messages where "response_messages = (case update_return.response result of None \ [] - | Some resp \ [Response_message (call_ctxt_origin ctxt) resp (Available - cycles_accepted_res)])" - define new_call_to_message :: "(?'p, 'canid, 's, 'b, 'c) method_call \ ('b, 'p, 'uid, 'canid, 's, 'c, 'cid) message" where - "new_call_to_message = (\call. Call_message (From_canister ctxt_id (callback call)) (principal_of_canid recv) - (callee call) (method_call.method_name call) (method_call.arg call) (transferred_cycles call) (Queue (Canister recv) (callee call)))" - define messages where "messages = take n (ic.messages S) @ drop (Suc n) (ic.messages S) @ map new_call_to_message new_calls_res @ response_messages" - 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 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, 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] 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 global_timer_def, folded S'_def] True - by (auto simp: cond_def msg_exec) - qed -qed - -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 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" - fix R :: "unit cycles_return + ('w, 'p, 'canid, 's, 'b, 'c) update_return" - assume ctxt: "list_map_get (call_contexts S) ctxt_id = Some ctxt" - assume "msgs = take n (messages S) @ drop (Suc n) (messages S) @ map new_call_to_message new_calls_res @ response_messages" - "new_call_to_message = (\call. Call_message (From_canister ctxt_id (callback call)) (principal_of_canid recv) (callee call) (method_call.method_name call) (method_call.arg call) (transferred_cycles call) - (Queue (Canister recv) (callee call)))" - "response_messages = (case update_return.response result of None \ [] | Some resp \ [Response_message (call_ctxt_origin ctxt) resp (Available - cycles_accepted_res)])" - "no_response \ call_ctxt_needs_to_respond ctxt" - "no_response = (case R of Inr result \ update_return.response result = None)" - "\ 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, 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 ic_inv_call_ctxt_stopped_def split: message.splits call_origin.splits can_status.splits dest!: in_set_takeD in_set_dropD list_map_range_setD)+ -next - fix recv bal Is_response cyc_used idx - show "ic_inv (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))\)" - using assms(2) - by (auto simp: ic_inv_def split: message.splits call_origin.splits can_status.splits dest!: in_set_takeD in_set_dropD) -qed - - - -(* System transition: Call context starvation [DONE] *) - -definition call_context_starvation_pre :: "'cid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "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 \ - (\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 - | _ \ True) \ - (\other_call_context \ list_map_range (call_contexts S). - call_ctxt_needs_to_respond other_call_context \ - calling_context (call_ctxt_origin other_call_context) \ Some ctxt_id) \ - (\can_status \ list_map_range (canister_status S). case can_status of Stopping os \ - \(orig, cyc) \ set os. calling_context orig \ Some ctxt_id - | _ \ True) - | None \ False)" - -definition call_context_starvation_post :: "'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_starvation_post ctxt_id S = ( - case list_map_get (call_contexts S) ctxt_id of Some call_context \ - let msg = Response_message (call_ctxt_origin call_context) (response.Reject CANISTER_ERROR (encode_string ''starvation'')) (call_ctxt_available_cycles call_context) - in S\call_contexts := list_map_set (call_contexts S) ctxt_id (call_ctxt_respond call_context), - messages := messages S @ [msg]\)" - -lemma call_context_starvation_cycles_inv: - assumes "call_context_starvation_pre ctxt_id S" - shows "total_cycles S = total_cycles (call_context_starvation_post ctxt_id S)" - using assms list_map_sum_in_ge[where ?f="call_contexts S" and ?x=ctxt_id and ?g=call_ctxt_carried_cycles] - by (auto simp: call_context_starvation_pre_def call_context_starvation_post_def total_cycles_def - call_ctxt_carried_cycles list_map_sum_in[where ?g=call_ctxt_carried_cycles] split: option.splits) - -lemma call_context_starvation_ic_inv: - assumes "call_context_starvation_pre ctxt_id S" "ic_inv S" - shows "ic_inv (call_context_starvation_post ctxt_id S)" - using assms - by (auto simp: ic_inv_def call_context_starvation_pre_def call_context_starvation_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 list_map_get_range - intro: ic_can_status_inv_mono2 ic_inv_call_ctxt_stopped_set_respond) - - - -(* System transition: Call context removal [DONE] *) - -definition call_context_removal_pre :: "'cid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "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 \ - (\msg \ set (messages S). case msg of - Call_message ctxt _ _ _ _ _ _ \ calling_context ctxt \ Some ctxt_id - | Response_message ctxt _ _ \ calling_context ctxt \ Some ctxt_id - | _ \ True) \ - (\other_call_context \ list_map_range (call_contexts S). - call_ctxt_needs_to_respond other_call_context \ - calling_context (call_ctxt_origin other_call_context) \ Some ctxt_id) \ - (\can_status \ list_map_range (canister_status S). case can_status of Stopping os \ - \(orig, cyc) \ set os. calling_context orig \ Some ctxt_id - | _ \ True) - | None \ False))" - -definition call_context_removal_post :: "'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_removal_post ctxt_id S = S\call_contexts := list_map_del (call_contexts S) ctxt_id\" - -definition call_context_removal_burned_cycles :: "'cid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where - "call_context_removal_burned_cycles ctxt_id S = call_ctxt_available_cycles (the (list_map_get (call_contexts S) ctxt_id))" - -lemma call_context_removal_cycles_monotonic: - assumes "call_context_removal_pre ctxt_id S" - shows "total_cycles S = total_cycles (call_context_removal_post ctxt_id S) + call_context_removal_burned_cycles ctxt_id S" - using assms call_ctxt_not_needs_to_respond_available_cycles - by (auto simp: call_context_removal_pre_def call_context_removal_post_def call_context_removal_burned_cycles_def total_cycles_def call_ctxt_carried_cycles list_map_del_sum split: option.splits) - -lemma call_context_removal_ic_inv: - assumes "call_context_removal_pre ctxt_id S" "ic_inv S" - shows "ic_inv (call_context_removal_post ctxt_id S)" - using assms - by (force simp: ic_inv_def call_context_removal_pre_def call_context_removal_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 list_map_get_range list_map_range_del - intro!: ic_can_status_inv_del[where ?z="list_map_dom (call_contexts S)"] ic_inv_call_ctxt_stopped_mono1) - - - -(* System transition: IC Management Canister: Canister creation [DONE] *) - -definition ic_canister_creation_pre :: "nat \ 'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_canister_creation_pre n cid t S = (n < length (messages S) \ (case messages S ! n of - Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''create_canister'' \ - parse_candid a \ None \ - 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_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 - "ic_canister_creation_post n cid t S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - 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_version := list_map_set (canister_version S) cid 0\)" - -lemma ic_canister_creation_cycles_inv: - assumes "ic_canister_creation_pre n cid t S" - shows "total_cycles S = total_cycles (ic_canister_creation_post n cid t S)" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: ic_canister_creation_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_canister_creation_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_canister_creation_pre_def ic_canister_creation_post_def total_cycles_def Let_def msgs - list_map_sum_out[where ?g=id] list_map_sum_out[where ?g=status_cycles] split: message.splits option.splits) -qed - -lemma ic_canister_creation_ic_inv: - assumes "ic_canister_creation_pre n cid t S" "ic_inv S" - shows "ic_inv (ic_canister_creation_post n cid t S)" - using assms - by (auto simp: ic_inv_def ic_canister_creation_pre_def ic_canister_creation_post_def Let_def - split: sum.splits message.splits call_origin.splits option.splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del - intro: ic_can_status_inv_mono1 ic_inv_stopped_ctxt_stopped_set_running) - - - -(* System transition: IC Management Canister: Changing settings [DONE] *) - -definition ic_update_settings_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_update_settings_pre n S = (n < length (messages S) \ (case messages S ! n of - Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''update_settings'' \ - (case candid_parse_cid a of Some cid \ - (case (list_map_get (controllers S) cid, list_map_get (canister_version S) cid) of (Some ctrls, Some idx) \ cer \ ctrls - | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_update_settings_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 - "ic_update_settings_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - 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); - 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: - assumes "ic_update_settings_pre n S" - shows "total_cycles S = total_cycles (ic_update_settings_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: ic_update_settings_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_update_settings_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_update_settings_pre_def ic_update_settings_post_def total_cycles_def Let_def msgs split: message.splits option.splits) -qed - -lemma ic_update_settings_ic_inv: - assumes "ic_update_settings_pre n S" "ic_inv S" - shows "ic_inv (ic_update_settings_post n S)" - using assms - by (auto simp: ic_inv_def ic_update_settings_pre_def ic_update_settings_post_def Let_def - split: sum.splits message.splits call_origin.splits option.splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del) - - - -(* System transition: IC Management Canister: Canister status [DONE] *) - -definition ic_canister_status_pre :: "nat \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_canister_status_pre n m S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''canister_status'' \ - (case candid_parse_cid a of Some cid \ - cid \ list_map_dom (canisters S) \ - cid \ list_map_dom (canister_status S) \ - cid \ list_map_dom (balances S) \ - cid \ list_map_dom (freezing_threshold S) \ - (case list_map_get (controllers S) cid of Some ctrls \ cer \ ctrls \ {principal_of_canid cid} | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_canister_status_post :: "nat \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where - "ic_canister_status_post n m S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a); - hash = (case the (list_map_get (canisters S) cid) of None \ Candid_null - | Some can \ Candid_opt (Candid_blob (sha_256 (raw_module can)))) in - S\messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid - (Candid_record (list_map_init [(encode_string ''status'', candid_of_status (simple_status (the (list_map_get (canister_status S) cid)))), - (encode_string ''module_hash'', hash), - (encode_string ''controllers'', Candid_vec (map (Candid_blob \ blob_of_principal) (principal_list_of_set (the (list_map_get (controllers S) cid))))), - (encode_string ''memory_size'', Candid_nat m), - (encode_string ''cycles'', Candid_nat (the (list_map_get (balances S) cid))), - (encode_string ''freezing_threshold'', Candid_nat (the (list_map_get (freezing_threshold S) cid))), - (encode_string ''idle_cycles_burned_per_day'', Candid_nat (ic_idle_cycles_burned_rate S cid))])))) trans_cycles]\)" - -lemma ic_canister_status_cycles_inv: - assumes "ic_canister_status_pre n m S" - shows "total_cycles S = total_cycles (ic_canister_status_post n m S)" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: ic_canister_status_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_canister_status_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_canister_status_pre_def ic_canister_status_post_def total_cycles_def Let_def msgs split: message.splits option.splits) -qed - -lemma ic_canister_status_ic_inv: - assumes "ic_canister_status_pre n m S" "ic_inv S" - shows "ic_inv (ic_canister_status_post n m S)" - using assms - by (auto simp: ic_inv_def ic_canister_status_pre_def ic_canister_status_post_def Let_def - split: sum.splits message.splits call_origin.splits option.splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del) - - - -(* System transition: IC Management Canister: Code installation [DONE] *) - -definition ic_code_installation_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_code_installation_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''install_code'' \ - (case candid_parse_cid a of Some cid \ - (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 \ - 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, list_map_get (canister_version S) cid) of - (Some ctrls, Some t, Some bal, Some can_status, Some idx) \ - let env = \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 ''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 \ 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))" - -definition ic_code_installation_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 - "ic_code_installation_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (case candid_parse_cid a of Some cid \ - (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, list_map_get (canister_version S) cid) of - (Some t, Some bal, Some can_status, Some idx) \ - let env = \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\; - (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 := list_map_set (certified_data S) cid (case new_certified_data of None \ empty_blob | Some cd \ 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]\)))))" - -definition ic_code_installation_burned_cycles :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where - "ic_code_installation_burned_cycles n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (case candid_parse_cid a of Some cid \ - (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, list_map_get (canister_version S) cid) of - (Some t, Some bal, Some can_status, Some idx) \ - let env = \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_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" - shows "total_cycles S = total_cycles (ic_code_installation_post n S) + ic_code_installation_burned_cycles n S" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: ic_code_installation_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_code_installation_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms list_map_sum_in_ge[where ?f="balances S" and ?g=id and ?x="the (candid_parse_cid a)"] - by (auto simp: ic_code_installation_pre_def ic_code_installation_post_def ic_code_installation_burned_cycles_def total_cycles_def Let_def msgs list_map_sum_in[where ?f="balances S"] split: message.splits option.splits sum.splits prod.splits) -qed - -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" - 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" - "candid_parse_blob a [encode_string ''arg''] = Some ar" - "parse_wasm_mod w = Some m" - and list_map_get: - "list_map_get (controllers S) cid = Some ctrls" - "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" - using assms - by (auto simp: ic_code_installation_pre_def split: message.splits option.splits) - show ?thesis - using assms - by (auto simp: ic_inv_def ic_code_installation_pre_def ic_code_installation_post_def msg parse list_map_get Let_def - split: sum.splits call_origin.splits message.splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del) -qed - - - -(* System transition: IC Management Canister: Code upgrade [DONE] *) - -definition ic_code_upgrade_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_code_upgrade_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''install_code'' \ - (case candid_parse_cid a of Some cid \ - (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 \ - 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, 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, 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) - | _ \ False))" - -definition ic_code_upgrade_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 - "ic_code_upgrade_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (case candid_parse_cid a of Some cid \ - (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, 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)\), - 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 - "ic_code_upgrade_burned_cycles n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (case candid_parse_cid a of Some cid \ - (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, 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" - shows "total_cycles S = total_cycles (ic_code_upgrade_post n S) + ic_code_upgrade_burned_cycles n S" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: ic_code_upgrade_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_code_upgrade_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms list_map_sum_in_ge[where ?f="balances S" and ?g=id and ?x="the (candid_parse_cid a)"] - by (auto simp: ic_code_upgrade_pre_def ic_code_upgrade_post_def ic_code_upgrade_burned_cycles_def total_cycles_def Let_def msgs list_map_sum_in[where ?f="balances S"] split: message.splits option.splits sum.splits) -qed - -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 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" - "candid_parse_blob a [encode_string ''arg''] = Some ar" - "parse_wasm_mod w = Some m" - and list_map_get: - "list_map_get (canisters S) cid = Some (Some can)" - "list_map_get (controllers S) cid = Some ctrls" - "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 - using assms - by (auto simp: ic_inv_def ic_code_upgrade_pre_def ic_code_upgrade_post_def msg parse list_map_get Let_def - split: sum.splits call_origin.splits message.splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del) -qed - - - -(* System transition: IC Management Canister: Code uninstallation [DONE] *) - -definition ic_code_uninstallation_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_code_uninstallation_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''uninstall_code'' \ - (case candid_parse_cid a of Some cid \ - (case (list_map_get (controllers S) cid, list_map_get (canister_version S) cid) of (Some ctrls, Some idx) \ cer \ ctrls - | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_code_uninstallation_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 - "ic_code_uninstallation_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (case candid_parse_cid a of Some cid \ - let call_ctxt_to_msg = (\ctxt. - 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); - 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)\))" - -lemma ic_code_uninstallation_cycles_inv: - assumes "ic_code_uninstallation_pre n S" - shows "total_cycles S = total_cycles (ic_code_uninstallation_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_code_uninstallation_pre_def split: message.splits option.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_code_uninstallation_pre_def msg younger_def older_def nth_append) - have F1: "list_map_sum_vals call_ctxt_carried_cycles (call_contexts S) = - list_map_sum_vals id - (list_map_map (\ctxt. if call_ctxt_canister ctxt = cid then call_ctxt_carried_cycles ctxt else 0) (call_contexts S)) + - list_map_sum_vals call_ctxt_carried_cycles - (list_map_map (\ctxt. if call_ctxt_canister ctxt = cid then call_ctxt_delete ctxt else ctxt) (call_contexts S))" - using list_map_sum_vals_split[where ?f="call_ctxt_carried_cycles" and ?g="call_ctxt_delete", unfolded call_ctxt_delete_carried_cycles diff_zero] - by auto - show ?thesis - using assms - by (auto simp: ic_code_uninstallation_pre_def ic_code_uninstallation_post_def total_cycles_def call_ctxt_carried_cycles cid_def Let_def msgs F1 - split: message.splits option.splits sum.splits if_splits intro!: list_map_sum_vals_filter) -qed - -lemma ic_code_uninstallation_ic_inv: - assumes "ic_code_uninstallation_pre n S" "ic_inv S" - shows "ic_inv (ic_code_uninstallation_post n S)" - using assms - by (auto simp: ic_inv_def ic_code_uninstallation_pre_def ic_code_uninstallation_post_def Let_def - simp del: list_map_range_map_map - split: sum.splits message.splits call_origin.splits option.splits if_splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del - in_set_map_filter_vals intro!: ic_inv_call_ctxt_stopped_map_map) auto - - - -(* System transition: IC Management Canister: Stopping a canister (running) [DONE] *) - -definition ic_canister_stop_running_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_canister_stop_running_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''stop_canister'' \ - (case candid_parse_cid a of Some cid \ - (case (list_map_get (canister_status S) cid, list_map_get (controllers S) cid) of (Some Running, Some ctrls) \ - cer \ ctrls - | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_canister_stop_running_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 - "ic_canister_stop_running_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a) in - S\messages := take n (messages S) @ drop (Suc n) (messages S), - canister_status := list_map_set (canister_status S) cid (Stopping [(orig, trans_cycles)])\)" - -lemma ic_canister_stop_running_cycles_inv: - assumes "ic_canister_stop_running_pre n S" - shows "total_cycles S = total_cycles (ic_canister_stop_running_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_canister_stop_running_pre_def split: message.splits option.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_canister_stop_running_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_canister_stop_running_pre_def ic_canister_stop_running_post_def total_cycles_def call_ctxt_carried_cycles cid_def Let_def msgs - list_map_sum_in[where ?g=status_cycles] split: message.splits option.splits sum.splits can_status.splits) -qed - -lemma ic_canister_stop_running_ic_inv: - assumes "ic_canister_stop_running_pre n S" "ic_inv S" - shows "ic_inv (ic_canister_stop_running_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_canister_stop_running_pre_def split: message.splits option.splits) - show ?thesis - using assms - by (auto simp: ic_inv_def ic_canister_stop_running_pre_def ic_canister_stop_running_post_def msg Let_def - split: sum.splits message.splits call_origin.splits option.splits if_splits can_status.splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del - in_set_map_filter_vals intro!: ic_can_status_inv_stopping[where ?x="list_map_range (canister_status S)" and ?os=orig] ic_inv_call_ctxt_stopped_set_stopping) -qed - - - -(* System transition: IC Management Canister: Stopping a canister (stopping) [DONE] *) - -definition ic_canister_stop_stopping_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_canister_stop_stopping_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''stop_canister'' \ - (case candid_parse_cid a of Some cid \ - (case (list_map_get (canister_status S) cid, list_map_get (controllers S) cid) of (Some (Stopping os), Some ctrls) \ - cer \ ctrls - | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_canister_stop_stopping_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 - "ic_canister_stop_stopping_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a) in - (case list_map_get (canister_status S) cid of Some (Stopping os) \ - S\messages := take n (messages S) @ drop (Suc n) (messages S), - canister_status := list_map_set (canister_status S) cid (Stopping (os @ [(orig, trans_cycles)]))\))" - -lemma ic_canister_stop_stopping_cycles_inv: - assumes "ic_canister_stop_stopping_pre n S" - shows "total_cycles S = total_cycles (ic_canister_stop_stopping_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_canister_stop_stopping_pre_def split: message.splits option.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_canister_stop_stopping_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_canister_stop_stopping_pre_def ic_canister_stop_stopping_post_def total_cycles_def call_ctxt_carried_cycles cid_def Let_def msgs - list_map_sum_in[where ?g=status_cycles] split: message.splits option.splits sum.splits can_status.splits) -qed - -lemma ic_canister_stop_stopping_ic_inv: - assumes "ic_canister_stop_stopping_pre n S" "ic_inv S" - shows "ic_inv (ic_canister_stop_stopping_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_canister_stop_stopping_pre_def split: message.splits option.splits) - show ?thesis - using assms - by (force simp: ic_inv_def ic_canister_stop_stopping_pre_def ic_canister_stop_stopping_post_def msg Let_def - split: sum.splits message.splits call_origin.splits option.splits if_splits can_status.splits - dest!: in_set_takeD in_set_dropD nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del - in_set_map_filter_vals intro!: ic_can_status_inv_stopping_app[where ?x="list_map_range (canister_status S)" and ?os=orig] ic_inv_call_ctxt_stopped_set_stopping) -qed - - - -(* System transition: IC Management Canister: Stopping a canister (done stopping) [DONE] *) - -definition ic_canister_stop_done_stopping_pre :: "'canid \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_canister_stop_done_stopping_pre cid S = - (case list_map_get (canister_status S) cid of Some (Stopping os) \ - (\ctxt \ list_map_range (call_contexts S). call_ctxt_canister ctxt \ cid) - | _ \ False)" - -definition ic_canister_stop_done_stopping_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 - "ic_canister_stop_done_stopping_post cid S = ( - let orig_cycles_to_msg = (\(or, cyc). Response_message or (Reply (blob_of_candid Candid_empty)) cyc) in - (case list_map_get (canister_status S) cid of Some (Stopping os) \ - S\canister_status := list_map_set (canister_status S) cid Stopped, - messages := messages S @ map orig_cycles_to_msg os\))" - -lemma ic_canister_stop_done_stopping_cycles_inv: - assumes "ic_canister_stop_done_stopping_pre cid S" - shows "total_cycles S = total_cycles (ic_canister_stop_done_stopping_post cid S)" -proof - - have F1: "(message_cycles \ (\(or, y). Response_message or (Reply (blob_of_candid Candid_empty)) y)) = (\(or, y). carried_cycles or + y)" - by auto - have F2: "(\(or, y)\xs. carried_cycles or + y) = sum_list (map (carried_cycles \ fst) xs) + sum_list (map snd xs)" for xs - by (induction xs) auto - show ?thesis - using assms list_map_sum_in_ge[where ?g=status_cycles and ?f="canister_status S" and ?x=cid] - by (auto simp: ic_canister_stop_done_stopping_pre_def ic_canister_stop_done_stopping_post_def total_cycles_def call_ctxt_carried_cycles Let_def - F1 F2 list_map_sum_in[where ?g=status_cycles] split: message.splits option.splits sum.splits can_status.splits) -qed - -lemma ic_canister_stop_done_stopping_ic_inv: - assumes "ic_canister_stop_done_stopping_pre cid S" "ic_inv S" - shows "ic_inv (ic_canister_stop_done_stopping_post cid S)" - using assms - by (force simp: ic_inv_def ic_can_status_inv_def ic_canister_stop_done_stopping_pre_def ic_canister_stop_done_stopping_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 intro!: ic_inv_call_ctxt_stopped_set_stopped) - - - -(* System transition: IC Management Canister: Stopping a canister (stopped) [DONE] *) - -definition ic_canister_stop_stopped_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_canister_stop_stopped_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''stop_canister'' \ - (case candid_parse_cid a of Some cid \ - (case (list_map_get (canister_status S) cid, list_map_get (controllers S) cid) of (Some Stopped, Some ctrls) \ - cer \ ctrls - | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_canister_stop_stopped_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 - "ic_canister_stop_stopped_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a) in - S\messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid Candid_empty)) trans_cycles]\)" - -lemma ic_canister_stop_stopped_cycles_inv: - assumes "ic_canister_stop_stopped_pre n S" - shows "total_cycles S = total_cycles (ic_canister_stop_stopped_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_canister_stop_stopped_pre_def split: message.splits option.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_canister_stop_stopped_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_canister_stop_stopped_pre_def ic_canister_stop_stopped_post_def total_cycles_def call_ctxt_carried_cycles cid_def Let_def msgs - split: message.splits option.splits sum.splits can_status.splits) -qed - -lemma ic_canister_stop_stopped_ic_inv: - assumes "ic_canister_stop_stopped_pre n S" "ic_inv S" - shows "ic_inv (ic_canister_stop_stopped_post n S)" - using assms - by (auto simp: ic_inv_def ic_canister_stop_stopped_pre_def ic_canister_stop_stopped_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 nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del - in_set_map_filter_vals) - - - -(* System transition: IC Management Canister: Starting a canister (not stopping) [DONE] *) - -definition ic_canister_start_not_stopping_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_canister_start_not_stopping_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''start_canister'' \ - (case candid_parse_cid a of Some cid \ - (case (list_map_get (canister_status S) cid, list_map_get (controllers S) cid) of (Some can_status, Some ctrls) \ - (can_status = Running \ can_status = Stopped) \ - cer \ ctrls - | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_canister_start_not_stopping_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 - "ic_canister_start_not_stopping_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a) in - S\canister_status := list_map_set (canister_status S) cid Running, - messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid Candid_empty)) trans_cycles]\)" - -lemma ic_canister_start_not_stopping_cycles_inv: - assumes "ic_canister_start_not_stopping_pre n S" - shows "total_cycles S = total_cycles (ic_canister_start_not_stopping_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_canister_start_not_stopping_pre_def split: message.splits option.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_canister_start_not_stopping_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_canister_start_not_stopping_pre_def ic_canister_start_not_stopping_post_def total_cycles_def call_ctxt_carried_cycles cid_def Let_def msgs - list_map_sum_in[where ?g=status_cycles] split: message.splits option.splits sum.splits) -qed - -lemma ic_canister_start_not_stopping_ic_inv: - assumes "ic_canister_start_not_stopping_pre n S" "ic_inv S" - shows "ic_inv (ic_canister_start_not_stopping_post n S)" - using assms - by (auto simp: ic_inv_def ic_canister_start_not_stopping_pre_def ic_canister_start_not_stopping_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 nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del - in_set_map_filter_vals intro: ic_can_status_inv_mono1 ic_inv_stopped_ctxt_stopped_set_running) - - - -(* System transition: IC Management Canister: Starting a canister (stopping) [DONE] *) - -definition ic_canister_start_stopping_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_canister_start_stopping_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''start_canister'' \ - (case candid_parse_cid a of Some cid \ - (case (list_map_get (canister_status S) cid, list_map_get (controllers S) cid) of (Some (Stopping _), Some ctrls) \ - cer \ ctrls - | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_canister_start_stopping_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 - "ic_canister_start_stopping_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a); - orig_cycles_to_msg = (\(or, cyc). Response_message or (response.Reject CANISTER_REJECT (encode_string ''Canister has been restarted'')) cyc) in - (case list_map_get (canister_status S) cid of Some (Stopping os) \ - S\canister_status := list_map_set (canister_status S) cid Running, - messages := take n (messages S) @ drop (Suc n) (messages S) @ Response_message orig (Reply (blob_of_candid Candid_empty)) trans_cycles # - map orig_cycles_to_msg os\))" - -lemma ic_canister_start_stopping_cycles_inv: - assumes "ic_canister_start_stopping_pre n S" - shows "total_cycles S = total_cycles (ic_canister_start_stopping_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_canister_start_stopping_pre_def split: message.splits option.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_canister_start_stopping_pre_def msg younger_def older_def nth_append) - have F1: "(message_cycles \ (\(or, y). Response_message or (response.Reject CANISTER_REJECT (encode_string ''Canister has been restarted'')) y)) = (\(or, y). carried_cycles or + y)" - by auto - have F2: "(\(or, y)\xs. carried_cycles or + y) = sum_list (map (carried_cycles \ fst) xs) + sum_list (map snd xs)" for xs - by (induction xs) auto - show ?thesis - using assms list_map_sum_in_ge[where ?g=status_cycles and ?f="canister_status S" and ?x=cid] - by (auto simp: ic_canister_start_stopping_pre_def ic_canister_start_stopping_post_def total_cycles_def call_ctxt_carried_cycles cid_def Let_def msgs F1 F2 - list_map_sum_in[where ?g=status_cycles and ?f="canister_status S"] - split: message.splits option.splits sum.splits can_status.splits) -qed - -lemma ic_canister_start_stopping_ic_inv: - assumes "ic_canister_start_stopping_pre n S" "ic_inv S" - shows "ic_inv (ic_canister_start_stopping_post n S)" - using assms - apply (auto simp: ic_inv_def ic_canister_start_stopping_pre_def ic_canister_start_stopping_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 nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del in_set_map_filter_vals - intro: ic_can_status_inv_mono1 ic_inv_stopped_ctxt_stopped_set_running) - apply (fastforce simp: ic_can_status_inv_def)+ - done - - - -(* System transition: IC Management Canister: Canister deletion [DONE] *) - -definition ic_canister_deletion_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_canister_deletion_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''delete_canister'' \ - (case candid_parse_cid a of Some cid \ - (case (list_map_get (canister_status S) cid, list_map_get (controllers S) cid, list_map_get (balances S) cid) of (Some Stopped, Some ctrls, Some bal) \ - cer \ ctrls - | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_canister_deletion_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 - "ic_canister_deletion_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a) in - S\canisters := list_map_del (canisters S) cid, - 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]\)" - -definition ic_canister_deletion_burned_cycles :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where - "ic_canister_deletion_burned_cycles n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a) in the (list_map_get (balances S) cid))" - -lemma ic_canister_deletion_cycles_monotonic: - assumes "ic_canister_deletion_pre n S" - shows "total_cycles S = total_cycles (ic_canister_deletion_post n S) + ic_canister_deletion_burned_cycles n S" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_canister_deletion_pre_def split: message.splits option.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_canister_deletion_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_canister_deletion_pre_def ic_canister_deletion_post_def ic_canister_deletion_burned_cycles_def total_cycles_def call_ctxt_carried_cycles cid_def Let_def msgs - list_map_del_sum[where ?g=id and ?f="balances S"] list_map_del_sum[where ?g=status_cycles and ?f="canister_status S"] - split: message.splits option.splits sum.splits can_status.splits) -qed - -lemma ic_canister_deletion_ic_inv: - assumes "ic_canister_deletion_pre n S" "ic_inv S" - shows "ic_inv (ic_canister_deletion_post n S)" - using assms - by (auto simp: ic_inv_def ic_canister_deletion_pre_def ic_canister_deletion_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 nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del in_set_map_filter_vals - intro: ic_can_status_inv_mono1 ic_inv_call_ctxt_stopped_mono2) - - - -(* System transition: IC Management Canister: Depositing cycles [DONE] *) - -definition ic_depositing_cycles_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_depositing_cycles_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''deposit_cycles'' \ - (case candid_parse_cid a of Some cid \ - (case list_map_get (balances S) cid of Some bal \ - True - | _ \ False) | _ \ False) - | _ \ False))" - -definition ic_depositing_cycles_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 - "ic_depositing_cycles_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a) in - (case list_map_get (balances S) cid of Some bal \ - S\balances := list_map_set (balances S) cid (bal + trans_cycles), - messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid Candid_empty)) 0]\))" - -lemma ic_depositing_cycles_cycles_monotonic: - assumes "ic_depositing_cycles_pre n S" - shows "total_cycles S = total_cycles (ic_depositing_cycles_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q cid where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - and cid_def: "candid_parse_cid a = Some cid" - using assms - by (auto simp: ic_depositing_cycles_pre_def split: message.splits option.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_depositing_cycles_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms list_map_sum_in_ge[where ?g=id and ?f="balances S" and ?x=cid] - by (auto simp: ic_depositing_cycles_pre_def ic_depositing_cycles_post_def total_cycles_def call_ctxt_carried_cycles cid_def Let_def msgs - list_map_sum_in[where ?g=id and ?f="balances S"] min_def split: message.splits option.splits sum.splits) -qed - -lemma ic_depositing_cycles_ic_inv: - assumes "ic_depositing_cycles_pre n S" "ic_inv S" - shows "ic_inv (ic_depositing_cycles_post n S)" - using assms - by (auto simp: ic_inv_def ic_depositing_cycles_pre_def ic_depositing_cycles_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 nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del - in_set_map_filter_vals) - - - -(* System transition: IC Management Canister: Random numbers [DONE] *) - -definition ic_random_numbers_pre :: "nat \ 'b \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_random_numbers_pre n b S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''raw_rand'' \ - a = blob_of_candid Candid_empty \ - blob_length b = 32 - | _ \ False))" - -definition ic_random_numbers_post :: "nat \ 'b \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where - "ic_random_numbers_post n b S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - S\messages := take n (messages S) @ drop (Suc n) (messages S) @ [Response_message orig (Reply (blob_of_candid (Candid_blob b))) trans_cycles]\)" - -lemma ic_random_numbers_cycles_inv: - assumes "ic_random_numbers_pre n b S" - shows "total_cycles S = total_cycles (ic_random_numbers_post n b S)" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: ic_random_numbers_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_random_numbers_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_random_numbers_pre_def ic_random_numbers_post_def total_cycles_def call_ctxt_carried_cycles Let_def msgs) -qed - -lemma ic_random_numbers_ic_inv: - assumes "ic_random_numbers_pre n b S" "ic_inv S" - shows "ic_inv (ic_random_numbers_post n b S)" - using assms - by (auto simp: ic_inv_def ic_random_numbers_pre_def ic_random_numbers_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 nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del - in_set_map_filter_vals) - - - -(* System transition: IC Management Canister: Canister creation with cycles [DONE] *) - -definition ic_provisional_canister_creation_pre :: "nat \ 'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_provisional_canister_creation_pre n cid t S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (case candid_parse_nat a [encode_string ''amount''] of Some cyc \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''provisional_create_canister_with_cycles'' \ - 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_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 - "ic_provisional_canister_creation_post n cid t S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - 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_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 \ - the (candid_parse_nat a [encode_string ''amount'']))" - -lemma ic_provisional_canister_creation_cycles_antimonotonic: - assumes "ic_provisional_canister_creation_pre n cid t S" - shows "total_cycles S + ic_provisional_canister_creation_minted_cycles n cid t S = total_cycles (ic_provisional_canister_creation_post n cid t S)" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: ic_provisional_canister_creation_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_provisional_canister_creation_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: ic_provisional_canister_creation_pre_def ic_provisional_canister_creation_post_def ic_provisional_canister_creation_minted_cycles_def total_cycles_def Let_def msgs - list_map_sum_out[where ?g=id] list_map_sum_out[where ?g=status_cycles] split: message.splits option.splits) -qed - -lemma ic_provisional_canister_creation_ic_inv: - assumes "ic_provisional_canister_creation_pre n cid t S" "ic_inv S" - shows "ic_inv (ic_provisional_canister_creation_post n cid t S)" - using assms - by (auto simp: ic_inv_def ic_provisional_canister_creation_pre_def ic_provisional_canister_creation_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 nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del in_set_map_filter_vals - intro: ic_can_status_inv_mono1 ic_inv_stopped_ctxt_stopped_set_running) - - - -(* System transition: IC Management Canister: Top up canister [DONE] *) - -definition ic_top_up_canister_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "ic_top_up_canister_pre n S = (n < length (messages S) \ (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - (case (candid_parse_cid a, candid_parse_nat a [encode_string ''amount'']) of (Some cid, Some cyc) \ - (q = Unordered \ (\j < n. message_queue (messages S ! j) \ Some q)) \ - cee = ic_principal \ - mn = encode_string ''provisional_top_up_canister'' \ - cid \ list_map_dom (balances S) - | _ \ False) | _ \ False))" - -definition ic_top_up_canister_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 - "ic_top_up_canister_post n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - let cid = the (candid_parse_cid a); - cyc = the (candid_parse_nat a [encode_string ''amount'']); - bal = the (list_map_get (balances S) cid) in - S\balances := list_map_set (balances S) cid (bal + cyc)\)" - -definition ic_top_up_canister_minted_cycles :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where - "ic_top_up_canister_minted_cycles n S = (case messages S ! n of Call_message orig cer cee mn a trans_cycles q \ - the (candid_parse_nat a [encode_string ''amount'']))" - -lemma ic_top_up_canister_cycles_antimonotonic: - assumes "ic_top_up_canister_pre n S" - shows "total_cycles S + ic_top_up_canister_minted_cycles n S = total_cycles (ic_top_up_canister_post n S)" -proof - - obtain orig cer cee mn a trans_cycles q where msg: "messages S ! n = Call_message orig cer cee mn a trans_cycles q" - using assms - by (auto simp: ic_top_up_canister_pre_def split: message.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Call_message orig cer cee mn a trans_cycles q # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: ic_top_up_canister_pre_def msg younger_def older_def nth_append) - define cid where "cid = the (candid_parse_cid a)" - show ?thesis - using assms - by (cases "list_map_get (balances S) cid") - (auto simp: ic_top_up_canister_pre_def ic_top_up_canister_post_def ic_top_up_canister_minted_cycles_def total_cycles_def Let_def msgs cid_def - list_map_sum_in[where ?g=id] split: message.splits option.splits) -qed - -lemma ic_top_up_canister_ic_inv: - assumes "ic_top_up_canister_pre n S" "ic_inv S" - shows "ic_inv (ic_top_up_canister_post n S)" - using assms - by (auto simp: ic_inv_def ic_top_up_canister_pre_def ic_top_up_canister_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 nth_mem[of n "messages S"] in_set_updD list_map_range_setD list_map_get_range list_map_range_del - in_set_map_filter_vals) - - - -(* System transition: Callback invocation (not deleted) [DONE] *) - -definition callback_invocation_not_deleted_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "callback_invocation_not_deleted_pre n S = (n < length (messages S) \ (case messages S ! n of Response_message (From_canister ctxt_id c) resp ref_cycles \ - (case list_map_get (call_contexts S) ctxt_id of Some ctxt \ - let cid = call_ctxt_canister ctxt in - \call_ctxt_deleted ctxt \ - (case list_map_get (balances S) cid of Some bal \ True - | _ \ False) - | _ \ False) - | _ \ False))" - -definition callback_invocation_not_deleted_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 - "callback_invocation_not_deleted_post n S = (case messages S ! n of Response_message (From_canister ctxt_id c) resp ref_cycles \ - (case list_map_get (call_contexts S) ctxt_id of Some ctxt \ - let cid = call_ctxt_canister ctxt in - (case list_map_get (balances S) cid of Some bal \ - S\balances := list_map_set (balances S) cid (bal + ref_cycles), - messages := list_update (messages S) n (Func_message ctxt_id cid (Callback c resp ref_cycles) Unordered)\)))" - -lemma callback_invocation_not_deleted_cycles_inv: - assumes "callback_invocation_not_deleted_pre n S" - shows "total_cycles S = total_cycles (callback_invocation_not_deleted_post n S)" -proof - - obtain ctxt_id c resp ref_cycles where msg: "messages S ! n = Response_message (From_canister ctxt_id c) resp ref_cycles" - using assms - by (auto simp: callback_invocation_not_deleted_pre_def split: message.splits option.splits call_origin.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Response_message (From_canister ctxt_id c) resp ref_cycles # younger" "(older @ w # younger) ! n = w" - and msgs_upd: "(older @ Response_message (From_canister ctxt_id c) resp ref_cycles # younger)[n := m] = older @ m # younger" for w m - using assms id_take_nth_drop[of n "messages S"] upd_conv_take_nth_drop[of n "messages S"] assms - by (auto simp: callback_invocation_not_deleted_pre_def msg older_def younger_def nth_append) - show ?thesis - using assms - by (auto simp: callback_invocation_not_deleted_pre_def callback_invocation_not_deleted_post_def total_cycles_def call_ctxt_carried_cycles Let_def msgs msgs_upd - list_map_sum_in[where ?g=id and ?f="balances S"] split: option.splits) -qed - -lemma callback_invocation_not_deleted_ic_inv: - assumes "callback_invocation_not_deleted_pre n S" "ic_inv S" - shows "ic_inv (callback_invocation_not_deleted_post n S)" - using assms - by (auto simp: ic_inv_def callback_invocation_not_deleted_pre_def callback_invocation_not_deleted_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 nth_mem[of n "messages S"] in_set_updD) - - - -(* System transition: Callback invocation (deleted) [DONE] *) - -definition callback_invocation_deleted_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "callback_invocation_deleted_pre n S = (n < length (messages S) \ (case messages S ! n of Response_message (From_canister ctxt_id c) resp ref_cycles \ - (case list_map_get (call_contexts S) ctxt_id of Some ctxt \ - let cid = call_ctxt_canister ctxt in - call_ctxt_deleted ctxt \ - (case list_map_get (balances S) cid of Some bal \ True - | _ \ False) - | _ \ False) - | _ \ False))" - -definition callback_invocation_deleted_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 - "callback_invocation_deleted_post n S = (case messages S ! n of Response_message (From_canister ctxt_id c) resp ref_cycles \ - (case list_map_get (call_contexts S) ctxt_id of Some ctxt \ - let cid = call_ctxt_canister ctxt in - (case list_map_get (balances S) cid of Some bal \ - S\balances := list_map_set (balances S) cid (bal + ref_cycles + MAX_CYCLES_PER_RESPONSE), - messages := take n (messages S) @ drop (Suc n) (messages S)\)))" - -lemma callback_invocation_deleted_cycles_inv: - assumes "callback_invocation_deleted_pre n S" - shows "total_cycles S = total_cycles (callback_invocation_deleted_post n S)" -proof - - obtain ctxt_id c resp ref_cycles where msg: "messages S ! n = Response_message (From_canister ctxt_id c) resp ref_cycles" - using assms - by (auto simp: callback_invocation_deleted_pre_def split: message.splits option.splits call_origin.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Response_message (From_canister ctxt_id c) resp ref_cycles # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: callback_invocation_deleted_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: callback_invocation_deleted_pre_def callback_invocation_deleted_post_def total_cycles_def call_ctxt_carried_cycles Let_def msgs - list_map_sum_in[where ?g=id and ?f="balances S"] split: option.splits) -qed - -lemma callback_invocation_deleted_ic_inv: - assumes "callback_invocation_deleted_pre n S" "ic_inv S" - shows "ic_inv (callback_invocation_deleted_post n S)" - using assms - by (auto simp: ic_inv_def callback_invocation_deleted_pre_def callback_invocation_deleted_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 nth_mem[of n "messages S"] in_set_updD) - - - -(* System transition: Respond to user request [DONE] *) - -definition respond_to_user_request_pre :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "respond_to_user_request_pre n S = (n < length (messages S) \ (case messages S ! n of Response_message (From_user req) resp ref_cycles \ - (case list_map_get (requests S) req of Some Processing \ True - | _ \ False) - | _ \ False))" - -definition respond_to_user_request_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 - "respond_to_user_request_post n S = (case messages S ! n of Response_message (From_user req) resp ref_cycles \ - let req_resp = (case resp of Reply b \ Replied b | response.Reject c b \ Rejected c b) in - S\messages := take n (messages S) @ drop (Suc n) (messages S), - requests := list_map_set (requests S) req req_resp\)" - -definition respond_to_user_request_burned_cycles :: "nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where - "respond_to_user_request_burned_cycles n S = (case messages S ! n of Response_message (From_user req) resp ref_cycles \ - ref_cycles)" - -lemma respond_to_user_request_cycles_monotonic: - assumes "respond_to_user_request_pre n S" - shows "total_cycles S = total_cycles (respond_to_user_request_post n S) + respond_to_user_request_burned_cycles n S" -proof - - obtain req resp ref_cycles where msg: "messages S ! n = Response_message (From_user req) resp ref_cycles" - using assms - by (auto simp: respond_to_user_request_pre_def split: message.splits option.splits call_origin.splits) - define older where "older = take n (messages S)" - define younger where "younger = drop (Suc n) (messages S)" - have msgs: "messages S = older @ Response_message (From_user req) resp ref_cycles # younger" "(older @ w # younger) ! n = w" - "take n older = older" "take (n - length older) ws = []" "drop (Suc n) older = []" - "drop (Suc n - length older) (w # ws) = ws" for w ws - using id_take_nth_drop[of n "messages S"] assms - by (auto simp: respond_to_user_request_pre_def msg younger_def older_def nth_append) - show ?thesis - using assms - by (auto simp: respond_to_user_request_pre_def respond_to_user_request_post_def respond_to_user_request_burned_cycles_def total_cycles_def call_ctxt_carried_cycles Let_def msgs - list_map_sum_in[where ?g=id and ?f="balances S"] split: option.splits request_status.splits) -qed - -lemma respond_to_user_request_ic_inv: - assumes "respond_to_user_request_pre n S" "ic_inv S" - shows "ic_inv (respond_to_user_request_post n S)" - using assms - by (auto simp: ic_inv_def respond_to_user_request_pre_def respond_to_user_request_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 nth_mem[of n "messages S"] in_set_updD) - - - -(* System transition: Request clean up [DONE] *) - -definition request_cleanup_pre :: "('b, 'p, 'uid, 'canid, 's) request \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "request_cleanup_pre req S = (case list_map_get (requests S) req of Some req_status \ - (case req_status of Replied _ \ True | Rejected _ _ \ True | _ \ False) - | _ \ False)" - -definition request_cleanup_post :: "('b, 'p, 'uid, 'canid, 's) request \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where - "request_cleanup_post req S = (S\requests := list_map_set (requests S) req Done\)" - -lemma request_cleanup_cycles_inv: - assumes "request_cleanup_pre n S" - shows "total_cycles S = total_cycles (request_cleanup_post n S)" - by (auto simp: request_cleanup_post_def total_cycles_def) - -lemma request_cleanup_ic_inv: - assumes "request_cleanup_pre req S" "ic_inv S" - shows "ic_inv (request_cleanup_post req S)" - using assms - by (auto simp: ic_inv_def request_cleanup_pre_def request_cleanup_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) - - - -(* System transition: Request clean up (expired) [DONE] *) - -definition request_cleanup_expired_pre :: "('b, 'p, 'uid, 'canid, 's) request \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - "request_cleanup_expired_pre req S = (case list_map_get (requests S) req of Some req_status \ - (case req_status of Replied _ \ True | Rejected _ _ \ True | Done \ True | _ \ False) \ - request.ingress_expiry req < system_time S - | _ \ False)" - -definition request_cleanup_expired_post :: "('b, 'p, 'uid, 'canid, 's) request \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic" where - "request_cleanup_expired_post req S = (S\requests := list_map_del (requests S) req\)" - -lemma request_cleanup_expired_cycles_inv: - assumes "request_cleanup_expired_pre n S" - shows "total_cycles S = total_cycles (request_cleanup_expired_post n S)" - by (auto simp: request_cleanup_expired_post_def total_cycles_def) - -lemma request_cleanup_expired_ic_inv: - assumes "request_cleanup_expired_pre req S" "ic_inv S" - shows "ic_inv (request_cleanup_expired_post req S)" - using assms - by (auto simp: ic_inv_def request_cleanup_expired_pre_def request_cleanup_expired_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) - - - -(* 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, 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 - "canister_out_of_cycles_post cid S = ( - let call_ctxt_to_msg = (\ctxt. - 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); - 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)\)" - -lemma canister_out_of_cycles_cycles_inv: - assumes "canister_out_of_cycles_pre cid S" - shows "total_cycles S = total_cycles (canister_out_of_cycles_post cid S)" -proof - - have F1: "list_map_sum_vals call_ctxt_carried_cycles (call_contexts S) = - list_map_sum_vals id - (list_map_map (\ctxt. if call_ctxt_canister ctxt = cid then call_ctxt_carried_cycles ctxt else 0) (call_contexts S)) + - list_map_sum_vals call_ctxt_carried_cycles - (list_map_map (\ctxt. if call_ctxt_canister ctxt = cid then call_ctxt_delete ctxt else ctxt) (call_contexts S))" - using list_map_sum_vals_split[where ?f="call_ctxt_carried_cycles" and ?g="call_ctxt_delete", unfolded call_ctxt_delete_carried_cycles diff_zero] - by auto - show ?thesis - using assms - by (auto simp: canister_out_of_cycles_pre_def canister_out_of_cycles_post_def total_cycles_def call_ctxt_carried_cycles Let_def F1 - split: message.splits option.splits sum.splits if_splits intro!: list_map_sum_vals_filter) -qed - -lemma canister_out_of_cycles_ic_inv: - assumes "canister_out_of_cycles_pre cid S" "ic_inv S" - shows "ic_inv (canister_out_of_cycles_post cid S)" - using assms - by (auto simp: ic_inv_def canister_out_of_cycles_pre_def canister_out_of_cycles_post_def Let_def - simp del: list_map_range_map_map - 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 intro!: ic_inv_call_ctxt_stopped_map_map) auto - - - -(* 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 \ - t0 < t1 - | _ \ False)" - -definition canister_time_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_time_progress_post cid t1 S = (S\time := list_map_set (time S) cid t1\)" - -lemma canister_time_progress_cycles_inv: - assumes "canister_time_progress_pre cid t1 S" - shows "total_cycles S = total_cycles (canister_time_progress_post cid t1 S)" - by (auto simp: canister_time_progress_post_def total_cycles_def) - -lemma canister_time_progress_ic_inv: - assumes "canister_time_progress_pre cid t1 S" "ic_inv S" - shows "ic_inv (canister_time_progress_post cid t1 S)" - using assms - by (auto simp: ic_inv_def canister_time_progress_pre_def canister_time_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) - - - -(* 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 \ - 0 \ b1 \ b1 < b0 - | _ \ False)" - -definition cycle_consumption_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 - "cycle_consumption_post cid b1 S = S\balances := list_map_set (balances S) cid b1\" - -definition cycle_consumption_burned_cycles :: "'canid \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ nat" where - "cycle_consumption_burned_cycles cid b1 S = the (list_map_get (balances S) cid) - b1" - -lemma cycle_consumption_cycles_monotonic: - assumes "cycle_consumption_pre cid b1 S" - shows "total_cycles S = total_cycles (cycle_consumption_post cid b1 S) + cycle_consumption_burned_cycles cid b1 S" - using assms list_map_sum_in_ge[where ?g=id and ?f="balances S" and ?x=cid] - by (auto simp: cycle_consumption_pre_def cycle_consumption_post_def cycle_consumption_burned_cycles_def total_cycles_def - list_map_sum_in[where ?g=id and ?f="balances S"] split: option.splits) - -lemma cycle_consumption_ic_inv: - assumes "cycle_consumption_pre cid b1 S" "ic_inv S" - shows "ic_inv (cycle_consumption_post cid b1 S)" - using assms - by (auto simp: ic_inv_def cycle_consumption_pre_def cycle_consumption_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) - - - -(* 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)" - -definition system_time_progress_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 - "system_time_progress_post t1 S = (S\system_time := t1\)" - -lemma system_time_progress_cycles_inv: - assumes "system_time_progress_pre t1 S" - shows "total_cycles S = total_cycles (system_time_progress_post t1 S)" - by (auto simp: system_time_progress_post_def total_cycles_def) - -lemma system_time_progress_ic_inv: - assumes "system_time_progress_pre t1 S" "ic_inv S" - shows "ic_inv (system_time_progress_post t1 S)" - using assms - by (auto simp: ic_inv_def system_time_progress_pre_def system_time_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) - - - -(* 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 \ - nat \ nat \ ('p, 'uid, 'canid, 'b, 'w, 'sm, 'c, 's, 'cid, 'pk) ic \ bool" where - ic_steps_refl: "ic_steps sig S 0 0 S" -| request_submission: "ic_steps sig S0 minted burned S \ request_submission_pre (E :: ('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) envelope) ECID S \ ic_steps sig S0 minted (burned + request_submission_burned_cycles E ECID S) (request_submission_post E ECID S)" -| request_rejection: "ic_steps sig S0 minted burned S \ request_rejection_pre (E :: ('b, 'p, 'uid, 'canid, 's, 'pk, 'sig) envelope) req code msg S \ ic_steps sig S0 minted burned (request_rejection_post E req code msg S)" -| initiate_canister_call: "ic_steps sig S0 minted burned S \ initiate_canister_call_pre req S \ ic_steps sig S0 minted burned (initiate_canister_call_post req S)" -| call_reject: "ic_steps sig S0 minted burned S \ call_reject_pre n S \ ic_steps sig S0 minted burned (call_reject_post n S)" -| call_context_create: "ic_steps sig S0 minted burned S \ call_context_create_pre n ctxt_id S \ ic_steps sig S0 minted burned (call_context_create_post n ctxt_id S)" -| call_context_heartbeat: "ic_steps sig S0 minted burned S \ call_context_heartbeat_pre cee ctxt_id S \ ic_steps sig S0 minted burned (call_context_heartbeat_post cee ctxt_id S)" -| message_execution: "ic_steps sig S0 minted burned S \ message_execution_pre n S \ ic_steps sig S0 minted (burned + message_execution_burned_cycles n S) (message_execution_post n S)" -| call_context_starvation: "ic_steps sig S0 minted burned S \ call_context_starvation_pre ctxt_id S \ ic_steps sig S0 minted burned (call_context_starvation_post ctxt_id S)" -| call_context_removal: "ic_steps sig S0 minted burned S \ call_context_removal_pre ctxt_id S \ ic_steps sig S0 minted (burned + call_context_removal_burned_cycles ctxt_id S) (call_context_removal_post ctxt_id S)" -| ic_canister_creation: "ic_steps sig S0 minted burned S \ ic_canister_creation_pre n cid t S \ ic_steps sig S0 minted burned (ic_canister_creation_post n cid t S)" -| ic_update_settings: "ic_steps sig S0 minted burned S \ ic_update_settings_pre n S \ ic_steps sig S0 minted burned (ic_update_settings_post n S)" -| ic_canister_status: "ic_steps sig S0 minted burned S \ ic_canister_status_pre n m S \ ic_steps sig S0 minted burned (ic_canister_status_post n m S)" -| ic_code_installation: "ic_steps sig S0 minted burned S \ ic_code_installation_pre n S \ ic_steps sig S0 minted (burned + ic_code_installation_burned_cycles n S) (ic_code_installation_post n S)" -| ic_code_upgrade: "ic_steps sig S0 minted burned S \ ic_code_upgrade_pre n S \ ic_steps sig S0 minted (burned + ic_code_upgrade_burned_cycles n S) (ic_code_upgrade_post n S)" -| ic_code_uninstallation: "ic_steps sig S0 minted burned S \ ic_code_uninstallation_pre n S \ ic_steps sig S0 minted burned (ic_code_uninstallation_post n S)" -| ic_canister_stop_running: "ic_steps sig S0 minted burned S \ ic_canister_stop_running_pre n S \ ic_steps sig S0 minted burned (ic_canister_stop_running_post n S)" -| ic_canister_stop_stopping: "ic_steps sig S0 minted burned S \ ic_canister_stop_stopping_pre n S \ ic_steps sig S0 minted burned (ic_canister_stop_stopping_post n S)" -| ic_canister_stop_done_stopping: "ic_steps sig S0 minted burned S \ ic_canister_stop_done_stopping_pre cid S \ ic_steps sig S0 minted burned (ic_canister_stop_done_stopping_post cid S)" -| ic_canister_stop_stopped: "ic_steps sig S0 minted burned S \ ic_canister_stop_stopped_pre n S \ ic_steps sig S0 minted burned (ic_canister_stop_stopped_post n S)" -| ic_canister_start_not_stopping: "ic_steps sig S0 minted burned S \ ic_canister_start_not_stopping_pre n S \ ic_steps sig S0 minted burned (ic_canister_start_not_stopping_post n S)" -| ic_canister_start_stopping: "ic_steps sig S0 minted burned S \ ic_canister_start_stopping_pre n S \ ic_steps sig S0 minted burned (ic_canister_start_stopping_post n S)" -| ic_canister_deletion: "ic_steps sig S0 minted burned S \ ic_canister_deletion_pre n S \ ic_steps sig S0 minted (burned + ic_canister_deletion_burned_cycles n S) (ic_canister_deletion_post n S)" -| ic_depositing_cycles: "ic_steps sig S0 minted burned S \ ic_depositing_cycles_pre n S \ ic_steps sig S0 minted burned (ic_depositing_cycles_post n S)" -| ic_random_numbers: "ic_steps sig S0 minted burned S \ ic_random_numbers_pre n b S \ ic_steps sig S0 minted burned (ic_random_numbers_post n b S)" -| ic_provisional_canister_creation: "ic_steps sig S0 minted burned S \ ic_provisional_canister_creation_pre n cid t S \ ic_steps sig S0 (minted + ic_provisional_canister_creation_minted_cycles n cid t S) burned (ic_provisional_canister_creation_post n cid t S)" -| ic_top_up_canister: "ic_steps sig S0 minted burned S \ ic_top_up_canister_pre n S \ ic_steps sig S0 (minted + ic_top_up_canister_minted_cycles n S) burned (ic_top_up_canister_post n S)" -| callback_invocation_not_deleted: "ic_steps sig S0 minted burned S \ callback_invocation_not_deleted_pre n S \ ic_steps sig S0 minted burned (callback_invocation_not_deleted_post n S)" -| callback_invocation_deleted: "ic_steps sig S0 minted burned S \ callback_invocation_deleted_pre n S \ ic_steps sig S0 minted burned (callback_invocation_deleted_post n S)" -| respond_to_user_request: "ic_steps sig S0 minted burned S \ respond_to_user_request_pre n S \ ic_steps sig S0 minted (burned + respond_to_user_request_burned_cycles n S) (respond_to_user_request_post n S)" -| request_cleanup: "ic_steps sig S0 minted burned S \ request_cleanup_pre req S \ ic_steps sig S0 minted burned (request_cleanup_post req S)" -| request_cleanup_expired: "ic_steps sig S0 minted burned S \ request_cleanup_expired_pre req S \ ic_steps sig S0 minted burned (request_cleanup_expired_post req S)" -| canister_out_of_cycles: "ic_steps sig S0 minted burned S \ canister_out_of_cycles_pre cid S \ ic_steps sig S0 minted burned (canister_out_of_cycles_post cid S)" -| 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" - shows "total_cycles S0 + minted = total_cycles S + burned" - using assms - apply (induction "TYPE('sig)" S0 minted burned S rule: ic_steps.induct) - apply auto[1] - using request_submission_cycles_inv apply fastforce - using request_rejection_cycles_inv apply fastforce - using initiate_canister_call_cycles_inv apply fastforce - using call_reject_cycles_inv apply fastforce - using call_context_create_cycles_inv apply fastforce - using call_context_heartbeat_cycles_inv apply fastforce - using message_execution_cycles_monotonic apply fastforce - using call_context_starvation_cycles_inv apply fastforce - using call_context_removal_cycles_monotonic apply fastforce - using ic_canister_creation_cycles_inv apply fastforce - using ic_update_settings_cycles_inv apply fastforce - using ic_canister_status_cycles_inv apply fastforce - using ic_code_installation_cycles_inv apply fastforce - using ic_code_upgrade_cycles_inv apply fastforce - using ic_code_uninstallation_cycles_inv apply fastforce - using ic_canister_stop_running_cycles_inv apply fastforce - using ic_canister_stop_stopping_cycles_inv apply fastforce - using ic_canister_stop_done_stopping_cycles_inv apply fastforce - using ic_canister_stop_stopped_cycles_inv apply fastforce - using ic_canister_start_not_stopping_cycles_inv apply fastforce - using ic_canister_start_stopping_cycles_inv apply fastforce - using ic_canister_deletion_cycles_monotonic apply fastforce - using ic_depositing_cycles_cycles_monotonic apply fastforce - using ic_random_numbers_cycles_inv apply fastforce - using ic_provisional_canister_creation_cycles_antimonotonic apply fastforce - using ic_top_up_canister_cycles_antimonotonic apply fastforce - using callback_invocation_not_deleted_cycles_inv apply fastforce - using callback_invocation_deleted_cycles_inv apply fastforce - using respond_to_user_request_cycles_monotonic apply fastforce - using request_cleanup_cycles_inv apply fastforce - using request_cleanup_expired_cycles_inv apply fastforce - using canister_out_of_cycles_cycles_inv apply fastforce - 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: - assumes "ic_steps TYPE('sig) S0 minted burned S" - shows "ic_inv S0 \ ic_inv S" - using assms - apply (induction "TYPE('sig)" S0 minted burned S rule: ic_steps.induct) - apply auto[1] - using request_submission_ic_inv apply fastforce - using request_rejection_ic_inv apply fastforce - using initiate_canister_call_ic_inv apply fastforce - using call_reject_ic_inv apply fastforce - using call_context_create_ic_inv apply fastforce - using call_context_heartbeat_ic_inv apply fastforce - using message_execution_ic_inv apply fastforce - using call_context_starvation_ic_inv apply fastforce - using call_context_removal_ic_inv apply fastforce - using ic_canister_creation_ic_inv apply fastforce - using ic_update_settings_ic_inv apply fastforce - using ic_canister_status_ic_inv apply fastforce - using ic_code_installation_ic_inv apply fastforce - using ic_code_upgrade_ic_inv apply fastforce - using ic_code_uninstallation_ic_inv apply fastforce - using ic_canister_stop_running_ic_inv apply fastforce - using ic_canister_stop_stopping_ic_inv apply fastforce - using ic_canister_stop_done_stopping_ic_inv apply fastforce - using ic_canister_stop_stopped_ic_inv apply fastforce - using ic_canister_start_not_stopping_ic_inv apply fastforce - using ic_canister_start_stopping_ic_inv apply fastforce - using ic_canister_deletion_ic_inv apply fastforce - using ic_depositing_cycles_ic_inv apply fastforce - using ic_random_numbers_ic_inv apply fastforce - using ic_provisional_canister_creation_ic_inv apply fastforce - using ic_top_up_canister_ic_inv apply fastforce - using callback_invocation_not_deleted_ic_inv apply fastforce - using callback_invocation_deleted_ic_inv apply fastforce - using respond_to_user_request_ic_inv apply fastforce - using request_cleanup_ic_inv apply fastforce - using request_cleanup_expired_ic_inv apply fastforce - using canister_out_of_cycles_ic_inv apply fastforce - 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 - -export_code request_submission_pre request_submission_post - request_rejection_pre request_rejection_post - initiate_canister_call_pre initiate_canister_call_post - call_reject_pre call_reject_post - call_context_create_pre call_context_create_post - call_context_heartbeat_pre call_context_heartbeat_post - message_execution_pre message_execution_post - call_context_starvation_pre call_context_starvation_post - call_context_removal_pre call_context_removal_post - ic_canister_creation_pre ic_canister_creation_post - ic_update_settings_pre ic_update_settings_post - ic_canister_status_pre ic_canister_status_post - ic_code_installation_pre ic_code_installation_post - ic_code_upgrade_pre ic_code_upgrade_post - ic_code_uninstallation_pre ic_code_uninstallation_post - ic_canister_stop_running_pre ic_canister_stop_running_post - ic_canister_stop_stopping_pre ic_canister_stop_stopping_post - ic_canister_stop_done_stopping_pre ic_canister_stop_done_stopping_post - ic_canister_stop_stopped_pre ic_canister_stop_stopped_post - ic_canister_start_not_stopping_pre ic_canister_start_not_stopping_post - ic_canister_start_stopping_pre ic_canister_start_stopping_post - ic_canister_deletion_pre ic_canister_deletion_post - ic_depositing_cycles_pre ic_depositing_cycles_post - ic_random_numbers_pre ic_random_numbers_post - ic_provisional_canister_creation_pre ic_provisional_canister_creation_post - ic_top_up_canister_pre ic_top_up_canister_post - callback_invocation_not_deleted_pre callback_invocation_not_deleted_post - callback_invocation_deleted_pre callback_invocation_deleted_post - respond_to_user_request_pre respond_to_user_request_post - request_cleanup_pre request_cleanup_post - request_cleanup_expired_pre request_cleanup_expired_post - canister_out_of_cycles_pre canister_out_of_cycles_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 diff --git a/theories/ROOT b/theories/ROOT deleted file mode 100644 index 7db8ae08d..000000000 --- a/theories/ROOT +++ /dev/null @@ -1,8 +0,0 @@ -chapter IC - -session Internet_Computer (IC) = "HOL-Library" + - options [timeout=600] - theories - IC -export_files (in ".") [2] - "Internet_Computer.IC:code/**" From e59dc7b2dc23d22f596af5ca0aac6d641b07f095 Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Fri, 28 Jul 2023 15:21:44 +0200 Subject: [PATCH 04/12] update contexts in which ic0.msg_caller_size and ic0.msg_caller_copy can be called (#201) * update contexts in which ic0.msg_caller_size and ic0.msg_caller_copy can be called * make ic_principal the caller of system tasks * update changelog --- spec/_attachments/interface-spec-changelog.md | 1 + spec/index.md | 50 +++++++++---------- 2 files changed, 26 insertions(+), 25 deletions(-) diff --git a/spec/_attachments/interface-spec-changelog.md b/spec/_attachments/interface-spec-changelog.md index af670f008..ee00bb809 100644 --- a/spec/_attachments/interface-spec-changelog.md +++ b/spec/_attachments/interface-spec-changelog.md @@ -2,6 +2,7 @@ ### ∞ (unreleased) * Canister cycle balance cannot decrease below the freezing limit after executing `install_code` on the management canister. +* System API calls `ic0.msg_caller_size` and `ic0.msg_caller_copy` can be called in all contexts except for (start) function. ### 0.20.0 (2023-07-11) {#0_20_0} * IC Bitcoin API, ECDSA API, canister HTTPS outcalls API, and 128-bit cycles System API are considered stable. diff --git a/spec/index.md b/spec/index.md index 23af818c8..6e28628a0 100644 --- a/spec/index.md +++ b/spec/index.md @@ -1132,7 +1132,7 @@ 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. Still, the function `canister_heartbeat` can initiate new calls. +`canister_heartbeat` is triggered by the IC, and therefore has no arguments and cannot reply or reject. Still, the function `canister_heartbeat` can initiate new calls. :::note @@ -1146,7 +1146,7 @@ For time-based execution, the WebAssembly module can export a function with name 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. +`canister_global_timer` is triggered by the IC, and therefore has no arguments and cannot reply or reject. Still, the function `canister_global_timer` can initiate new calls. :::note @@ -1166,8 +1166,8 @@ The following sections describe various System API functions, also referred to a ic0.msg_arg_data_size : () -> i32; // I U Q CQ Ry CRy F ic0.msg_arg_data_copy : (dst : i32, offset : i32, size : i32) -> (); // I U Q CQ Ry CRy F - ic0.msg_caller_size : () -> i32; // I G U Q CQ F - ic0.msg_caller_copy : (dst : i32, offset: i32, size : i32) -> (); // I G U Q CQ F + ic0.msg_caller_size : () -> i32; // * + ic0.msg_caller_copy : (dst : i32, offset: i32, size : i32) -> (); // * ic0.msg_reject_code : () -> i32; // Ry Rt CRy CRt ic0.msg_reject_msg_size : () -> i32; // Rt CRt ic0.msg_reject_msg_copy : (dst : i32, offset : i32, size : i32) -> (); // Rt CRt @@ -1294,7 +1294,7 @@ The canister can access an argument. For `canister_init`, `canister_post_upgrade - `ic0.msg_caller_size : () → i32` and `ic0.msg_caller_copy : (dst : i32, offset: i32, size : i32) → ()` - The identity of the caller, which may be a canister id or a user id. During canister installation or upgrade, this is the id of the user or canister requesting the installation or upgrade. + The identity of the caller, which may be a canister id or a user id. During canister installation or upgrade, this is the id of the user or canister requesting the installation or upgrade. During a system task (heartbeat or global timer), this is the id of the management canister. - `ic0.msg_reject_code : () → i32` @@ -4740,7 +4740,7 @@ We can model the execution of WebAssembly functions as stateful functions that h Params = { arg : NoArg | Blob; - caller : NoCaller | Principal; + caller : Principal; reject_code : 0 | SYS_FATAL | SYS_TRANSIENT | …; reject_message : Text; sysenv : Env; @@ -4776,7 +4776,7 @@ It is nonsensical to pass to an execution function a WebAssembly store `S` that empty_params = { arg = NoArg; - caller = NoCaller; + caller = ic_principal; reject_code = 0; reject_message = ""; sysenv = (undefined); @@ -4890,7 +4890,7 @@ Finally we can specify the abstract `CanisterModule` that models a concrete WebA pre_upgrade = λ (old_state, caller, sysenv) → let es = ref {empty_execution_state with wasm_state = old_state - params = { empty_params with caller = caller; sysenv } + params = empty_params with { caller = caller; sysenv } balance = sysenv.balance context = G } @@ -4913,7 +4913,7 @@ Finally we can specify the abstract `CanisterModule` that models a concrete WebA post_upgrade = λ (self_id, stable_mem, arg, caller, sysenv) → let es = ref {empty_execution_state with wasm_state = { store = initial_wasm_store; self_id = self_id; stable_mem = stable_mem } - params = { empty_params with arg = arg; caller = caller; sysenv } + params = empty_params with { arg = arg; caller = caller; sysenv } balance = sysenv.balance context = I } @@ -4985,7 +4985,7 @@ Finally we can specify the abstract `CanisterModule` that models a concrete WebA heartbeat = λ (sysenv) → λ wasm_state → let es = ref {empty_execution_state with wasm_state = wasm_state; - params = empty_params with { arg = NoArg; caller = NoCaller; sysenv } + params = empty_params with { arg = NoArg; caller = ic_principal; sysenv } balance = sysenv.balance context = T } @@ -5011,7 +5011,7 @@ heartbeat = λ (sysenv) → λ wasm_state → Trap {cycles_used = 0;} 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 } + params = empty_params with { arg = NoArg; caller = ic_principal; sysenv } balance = sysenv.balance context = T } @@ -5035,7 +5035,7 @@ global_timer = λ (sysenv) → λ wasm_state → Trap {cycles_used = 0;} - The function `callbacks` of the `CanisterModule` is defined as follows callbacks = λ(callbacks, response, refunded_cycles, sysenv, available) → λ wasm_state → - let params0 = { empty_params with + let params0 = empty_params with { sysenv cycles_refunded = refund_cycles; } @@ -5094,7 +5094,7 @@ global_timer = λ (sysenv) → λ wasm_state → Trap {cycles_used = 0;} - The function `composite_callbacks` of the `CanisterModule` is defined as follows composite_callbacks = λ(callbacks, response, sysenv) → λ wasm_state → - let params0 = { empty_params with + let params0 = empty_params with { sysenv } let (fun, env, params, context) = match response with @@ -5202,11 +5202,11 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im copy_to_canister(dst, offset, size, es.params.arg) ic0.msg_caller_size() : i32 = - if es.context ∉ {I, G, U, Q, CQ, F} then Trap {cycles_used = es.cycles_used;} + if es.context = s 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, CQ, F} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} copy_to_canister(dst, offset, size, es.params.caller) ic0.msg_reject_code() : i32 = @@ -5276,32 +5276,32 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im copy_cycles_to_canister(dst, amount.to_little_endian_bytes()) ic0.canister_self_size() : i32 = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} return |es.wasm_state.self_id| ic0.canister_self_copy(dst:i32, offset:i32, size:i32) = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} copy_to_canister(dst, offset, size, es.wasm_state.self_id) ic0.canister_cycle_balance() : i64 = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} if es.balance >= 2^64 then Trap {cycles_used = es.cycles_used;} return es.balance ic0.canister_cycles_balance128(dst : i32) = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} let amount = es.balance copy_cycles_to_canister(dst, amount.to_little_endian_bytes()) ic0.canister_status() : i32 = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} match es.params.sysenv.canister_status with Running -> return 1 Stopping -> return 2 Stopped -> return 3 ic0.canister_version() : i64 = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} return es.params.sysenv.canister_version ic0.msg_method_name_size() : i32 = @@ -5466,23 +5466,23 @@ The pseudo-code below does *not* explicitly enforce the restrictions of which im es.new_certified_data := es.wasm_state[src..src+size] ic0.data_certificate_present() : i32 = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} if es.params.sysenv.certificate = NoCertificate then return 0 else return 1 ic0.data_certificate_size() : i32 = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} if es.params.sysenv.certificate = NoCertificate then Trap {cycles_used = es.cycles_used;} return |es.params.sysenv.certificate| ic0.data_certificate_copy(dst: i32, offset: i32, size: i32) = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} if es.params.sysenv.certificate = NoCertificate then Trap {cycles_used = es.cycles_used;} copy_to_canister(dst, offset, size, es.params.sysenv.certificate) ic0.time() : i32 = - if es.context ∉ {I, G, U, Q, Ry, Rt, C, F, T} then Trap {cycles_used = es.cycles_used;} + if es.context = s then Trap {cycles_used = es.cycles_used;} return es.params.sysenv.time ic0.global_timer_set(timestamp: i64) : i64 = From d4369c1eb07e403ad2d5e22dcf2203697ea5a783 Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Mon, 31 Jul 2023 15:55:44 +0200 Subject: [PATCH 05/12] add note on confidentiality of values in certified state tree (#209) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * add note on confidentiality of values in certified state tree * add recommendation to salt responses * Update spec/index.md Co-authored-by: Björn Tackmann <54846571+Dfinity-Bjoern@users.noreply.github.com> --------- Co-authored-by: Björn Tackmann <54846571+Dfinity-Bjoern@users.noreply.github.com> --- spec/_attachments/interface-spec-changelog.md | 1 + spec/index.md | 11 +++++++++++ 2 files changed, 12 insertions(+) diff --git a/spec/_attachments/interface-spec-changelog.md b/spec/_attachments/interface-spec-changelog.md index ee00bb809..46a94a5c3 100644 --- a/spec/_attachments/interface-spec-changelog.md +++ b/spec/_attachments/interface-spec-changelog.md @@ -3,6 +3,7 @@ ### ∞ (unreleased) * Canister cycle balance cannot decrease below the freezing limit after executing `install_code` on the management canister. * System API calls `ic0.msg_caller_size` and `ic0.msg_caller_copy` can be called in all contexts except for (start) function. +* Added note on confidentiality of values in the certified state tree. ### 0.20.0 (2023-07-11) {#0_20_0} * IC Bitcoin API, ECDSA API, canister HTTPS outcalls API, and 128-bit cycles System API are considered stable. diff --git a/spec/index.md b/spec/index.md index 6e28628a0..25661f872 100644 --- a/spec/index.md +++ b/spec/index.md @@ -643,6 +643,17 @@ The HTTP response to this request consists of a CBOR (see [CBOR](#cbor)) map wit The returned certificate reveals all values whose path is a suffix of a requested path. It also always reveals `/time`, even if not explicitly requested. +:::note + +The returned certificate might also reveal the SHA-256 hashes of values whose paths have not been requested +and whose paths might not even be allowed to be requested by the sender of the HTTP request. +This means that unauthorized users might obtain the SHA-256 hashes of ingress message responses +and private custom sections of the canister's module. +Hence, users are advised to use cryptographically strong nonces in their HTTP requests and +canister developers that aim at keeping data confidential are advised to add a secret cryptographic salt to their canister's responses and private custom sections. + +::: + All requested paths must have one of the following paths as prefix: - `/time`. Can always be requested. From cbe1758b1aa1fbcaaf430a9a46cd37bd8377c7c6 Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Wed, 9 Aug 2023 13:49:37 +0200 Subject: [PATCH 06/12] update changelog (#212) --- spec/_attachments/interface-spec-changelog.md | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/_attachments/interface-spec-changelog.md b/spec/_attachments/interface-spec-changelog.md index 46a94a5c3..a13e2f765 100644 --- a/spec/_attachments/interface-spec-changelog.md +++ b/spec/_attachments/interface-spec-changelog.md @@ -4,6 +4,7 @@ * Canister cycle balance cannot decrease below the freezing limit after executing `install_code` on the management canister. * System API calls `ic0.msg_caller_size` and `ic0.msg_caller_copy` can be called in all contexts except for (start) function. * Added note on confidentiality of values in the certified state tree. +* Update algorithm computing the request and response hash in the HTTP Gateway including clarification of when the HTTP Gateway can allow for arbitrary certification version in the canister's response. ### 0.20.0 (2023-07-11) {#0_20_0} * IC Bitcoin API, ECDSA API, canister HTTPS outcalls API, and 128-bit cycles System API are considered stable. From 7de16b9de7025f81bef7098eb74c80d8e6ef6209 Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Wed, 9 Aug 2023 14:46:55 +0200 Subject: [PATCH 07/12] add canister_composite_query to WASM module requirements section (#214) --- spec/index.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/index.md b/spec/index.md index 25661f872..0f59975d4 100644 --- a/spec/index.md +++ b/spec/index.md @@ -1067,9 +1067,9 @@ In order for a WebAssembly module to be usable as the code for the canister, it - declare more than 16 exported custom sections (the custom section names with prefix `icp:`), or - - the number of all exported functions called `canister_update ` or `canister_query ` exceeds 1,000, or + - the number of all exported functions called `canister_update `, `canister_query `, or `canister_composite_query ` exceeds 1,000, or - - the sum of `` lengths in all exported functions called `canister_update ` or `canister_query ` exceeds 20,000, or + - the sum of `` lengths in all exported functions called `canister_update `, `canister_query `, or `canister_composite_query ` exceeds 20,000, or - the total size of the custom sections (the sum of `` lengths in their names `icp:public ` and `icp:private ` plus the sum of their content lengths) exceeds 1MiB. From f1140512db913bf8bb81e1da8975bdb609f98e12 Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Wed, 9 Aug 2023 17:46:41 +0200 Subject: [PATCH 08/12] refine definition of path lookup values (#213) * refine definition of path lookup values * add note * drop Unknown from read_state spec * Update spec/index.md Co-authored-by: Oleksandr Tkachenko <108659113+altkdf@users.noreply.github.com> * some reformulations --------- Co-authored-by: Oleksandr Tkachenko <108659113+altkdf@users.noreply.github.com> --- spec/index.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/spec/index.md b/spec/index.md index 0f59975d4..fd26dba04 100644 --- a/spec/index.md +++ b/spec/index.md @@ -2121,7 +2121,7 @@ To validate a value using a certificate, the user conceptually 1. checks the validity of the partial tree using `verify_cert`, -2. looks up the value in the certificate using `lookup` at a given path, which uses the subroutine `lookup_path` on the certificate's tree +2. looks up the value in the certificate using `lookup` at a given path, which uses the subroutine `lookup_path` on the certificate's tree. This mechanism is used in the `read_state` request type, and eventually also for other purposes. @@ -2186,19 +2186,19 @@ implements DER decoding of the public key, following [RFC5480](https://datatrack All state trees include the time at path `/time` (see [Time](#state-tree-time)). Users that get a certificate with a state tree can look up the timestamp to guard against working on obsolete data. -### Lookup +### Lookup {#lookup} Given a (verified) tree, the user can fetch the value at a given path, which is a sequence of labels (blobs). In this document, we write paths suggestively with slashes as separators; the actual encoding is not actually using slashes as delimiters. The following algorithm looks up a `path` in a certificate, and returns either -- the value +- `Found v`: the requested `path` has an associated value `v` in the tree, -- `Absent`, if the value is guaranteed to be absent in the original state tree, +- `Absent`: the requested path is not in the tree, -- `Unknown`, if this partial view does not include information about this path, or +- `Unknown`: it cannot be syntactically determined if the requested `path` was pruned or not; i.e., there exist at least two trees (one containing the requested path and one *not* containing the requested path) from which the given tree can be obtained by pruning some subtrees, -- `Error`, if the path does not make sense for this certificate: +- `Error`: the requested path does not have an associated value in the tree, but the requested path is in the tree: ```html @@ -4685,7 +4685,7 @@ where `UTF8(name)` holds if `name` is encoded in UTF-8. The response is a certificate `cert`, as specified in [Certification](#certification), which passes `verify_cert` (assuming `S.root_key` as the root of trust), and where for every `path` documented in [The system state tree](#state-tree) that is a suffix of a path in `RS.paths` or of `["time"]`, we have - lookup(path, cert) = lookup_in_tree(path, state_tree(S)) + lookup_in_tree(path, cert.tree) = lookup_in_tree(path, state_tree(S)) where `state_tree` constructs a labeled tree from the IC state `S` and the (so far underspecified) set of subnets `subnets`, as per [The system state tree](#state-tree) @@ -4712,7 +4712,7 @@ where `state_tree` constructs a labeled tree from the IC state `S` and the (so f request_status_tree(Done) = { "status": "done" } -and where `lookup_in_tree` is a function that returns the value or `Absent` as appropriately. +and where `lookup_in_tree` is a function that returns `Found v` for a value `v`, `Absent`, or `Error`, appropriately. See the Section [Lookup](#lookup) for more details. ### Abstract Canisters to System API {#concrete-canisters} From 8981100cd6fa788848e31187277e0fc80a0a244a Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Wed, 9 Aug 2023 17:53:02 +0200 Subject: [PATCH 09/12] add note on supported certificate versions in HTTP Gateway (#211) --- spec/http-gateway-protocol-spec.md | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/spec/http-gateway-protocol-spec.md b/spec/http-gateway-protocol-spec.md index 1423f3265..76b0d7afb 100644 --- a/spec/http-gateway-protocol-spec.md +++ b/spec/http-gateway-protocol-spec.md @@ -375,10 +375,18 @@ The steps for response verification are as follows: ## Response Verification Version Assertion -Canisters can report the versions of response verification that they support using public metadata in the [system state tree](https://internetcomputer.org/docs/current/references/ic-interface-spec/#state-tree-canister-information). This metadata will be read by the HTTP Gateway using a [read_state request](https://internetcomputer.org/docs/current/references/ic-interface-spec/#http-read-state). This metadata is a comma-delimited string of versions under the key "supported_certificate_versions”, for example: "1,2". This is treated as an optional, additional layer of security for canisters supporting multiple versions. If the metadata has not been added (i.e. the lookup of this metadata in the `read_state` response returns `Absent`), then the HTTP Gateway will allow for whatever version the canister has responded with. +Canisters can report the supported versions of response verification using (public) metadata sections available in the [system state tree](https://internetcomputer.org/docs/current/references/ic-interface-spec/#state-tree-canister-information). This metadata will be read by the HTTP Gateway using a [read_state request](https://internetcomputer.org/docs/current/references/ic-interface-spec/#http-read-state). The metadata section must be a (public) custom section with the name `supported_certificate_versions` and contain a comma-delimited string of versions, e.g., `1,2`. This is treated as an optional, additional layer of security for canisters supporting multiple versions. If the metadata has not been added (i.e., the `read_state` request *succeeds* and the lookup of the metadata section in the `read_state` response certificate returns `Absent`), then the HTTP Gateway will allow for whatever version the canister has responded with. + The request for the metadata will only be made by the HTTP Gateway if there is a downgrade. If the HTTP Gateway requests v2 and the canister responds with v2, then a request will not be made. If the HTTP Gateway requests v2 and the canister responds with v1, a request will be made. If a request is made, the HTTP Gateway will not accept any response from the canister that is below the max version supported by both the HTTP Gateway and the canister. This will guarantee that a canister supporting both v1 and v2 will always have v2 security when accessed by an HTTP Gateway that supports v2. +:::note + +The HTTP Gateway can only allow for arbitrary certification version if the custom section `supported_certificate_versions` is *provably* not present, i.e., if the `read_state` response contains a valid certificate whose lookup of the corresponding path yields `Absent`. Otherwise, e.g., if the replica is overloaded or if the `read_state` is rejected because the custom section with the name `supported_certificate_versions` is private, the HTTP Gateway should also reject the canister's response. + +::: + + ## Canister HTTP Interface The full [Candid](https://github.com/dfinity/candid/blob/master/spec/Candid.md) interface that a canister is expected to implement is as follows: From e3e5039d45fa374670ce78c50c9c6b5bdca25bf5 Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Mon, 14 Aug 2023 07:22:53 +0200 Subject: [PATCH 10/12] fix formatting of HTTP read_state request and response definitions (#218) --- spec/index.md | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/index.md b/spec/index.md index fd26dba04..634006b78 100644 --- a/spec/index.md +++ b/spec/index.md @@ -635,6 +635,7 @@ In order to read parts of the [The system state tree](#state-tree), the user mak - `sender`, `nonce`, `ingress_expiry`: See [Authentication](#authentication) - `paths` (sequence of paths): A list of at most 1000 paths, where a path is itself a sequence of at most 127 blobs. + The HTTP response to this request consists of a CBOR (see [CBOR](#cbor)) map with the following fields: - `certificate` (`blob`): A certificate (see [Certification](#certification)). From aba6c6d6db38e17d69df44420211370a4795e89f Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Mon, 14 Aug 2023 07:26:03 +0200 Subject: [PATCH 11/12] update conditions on requested paths in HTTP read_state requests (#216) * update conditions on requested paths in HTTP read_state requests * allow requesting /subnet/ * update changelog --- spec/_attachments/interface-spec-changelog.md | 1 + spec/index.md | 28 ++++++++++++------- 2 files changed, 19 insertions(+), 10 deletions(-) diff --git a/spec/_attachments/interface-spec-changelog.md b/spec/_attachments/interface-spec-changelog.md index a13e2f765..5c36f7380 100644 --- a/spec/_attachments/interface-spec-changelog.md +++ b/spec/_attachments/interface-spec-changelog.md @@ -5,6 +5,7 @@ * System API calls `ic0.msg_caller_size` and `ic0.msg_caller_copy` can be called in all contexts except for (start) function. * Added note on confidentiality of values in the certified state tree. * Update algorithm computing the request and response hash in the HTTP Gateway including clarification of when the HTTP Gateway can allow for arbitrary certification version in the canister's response. +* Update conditions on requested paths in HTTP read state requests. ### 0.20.0 (2023-07-11) {#0_20_0} * IC Bitcoin API, ECDSA API, canister HTTPS outcalls API, and 128-bit cycles System API are considered stable. diff --git a/spec/index.md b/spec/index.md index 634006b78..9f7e950e9 100644 --- a/spec/index.md +++ b/spec/index.md @@ -655,13 +655,13 @@ canister developers that aim at keeping data confidential are advised to add a s ::: -All requested paths must have one of the following paths as prefix: +All requested paths must have the following form: - `/time`. Can always be requested. -- `/subnet`. Can always be requested. +- `/subnet`, `/subnet/`, `/subnet//public_key`, `/subnet//canister_ranges`. Can always be requested. -- `/request_status/`. Can be requested if no path with such a prefix exists in the state tree or +- `/request_status/`, `/request_status//status`, `/request_status//reply`, `/request_status//reject_code`, `/request_status//reject_message`, `/request_status//error_code`. Can be requested if no path with such a prefix exists in the state tree or - the sender of the original request referenced by `` is the same as the sender of the read state request and @@ -4667,13 +4667,21 @@ A record with The predicate `may_read_path` is defined as follows, implementing the access control outlined in [Request: Read state](#http-read-state): - may_read_path(S, _, ["time"] · _) = True - may_read_path(S, _, ["subnet"] · _) = True - may_read_path(S, _, ["request_status", Rid] · _) = + may_read_path(S, _, ["time"]) = True + may_read_path(S, _, ["subnet"]) = True + may_read_path(S, _, ["subnet", sid]) = True + may_read_path(S, _, ["subnet", sid, "public_key"]) = True + may_read_path(S, _, ["subnet", sid, "canister_ranges"]) = True + may_read_path(S, _, ["request_status", Rid]) = + may_read_path(S, _, ["request_status", Rid, "status"]) = + may_read_path(S, _, ["request_status", Rid, "reply"]) = + may_read_path(S, _, ["request_status", Rid, "reject_code"]) = + may_read_path(S, _, ["request_status", Rid, "reject_message"]) = + may_read_path(S, _, ["request_status", Rid, "error_code"]) = ∀ (R ↦ (_, ECID')) ∈ dom(S.requests). hash_of_map(R) = Rid => RS.sender == R.sender ∧ ECID == ECID' - may_read_path(S, _, ["canister", cid, "module_hash"] · _) = cid == ECID - may_read_path(S, _, ["canister", cid, "controllers"] · _) = cid == ECID - may_read_path(S, _, ["canister", cid, "metadata", name] · _) = cid == ECID ∧ UTF8(name) ∧ + may_read_path(S, _, ["canister", cid, "module_hash"]) = cid == ECID + may_read_path(S, _, ["canister", cid, "controllers"]) = cid == ECID + may_read_path(S, _, ["canister", cid, "metadata", name]) = cid == ECID ∧ UTF8(name) ∧ (cid ∉ dom(S.canisters[cid]) ∨ S.canisters[cid] = EmptyCanister ∨ name ∉ (dom(S.canisters[cid].public_custom_sections) ∪ dom(S.canisters[cid].private_custom_sections)) ∨ @@ -4707,7 +4715,7 @@ where `state_tree` constructs a labeled tree from the IC state `S` and the (so f request_status_tree(Processing) = { "status": "processing" } request_status_tree(Rejected (code, msg)) = - { "status": "rejected"; "reject_code": code; "reject_message": msg, error_code: } + { "status": "rejected"; "reject_code": code; "reject_message": msg; "error_code": } request_status_tree(Replied arg) = { "status": "replied"; "reply": arg } request_status_tree(Done) = From 5f65cc9210d8df30befac8c35473632dd7bd17cf Mon Sep 17 00:00:00 2001 From: mraszyk <31483726+mraszyk@users.noreply.github.com> Date: Wed, 16 Aug 2023 11:59:14 +0200 Subject: [PATCH 12/12] point out that stable memory is cleared during reinstall (#220) --- spec/index.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/index.md b/spec/index.md index 9f7e950e9..5ed81bd6e 100644 --- a/spec/index.md +++ b/spec/index.md @@ -1836,7 +1836,7 @@ Only controllers of the canister can install code. - If `mode = install`, the canister must be empty before. This will instantiate the canister module and invoke its `canister_init` method (if present), as explained in Section "[Canister initialization](#system-api-init)", passing the `arg` to the canister. -- If `mode = reinstall`, if the canister was not empty, its existing code and state is removed before proceeding as for `mode = install`. +- If `mode = reinstall`, if the canister was not empty, its existing code and state (including stable memory) is removed before proceeding as for `mode = install`. Note that this is different from `uninstall_code` followed by `install_code`, as `uninstall_code` generates a synthetic reject response to all callers of the uninstalled canister that the uninstalled canister did not yet reply to and ensures that callbacks to outstanding calls made by the uninstalled canister won't be executed (i.e., upon receiving a response from a downstream call made by the uninstalled canister, the cycles attached to the response are refunded, but no callbacks are executed).