Skip to content
This repository has been archived by the owner on Nov 19, 2024. It is now read-only.

Commit

Permalink
adjust formal semantics
Browse files Browse the repository at this point in the history
  • Loading branch information
mraszyk committed Nov 14, 2023
1 parent 0ea9bcd commit ec99b69
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions spec/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -5212,6 +5212,7 @@ Conditions

E.content = CanisterQuery Q
Q.canister_id ∈ verify_envelope(E, Q.sender, S.system_time)
|Q.nonce| <= 32
is_effective_canister_id(E.content, ECID)
S.system_time <= Q.ingress_expiry

Expand Down Expand Up @@ -5256,6 +5257,7 @@ Conditions

E.content = ReadState RS
TS = verify_envelope(E, RS.sender, S.system_time)
|E.content.nonce| <= 32
S.system_time <= RS.ingress_expiry
∀ path ∈ RS.paths. may_read_path_for_canister(S, R.sender, path)
∀ (["request_status", Rid] · _) ∈ RS.paths. ∀ R ∈ dom(S.requests). hash_of_map(R) = Rid => R.canister_id ∈ TS
Expand Down Expand Up @@ -5306,6 +5308,7 @@ Conditions

E.content = ReadState RS
TS = verify_envelope(E, RS.sender, S.system_time)
|E.content.nonce| <= 32
S.system_time <= RS.ingress_expiry
∀ path ∈ RS.paths. may_read_path_for_subnet(S, RS.sender, path)

Expand Down

0 comments on commit ec99b69

Please sign in to comment.