Merge branch 'bogwar/largewasm' of github.com:dfinity/interface-spec …

…into bogwar/largewasm

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/).

spec/_attachments/ic.did

@@ -126,9 +126,9 @@ service ic : {
   upload_chunk : (record {
     canister_id : principal;
     chunk : blob;
-  }) -> chunk_hash;
-  stored_chunks: (record {canister_id : canister_id}) -> vec chunk_hash;
-  delete_chunks: (record {canister_id : canister_id, hash_list : vec chunk_hash}) -> ();
+  }) -> (chunk_hash);
+  stored_chunks: (record {canister_id : canister_id}) -> (vec chunk_hash);
+  delete_chunks: (record {canister_id : canister_id; hash_list : vec chunk_hash}) -> ();
   clear_chunk_store: (record {canister_id: canister_id}) -> ();
   install_code : (record {
     mode : variant {install; reinstall; upgrade};

spec/_attachments/interface-spec-changelog.md

@@ -1,5 +1,12 @@
 ## Changelog {#changelog}
 
+### ∞ (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.
+* 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.
 * Add conditions on requested paths in read state requests.

spec/http-gateway-protocol-spec.md

@@ -288,6 +288,7 @@ HEADER = 'IC-CertificateExpression: ', HEADER-VALUE
 The request hash is calculated as follows:
 
 1. Let `request_headers_hash` be the [representation-independent hash](https://internetcomputer.org/docs/current/references/ic-interface-spec#hash-of-map) of the request headers:
+   - The header names are lower-cased.
    - Only include headers listed in the `certified_request_headers` field of [the certificate expression header](#the-certificate-expression-header).
      - If the field is empty or no value was supplied, no headers are included.
      - Headers can be repeated and each repetition should be included.
@@ -305,6 +306,7 @@ The request hash is calculated as follows:
 The response hash is calculated as follows:
 
 1. Let `response_headers_hash` be the [representation-independent hash](https://internetcomputer.org/docs/current/references/ic-interface-spec#hash-of-map) of the response headers:
+   - The header names are lower-cased.
    - The `IC-Certificate` header is always excluded.
    - The `IC-CertificateExpression` header is always included.
    - If the `no_certification` field of [the certificate expression header](#the-certificate-expression-header) is present:
@@ -316,6 +318,7 @@ The response hash is calculated as follows:
      - All headers listed (except for the `IC-CertificateExpression` header) are excluded from the certification
      - All other headers (except for the IC-Certificate header) are included in the certification
    - Headers can be repeated and each repetition should be included.
+   - Include an additional `:ic-cert-status` header that contains the numerical HTTP status code of the response.
 2. Let `response_body_hash` be the sha256 of the response body.
 3. Concatenate `response_headers_hash` and `response_body_hash` and calculate the sha256 of that concatenation.
 
@@ -372,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, 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: