From b74b1c2b68eabc3fa4ca8fdf0dc732e75cdac11a Mon Sep 17 00:00:00 2001 From: Josef Widder <44643235+josef-widder@users.noreply.github.com> Date: Thu, 10 Sep 2020 12:56:15 +0200 Subject: [PATCH] Current versions of light client specs from tendermint-rs (#158) * current versions of light client specs from tendermint-rs * markdown lint * linting * links * links * links Co-authored-by: Marko Baricevic --- .markdownlint.yml | 1 + rust-spec/lightclient/README.md | 92 ++ .../lightclient/attacks/evidence-handling.md | 219 ++++ rust-spec/lightclient/detection/README.md | 69 + rust-spec/lightclient/detection/detection.md | 696 ++++++++++ .../lightclient/detection/discussions.md | 178 +++ .../lightclient/detection/draft-functions.md | 289 ++++ .../detection/req-ibc-detection.md | 345 +++++ rust-spec/lightclient/experiments.png | Bin 0 -> 83681 bytes .../verification/001bmc-apalache.csv | 49 + .../verification/Blockchain_A_1.tla | 171 +++ .../verification/Lightclient_A_1.tla | 440 +++++++ .../verification/MC4_3_correct.tla | 15 + .../lightclient/verification/MC4_3_faulty.tla | 15 + .../lightclient/verification/MC4_4_faulty.tla | 15 + .../verification/MC4_5_correct.tla | 15 + .../lightclient/verification/MC4_5_faulty.tla | 15 + .../lightclient/verification/MC4_6_faulty.tla | 15 + .../lightclient/verification/MC4_7_faulty.tla | 15 + .../verification/MC5_5_correct.tla | 15 + .../lightclient/verification/MC5_5_faulty.tla | 15 + .../lightclient/verification/MC5_7_faulty.tla | 15 + .../lightclient/verification/MC7_5_faulty.tla | 15 + .../lightclient/verification/MC7_7_faulty.tla | 15 + .../lightclient/verification/verification.md | 1162 +++++++++++++++++ 25 files changed, 3891 insertions(+) create mode 100644 rust-spec/lightclient/README.md create mode 100644 rust-spec/lightclient/attacks/evidence-handling.md create mode 100644 rust-spec/lightclient/detection/README.md create mode 100644 rust-spec/lightclient/detection/detection.md create mode 100644 rust-spec/lightclient/detection/discussions.md create mode 100644 rust-spec/lightclient/detection/draft-functions.md create mode 100644 rust-spec/lightclient/detection/req-ibc-detection.md create mode 100644 rust-spec/lightclient/experiments.png create mode 100644 rust-spec/lightclient/verification/001bmc-apalache.csv create mode 100644 rust-spec/lightclient/verification/Blockchain_A_1.tla create mode 100644 rust-spec/lightclient/verification/Lightclient_A_1.tla create mode 100644 rust-spec/lightclient/verification/MC4_3_correct.tla create mode 100644 rust-spec/lightclient/verification/MC4_3_faulty.tla create mode 100644 rust-spec/lightclient/verification/MC4_4_faulty.tla create mode 100644 rust-spec/lightclient/verification/MC4_5_correct.tla create mode 100644 rust-spec/lightclient/verification/MC4_5_faulty.tla create mode 100644 rust-spec/lightclient/verification/MC4_6_faulty.tla create mode 100644 rust-spec/lightclient/verification/MC4_7_faulty.tla create mode 100644 rust-spec/lightclient/verification/MC5_5_correct.tla create mode 100644 rust-spec/lightclient/verification/MC5_5_faulty.tla create mode 100644 rust-spec/lightclient/verification/MC5_7_faulty.tla create mode 100644 rust-spec/lightclient/verification/MC7_5_faulty.tla create mode 100644 rust-spec/lightclient/verification/MC7_7_faulty.tla create mode 100644 rust-spec/lightclient/verification/verification.md diff --git a/.markdownlint.yml b/.markdownlint.yml index 9f8a8d689..6b4e78a33 100644 --- a/.markdownlint.yml +++ b/.markdownlint.yml @@ -1,4 +1,5 @@ default: true +MD001: false MD007: { indent: 4 } MD013: false MD024: { siblings_only: true } diff --git a/rust-spec/lightclient/README.md b/rust-spec/lightclient/README.md new file mode 100644 index 000000000..a0e14e380 --- /dev/null +++ b/rust-spec/lightclient/README.md @@ -0,0 +1,92 @@ +# Light Client Specification + +This directory contains work-in-progress English and TLA+ specifications for the Light Client +protocol. Implementations of the light client can be found in +[Rust](https://github.com/informalsystems/tendermint-rs/tree/master/light-client) and +[Go](https://github.com/tendermint/tendermint/tree/master/light). + +Light clients are assumed to be initialized once from a trusted source +with a trusted header and validator set. The light client +protocol allows a client to then securely update its trusted state by requesting and +verifying a minimal set of data from a network of full nodes (at least one of which is correct). + +The light client is decomposed into three components: + +- Commit Verification - verify signed headers and associated validator set changes from a single full node +- Fork Detection - verify commits across multiple full nodes and detect conflicts (ie. the existence of forks) +- Fork Accountability - given a fork, which validators are responsible for it. + +## Commit Verification + +The [English specification](verification/verification.md) describes the light client +commit verification problem in terms of the temporal properties +[LCV-DIST-SAFE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification.md#lcv-dist-safe1) and +[LCV-DIST-LIVE.1](https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification.md#lcv-dist-live1). +Commit verification is assumed to operate within the Tendermint Failure Model, where +2/3 of validators are correct for some time period and +validator sets can change arbitrarily at each height. + +A light client protocol is also provided, including all checks that +need to be performed on headers, commits, and validator sets +to satisfy the temporal properties - so a light client can continuously +synchronize with a blockchain. Clients can skip possibly +many intermediate headers by exploiting overlap in trusted and untrusted validator sets. +When there is not enough overlap, a bisection routine can be used to find a +minimal set of headers that do provide the required overlap. + +The [TLA+ specification](verification/Lightclient_A_1.tla) is a formal description of the +commit verification protocol executed by a client, including the safety and +liveness properties, which can be model checked with Apalache. + +The `MC*.tla` files contain concrete parameters for the +[TLA+ specification](verification/Lightclient_A_1.tla), in order to do model checking. +For instance, [MC4_3_faulty.tla](verification/MC4_3_faulty.tla) contains the following parameters +for the nodes, heights, the trusting period, and correctness of the primary node: + +```tla +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 3 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE +``` + +To run a complete set of experiments, clone [apalache](https://github.com/informalsystems/apalache) and [apalache-tests](https://github.com/informalsystems/apalache-tests) into a directory `$DIR` and run the following commands: + +```sh +$DIR/apalache-tests/scripts/mk-run.py --memlimit 28 001bmc-apalache.csv $DIR/apalache . out +./out/run-all.sh +``` + +After the experiments have finished, you can collect the logs by executing the following command: + +```sh +cd ./out +$DIR/apalache-tests/scripts/parse-logs.py --human . +``` + +The following table summarizes the experimental results. The TLA+ properties can be found in the +[TLA+ specification](verification/Lightclient_A_1.tla). + The experiments were run in an AWS instance equipped with 32GB +RAM and a 4-core Intel® Xeon® CPU E5-2686 v4 @ 2.30GHz CPU. +We write “✗=k” when a bug is reported at depth k, and “✓<=k” when +no bug is reported up to depth k. + +![Experimental results](experiments.png) + +## Fork Detection + +This is a work-in-progress draft. + +The [English specification](detection/detection.md) defines blockchain forks and describes +the problem of a light client detecting them from communication with a network +of full nodes, where at least one is correct. + +There is no TLA+ yet. + +## Fork Accountability + +There is no English specification yet. TODO: Jovan's work? + +TODO: there is a WIP [TLA+ +specification](https://github.com/informalsystems/verification/pull/13) in the +verification repo that should be moved over here. diff --git a/rust-spec/lightclient/attacks/evidence-handling.md b/rust-spec/lightclient/attacks/evidence-handling.md new file mode 100644 index 000000000..4b7d81919 --- /dev/null +++ b/rust-spec/lightclient/attacks/evidence-handling.md @@ -0,0 +1,219 @@ + +# Light client attacks + +We define a light client attack as detection of conflicting headers for a given height that can be verified +starting from the trusted light block. A light client attack is defined in the context of interactions of +light client with two peers. One of the peers (called primary) defines a trace of verified light blocks +(primary trace) that are being checked against trace of the other peer (called witness) that we call +witness trace. + +A light client attack is defined by the primary and witness traces +that have a common root (the same trusted light block for a common height) but forms +conflicting branches (end of traces is for the same height but with different headers). +Note that conflicting branches could be arbitrarily big as branches continue to diverge after +a bifurcation point. We propose an approach that allows us to define a valid light client attack +only with a common light block and a single conflicting light block. We rely on the fact that +we assume that the primary is under suspicion (therefore not trusted) and that the witness plays +support role to detect and process an attack (therefore trusted). Therefore, once a light client +detects an attack, it needs to send to a witness only missing data (common height +and conflicting light block) as it has its trace. Keeping light client attack data of constant size +saves bandwidth and reduces an attack surface. As we will explain below, although in the context of +light client core +[verification](https://github.com/informalsystems/tendermint-rs/tree/master/docs/spec/lightclient/verification) +the roles of primary and witness are clearly defined, +in case of the attack, we run the same attack detection procedure twice where the roles are swapped. +The rationale is that the light client does not know what peer is correct (on a right main branch) +so it tries to create and submit an attack evidence to both peers. + +Light client attack evidence consists of a conflicting light block and a common height. + +```go +type LightClientAttackEvidence struct { + ConflictingBlock LightBlock + CommonHeight int64 +} +``` + +Full node can validate a light client attack evidence by executing the following procedure: + +```go +func IsValid(lcaEvidence LightClientAttackEvidence, bc Blockchain) boolean { + commonBlock = GetLightBlock(bc, lcaEvidence.CommonHeight) + if commonBlock == nil return false + + // Note that trustingPeriod in ValidAndVerified is set to UNBONDING_PERIOD + verdict = ValidAndVerified(commonBlock, lcaEvidence.ConflictingBlock) + conflictingHeight = lcaEvidence.ConflictingBlock.Header.Height + + return verdict == OK and bc[conflictingHeight].Header != lcaEvidence.ConflictingBlock.Header +} +``` + +## Light client attack creation + +Given a trusted light block `trusted`, a light node executes the bisection algorithm to verify header +`untrusted` at some height `h`. If the bisection algorithm succeeds, then the header `untrusted` is verified. +Headers that are downloaded as part of the bisection algorithm are stored in a store and they are also in +the verified state. Therefore, after the bisection algorithm successfully terminates we have a trace of +the light blocks ([] LightBlock) we obtained from the primary that we call primary trace. + +### Primary trace + +The following invariant holds for the primary trace: + +- Given a `trusted` light block, target height `h`, and `primary_trace` ([] LightBlock): + *primary_trace[0] == trusted* and *primary_trace[len(primary_trace)-1].Height == h* and + successive light blocks are passing light client verification logic. + +### Witness with a conflicting header + +The verified header at height `h` is cross-checked with every witness as part of +[detection](https://github.com/informalsystems/tendermint-rs/tree/master/docs/spec/lightclient/detection). +If a witness returns the conflicting header at the height `h` the following procedure is executed to verify +if the conflicting header comes from the valid trace and if that's the case to create an attack evidence: + +#### Helper functions + +We assume the following helper functions: + +```go +// Returns trace of verified light blocks starting from rootHeight and ending with targetHeight. +Trace(lightStore LightStore, rootHeight int64, targetHeight int64) LightBlock[] + +// Returns validator set for the given height +GetValidators(bc Blockchain, height int64) Validator[] + +// Returns validator set for the given height +GetValidators(bc Blockchain, height int64) Validator[] + +// Return validator addresses for the given validators +GetAddresses(vals Validator[]) ValidatorAddress[] +``` + +```go +func DetectLightClientAttacks(primary PeerID, + primary_trace []LightBlock, + witness PeerID) (LightClientAttackEvidence, LightClientAttackEvidence) { + primary_lca_evidence, witness_trace = DetectLightClientAttack(primary_trace, witness) + + witness_lca_evidence = nil + if witness_trace != nil { + witness_lca_evidence, _ = DetectLightClientAttack(witness_trace, primary) + } + return primary_lca_evidence, witness_lca_evidence +} + +func DetectLightClientAttack(trace []LightBlock, peer PeerID) (LightClientAttackEvidence, []LightBlock) { + + lightStore = new LightStore().Update(trace[0], StateTrusted) + + for i in 1..len(trace)-1 { + lightStore, result = VerifyToTarget(peer, lightStore, trace[i].Header.Height) + + if result == ResultFailure then return (nil, nil) + + current = lightStore.Get(trace[i].Header.Height) + + // if obtained header is the same as in the trace we continue with a next height + if current.Header == trace[i].Header continue + + // we have identified a conflicting header + commonBlock = trace[i-1] + conflictingBlock = trace[i] + + return (LightClientAttackEvidence { conflictingBlock, commonBlock.Header.Height }, + Trace(lightStore, trace[i-1].Header.Height, trace[i].Header.Height)) + } + return (nil, nil) +} +``` + +## Evidence handling + +As part of on chain evidence handling, full nodes identifies misbehaving processes and informs +the application, so they can be slashed. Note that only bonded validators should +be reported to the application. There are three types of attacks that can be executed against +Tendermint light client: + +- lunatic attack +- equivocation attack and +- amnesia attack. + +We now specify the evidence handling logic. + +```go +func detectMisbehavingProcesses(lcAttackEvidence LightClientAttackEvidence, bc Blockchain) []ValidatorAddress { + assume IsValid(lcaEvidence, bc) + + // lunatic light client attack + if !isValidBlock(current.Header, conflictingBlock.Header) { + conflictingCommit = lcAttackEvidence.ConflictingBlock.Commit + bondedValidators = GetNextValidators(bc, lcAttackEvidence.CommonHeight) + + return getSigners(conflictingCommit) intersection GetAddresses(bondedValidators) + + // equivocation light client attack + } else if current.Header.Round == conflictingBlock.Header.Round { + conflictingCommit = lcAttackEvidence.ConflictingBlock.Commit + trustedCommit = bc[conflictingBlock.Header.Height+1].LastCommit + + return getSigners(trustedCommit) intersection getSigners(conflictingCommit) + + // amnesia light client attack + } else { + HandleAmnesiaAttackEvidence(lcAttackEvidence, bc) + } +} + +// Block validity in this context is defined by the trusted header. +func isValidBlock(trusted Header, conflicting Header) boolean { + return trusted.ValidatorsHash == conflicting.ValidatorsHash and + trusted.NextValidatorsHash == conflicting.NextValidatorsHash and + trusted.ConsensusHash == conflicting.ConsensusHash and + trusted.AppHash == conflicting.AppHash and + trusted.LastResultsHash == conflicting.LastResultsHash +} + +func getSigners(commit Commit) []ValidatorAddress { + signers = []ValidatorAddress + for (i, commitSig) in commit.Signatures { + if commitSig.BlockIDFlag == BlockIDFlagCommit { + signers.append(commitSig.ValidatorAddress) + } + } + return signers +} +``` + +Note that amnesia attack evidence handling involves more complex processing, i.e., cannot be +defined simply on amnesia attack evidence. We explain in the following section a protocol +for handling amnesia attack evidence. + +### Amnesia attack evidence handling + +Detecting faulty processes in case of the amnesia attack is more complex and cannot be inferred +purely based on attack evidence data. In this case, in order to detect misbehaving processes we need +access to votes processes sent/received during the conflicting height. Therefore, amnesia handling assumes that +validators persist all votes received and sent during multi-round heights (as amnesia attack +is only possible in heights that executes over multiple rounds, i.e., commit round > 0). + +To simplify description of the algorithm we assume existence of the trusted oracle called monitor that will +drive the algorithm and output faulty processes at the end. Monitor can be implemented in a +distributed setting as on-chain module. The algorithm works as follows: + 1) Monitor sends votesets request to validators of the conflicting height. Validators + are expected to send their votesets within predefined timeout. + 2) Upon receiving votesets request, validators send their votesets to a monitor. + 2) Validators which have not sent its votesets within timeout are considered faulty. + 3) The preprocessing of the votesets is done. That means that the received votesets are analyzed + and each vote (valid) sent by process p is added to the voteset of the sender p. This phase ensures that + votes sent by faulty processes observed by at least one correct validator cannot be excluded from the analysis. + 4) Votesets of every validator are analyzed independently to decide whether the validator is correct or faulty. + A faulty validators is the one where at least one of those invalid transitions is found: + - More than one PREVOTE message is sent in a round + - More than one PRECOMMIT message is sent in a round + - PRECOMMIT message is sent without receiving +2/3 of voting-power equivalent + appropriate PREVOTE messages + - PREVOTE message is sent for the value V’ in round r’ and the PRECOMMIT message had + been sent for the value V in round r by the same process (r’ > r) and there are no + +2/3 of voting-power equivalent PREVOTE(vr, V’) messages (vr ≥ 0 and vr > r and vr < r’) + as the justification for sending PREVOTE(r’, V’) diff --git a/rust-spec/lightclient/detection/README.md b/rust-spec/lightclient/detection/README.md new file mode 100644 index 000000000..8f92bdaa2 --- /dev/null +++ b/rust-spec/lightclient/detection/README.md @@ -0,0 +1,69 @@ + +# Tendermint fork detection and IBC fork detection + +## Status + +This is a work in progress. +This directory captures the ongoing work and discussion on fork +detection both in the context of a Tendermint light node and in the +context of IBC. It contains the following files + +### [detection.md](./detection.md) + +a draft of the light node fork detection including "proof of fork" + definition, that is, the data structure to submit evidence to full + nodes. + +### [discussions.md](./discussions.md) + +A collection of ideas and intuitions from recent discussions + +- the outcome of recent discussion +- a sketch of the light client supervisor to provide the context in + which fork detection happens +- a discussion about lightstore semantics + +### [req-ibc-detection.md](./req-ibc-detection.md) + +- a collection of requirements for fork detection in the IBC + context. In particular it contains a section "Required Changes in + ICS 007" with necessary updates to ICS 007 to support Tendermint + fork detection + +### [draft-functions.md](./draft-functions.md) + +In order to address the collected requirements, we started to sketch +some functions that we will need in the future when we specify in more +detail the + +- fork detections +- proof of fork generation +- proof of fork verification + +on the following components. + +- IBC on-chain components +- Relayer + +### TODOs + +We decided to merge the files while there are still open points to +address to record the current state an move forward. In particular, +the following points need to be addressed: + +- + +- + +- + +- + +Most likely we will write a specification on the light client +supervisor along the outcomes of + +- + +that also addresses initialization + +- diff --git a/rust-spec/lightclient/detection/detection.md b/rust-spec/lightclient/detection/detection.md new file mode 100644 index 000000000..4faa0f4ca --- /dev/null +++ b/rust-spec/lightclient/detection/detection.md @@ -0,0 +1,696 @@ +# Fork detector + +> ***This an unfinished draft. Comments are welcome!*** + +A detector (or detector for short) is a mechanism that expects as +input a header with some height *h*, connects to different Tendermint +full nodes, requests the header of height *h* from them, and then +cross-checks the headers and the input header. + +There are two foreseeable use cases: + +1) strengthen the light client: If a light client accepts a header +*hd* (after performing skipping or sequential verification), it can +use the detector to probe the system for conflicting headers and +increase the trust in *hd*. Instead of communicating with a single +full node, communicating with several full nodes shall increase the +likelihood to be aware of a fork (see [[accountability]] for +discussion about forks) in case there is one. + +2) to support fork accountability: In the case when more than 1/3 of +the voting power is held by faulty validators, faulty nodes may +generate two conflicting headers for the same height. The goal of the +detector is to learn about the conflicting headers by probing +different full nodes. Once a detector has two conflicting headers, +these headers are evidence of misbehavior. A natural extension is to +use the detector within a monitor process (on a full node) that calls +the detector on a sample (or all) headers (in parallel). (If the +sample is chosen at random, this adds a level of probabilistic +reasoning.) If conflicting headers are found, they are evidence that +can be used for punishing processes. + +In this document we will focus onn strengthening the light client, and +leave other uses of the detection mechanism (e.g., when run on a full +node) to the future. + +## Context of this document + +The light client verification specification [[verification]] is +designed for the Tendermint failure model (1/3 assumption) +[TMBC-FM-2THIRDS]. It is safe under this assumption, and live +if it can reliably (that is, no message loss, no duplication, and +eventually delivered) and timely communicate with a correct full node. If +this assumption is violated, the light client can be fooled to trust a +header that was not generated by Tendermint consensus. + +This specification, the fork detector, is a "second line of defense", +in case the 1/3 assumption is violated. Its goal is to detect fork (conflicting headers) and collect +evidence. However, it is impractical to probe all full nodes. At this +time we consider a simple scheme of maintaining an address book of +known full nodes from which a small subset (e.g., 4) are chosen +initially to communicate with. More involved book keeping with +probabilistic guarantees can be considered at later stages of the +project. + +The light client maintains a simple address book containing addresses +of full nodes that it can pick as primary and secondaries. To obtain +a new header, the light client first does [verification][verification] +with the primary, and then cross-checks the header with the +secondaries using this specification. + +### Tendermint Consensus and Forks + +#### **[TMBC-GENESIS.1]** + +Let *Genesis* be the agreed-upon initial block (file). + +#### **[TMBC-FUNC.1]** + +> **TODO** be more precise. +2/3 of b.NextV = c.Val signed c. For now +> the following will do: + +Let b and c be two light blocks +with *b.Header.Height + 1 = c.Header.Height*. We define **signs(b,c)** + iff `ValidAndVerified(b, c)` + +> **TODO** be more precise. +1/3 of b.NextV signed c. For now +> the following will do: + +Let *b* and *c* be two light blocks. We define **supports(b,c,t)** + iff `ValidAndVerified(b, c)` at time *t* + +> The following formalizes that *b* was properly generated by +> Tendermint; *b* can be traced back to genesis + +#### **[TMBC-SEQ-ROOTED.1]** + +Let *b* be a light block. +We define *sequ-rooted(b)* iff for all i, 1 <= i < h = b.Header.Height, +there exist light blocks a(i) s.t. + +- *a(1) = Genesis* and +- *a(h) = b* and +- *signs( a(i) , a(i+1) )*. + +> The following formalizes that *c* is trusted based on *b* in +> skipping verification. Observe that we do not require here (yet) +> that *b* was properly generated. + +#### **[TMBC-SKIP-ROOT.1]** + +Let *b* and *c* be light blocks. We define *skip-root(b,c,t)* if at +time t there exists an *h* and a sequence *a(1)*, ... *a(h)* s.t. + +- *a(1) = b* and +- *a(h) = c* and +- *supports( a(i), a(i+1), t)*, for all i, *1 <= i < h*. + +> **TODO** In the above we might use a sequence of times t(i). Not sure. +> **TODO:** I believe the following definition +> corresponds to **Slashable fork** in +> [forks][tendermintfork]. Please confirm! +> Observe that sign-skip-match is even defined if there is a fork on +> the chain. + +#### **[TMBC-SIGN-SKIP-MATCH.1]** + +Let *a*, *b*, *c*, be light blocks and *t* a time, we define +*sign-skip-match(a,b,c,t) = true* iff + +- *sequ-rooted(a)* and + +- *b.Header.Height = c.Header.Height* and +- *skip-root(a,b,t)* +- *skip-root(a,c,t)* + +implies *b = c*. + +#### **[TMBC-SIGN-FORK.1]** + +If there exists three light blocks a, b, and c, with +*sign-skip-match(a,b,c,t) = +false* then we have a *slashable fork*. +We call *a* a bifurcation block of the fork. +We say we have **a fork at height** *b.Header.Height*. + +> The lightblock *a* need not be unique, that is, a there may be +> several blocks that satisfy the above requirement for blocks *b* and +> *c*. +> **TODO:** I think the following definition is +> the intuition behind **main chain forks** +> in the document on [forks][tendermintfork]. However, main chain +> forks were defined more operational "forks that are observed by +> full nodes as part of normal Tendermint consensus protocol". Please +> confirm! + +#### **[TMBC-SIGN-UNIQUE.1]** + +Let *b* and *c* be light blocks, we define *sign-unique(b,c) = +true* iff + +- *b.Header.Height = c.Header.Height* and +- *sequ-rooted(b)* and +- *sequ-rooted(c)* + +implies *b = c*. + +If there exists two light blocks b and c, with *sign-unique(b,c) = +false* then we have a *fork on the chain*. + +> The following captures what I believe is called a light client fork +> in our discussions. There is no fork on the chain up to the height +> of block b. However, c is of that height, is different, and passes skipping +> verification +> Observe that a light client fork is a special case of a slashable +> fork. + +#### **[TMBC-LC-FORK.1]** + +Let *a*, *b*, *c*, be light blocks and *t* a time. We define +*light-client-fork(a,b,c,t)* iff + +- *sign-skip-match(a,b,c,t) = false* and +- *sequ-rooted(b)* and +- *b* is "unique", that is, for all *d*, *sequ-rooted(d)* and + *d.Header.Height=b.Header.Height* implies *d = b* + +> Finally, let's also define bogus blocks that have no support. +> Observe that bogus is even defined if there is a fork on the chain. +> Also, for the definition it would be sufficient to restrict *a* to +> *a.height < b.height* (which is implied by the definitions which +> unfold until *supports()*. + +#### **[TMBC-BOGUS.1]** + +Let *b* be a light block and *t* a time. We define *bogus(b,t)* iff + +- *sequ-rooted(b) = false* and +- for all *a*, *sequ-rooted(a)* implies *skip-root(a,b,t) = false* + +> Relation to [fork accountability][accountability]: F1, F2, and F3 +> (equivocation, amnesia, back to the past) can lead to a fork on the +> chain and to a light client fork. +> F4 and F5 (phantom validators, lunatic) cannot lead to a fork on the +> chain but to a light client +> fork if *t+1 < f < 2t+1*. +> F4 and F5 can also lead to bogus blocks + +### Informal Problem statement + +> We put tags to informal problem statements as there is no sequential +> specification. + +The following requirements are operational in that they describe how +things should be done, rather than what should be done. However, they +do not constitute temporal logic verification conditions. For those, +see [LCD-DIST-*] below. + +#### **[LCD-IP-STATE.1]** + +The detector works on a LightStore that contains LightBlocks in one of +the state `StateUnverified`, `StateVerified`, `StateFailed`, or +`StateTrusted`. + +#### **[LCD-IP-Q.1]** + +Whenever the light client verifier performs `VerifyToTarget` with the +primary and returns with +`(lightStore, ResultSuccess)`, the + detector should query the secondaries by calling `FetchLightBlock` for height + *LightStore.LatestVerified().Height* remotely. +Then, +the detector returns the set of all headers *h'* downloaded from +secondaries that satisfy + +- *h'* is different from *LightStore.LatestVerified()* +- *h'* is a (light) fork. + +#### **[LCD-IP-PEERSET.1]** + +Whenever the detector observes *detectable misbehavior* of a full node +from the set of Secondaries it should be replaced by a fresh full +node. (A full node that has not been primary or secondary +before). Detectable misbehavior can be + +- a timeout +- The case where *h'* is different +from *LightStore.LatestVerified()* but *h'* is not a fork, that is, if +*h'* is bogus. In other words, the +secondary cannot provide a sequence of light blocks that constitutes +proof of *h'*. + +## Assumptions/Incentives/Environment + +It is not in the interest of faulty full nodes to talk to the +detector as long as the detector is connected to at least one +correct full node. This would only increase the likelihood of +misbehavior being detected. Also we cannot punish them easily +(cheaply). The absence of a response need not be the fault of the full +node. + +Correct full nodes have the incentive to respond, because the +detector may help them to understand whether their header is a good +one. We can thus base liveness arguments of the detector on +the assumptions that correct full nodes reliably talk to the +detector. + +### Assumptions + +#### **[LCD-A-CorrFull.1]** + +At all times there is at least one correct full +node among the primary and the secondaries. + +**Remark:** Check whether [LCD-A-CorrFull.1] is not needed in the end because +the verification conditions [LCD-DIST-*] have preconditions on specific +cases where primary and/or secondaries are faulty. + +#### **[LCD-A-RelComm.1]** + +Communication between the detector and a correct full node is +reliable and bounded in time. Reliable communication means that +messages are not lost, not duplicated, and eventually delivered. There +is a (known) end-to-end delay *Delta*, such that if a message is sent +at time *t* then it is received and processed by time *t + Delta*. +This implies that we need a timeout of at least *2 Delta* for remote +procedure calls to ensure that the response of a correct peer arrives +before the timeout expires. + +## (Distributed) Problem statement + +> As the fork detector from the beginning is there to reduce the +> impact of faulty nodes, and faulty nodes imply that there is a +> distributed system, there is no sequential specification. + +The detector gets as input a lightstore *lightStore*. +Let *h-verified = lightStore.LatestVerified().Height* and + *h-trust=lightStore.LatestTrusted().Height* (see + [LCV-DATA-LIGHTSTORE]). +It queries the secondaries for headers at height *h-verified*. +The detector returns a set *PoF* of *Proof of Forks*, and should satisfy the following + temporal formulas: + +#### **[LCD-DIST-INV.1]** + +If there is no fork at height *h-verified* ([TMBC-SIGN-FORK.1]), +then the detector should return the empty set. + +> If the empty set is returned the supervisor will change the state of +> the header at height *h-verified* to *stateTrusted*. + +#### **[LCD-DIST-LIVE-FORK.1]** + +If there is a fork at height *h-verified*, and +there are two correct full nodes *i* and *j* that are + +- on different branches, and +- *i* is primary and +- *j* is secondary, + +then the detector eventually outputs the fork. + +#### **[LCD-DIST-LIVE-FORK-FAULTY.1]** + +If there is a fork at height *h-verified*, and +there is a correct secondary that is on a different branch than the +primary reported, +then the detector eventually outputs the fork. + +> The above property is quite operational ("Than the primary +> reported"), but it captures quite closely the requirement. As the +> fork detector only makes sense in a distributed setting, and does +> not have a sequential specification, less "pure" +> specification are acceptable. +> These properties capture the following operational requirement: +> +> **[LCD-REQ-REP.1]** +> If the detector observes two conflicting headers for height *h*, +> it should try to verify both. If both are verified it should report evidence. +> If the primary reports header *h* and a secondary reports header *h'*, +> and if *h'* can be verified based on common root of trust, then +> evidence should be generated; +> By verifying we mean calling `VerifyToTarget` from the +> [[verification]] specification. + +## Definitions + +- A fixed set of full nodes is provided in the configuration upon + initialization. Initially this set is partitioned into + - one full node that is the *primary* (singleton set), + - a set *Secondaries* (of fixed size, e.g., 3), + - a set *FullNodes*. +- A set *FaultyNodes* of nodes that the light client suspects of being faulty; it is initially empty + +- *Lightstore* as defined in the [verification specification][verification]. + +#### **[LCD-INV-NODES.1]:** + +The detector shall maintain the following invariants: + +- *FullNodes \intersect Secondaries = {}* +- *FullNodes \intersect FaultyNodes = {}* +- *Secondaries \intersect FaultyNodes = {}* + +and the following transition invariant + +- *FullNodes' \union Secondaries' \union FaultyNodes' = FullNodes \union Secondaries \union FaultyNodes* + +> The following invariant is very useful for reasoning, and underlies +> many intuition when we + +#### **[LCD-INV-TRUSTED-AGREED.1]:** + +It is always the case the light client has downloaded a lightblock for height +*lightStore.LatestTrusted().Height* +from each of the current primary and the secondary, that all reported +the identical lightblock for that height. + +> In the above, I guess "the identical" might be replaced with "a +> matching" to cover commits that might be different. +> The above requires us that before we pick a new secondary, we have to +> query the secondary for the header of height +> *lightStore.LatestTrusted().Height*. + +## Solution + +### Data Structures + +Lightblocks and LightStores are +defined at [LCV-DATA-LIGHTBLOCK.1] and [LCV-DATA-LIGHTSTORE.1]. See the [verification specification][verification] for details. + +> The following data structure [LCV-DATA-POF.1] +> defines a **proof of fork**. Following +> [TMBC-SIGN-FORK.1], we require two blocks *b* and *c* for the same +> height that can both be verified from a common root block *a* (using +> the skipping or the sequential method). +> [LCV-DATA-POF.1] mirrors the definition [TMBC-SIGN-FORK.1]: +> *TrustedBlock* corresponds to *a*, and *PrimaryTrace* and *SecondaryTrace* +> are traces to two blocks *b* and *c*. The traces establish that both +> *skip-root(a,b,t)* and *skip-root(a,c,t)* are satisfied. + +#### **[LCV-DATA-POF.1]** + +```go +type LightNodeProofOfFork struct { + TrustedBlock LightBlock + PrimaryTrace []LightBlock + SecondaryTrace []LightBlock +} +``` + + + + + + + + + +#### **[LCV-DATA-POFSTORE.1]** + +Proofs of Forks are stored in a structure which stores all proofs +generated during detection. + +```go +type PoFStore struct { + ... +} +``` + +In additions to the functions defined in +the [verification specification][verification], the +LightStore exposes the following function + +#### **[LCD-FUNC-SUBTRACE.1]:** + +```go +func (ls LightStore) Subtrace(from int, to int) LightStore +``` + +- Expected postcondition + - returns a lightstore that contains all lightblocks *b* from *ls* + that satisfy: *from < b.Header.Height <= to* + +---- + +### Inter Process Communication + +```go +func FetchLightBlock(peer PeerID, height Height) LightBlock +``` + +See the [verification specification][verification] for details. + +#### **[LCD-FUNC-SUBMIT.1]:** + +```go +func SubmitProofOfFork(pof LightNodeProofOfFork) Result +``` + +**TODO:** finalize what this should do, and what detail of + specification we need. + +- Implementation remark +- Expected precondition + - none +- Expected postcondition + - submit evidence to primary and the secondary in *pof*, that is, + to + - `pof.PrimaryTrace[1].Provider` + - `pof.SecondaryTrace[1].Provider` + - **QUESTION** minimize data? We could submit to the primary only + the trace of the secondary, and vice versa. Do we need to spell + that out here? (Also, by [LCD-INV-TRUSTED-AGREED.1], we do not + need to send `pof.TrustedBlock`) + - **FUTURE WORK:** we might send *pof* to primary or all + secondaries or broadcast to all full nodes. However, in evidence + detection this might need that a full node has to check a *pof* + where both traces are not theirs. This leads to more complicated + logic at the full node, which we do not need right now. + +- Error condition + - none + +### Auxiliary Functions (Local) + +#### **[LCD-FUNC-CROSS-CHECK.1]:** + +```go +func CrossCheck(peer PeerID, testedLB LightBlock) (result) { + sh := FetchLightBlock(peer, testedLB.Height); + // as the check below only needs the header, it is sufficient + // to download the header rather than the LighBlock + if testedLB.Header == sh.Header { + return OK + } + else { + return DoesNotMatch + } +} +``` + +- Implementation remark + - download block and compare to previously downloaded one. +- Expected precondition +- Expected postcondition +- Error condition + +#### **[LCD-FUNC-REPLACE-PRIMARY.1]:** + +```go +Replace_Primary() +``` + +**TODO:** formalize conditions + +- Implementation remark + - the primary is replaced by a secondary, and lightblocks above + trusted blocks are removed + - to maintain a constant size of secondaries, at this point we + might need to + - pick a new secondary *nsec* + - maintain [LCD-INV-TRUSTED-AGREED.1], that is, + - call `CrossCheck(nsec,lightStore.LatestTrusted()`. + If it matches we are OK, otherwise + - we repeat with another full node as new + secondary candidate + - **FUTURE:** try to do fork detection from some possibly old + lightblock in store. (Might be the approach for the + light node that assumes to be connected to correct + full nodes only from time to time) + +- Expected precondition + - *FullNodes* is nonempty + +- Expected postcondition + - *primary* is moved to *FaultyNodes* + - all lightblocks with height greater than + lightStore.LatestTrusted().Height are removed from *lightStore*. + - a secondary *s* is moved from *Secondaries* to primary + +> this ensures that *s* agrees on the Last Trusted State + +- Error condition + - if precondition is violated + +#### **[LCD-FUNC-REPLACE-SECONDARY.1]:** + +```go +Replace_Secondary(addr Address) +``` + +**TODO:** formalize conditions + +- Implementation remark + - maintain [LCD-INV-TRUSTED-AGREED.1], that is, + - call `CrossCheck(nsec,lightStore.LatestTrusted()`. + If it matches we are OK, otherwise + - we might just repeat with another full node as new secondary + - **FUTURE:** try to do fork detection from some possibly old + lightblock in store. (Might be the approach for the + light node that assumes to be connected to correct + full nodes only from time to time) + +- Expected precondition + - *FullNodes* is nonempty +- Expected postcondition + - addr is moved from *Secondaries* to *FaultyNodes* + - an address *a* is moved from *FullNodes* to *Secondaries* +- Error condition + - if precondition is violated + +### From the verifier + +```go +func VerifyToTarget(primary PeerID, lightStore LightStore, + targetHeight Height) (LightStore, Result) +``` + +See the [verification specification][verification] for details. + +## Protocol + +### Shared data of the light client + +- a pool of full nodes *FullNodes* that have not been contacted before +- peer set called *Secondaries* +- primary +- lightStore + +### Outline + +The problem laid out is solved by calling the function `ForkDetector` + with a lightstore that contains a light block that has just been + verified by the verifier. + +- **TODO:** We should clarify what is the expectation of VerifyToTarget so if it + returns TimeoutError it can be assumed faulty. I guess that + VerifyToTarget with correct full node should never terminate with + TimeoutError. + +- **TODO:** clarify EXPIRED case. Can we always punish? Can we give sufficient + conditions. + +### Fork Detector + +#### **[LCD-FUNC-DETECTOR.1]:** + +```go +func ForkDetector(ls LightStore, PoFs PoFStore) +{ + testedLB := LightStore.LatestVerified() + for i, secondary range Secondaries { + if OK = CrossCheck(secondary, testedLB) { + // header matches. we do nothing. + } + else { + // [LCD-REQ-REP] + // header does not match. there is a situation. + // we try to verify sh by querying s + // we set up an auxiliary lightstore with the highest + // trusted lightblock and the lightblock we want to verify + auxLS.Init + auxLS.Update(LightStore.LatestTrusted(), StateVerified); + auxLS.Update(sh,StateUnverified); + LS,result := VerifyToTarget(secondary, auxLS, sh.Header.Height) + if (result = ResultSuccess || result = EXPIRED) { + // we verified header sh which is conflicting to hd + // there is a fork on the main blockchain. + // If return code was EXPIRED it might be too late + // to punish, we still report it. + pof = new LightNodeProofOfFork; + pof.TrustedBlock := LightStore.LatestTrusted() + pof.PrimaryTrace := + LightStore.Subtrace(LightStore.LatestTrusted().Height, + testedLB.Height); + pof.SecondaryTrace := + auxLS.Subtrace(LightStore.LatestTrusted().Height, + testedLB.Height); + PoFs.Add(pof); + } + else { + // secondary might be faulty or unreachable + // it might fail to provide a trace that supports sh + // or time out + Replace_Secondary(secondary) + } + } + } + return PoFs +} +``` + +**TODO:** formalize conditions + +- Expected precondition + - Secondaries initialized and non-empty + - `PoFs` initialized and empty + - *lightStore.LatestTrusted().Height < lightStore.LatestVerified().Height* +- Expected postcondition + - satisfies [LCD-DIST-INV.1], [LCD-DIST-LIFE-FORK.1] + - removes faulty secondary if it reports wrong header + - **TODO** submit proof of fork +- Error condition + - fails if precondition is violated + - fails if [LCV-INV-TP] is violated (no trusted header within + trusting period + +---- + +## Correctness arguments + +#### Argument for [LCD-DIST-INV] + +**TODO** + +#### Argument for [LCD-DIST-LIFE-FORK] + +**TODO** + +# References + +> links to other specifications/ADRs this document refers to + +[[verification]] The specification of the light client verification. + +[[tendermintfork]] Tendermint fork detection and accountability + +[[accountability]] Fork accountability + +[TMBC-FM-2THIRDS-linkVDD]: https://github.com/informalsystems/VDD/tree/master/blockchain/blockchain.md#**[TMBC-FM-2THIRDS-link]**: + +[TMBC-FM-2THIRDS-link]: https://github.com/tendermint/spec/blob/master/spec/consensus/light-client/verification.md + +[block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md + +[blockchain]: https://github.com/informalsystems/VDD/tree/master/blockchain/blockchain.md + +[lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md + +[verificationVDD]: https://github.com/informalsystems/VDD/blob/master/lightclient/failuredetector.md + +[verification]: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification/verification.md + +[accountability]: https://github.com/tendermint/spec/blob/master/spec/consensus/light-client/accountability.md + +[tendermintfork]: https://docs.google.com/document/d/1xjyp5JOPt7QfHem1AFEaowBH2Plk0IHACWtYFXFvO7E/edit#heading=h.th2369ptc2ve diff --git a/rust-spec/lightclient/detection/discussions.md b/rust-spec/lightclient/detection/discussions.md new file mode 100644 index 000000000..82702dd69 --- /dev/null +++ b/rust-spec/lightclient/detection/discussions.md @@ -0,0 +1,178 @@ +# Results of Discussions and Decisions + +- Generating a minimal proof of fork (as suggested in [Issue #5083](https://github.com/tendermint/tendermint/issues/5083)) is too costly at the light client + - we do not know all lightblocks from the primary + - therefore there are many scenarios. we might even need to ask + the primary again for additional lightblocks to isolate the + branch. + +> For instance, the light node starts with block at height 1 and the +> primary provides a block of height 10 that the light node can +> verify immediately. In cross-checking, a secondary now provides a +> conflicting header b10 of height 10 that needs another header b5 +> of height 5 to +> verify. Now, in order for the light node to convince the primary: +> +> - The light node cannot just sent b5, as it is not clear whether +> the fork happened before or after 5 +> - The light node cannot just send b10, as the primary would also +> need b5 for verification +> - In order to minimize the evidence, the light node may try to +> figure out where the branch happens, e.g., by asking the primary +> for height 5 (it might be that more queries are required, also +> to the secondary. However, assuming that in this scenario the +> primary is faulty it may not respond. + + As the main goal is to catch misbehavior of the primary, + evidence generation and punishment must not depend on their + cooperation. So the moment we have proof of fork (even if it + contains several light blocks) we should submit right away. + +- decision: "full" proof of fork consists of two traces that originate in the + same lightblock and lead to conflicting headers of the same height. + +- For submission of proof of fork, we may do some optimizations, for + instance, we might just submit a trace of lightblocks that verifies a block + different from the one the full node knows (we do not send the trace + the primary gave us back to the primary) + +- The light client attack is via the primary. Thus we try to + catch if the primary installs a bad light block + - We do not check secondary against secondary + - For each secondary, we check the primary against one secondary + +- Observe that just two blocks for the same height are not +sufficient proof of fork. +One of the blocks may be bogus [TMBC-BOGUS.1] which does +not constitute slashable behavior. +Which leads to the question whether the light node should try to do +fork detection on its initial block (from subjective +initialization). This could be done by doing backwards verification +(with the hashes) until a bifurcation block is found. +While there are scenarios where a +fork could be found, there is also the scenario where a faulty full +node feeds the light node with bogus light blocks and forces the light +node to check hashes until a bogus chain is out of the trusting period. +As a result, the light client +should not try to detect a fork for its initial header. **The initial +header must be trusted as is.** + +# Light Client Sequential Supervisor + +**TODO:** decide where (into which specification) to put the +following: + +We describe the context on which the fork detector is called by giving +a sequential version of the supervisor function. +Roughly, it alternates two phases namely: + +- Light Client Verification. As a result, a header of the required + height has been downloaded from and verified with the primary. +- Light Client Fork Detections. As a result the header has been + cross-checked with the secondaries. In case there is a fork we + submit "proof of fork" and exit. + +#### **[LC-FUNC-SUPERVISOR.1]:** + +```go +func Sequential-Supervisor () (Error) { + loop { + // get the next height + nextHeight := input(); + + // Verify + result := NoResult; + while result != ResultSuccess { + lightStore,result := VerifyToTarget(primary, lightStore, nextHeight); + if result == ResultFailure { + // pick new primary (promote a secondary to primary) + /// and delete all lightblocks above + // LastTrusted (they have not been cross-checked) + Replace_Primary(); + } + } + + // Cross-check + PoFs := Forkdetector(lightStore, PoFs); + if PoFs.Empty { + // no fork detected with secondaries, we trust the new + // lightblock + LightStore.Update(testedLB, StateTrusted); + } + else { + // there is a fork, we submit the proofs and exit + for i, p range PoFs { + SubmitProofOfFork(p); + } + return(ErrorFork); + } + } +} +``` + +**TODO:** finish conditions + +- Implementation remark +- Expected precondition + - *lightStore* initialized with trusted header + - *PoFs* empty +- Expected postcondition + - runs forever, or + - is terminated by user and satisfies LightStore invariant, or **TODO** + - has submitted proof of fork upon detecting a fork +- Error condition + - none + +---- + +# Semantics of the LightStore + +Currently, a lightblock in the lightstore can be in one of the +following states: + +- StateUnverified +- StateVerified +- StateFailed +- StateTrusted + +The intuition is that `StateVerified` captures that the lightblock has +been verified with the primary, and `StateTrusted` is the state after +successful cross-checking with the secondaries. + +Assuming there is **always one correct node among primary and +secondaries**, and there is no fork on the blockchain, lightblocks that +are in `StateTrusted` can be used by the user with the guarantee of +"finality". If a block in `StateVerified` is used, it might be that +detection later finds a fork, and a roll-back might be needed. + +**Remark:** The assumption of one correct node, does not render +verification useless. It is true that if the primary and the +secondaries return the same block we may trust it. However, if there +is a node that provides a different block, the light node still needs +verification to understand whether there is a fork, or whether the +different block is just bogus (without any support of some previous +validator set). + +**Remark:** A light node may choose the full nodes it communicates +with (the light node and the full node might even belong to the same +stakeholder) so the assumption might be justified in some cases. + +In the future, we will do the following changes + +- we assume that only from time to time, the light node is + connected to a correct full node +- this means for some limited time, the light node might have no + means to defend against light client attacks +- as a result we do not have finality +- once the light node reconnects with a correct full node, it + should detect the light client attack and submit evidence. + +Under these assumptions, `StateTrusted` loses its meaning. As a +result, it should be removed from the API. We suggest that we replace +it with a flag "trusted" that can be used + +- internally for efficiency reasons (to maintain + [LCD-INV-TRUSTED-AGREED.1] until a fork is detected) +- by light client based on the "one correct full node" assumption + +---- diff --git a/rust-spec/lightclient/detection/draft-functions.md b/rust-spec/lightclient/detection/draft-functions.md new file mode 100644 index 000000000..c56594a53 --- /dev/null +++ b/rust-spec/lightclient/detection/draft-functions.md @@ -0,0 +1,289 @@ +# Draft of Functions for Fork detection and Proof of Fork Submisstion + +This document collects drafts of function for generating and +submitting proof of fork in the IBC context + +- [IBC](#on---chain-ibc-component) + +- [Relayer](#relayer) + +## On-chain IBC Component + +> The following is a suggestions to change the function defined in ICS 007 + +#### [TAG-IBC-MISBEHAVIOR.1] + +```go +func checkMisbehaviourAndUpdateState(cs: ClientState, PoF: LightNodeProofOfFork) +``` + +**TODO:** finish conditions + +- Implementation remark +- Expected precondition + - PoF.TrustedBlock.Header is equal to lightBlock on store with + same height + - both traces end with header of same height + - headers are different + - both traces are supported by PoF.TrustedBlock (`supports` + defined in [TMBC-FUNC]), that is, for `t = currentTimestamp()` (see + ICS 024) + - supports(PoF.TrustedBlock, PoF.PrimaryTrace[1], t) + - supports(PoF.PrimaryTrace[i], PoF.PrimaryTrace[i+1], t) for + *0 < i < length(PoF.PrimaryTrace)* + - supports(PoF.TrustedBlock, PoF.SecondaryTrace[1], t) + - supports(PoF.SecondaryTrace[i], PoF.SecondaryTrace[i+1], t) for + *0 < i < length(PoF.SecondaryTrace)* +- Expected postcondition + - set cs.FrozenHeight to min(cs.FrozenHeight, PoF.TrustedBlock.Header.Height) +- Error condition + - none + +---- + +> The following is a suggestions to add functionality to ICS 002 and 007. +> I suppose the above is the most efficient way to get the required +> information. Another option is to subscribe to "header install" +> events via CosmosSDK + +#### [TAG-IBC-HEIGHTS.1] + +```go +func QueryHeightsRange(id, from, to) ([]Height) +``` + +- Expected postcondition + - returns all heights *h*, with *from <= h <= to* for which the + IBC component has a consensus state. + +---- + +> This function can be used if the relayer has no information about +> the IBC component. This allows late-joining relayers to also +> participate in fork dection and the generation in proof of +> fork. Alternatively, we may also postulate that relayers are not +> responsible to detect forks for heights before they started (and +> subscribed to the transactions reporting fresh headers being +> installed at the IBC component). + +## Relayer + +### Auxiliary Functions to be implemented in the Light Client + +#### [LCV-LS-FUNC-GET-PREV.1] + +```go +func (ls LightStore) GetPreviousVerified(height Height) (LightBlock, bool) +``` + +- Expected postcondition + - returns a verified LightBlock, whose height is maximal among all + verified lightblocks with height smaller than `height` + +---- + +### Relayer Submitting Proof of Fork to the IBC Component + +There are two ways the relayer can detect a fork + +- by the fork detector of one of its lightclients +- be checking the consensus state of the IBC component + +The following function ignores how the proof of fork was generated. +It takes a proof of fork as input and computes a proof of fork that + will be accepted by the IBC component. +The problem addressed here is that both, the relayer's light client + and the IBC component have incomplete light stores, that might + not have all light blocks in common. +Hence the relayer has to figure out what the IBC component knows + (intuitively, a meeting point between the two lightstores + computed in `commonRoot`) and compute a proof of fork + (`extendPoF`) that the IBC component will accept based on its + knowledge. + +The auxiliary functions `commonRoot` and `extendPoF` are +defined below. + +#### [TAG-SUBMIT-POF-IBC.1] + +```go +func SubmitIBCProofOfFork( + lightStore LightStore, + PoF: LightNodeProofOfFork, + ibc IBCComponent) (Error) { + if ibc.queryChainConsensusState(PoF.TrustedBlock.Height) = PoF.TrustedBlock { + // IBC component has root of PoF on store, we can just submit + ibc.submitMisbehaviourToClient(ibc.id,PoF) + return Success + // note sure about the id parameter + } + else { + // the ibc component does not have the TrustedBlock and might + // even be on yet a different branch. We have to compute a PoF + // that the ibc component can verifiy based on its current + // knowledge + + ibcLightBlock, lblock, _, result := commonRoot(lightStore, ibc, PoF.TrustedBlock) + + if result = Success { + newPoF = extendPoF(ibcLightBlock, lblock, lightStore, PoF) + ibc.submitMisbehaviourToClient(ibc.id, newPoF) + return Success + } + else{ + return CouldNotGeneratePoF + } + } +} +``` + +**TODO:** finish conditions + +- Implementation remark +- Expected precondition +- Expected postcondition +- Error condition + - none + +---- + +### Auxiliary Functions at the Relayer + +> If the relayer detects a fork, it has to compute a proof of fork that +> will convince the IBC component. That is it has to compare the +> relayer's local lightstore against the lightstore of the IBC +> component, and find common ancestor lightblocks. + +#### [TAG-COMMON-ROOT.1] + +```go +func commonRoot(lightStore LightStore, ibc IBCComponent, lblock +LightBlock) (LightBlock, LightBlock, LightStore, Result) { + + auxLS.Init + + // first we ask for the heights the ibc component is aware of + ibcHeights = ibc.QueryHeightsRange( + ibc.id, + lightStore.LowestVerified().Height, + lblock.Height - 1); + // this function does not exist yet. Alternatively, we may + // request all transactions that installed headers via CosmosSDK + + + for { + h, result = max(ibcHeights) + if result = Empty { + return (_, _, _, NoRoot) + } + ibcLightBlock = ibc.queryChainConsensusState(h) + auxLS.Update(ibcLightBlock, StateVerified); + connector, result := Connector(lightStore, ibcLightBlock, lblock.Header.Height) + if result = success { + return (ibcLightBlock, connector, auxLS, Success) + } + else{ + ibcHeights.remove(h) + } + } +} +``` + +- Expected postcondition + - returns + - a lightBlock b1 from the IBC component, and + - a lightBlock b2 + from the local lightStore with height less than + lblock.Header.Hight, s.t. b1 supports b2, and + - a lightstore with the blocks downloaded from + the ibc component + +---- + +#### [TAG-LS-FUNC-CONNECT.1] + +```go +func Connector (lightStore LightStore, lb LightBlock, h Height) (LightBlock, bool) +``` + +- Expected postcondition + - returns a verified LightBlock from lightStore with height less + than *h* that can be + verified by lb in one step. + +**TODO:** for the above to work we need an invariant that all verified +lightblocks form a chain of trust. Otherwise, we need a lightblock +that has a chain of trust to height. + +> Once the common root is found, a proof of fork that will be accepted +> by the IBC component needs to be generated. This is done in the +> following function. + +#### [TAG-EXTEND-POF.1] + +```go +func extendPoF (root LightBlock, + connector LightBlock, + lightStore LightStore, + Pof LightNodeProofofFork) (LightNodeProofofFork} +``` + +- Implementation remark + - PoF is not sufficient to convince an IBC component, so we extend + the proof of fork farther in the past +- Expected postcondition + - returns a newPOF: + - newPoF.TrustedBlock = root + - let prefix = + connector + + lightStore.Subtrace(connector.Header.Height, PoF.TrustedBlock.Header.Height-1) + + PoF.TrustedBlock + - newPoF.PrimaryTrace = prefix + PoF.PrimaryTrace + - newPoF.SecondaryTrace = prefix + PoF.SecondaryTrace + +### Detection a fork at the IBC component + +The following functions is assumed to be called regularly to check +that latest consensus state of the IBC component. Alternatively, this +logic can be executed whenever the relayer is informed (via an event) +that a new header has been installed. + +#### [TAG-HANDLER-DETECT-FORK.1] + +```go +func DetectIBCFork(ibc IBCComponent, lightStore LightStore) (LightNodeProofOfFork, Error) { + cs = ibc.queryClientState(ibc); + lb, found := lightStore.Get(cs.Header.Height) + if !found { + **TODO:** need verify to target + lb, result = LightClient.Main(primary, lightStore, cs.Header.Height) + // [LCV-FUNC-IBCMAIN.1] + **TODO** decide what to do following the outcome of Issue #499 + + // I guess here we have to get into the light client + + } + if cs != lb { + // IBC component disagrees with my primary. + // I fetch the + ibcLightBlock, lblock, ibcStore, result := commonRoot(lightStore, ibc, lb) + pof = new LightNodeProofOfFork; + pof.TrustedBlock := ibcLightBlock + pof.PrimaryTrace := ibcStore + cs + pof.SecondaryTrace := lightStore.Subtrace(lblock.Header.Height, + lb.Header.Height); + return(pof, Fork) + } + return(nil , NoFork) +} +``` + +**TODO:** finish conditions + +- Implementation remark + - we ask the handler for the lastest check. Cross-check with the + chain. In case they deviate we generate PoF. + - we assume IBC component is correct. It has verified the + consensus state +- Expected precondition +- Expected postcondition diff --git a/rust-spec/lightclient/detection/req-ibc-detection.md b/rust-spec/lightclient/detection/req-ibc-detection.md new file mode 100644 index 000000000..439ca26b6 --- /dev/null +++ b/rust-spec/lightclient/detection/req-ibc-detection.md @@ -0,0 +1,345 @@ +# Requirements for Fork Detection in the IBC Context + +## What you need to know about IBC + +In the following, I distilled what I considered relevant from + + + +### Components and their interface + +#### Tendermint Blockchains + +> I assume you know what that is. + +#### An IBC/Tendermint correspondence + +| IBC Term | Tendermint-RS Spec Term | Comment | +|----------|-------------------------| --------| +| `CommitmentRoot` | AppState | app hash | +| `ConsensusState` | Lightblock | not all fields are there. NextValidator is definitly needed | +| `ClientState` | latest light block + configuration parameters (e.g., trusting period + `frozenHeight` | NextValidators missing; what is `proofSpecs`?| +| `frozenHeight` | height of fork | set when a fork is detected | +| "would-have-been-fooled" | light node fork detection | light node may submit proof of fork to IBC component to halt it | +| `Height` | (no epochs) | (epoch,height) pair in lexicographical order (`compare`) | +| `Header` | ~signed header | validatorSet explicit (no hash); nextValidators missing | +| `Evidence` | t.b.d. | definition unclear "which the light client would have considered valid". Data structure will need to change | +| `verify` | `ValidAndVerified` | signature does not match perfectly (ClientState vs. LightBlock) + in `checkMisbehaviourAndUpdateState` it is unclear whether it uses traces or goes to h1 and h2 in one step | + +#### Some IBC links + +- [QueryConsensusState](https://github.com/cosmos/cosmos-sdk/blob/2651427ab4c6ea9f81d26afa0211757fc76cf747/x/ibc/02-client/client/utils/utils.go#L68) + +#### Required Changes in ICS 007 + +- `assert(height > 0)` in definition of `initialise` doesn't match + definition of `Height` as *(epoch,height)* pair. + +- `initialise` needs to be updated to new data structures + +- `clientState.frozenHeight` semantics seem not totally consistent in + document. E.g., `min` needs to be defined over optional value in + `checkMisbehaviourAndUpdateState`. Also, if you are frozen, why do + you accept more evidence. + +- `checkValidityAndUpdateState` + - `verify`: it needs to be clarified that checkValidityAndUpdateState + does not perform "bisection" (as currently hinted in the text) but + performs a single step of "skipping verification", called, + `ValidAndVerified` + - `assert (header.height > clientState.latestHeight)`: no old + headers can be installed. This might be OK, but we need to check + interplay with misbehavior + - clienstState needs to be updated according to complete data + structure + +- `checkMisbehaviourAndUpdateState`: as evidence will contain a trace + (or two), the assertion that uses verify will need to change. + +- ICS 002 states w.r.t. `queryChainConsensusState` that "Note that + retrieval of past consensus states by height (as opposed to just the + current consensus state) is convenient but not required." For + Tendermint fork detection, this seems to be a necessity. + +- `Header` should become a lightblock + +- `Evidence` should become `LightNodeProofOfFork` [LCV-DATA-POF.1] + +- `upgradeClientState` what is the semantics (in particular what is + `height` doing?). + +- `checkMisbehaviourAndUpdateState(cs: ClientState, PoF: + LightNodeProofOfFork)` needs to be adapted + +#### Handler + +A blockchain runs a **handler** that passively collects information about + other blockchains. It can be thought of a state machine that takes + input events. + +- the state includes a lightstore (I guess called `ConsensusState` + in IBC) + +- The following function is used to pass a header to a handler + +```go +type checkValidityAndUpdateState = (Header) => Void +``` + + For Tendermint, it will perform + `ValidandVerified`, that is, it does the trusting period check and the + +1/3 check (+2/3 for sequential headers). + If it verifies a header, it adds it to its lightstore, + if it does not pass verification it drops it. + Right now it only accepts a header more recent then the latest + header, + and drops older + ones or ones that could not be verified. + +> The above paragraph captures what I believe what is the current + logic of `checkValidityAndUpdateState`. It may be subject to + change. E.g., maintain a lightstore with state (unverified, verified) + +- The following function is used to pass "evidence" (this we + will need to make precise eventually) to a handler + +```go +type checkMisbehaviourAndUpdateState = (bytes) => Void +``` + + We have to design this, and the data that the handler can use to + check that there was some misbehavior (fork) in order react on + it, e.g., flagging a situation and + stop the protocol. + +- The following function is used to query the light store (`ConsensusState`) + +```go +type queryChainConsensusState = (height: uint64) => ConsensusState +``` + +#### Relayer + +- The active components are called **relayer**. + +- a relayer contains light clients to two (or more?) blockchains + +- the relayer send headers and data to the handler to invoke + `checkValidityAndUpdateState` and + `checkMisbehaviourAndUpdateState`. It may also query + `queryChainConsensusState`. + +- multiple relayers may talk to one handler. Some relayers might be + faulty. We assume existence of at least single correct relayer. + +## Informal Problem Statement: Fork detection in IBC + +### Relayer requirement: Evidence for Handler + +- The relayer should provide the handler with + "evidence" that there was a fork. + +- The relayer can read the handler's consensus state. Thus the relayer can + feed the handler precisely the information the handler needs to detect a + fork. + What is this + information needs to be specified. + +- The information depends on the verification the handler does. It + might be necessary to provide a bisection proof (list of + lightblocks) so that the handler can verify based on its local + lightstore a header *h* that is conflicting with a header *h'* in the + local lightstore, that is, *h != h'* and *h.Height = h'.Height* + +### Relayer requirement: Fork detection + +Let's assume there is a fork at chain A. There are two ways the +relayer can figure that out: + +1. as the relayer contains a light client for A, it also includes a fork + detector that can detect a fork. + +2. the relayer may also detect a fork by observing that the + handler for chain A (on chain B) + is on a different branch than the relayer + +- in both detection scenarios, the relayer should submit evidence to + full nodes of chain A where there is a fork. As we assume a fullnode + has a complete list of blocks, it is sufficient to send "Bucky's + evidence" (), + that is, + - two lightblocks from different branches + + - a lightblock (perhaps just a height) from which both blocks + can be verified. + +- in the scenario 2., the relayer must feed the A-handler (on chain B) + a proof of a fork on A so that chain B can react accordingly + +### Handler requirement + +- there are potentially many relayers, some correct some faulty + +- a handler cannot trust the information provided by the relayer, + but must verify + (Доверя́й, но проверя́й) + +- in case of a fork, we accept that the handler temporarily stores + headers (tagged as verified). + +- eventually, a handler should be informed + (`checkMisbehaviourAndUpdateState`) + by some relayer that it has + verified a header from a fork. Then the handler should do what is + required by IBC in this case (stop?) + +### Challenges in the handler requirement + +- handlers and relayers work on different lightstores. In principle + the lightstore need not intersect in any heights a priori + +- if a relayer sees a header *h* it doesn't know at a handler (`queryChainConsensusState`), the + relayer needs to + verify that header. If it cannot do it locally based on downloaded + and verified (trusted?) light blocks, it might need to use + `VerifyToTarget` (bisection). To call `VerifyToTarget` we might keep + *h* in the lightstore. If verification fails, we need to download the + "alternative" header of height *h.Height* to generate evidence for + the handler. + +- we have to specify what precisely `queryChainConsensusState` + returns. It cannot be the complete lightstore. Is the last header enough? + +- we would like to assume that every now and then (smaller than the + trusting period) a correct relayer checks whether the handler is on a + different branch than the relayer. + And we would like that this is enough to achieve + the Handler requirement. + + - here the correctness argument would be easy if a correct relayer is + based on a light client with a *trusted* state, that is, a light + client who never changes its opinion about trusted. Then if such a + correct relayer checks-in with a handler, it will detect a fork, and + act in time. + + - if the light client does not provide this interface, in the case of + a fork, we need some assumption about a correct relayer being on a + different branch than the handler, and we need such a relayer to + check-in not too late. Also + what happens if the relayer's light client is forced to roll-back + its lightstore? + Does it have to re-check all handlers? + +## On the interconnectedness of things + +In the broader discussion of so-called "fork accountability" there are +several subproblems + +- Fork detection + +- Evidence creation and submission + +- Isolating misbehaving nodes (and report them for punishment over abci) + +### Fork detection + +The preliminary specification ./detection.md formalizes the notion of +a fork. Roughly, a fork exists if there are two conflicting headers +for the same height, where both are supported by bonded full nodes +(that have been validators in the near past, that is, within the +trusting period). We distinguish between *fork on the chain* where two +conflicting blocks are signed by +2/3 of the validators of that +height, and a *light client fork* where one of the conflicting headers +is not signed by +2/3 of the current height, but by +1/3 of the +validators of some smaller height. + +In principle everyone can detect a fork + +- ./detection talks about the Tendermint light client with a focus on + light nodes. A relayer runs such light clients and may detect + forks in this way + +- in IBC, a relayer can see that a handler is on a conflicting branch + - the relayer should feed the handler the necessary information so + that it can halt + - the relayer should report the fork to a full node + +### Evidence creation and submission + +- the information sent from the relayer to the handler could be called + evidence, but this is perhaps a bad idea because the information sent to a + full node can also be called evidence. But this evidence might still + not be enough as the full node might need to run the "fork + accountability" protocol to generate evidence in the form of + consensus messages. So perhaps we should + introduce different terms for: + + - proof of fork for the handler (basically consisting of lightblocks) + - proof of fork for a full node (basically consisting of (fewer) lightblocks) + - proof of misbehavior (consensus messages) + +### Isolating misbehaving nodes + +- this is the job of a full node. + +- might be subjective in the future: the protocol depends on what the + full node believes is the "correct" chain. Right now we postulate + that every full node is on the correct chain, that is, there is no + fork on the chain. + +- The full node figures out which nodes are + - lunatic + - double signing + - amnesic; **using the challenge response protocol** + +- We do not punish "phantom" validators + - currently we understand a phantom validator as a node that + - signs a block for a height in which it is not in the + validator set + - the node is not part of the +1/3 of previous validators that + are used to support the header. Whether we call a validator + phantom might be subjective and depend on the header we + check against. Their formalization actually seems not so + clear. + - they can only do something if there are +1/3 faulty validators + that are either lunatic, double signing, or amnesic. + - abci requires that we only report bonded validators. So if a + node is a "phantom", we would need the check whether the node is + bonded, which currently is expensive, as it requires checking + blocks from the last three weeks. + - in the future, with state sync, a correct node might be + convinced by faulty nodes that it is in the validator set. Then + it might appear to be "phantom" although it behaves correctly + +## Next steps + +> The following points are subject to my limited knowledge of the +> state of the work on IBC. Some/most of it might already exist and we +> will just need to bring everything together. + +- "proof of fork for a full node" defines a clean interface between + fork detection and misbehavior isolation. So it should be produced + by protocols (light client, the relayer). So we should fix that + first. + +- Given the problems of not having a light client architecture spec, + for the relayer we should start with this. E.g. + + - the relayer runs light clients for two chains + - the relayer regularly queries consensus state of a handler + - the relayer needs to check the consensus state + - this involves local checks + - this involves calling the light client + - the relayer uses the light client to do IBC business (channels, + packets, connections, etc.) + - the relayer submits proof of fork to handlers and full nodes + +> the list is definitely not complete. I think part of this +> (perhaps all) is +> covered by what Anca presented recently. + +We will need to define what we expect from these components + +- for the parts where the relayer talks to the handler, we need to fix + the interface, and what the handler does + +- we write specs for these components. diff --git a/rust-spec/lightclient/experiments.png b/rust-spec/lightclient/experiments.png new file mode 100644 index 0000000000000000000000000000000000000000..94166ffa31ee93970b8b97cafe375ba580c1d319 GIT binary patch literal 83681 zcmZ_01yo!;xA+Z(A}vs~#a#;&m*Nz6C`AUhf#T5OZpCfzfg%rHoWb3S4FeQ+cZb3K zo4)V8_x;wo_Ya(v%pqAPC&}JB+4=2>P*;`1ent8U2?+^XL0Abfrsl#VO1|B?26l{sdv*7vXe@X;BBG*6cqemjPRqzQ2flQ zC{g>}PZFqM=_MNxM8}!`nMmY3;nIaL8Y>!$m{?*BN8|A$E_qh8nH8=XMgVRGU03I7 zM^a$m)|*eT{M10xKpYg5=Pw~?=`<+80b(dU?H>mVWPs}C#NcQWVvIB7@5YLLFJJt# zgy=atpss?YiVD(uL>>bP6`2(2B_fB6xWtgj{wFVs%#4Kculp~Mkix8yQ2(opDkA;+ zlY+SZ*7F~9`GFr=^g&x3)w1r95J90ND9)D zUp$ZxGhepS_n!5Wxx0&#90?w8xIOT@C5s#Erj-F5!{zDdP+$t2f_=Y&d*{C^}~$S-=XUr=Vs{2%}O zuL^|7Iu;(1|Bw3QfkwdrtlVBI+8^^`1L#&U1Yi8`Bod1Q<$vG(chNt#xK1*%m4olC zCjVb;Gytsu|KBfw{i0%Emk+QNE%bjp`R_9%;@)$M-5=JR-fYCBZg)RFU3Z+WM{$H+ zFMC%`+WWhlW0K6I|%NT_gzk?iI*p3WAo_sOO;NjGrfP_#Bh22!l+~Pa519x zmeruwFT|PTa*{D>bF*jdvKx~3b~mf;XvJa*f02OYvfRcSYXvS|3J3Oomg$=@_NN#@ zG}mbknEJ#2@xXYkkIWIPVa3n8aU)jv!fS}VA>^R4L(IVUa%z58^c=?HdT{+l`~i16 z-L`^rFF!H#tdER?t@=0qk7G5l+fB~Li-|Ct&6b3D80UJt?ES_ zAlgE<{qy?>=OBGz$XP#?I9m;jJNb4uvd40q(`EOMQ#U44$WFF@JFCXEe#i5}j(87= z)z7uyR5V2iI$#Bu+b}tqqy2`~!0&cTE3>7ApU&x|?K(8o*sp20x|ZK#-hV#*b|+i> z;VjM{OH)nMHO;2vSFNb6y|O5Qo@0t5Q>M%3S?i+A?tUu&pF!8#8IGYJx6|m9dB>zp z*CUv4?vGm>@5&FiGu@XlGwkaDjk~!~Hb2M1*4!8D8}{P7?}A3f?(K3McQ!FLY1F6H z%EndQ3Pv;fHI2Pz-kn+VstiM0RmoE8YdCbj9G^7pWI3(c#q}N{N_oKJR`4d^ z!|KEN=o`^4bG#EQ#r^Te>y^yy%2N^MYh;MGMZ%om#lCHF1Lf!v>Xgn!ZC55ZHm3z8%kx zj8ypH zyI*tAQ~6$K1eFyXk-0BA>rJ{Jhz*Pwtf$Y{<;zZjd*_RCDO_N zcAsV*tI(0W^l;?pujxMyD0gmNa$B(W)6WibGiC%Qtc8-Pu4H>3H}M@m{^N;if6T?|LlPmLA6H`%Tb?2K$y0^VXbofb>DrA;${vT#)(K^Mo|#j)~k8j zW_t-zpUlA25Eg|VB3*lGiVRMZ&H%*)@w8r3OZ0@1I-~Qa{BsIvg#^En9e&p@Yukxx zVwg->9%gC46hM$g*2uULdQQ-&9@9a2gOT8Vao%{Un)qX_8L0i{a=WZ%lRavxd`YwUatC(+Q#04k9I%FW*8--A|Vn zHua+g7QO={X$a^8pMHRtvs{w%MLFtc&D`|8+7R6|6@$fTyO^+JTUH&~ZZ5;F57?zU zZap7qruU8$y*f=M;S1+`>f|@QW1dhEFl=y~vj4fTFSdV45H&w2c=31ee&*geu6Uo< z5#6}x-I1wi>R1@5#VMH|E{wg4?ip>7i>)b%6QdKx(sebJ&KPxg4HK@ymmWh@@z&4U5Ah1j`4V|omeb{>x+=wQSj-q;Nz#%r6idSdlUYAPD06l}#i)k8 zoat9FjOc9UEBJ#F*}{vtKC6rCj^`x@eK&g@a3%f+coJHj0PX@W`Wwoh^#!#QY%7N@ zcL?d2IP#cY?m5@9EhkDNEN%w=BCxQ~Xgjcnvwz@`QAA(-vl2**3llzR^)kM?p3*V? zfyioZwO-zvi92>Y){8-*eblTfmqwPS7tp6~eyYQCr>ntlLJ<@56Uy%1Rq5@Q&3iVR zmB{%)JLc-=8?l3m-KOHFcTFeuC+5oQ_sc1J6 zYs03Z%HH3CkzzeaTkUv^l+jd-e8rW~8Aq8-2fq%&fq0cQBSJlbk_SLu_yFC4y)Htr zPk7ft51Tx%m)v_kE3p%yVUs5L4K4rCXof>sU019Be0u#u<}HB!Api6hBu9yf;pg!w zD(2ZMB=@B~fpb|a96Aq*o-py_`T%7sv@5FCY0?=FBLg^)wcj5LA5H#qBUz1N_DH++Q3TRUbqIuVE02&;W|rWv8|x8Li82S-Ao#ISO zsy6BmZ?l;(bT>@<24!(Al&`16Ch#G8O0&+@WEjFn$=oHIh5QMZOsia zw~UeegD`ppTP6s*@Pz?|LhsZFn5<=Exz2X%<)In7Ct`XHM5vbO+Ny6Dhr2L1MOMW3 zz?X03iBgD<*O$!WL<^r}seE0QbmVSPh4nRhVHEci)p5Zh0|Wt=H$#0=kDuDBUfCSg z%}l!_s&eN2)U!$#-PmL}D{sHsfAvxi=+ULSMyRR$k4JT!NL(ipjapWKxVWWQM79$# zwK^Kc0b&Fud}vRK$r4rg=Qx2Cul%{Feyaea^xF|D5F2oG$4m>;2g1_(lMa8u=ZABx zzWDxGOA|glMvCzI^2i0YUbj_sa@GWK*;v~h5S+c+|@+PhitT*~?P z>^ET7X@J)B3@V{0_4i*H1A^;qn+Zy}l^u%-==nQInyL!PW2dn9$cu>_VH9p@eM*as zOb(l@*qmEEn|LRnl|$?puByI8TDg??>_Y z`O4P}yHE62qwT;=^<^mWoht?avt*dwSCV^!kATtNBlsaNvFPwC8+py1F#TPJ#`r6tkaVO;KK{{XwQ?`MD)N_>~S&SpxVLov@Z zo_Al58~@`&Ga+B2F~to$ZsJdP-mZ*7Sj`@xjXQ?rlC09#qA{8u6{%Cn#)tPPp>e!~ri zD6I+nd%OjHPj@pNg(Lajf0`^v3H{k~$4l6A2d}B-_f)Q|%8{D2rK&39xAX+NAmLlX z2=z%gXJ&V1Ei>%LIZI76Lu^UqUFc#=X(_a}l!RVKlo^fP)5QwXx-!g*`1T7Ny2_i* zSUDx(Xbu~VzJI{0!ur5lzFE$jLYjp&NpKSgA9s2<>o4;5D5yzFL4N>bL8)aPl?s$B zRx{hJDo+qvq{zE#nEjR-JHL5H?S0EJK`JtUmcryx=@x{OzFm!xFlm1!t8GU=KB#%m z8JfzQl0G^~w!mcL90g%E%`S6+^HJ_qF&#=4!oXw|0RKb7)DcHgUy|ibbMocte#(pi z3BwgrHEGLB*Eh9Ics&qOx9Jtc-s5MuSq>xHqV62mbJBGh>DEaA3XZ%qO+ud(AW=(= zlpZcGL}`7Sh|?~nSxLPYz`#xXN2F65TV(Kx;4$U8Kg$Vk-P#~mege*fBAEQ~kRik( z{-?S&hFS_U<2bSk9BM$~?+liuOk=0%E?A6A;EfwzbRWmCy-h*;h-V&PO)6c@745yp z#uSR~Jg68bEp&{z_0!64yi4^_p#iXTQYv z8<=w>gZ{$SyvZrRMo*7CkI}gt7us0_4W(>BnS}%M<$kvg@Zh(oQM!8%S9@ zERq)bhebSBLam~CzhqO*|1PmTvCEEDaoqIblve-v>%=aT?z}W+<b6-WJI@ zZBTorBl9USN5I47en+qCHrUF>TcL$L)M27I7?#pyy~S;}=4{XVe5NV0y^2#3sg?{` z{<=~O)#YGqIk;T%Q_#5N1>fJym%(Z{n}t5u)1N@+&l@?uny=)ZVLu4GCu19y(U~_c zz2}ZdIbhqaR`jpSDuc!3tPg!Q&-PrK)U@FILwm-{i5u*JBE<`|cG5Q4Ei+Rmlpro% zOTkHi!Alm1nTM3cs85}3UnO)rY;pWDMztq;|Jh=IO%nPYY$`?S>|wfUwwJ#ah|7(Y zz8gK1ka^KUZkP(O3Kk*zI)?dKD)}*JHVLPY8LEVm z$sy!VToHlYNV{s$r`xm90)lv(_0V=pRbikhj* z6$M^UQxjw8GZ8VQX_V#1gQ?hsxykY<{G$&fa@TZTVw;}jkx$SR)R>=GOohAz=;?gT z-+&JW#Kdx$9yK3SkjBCoi%faq15W!_d)AWxB_ShfFmy#lRQ|pTWtw1bp;cMn77f{( zZ$Uy5MUik>4}eq)zk2>*A3cx9zTc?m_2dk<@K5TfeLSd!Ql6dC=OS*_@)Px3T?!er zz)bAvC@48H;n}-X>m+$I8X?dWopn4J z%ma%gp7o0I2yH*R(Y`&8bmPD~)@$wUhy%nXgcTbSDN;6{!b^K@5`8tv`SE5oSkuV7 zAdzIf;ys-PP6jRN%XGX~UQtSR5xWQP;h0-APn?}9ZRR<@zt=mwn`#lcmEAn*o*XAL zR$)P2fj}hDBd|_2OyDD&v5zLviH>v40c3aTJ{w`(rcvzm>bD_SQW`I&YZxL@?{vuy2FQd13!drI90d{fp|VAPtIwl5TD+micQDzrDk=5q- z1*9=;Tu#ecBl5-9p@}xQkGQ-M`w7b=#B$NJ=0&gxSFST3vfss++`&OBOq$FglUm!H zvsn61nlb6o`!D$eIq<>pt&lE7BXi2I;b=CV7}H_r>l66~ww7^s-m>jjWWg^)86pOJ0kCW~GNp|wum_qA1SV1q{gK*= z7D-~TG0Ik`vo%VpXW3)DOO56VdppNw_Y)0`iC31{TXzt*GFN>RZpAZ#Guzx@CZnkHz9S|XA|wfxpXgS3Qo^p2pWE{yR{w`2cg>B6pjqABD|wf zx&JZ>V0$AA*7@<9GO$_hHXIU>-K!w@JCT7f#Am~*l;ih}=G_OQOxfU=#VBCC>+yz@ zN|$n)bCHOf`Sql+T@iZ-MT1A-y$Rdm%s6M1oxi4u@ zWbrKv_j>&j+IY->yyhV!sGC{)XJC^Cn^jqRFI*v7y<~hUDSVp6iceKp8y)hEMy>bRSprH!d*nT8J$L`6LbNI9Syx+wN!<^Glkun1c<}%xD9DdvLMx0(g`I29QXeVO}XhfnN_tAfw35TgNZY~`5D^hLhUxsU6 zmm_5f=-W_Y4Gq*a2K&%*ltNnt%POLk$OeT={mV&Lcv;ETYpqVmv@DV?bxNU7HY%;G zFg^onh8$LUBCTtnlH5o6;9RQ_J&(hpayjl@1@Rj9;_!Tws28&0QGdoBqeKRxgO7nH zC0w7Z^Ig?EG#<{puac@)2oj>lMQ0al>5R{rPuj5ZKNr3I;2l&DOp;$y<}Fu^Y3@mqx-@C- z((|N;p*-7Qvjn{j;hAn0 zs8=+M;OcyfM2}r(bQ{%C#BtD?I>orJjOO?2yLW$-?2wekLyB68+*`1y{`^rJR=aC< zl}m1L8UL8*e6C5|Xp;^W1xSb6X+kI_2GhWQKJV3V_s+-noMsx3z=baJsl+DM$(9(u9hKR=DqT zJ|?USDT87d*L$(rytCbF?~4s?zJ{ediuV+YPHWskfSm{suCC2jXteIMUjJtvpL{!6 zsZ`0Q0Y2!9xAkKzJQ{YMeI0wVaqS6Lup~$EMTWBS6JW*JW%rCHC%<;SNm-Vi-(ib; zD@&KwSC3cho$FC-Z3XNb3Yubtg!#R-k2A#=t`bAB4`Z&YBR6je7t_PjP^AGB{ydOQ zYQM|kRL)A=xzG^oQbDt_iGyxx@#FS@;cEKm0DZ%{7?|z-*XwA+U*vk;2VIilnXum} zulcE~GN=`Wjxs>1HE%vATW$2*tm}Q@FNUez$0$K=|R;KSmaTY?nGrn*>Sh zns?miVM`pW@3;eV>qDeX$t`Tv_aQcqN}?7H@Y8Cz5};&ehoQLSjI5rk;-;ZFmK_Po zh^n^90|9e0pty@F^mz=k_Uv=*j6VF%hQn8GIt{_(l?YiAbI47 zya3#>t9j_~sWcALov(z$hF&xIy}Ld-h(X9*3*<^9Hv1lOroscEA(LaxRzaA*sS*f; zM9j}xA^i-nir!;PJeMn>!G-HXOci1$p|`3PQ#vbP%Y68;eSQ_>j$tLVBr4;ATPCGq z{>(=#I|;X?+8OW^}L|Sjc5`>q*Jhc_6Bd zq5|K`q1nAdIl*03Y>s7Q6h(hlQ#RHtwiSn#LdhI-XVmhjxQhEaWi8)KHdnHlYW+Y9 zHUN}=77$bt*h>I{Z8%E@P+p<>g(9QKVCnU36%17N_PC?1Iydd_H7E3chdHv|^1M{6 z@AA@DIJc?1(G8*8#H56cyLxx%bK;)H*UMrM~2{Fzj+OvL;!@?_E-jY_LHyyLy! z&|=P4sbeV2-)8cyICpS)=ne6r>F-xSbczNMvv_va)F2p6$+s81=^&Wb*Zzc!A{sPW z;ynwbi2K&S(A&CFSa*r31)#2wLRJWaIgpd^tD?vv?STbD%KJ=@P$s(ldn7Jy9a(0b zf$wyLI-5EqG(*6tEK&wkCM^4ZV0?Mrz^9{@OuZk0y^T_;H&~I(uZdZbrx>?^X{Ccf zw4TI6p^YOubqqbI%iZq`K_ElZVD1Qz?z}#y3=88zVCb)jn8}vozAxImEU5X&Qfcw7 zFc2$0D2HlO%~EKJ(-Ab@)xFX9Ws@3;2PFnJ7mN0q@Mfw5_Dshn4OBp&qijH?)t}Gw znl>+>o>lcZie%tR2R~1>79H8@dx%?D1Ui^Sy8yqHt5_m}&W&(9BHGg9!}=JMd8Ot^ zN7M-3-P4%&LvA@y{9;U{iGAS)-a6H49#3B?SC=XEHt&z5L%;8Q$z>(uYC>3vuTju1 z(hgHl@6^6fp9oi@&5?)uklIEtZ}Q+-$;}t`gP5zBX6|V^U(YXmDxQ9xGtn^CS3}F@ z7Zc2^*N37rvha#B(YT(icIZu^#$0?%-qNTxjy?-(%+6h&)c543KE0G1N-Ic`Zu#}l z=l6!m)S=%$uT-Cgp9~|Ds)fgL1;1v-Svj`$h$gNbZ{qp%hqkp8w+4bsai2zoWQ;gS zsp~2VHj=i$P{hn=lKqE9Nn3M=*F(1YkAMtXOt>raSMq4}SYlHJD#)u4>iUtGrZp(_ z%aX_#(}?VwterGAqvb)jjC7v$y;(8%c25N+@WiJ-W!#;>0$EXrOAksZAo?9# zuU@0TXf0-fB`wgB5jA0}Ow!IO-yzaLJ}jATZaY8tQ`9^0%l$~xfR>vqtAU#>u|5vB zj4A606f9+@L5@k^RSXwq?jqG2}yy9Lh#>0d_Tv#F)3Xv?CX&i z!N~&&Yj4d%Gen*|sEX)LvSPJKxYUc<|Iv-XWay-NIz{*W0SV?N*CeMxVM*eJx%4Vx zZDL*G0Xm^revQGqAp`jRf&=N`M`9F0%Cc~-2MgOE90}bvi8SUgWy@R2O{KLL4J< zs3WAwLxAoavZgE6dr}&!lrh+%9pebKkeYf@{CO;Byng@Q0p`1CT=z|vk#*ygbw#O< zPx>=10gGLPbWX=?I34nw5l=LRX|bZv#4r7^Lq_hFva>m(k7IVFJXkFk&S0AZ@cD!$vkd7_!8ct6`3Z*L4>Pa>+VPzx^uN zIu1p5D6Zbn_k8xR29DaZG5}|efni;^1bIO4w9-b^mv!$qS#MUrzGi7+su>o6eDgCdMH%K_5jw|OMB8V4z`t0@J8=fAH`qMpm8=R4UJYu%v8DOJL* zip%k?Qq9LQMBUYYq6wEXij@ZtXy;dJHjGOYZlyTcbF^XId|sBJDUcOBGx2==Jc~kO zY+;>Lh`yoo(?J5z2N7`%aGZ>xH9O&Y!g^yTZxRwOD6^NlJiB6F|IPxO4ri`0|3y_c zO%}?1kMK&Wv0KP?hljx}zr1t=kIDC#zwuAu^!eIqUcStH6^6_i{@Bykz>G7_ZFf(F z8P>{UlO!G`7h+-4nJnVF5hK7hFbNli|9~rs(U^ym3A5(rOit)}yk*c`YORp~i8rP) z6j*m!K!X-x+;VDdHPSnJzCi>B(#uKfwf^^NDGvO4u zZwT_SeOCxozCica#t{re&pjN=f@j^mIhk%)%V5@?(v~Dt_9EK>C#wM@3rz=KeX4VE z42>Ela4QQ}N=mva*?u3KlO%UYPqPDj%h@$R_7opz*-_HBQTfKXDbKglUm4+zSk%mp zcyrG*;4=R$5p%#i4{}pdD?C6C)}8nkBf_(wHodLA_HjF}EDrg^`8hEWqe_Y%MMadT zoRTBu_{PS1^MaXfALZsO&yh({`~HhZ@}OuhviNLG_%EBssQZXXB|92PnIj8?dvNL| zqO|zQeDX{EH)h6YM}!B^R{PnG9Crt?(PE5c>-8(y^w$Dw5>ee$f0KCHib+l1Bh#Wd z=!LYDolMK8Lj?Z{xT%Y)fgayUN$rlaah08qCSy^_m5!N+nFy$9x-x3%w}{?zd2xrH zjCP-?z_-yuS>Pv+ehQBFFDX8becA5}2-wxtvqEhkZsMg& zF|Q+zp7_X}OD9EsHi|_T8OpNOg6)PUh+!)P2ZnGJd#GElWo-EhsqyMEW0lb*WAlti zbmvxc(Y8(hIg8y`;^eeGbCMY|MWGUUxhg5>GO{;osvx|;Vv_TID3zC-lMx48H%Wj^ z+-QRF=6z2gWd*6kcHF6;Uw>67x+(^4d3_cPpDIFj9(S5K6hdr{i}ikEG`By80od)- zb6S9n0Uz%)34_Rd*1fq4iC?fzptdXG~`*5F~(Nk4h2VHyO`iMWKVJ9M|z;dRD-|;PPuqrw{ zkc}Du`SpmXA+-&KI0+3{J~aELJ|dK+xd!X>q!#ZZ@n27@2QvvJW!OOmIb9y{-rRt!wdfBXL21wZQR^L z3DbEQ3gLM~mp+>QDOpER&0=`8^leBhE!I5Y+^aN7O;vytS8s$R;A8N;t{BKoXzH}* z%}e4?y%+(2MiM1Yy3R@DrhW@&ozn*EC5azsL)&T(mo`tHAe2!9pTyaW;8?}k>g32q zR+D6v%(N`kOTy61jAnsLrcl#Soxe{y!v;m7Cy8}UT@9oL$z;-s?DIPkt6bE`hCmvO z$gEAlv?!Fj&woF?@j1UuG&q6SsJY?3`&-w&O9~OcXJy z!YO_BUTd$teC7hQ_d>#2Y3=4^09q;Ux6J)LuiXqjKug(@r^FFtfH(*uOI7wShlu{$ z4ic5&(&v=7gnrD+zk*K{+v)ODs#8-_J%O{`8|gbmY|m#pjQ!3iTD?Vz0LNO#FTgS@ zU?|*j3oK^V)~-Lr`xw;e_>Ax=uJ}BEo0)QE`RB`Ui`S8-k#W^mpPqZ}IrVAd28=FKmt@yDXQr7ljFOhiK1DDK3% ziGf9=F6-c}kB3(E1)gkFmK=G!pPFAv2!UL-l~S>@o4}{p>zu4vRffZojzt zT6D9pRo|wd;XZ9A=C9@Rx}FzZ-?95E-yX-$41v*3By`Fgzbo(L$`OH^8-^ z%6u})t}f2-34`CpdP9$nZs3*H_vD~YKh=b4<; z8-{2_Hcm=}MmBVTTM@(u=D!L_W-UlO?NEnqVk$#=Ao2@nJpvmMf=yxWbRMA|Z~P}| z?8w8Z$F3J^=s8B-J;vX%b_-X$@u0z3Z)n!LpjdQ%x5ITqRvl~?d_|8sixJ}O1 z;~q9eJJQ&m+11Jn;rmzn=3t^6OR*BFm z-_R-hab*pBB4Nf#Jn2JUBk}t!<%Rvan-^^1+`HGn39s;ka~@O_v(p$2y{mfZxc-B~ zgV(2NhpZLwqzm{h>NiZ~{5?*1lg4|W31dwpldk#$Q7Qm5pwLdx5ih^Y*MX zXt^{VG}xOO%5z>id=J{Dq^UF;uPJxwx=OJQ59_YbJN3{q_ksJ2p_Mrf! z7#_$LwlGbS7F10+=C__je?Aj9 zUP~^I$^9dLv@&z0zdCL*qNPSv3fg57Q%a6BUp&V4>x>Mpa{9ArumilCJ)%=lwwnf@-x?BI=n()7wUl+y~9m?2l zjE*D8bbmB3a%4i(X>6mM%GPtf<6urn|6nWW=-EMD?$x-M#(G8SCHf{j#Qe!L|d$ zeD}5%0AclRxYYfkI=g0Mhn+uEF+UJW$wfwW?S+6fOSLZD`u0r!)k5`9iK2l4ZZYq3 z_t+2HgqVKiwAvrT%j2oN^Yn=t$PhjO&>-3=_gL1ex&qC%m(1_b7Ln)~XfOP>Sl& z_#c@34*^E>ECC1~;jFtIJw0wY3AJxn;>QwLbQ0~A)nBI&a{1c09?9DMZHWDyWw!5C z{qMEFZMxH=h847EM>DL%Jfwa~@556BZ@eRXyxq{S_${h$V2}wHR+Nb1z?Fu z7bgN~KRFghGgA{e3nArVI7UW63qjzXjM3sxH%r5cOE;Vs^#~HBcyV>NEk}HW1P&ae_5MZMC%|ULdQ*&LrK~V=zp=%S^ww9p544SO0lP#4bHRQ z1YyF*jd?(LW8#)_{i)kG@ChOK25~46f&l(_UKFntg<}k$uu~y4bhMXSu0z|`Hy>T{J4*5Cu}Ig6LRd&cuA|s zQ&Xc6544^Ollyq}0Z%5YT^xZglVL-Yjys<24lF9$t`w!g34h7M2xiO#1n|y5;yS58 zQ2i?V5HU7}uR5l(SOlJL`o%v#)GvM;8fS(8RV?=s5wQ9P?2Xz9RaWdg0`dzWczplL z zjKXh{s`-itjCy5HEotq}ujBE`me9-nvAK#kQZc*bDgF8K8RVzUb4 zpkrHwgKu6qA2;Lwg{zm>&zB6D620U^JoljFMf-PU{h~j6McI_oy5`tGtJbr=*BosZ zpFN&#cX~#IPssnq4Nyl0cfw5E{~%yB66py1Sn($h!{oog1YwD)LM#Sedj)HVx0%X2 z(&d^`pnsK;PG>m;=dUb_;h+C1iNIr?8YeyulG%MH*(;{;l$HE9qbS zy&So-^eh6#*H4eS+{9YQihuq~%*Hu79&B>2uyBK>tgNzq-H5I8LAB9U={sX`R8uRq zm2GdOk;_Z(_4EQnIR7J&yZA3ea|ejcqq%}$UtXptjUqr8Lq!QDFUw!euehaVwagGRX*vK+gwe=Ti7t){3YaF3xA%#zKI})-4p>!V!Y;Pt)lHR@?AE~ z!S+9NY=693Kyj|9>VCDS{GMm-Fg4q@qNy7Ju4?gM&{13VAR;*^m(WMAC4XM^#;WD>cUsD{q7VdOi^5~%8e2HYr4Cq;Af*w$}<0_TdT+N+Hu8s@NWsa znsY2=i#?CVllJ>0Dm&ExY|mr{ZE6DqnW|@m8TK&rxvdsB#F(iEokc{uP)r+n+hYrm z87=bwU#FYLejFdwG4`!np76Bf@W%^WB6DojxMk~qb4_|6f;mdab9|CD@_;el+z^`TNmz38L?;YFpM?&}2;vn663UeSF$xfH&4!1I zZ|+~t7*oX)AvA@b1POzFcsD|s7P`vR8zYiF<_C}f)f!sViLoA+Dyh{K;hZs8BqAM{^dy%y+r&|x`8 z#9>6FkipTw>2(#}wTit1M$SU|7nq83Dff$b<%N==`^! z=V;=_t7@{%QL+sO{VRq8NJ{N9LO z{4wx18{h!N+N$V=uxI{CcUNMomWFm}fxuS_G5 zcjOd|MCy05^nFy+ zw%v8>A8@nIOF5E7CNmSYgNv&L$4c*M_N4{88kG-2K%hzzEsI;Ov{E5LG%vtHtf92F z-R!JXe6d@SXdb@|(L6E{D0AZ9SgM#{cSdmwiC>p9XR~W<}yj77eU?Hi1M(062CL6zHEWrm<{uGaH|igr9_I zNqGiTSxMfT>T+~E!0(Kbe192iWng7piuyBJF=o1qUr<1XHieHt0s}%fw)OVN!ux?| zjIS!Cv6gIp_LF~)Zudt7QCyIKqm^^ZsEu=Ehgz8(@ij_pma2Fo6GT+Jiw30Uy?XMO zT@hrqI{E&iDM~P>bXT&8z8s-l`cq^3BTQJ38-NyuNqtGT}}m}Qx=b&B5{3fxCkU7B$KK| zmI0&>wG({E{JzdzfJ=M|Lz1=3a?VBh<@K;08i?W`uTRnoRIT4DMo@)X&zo;3R4|N~ zt+1$L%Ffwqa%^hxfrO!K5gFOAD)7YkUp*WQLBzC(fB?rKr(`3PYi7Q9N22e1U*qrla29ulp(*ktT$LFsWjEl4UB_uILSW7{8F5YTl%gxm+#jjj6!$nxs&OR56^UeAZGiN zKS&td`fdRS6N2Lp!KY(MV1caDT!wL<575Oat3Tu{)(NU(XkKY}%nOq(;=51zuqN&~ zFGUVbA(kWM!FRO1q#~Pj=&h+*Y|t8(MSddlXcNu2^;VfPa)L-zPF!KmNERr1&%z?j zh6+nC{5J+e`r0)jh;shGKn9J9i_PZP7_nfU^wpVv`!Rw=EB>FxLc`E_%-_IZ*CYdG zI~=i_Ro-RdR0uZ*E9Vzy`7~yGb-(eHGd5OTUYIH<0`jRkK_uTH2~>8aaE>L@Qsy^i zmE^1X|Jx;aVtn~*(aB!}nC42%gO4ZaGDSM_S0!zw{aVP26;fR4OIZN2e7iG@6<6+w zeB}Dd1HoYqMxx{ToEB=zqruFZw#WOV?1|)v=&~$Nm30sJP0v4UTxva5PDoq_Bl`rF zw)>!AN{CmFd@NY0M`};X3N(cZIqLg4X#iw#-e1-(=M-G>IUgoC$jMu+5~&V+L7}Wa z*v(e10Z2dawVDcdJqE-`0wfg7oNFLCuR2b8r{hywN0R0(_FACQUuLcI`tS(}xWHuNHp{WD9laRA6wazwwRT%1mjq?-LwC4G@c1J&Hp6;@xufeNv_z8DJdlh+ zl#IYd*bK`16p*a!axZgWgoZIFB85`B7v!KlBw5B?PCGN)VNCHqyHtddDYiRId~EZi zr^vXtBfZHlaS4+tjN&^6z2=;{I z`)jus_s>ek6Uj9TtaR6&T-nXEUTfDonR64kA6|y7U+^JJ)vZKY{%f*VxcovEQ$h2n zU1AAX(U-ns#zv%0tcn7?p9pE+$5mHbY~?eTd7S`(F`+E15|gSC%*|7t2238Hezj%c zOM_D@VBF{&d?vYGhH%b0de#7>1^RXP?xhND!MAvJCS-l)SrwMNR_-`f@AAZYCE~Xx1?>?;{UyR>cra>K@F|*n5B** zM&&VEol6Xnl#6cQLdqpz<5937$H^il=KVyh(IY{QLIRkske%Y3WgK!R!z}D$r}zX0 zY6DTxZqy?=cf*ClwgXROxmoQR_;e09&Dd~JzC+&Wcl1-tzRw&?m-tS(E>f824rM9A z+ISTlEGzQ>UqaKK8)>^8Hrf;6S?yf;3+wc0aB)M&(uq4aghNf(j{wiWM;7BwuCiEBbm;aY?5wN% z(^-S%HcGdpx};bSvSb3Q<-?mhS6jw}7QX^&JT`1ghvdkO)P|JC=b%1P^-IqE6u-vb zZ4^Un82JiGHuScPwErny$7f(r1SEkWQ)z)jn$WR6Y3DKs&<6@R>-|fGg;IX={+(6c)r@13Nn9O!s05%6zF>Z$U_^ z!wz2=xUYapCs}9_LLhBg$-*+NgC$_zY-Lc_rV`OhPmQ#v<^SyX=A$IGh!Ae@Ka%FI z$ny*K_p z_Wt^>s;=!Dg((SXX=#v6s|}y5AeL&> zj^%u=bOYl)QY@ZCDgw;Fgn7%U*-d*3qrHpz1*bsQ4tWC zRIhtldc+Evp4x`^y)@;v@FkMQ6?#J~)oAJejwC$}uj!PzwO(_U!J@0;WW+;vF0`vx zE}kC8CCv#DwfaChZHWD%R@?aDZ1^dOY0S`avISOmTdqt9$oKA)|!t1E=o6 zN2~p0I^}EA!?Vf_H{IKH=aG$+9_eegtk0Fo(#FJ+QI?nnU>}P}+gR3`zcy!&nO09- zrCPA_nN3tQp;=KfpHhzPwFqVFz-+ep7zAOQJl42@Gnq7^L+TkccD&vrFOdyn5^S2k z;~s|Gbjj6NqS}qAnb^D!o|Tz!@`_QRU?u0a(Rb}kXpL=4Y-_%2W>;vfgd0B%bP|W8 zYeaE2^k`^ZJIMiQAaZ>PyV8DI?4a0&N&0=z9GhS}mo6t>QbSI9{Ir8|ffC zMmZi!<(mUT$y+kK%nCmok3qdK+FoPHRb@TrTx!P}^6*32cN<~8our;b9J$J2uAi53 zD{zh>V%}IL2wTPq7&dJ@!hQ|>8oOuJVt#{v9*rR%C(lF5D}&=JT4yLs63TEX?BI{I zAlsdo(fS*Cjz1edk}s&%Zl8hFrfw)`1kGb?7c1h0pW3QRort+}Nu0D1P)AHhD8JId|zX+Q9DxCtdDzGdFv4##!RvOD&D^2!~ zJ7E}T5gAE{kgFDxEm;+{O%uQ6QtQxIUWcDl+4W`)?ZRzN9olBl4CbIW6J@TYm%SkA z8K4Mt=tsfOwB{TuBTFNl~|DGfc-Fl%=FvIUr3CGPl~{JB{9K z>rQQwA!3b9L>oROaHi}>Z89`iL8ygx>_^obH0OzkC$6IMQ&x8s^9$u}*#I137Res6 zDl_?R!zw0`^fEQ7#!L9B>UP8oG%8D*QHI$4_Ij!O?#IHrH-sbc_UqKzyKrxpG9!fJ zk-|4p)^cIrde*|1vU5D+<7T+p|Gxb^(5xEAMLHQwq?pX`^sgxq4{6U%JB>`2ke>v- z#Fc78?|*qlug?>J2M5mOO%I zp>D;R^4L|PkNK82J!Z&&>6LB_=~g>SvV-Sx30aaDyw`O*$g|`%uvIzpf`zYTenvgd zX|a!xB-NG^!XJiLlglX6Zy03s;a8cargJRbE_2DVKSzHaS?=aC{?#t0k)MGqTMEYk2n*RA~*wU-MwSkH27jEao zD?AgpzR9M+WRLQKH^u_DQAep1?M37yJw$WP$du4AFRZI{4gV_O!h`)m&eK_<*!IiE_O9RH@r*IIO_7gQMDu zvCk&CLtp+r+FN-y;`(Kq)8PAP*)`mZQlSW!9*U~Gj`9YY$b%%t)2PV|&}!cIol?uU z(L*MF88V}vT z8M?C2jO&-2Cd~#Z5ZT!ZljAu0Ipy2ES#v-2>IO%i(r{e&h5*7{>m&al zJfdoF#;L*E4{Y1-$hu<#Wi*re+6#!n5s@ZHhvr+UaDb?4Gmf9?Ps7BUp%-t_3|v_T zMLFF=_>7}t{*#JxP6F43{mnt;U9d;P1m%0@#hQI$>R40ZQ8<04I10k1<@#ZZr_)DQjZ!>W(b1 zCmwCzR;uq!e-YD3!Fg+#o+-`_}f1-uST%*IX@^3;y6QXaHajWp$UM$yIJd_>{ zSxiw}YOVblvq8p6^M>xjEH~0~v=I%E56cCzgL2xm#ra&9E2C~|CC6R8QeomGbPbiy z13b27Ltkb~?CMf;KNBj^p=Vi@(b2#0)W#3_JQ&ZZ^$jZl{&N;n?52s*4Sk3fVtk`$ z$n?8eE?9E4Sa@Y_jkjK1iD9}z8TGn#eNWa3eP2Q)Jo%m==amGac z;U&jrzq%aPrT-v(xmJTe7b}~~a50*3eyVodb0g-b9HUyOs7&j2%#y3c&T8($cDY4c zEkvx-32l#6@BQxKxH@}}U@RmvOH+f-{Ou5;@zo%>1A`I^_~_>|LTWRKXy2|%c@6l` z9C`8y35Je}P15m@OKGc_#qh0Ct?^B*u;Bb!{4}ruWC-Sgk_qE;NyFsJV=+2gh80C>yFI3CTw>s4iGNwZ*P_Hq(HnwbDeW) zD4NB!V~}WHh&P1XhyG_Val@G)-?Lk)Z@p{nyQ?!YGQ(@WjRWNe(8%)0f)RNe4(P{F`(>nj#-{~X~+zC&&u9%`-L_f2omMSuQIb6c4B zT{DaGFB)*kPdE?6qmEPljw~ASfMCTVV3HlD_)n=T*;)P55Q+ zKSWN1FacI!Zhr%S;~iOSn~#zOdPoT7)OP@cJ}odx&(5^u!C9963Uu=3q;RS7olo&= z^g7brAgcOC2*htZqNOsJE;s3s2|NbOXBH$H{ z?I#NV{?C7>XN_wjH&Er&oOXS;{oA|nLSKQw{W$QShWS6h8ZSL}NI%J}b3_n+@FYoJ+U zW}AWbzy9_vj?h<-+T8!EX#e-;arj3EP{75ArddB0 z`C>Hy^0*76u*`^%@G$-_>+xI{Aztsx4eKC%&iOLJxzVUj^bZ;KKLd0bXyCt1Sk`{d z0d0Y|8YQc7e-!Ixta1QAA6ryKT)B1Lu0kn4cq9xo>M&MO0x`RzGSStdg7l}**sBts zGaJ{JaDd7Fkob8$xC_c%$|$cw>fyXWLfYHA;YnEzIYyr|)?02k8Rl=XAkNN$4CLlr zykAbU{AaP<^20${r+=t=5RkF_dvaduSwlZns2@mB>OqnrjWwtld7}j|Oak5@YO_2# ztXZc8%Px?fKmw9)rf`0^rIPxzL+LBB&#T@x8_|+Z$daQ0pfuFN!`4Utz)%s8{oATG zM}=xLP)o@Q|5i!B?@%|cg;&L#{975A_W@7FJX{IV?%&q^fiS2>2g1``e^qbPK_BwE z_FeD4=Irrd5mu3UyCw>RwntHlbwYFES^=Yb48qL(0m{HN%sHcNaJ{BuJzc}|tBMcq z0p6Qy#a(%Gbk-nk>feD41aLfc^yH@P=z00F*(CPG#sG+Ovhd0 zznrJ&1`2bSbnH1+3~dDvjh5VrduuEl0}2%QB|zX=uKXVm)#U#&Kaon7d(Cf$ugw;L z_X)IszLT$wiWIn7l9~7b-TdY_oxf}ox~C(w%x~I9S1_0 zdhjF&7A@e&bBn}n266s9KW$^1#Or{@r;4HLa6SA{aQ`X+A%00>^z00pa>FQ=C}IOPaPQ^NcA%5M8Rb74PEOK&FV>fg zhg+I2EX}s$Fj>TI1cDgR33NYaVKmYv89$S|j#Jkq`l)F~+9Ii01;h}3KosB)uC5H9 zsnGqgn1*36jXSLrcJbv^fzZRtMUSf`g9x6j!V~=)(K|2V*d_V|MFt@tD_Ki-JCt7P zyXg#Ry;||q>q<3EwwOYPH!ZlNJO=%aKOmdM%tVqX#e;E`Q-y|0V+yA5=5If5KKTNT z|FD7PGXhM5^?nW06Bz{XMKipHh>w5=BX4E>_@UJvOX}+jevnAW%htoNpd>*=Bl~8~ z_@%F{COspU8vgPA1+RbQ%rZaF9IXLDb>>!q3h0lF4)(Ns*6+*d=t?a!M@&y)4e_pW zA_a@Dg#O&y3uEx`z@-I2cVRa5#{Nm5S<=Pn1P@u>*lVxXLFNZZN^U!O2`YPyBX1V` z$UX1bSUI|w7&z?Fgf#^30c#ovo-~~VY>sPv+DIaD-cE?BK>&=1>%+y&r!FZC99dQo zD}E*g2`Qkkxn7GB!}u{x1sKX|-5G6rxy|S#9o_*g%WtZ3&+j{+oedJK=|fVM!2(i^ zFq;lgv=ssKVh_on4QP8fu%7=R(lo|| z2_L58G)I#PC}&u7)*%vrCA=`P2a$Z^Cgxx-jBH)d_eDSV(B&WA%9<8ed{x;FX8_`I zrYfCh4Ujyn)3}tI9q^E@pyH|n5ie%cf>gT@3@;`5?rx@WK-A||DC&-X7iAj=6Jq4n zphExgW1Vcy@AMQX!6vUb#`tS=561Wu1KvI`4${;iRW1@1C$Q+tFF<8PJ8#lKQX&sJ z|7Zd?$tl(q*lAU4h|)Tz;==$e9}Ea8=inCR!aL9kxTrE%HSXkdmN2fv zK3%BI)HF@%@p)IF+xMQH_b{Nk9RU|ds#e0KqX8kjYWK8mNOPl!f@iSAwi zu~x>Q^C`n-|eqEJ`!1Q#34XONYGAZ1QwL{o%I)3inKz}IR zN$pprzVT@X&Zb`4Zk<$UuT%H0IzBM~n=H3+)ldZ0JWoAKH5z?LkCW}&*(dNo$T z@}6Uu#8I=E$KjHG;e<)nJk1H)qd|G9*GV=j^P|4n+1-IIfU6dB2~Ws+OitTC58o7HNF*RwF#9 zyb1kfK>W0Mj%$4u$hppwlHP{F8P0V1)AnPh!4}i!5@QT>u1+AfUg*p^)R#R!N=y!r4M0UMAiW+y?N|SK^8qA z6T{Q-2wV>?Lm6%tv28tu9H8{(uptLlr!Wi2ABeT@ce3i6z=Vn{L6d8r8@%x(9G}Qf z#$EziN{JGhh`8et0_9;cEjn~WuhMCqSZT!djW?1c&J z_#uWVfa^4GK^NZl2TUcI9N7B#zkzm4X#s!gDwr;v8|X5bKdz-(*Oeh0CQ(XIKAm$y zFn&VHT$h&Eym}{sM4J2V2hbpB$5A(nnO1f$t3{rST4*3}hd<>BYr%#*7a5+Yi9-rG zd*Vhws3D$jw1Qyr+AbAVS+`Y#&+w)I_Ev8Jt6d%~MCjE2-UTRoFKXGs>`l)CaS-=w zu{nkVtF-C)ggc^M1qdr~C$nQaLvGgJ;`~!9TOpL*QB7Dbsm!PsgK~9DSOGJi6t^F` zKcdkhbNlzxr>tCTyj^^=x-#USwLP;8?PFbKTgR3BNm=Ex1y2hE|+(A_Rhj93_Mneo%Qg z7^vbicFp#UJw=b7#-SaQFZhU@xX3a{fcuQTWNy6+Uo4*b&oA;niVNZ{H->9T&E>uR zO&{@LPs7XNXVVO;z1~E3ARd^#@lK<;1kltfyfD1 zx25Q#sHZ%o)ZV`^6t*K2ym_TX{&6|fTQ822lO+dfCzdW7A$Zy0XIZJ5jPX`+P2z1F zam)kluh7#cVJ3g<<({8{B_n1vDd@nCPQqOoGxsTxYp|^}z33z%L1-f!f?4)5vUZ_5 zueR6vo?<}=XYpM8tH(p|?C!3zbWZw2Up24X`spCtQO#z4A=7!ht6Xw2C66v|G>%L1 z$^55#MX~@iqOTM~;UTAd3i2D@(0_i>XtG+noyOi)K?v}zikPY6_7wuL1Na_ zN2$RH>rPN}KFn4Lie?mwd(q?op-tOp`p+*X1?i&t(c<_&4qiK{=qQ}5ojeA#gN`=d z%INl>Y~_LrVRp1P1ZTl;a%JLZ=iv#g8mGWY)q?o*wP8!~3GQc( z6Vi05;$n=QLjfJFx|c_3K*Bkv@VNiKPiSaRY$L$CTdy0rGBDm~WnNt4SDmu*JYHbn zzwxvG3*C%6W7!yGc+jy3(EKlxHh?sQGbBN~>>(H`;Qf~utcbLSdt82PUIeonyd)8n zj1&GN>Q$x=dV4EEmyPH<^-ezSZ;<*F_sdZBw+LtUpp|jgMHS(SMuE4i|c1dy% z++Gsie+NS!)j z+mw3Ysa*=(mG&o`$}$Y6)pqYPjEOFLFdgW6!O$V06SB5P>K$Y@-vXU7JSn-*mv8p$ zn*a($1e&{=g4qE59cxE!zb0_)W^=Uxz;TgY9LoVXvi;O0Nbn^+Z+?F^;Mlf zgKOdce!ab@#}T0@8KRT39F+0IPyI@mDMWx{~I7 zO9KCj1z19{085x@-@jr3mryL=a&Nx%{V;rf>nQ)^inpr19ER#iuj1nT=h`+56)7tI}>eK-4IV9FW!{=4}fo6UGQ z^8JzLA5>_Q{TU?OPH2F+S}Tm$I=b1NMD7|#oL;Eir4kTgj%bl( zrY}+i)kXwvw{xIih`FOm3j;qRDlJYm_eF7ct=AlX(wa%$llIFl3JGqFLh}5Dn1AY! zaE0(H0P8V8bM+YtoypvoH1$vhk~~WX#p)ki2TcEzOh8<@2JkTqKYK7r_(7*qDAe=( z=XjP_7l35SLV^J5#|4zY{JftWz&QN`(FlwJF5JMc(FGFlOINo2upfa-h6pfnVrdpe zCf!oh;kjD;@nD#KPnKeP3@WJk2e7;Z!b8uGeOXK$6>Xp`O>!&rtb;{|Nx3y3asBxk z2<*7lz)Xf((R%wa(IP*ovoI&3n5nYZkB9SVDo|yn<{y0Ul7rprUhps5{{pfR7eL z#NgzFL_n-K_)kD_fq(Ez;Gc2U5-5tj#^=la!uE@7$omO_Hft35DpbiG0AMk#`Z)?~ z8&7ap0pg)ql1aP`kO=ufW%he3!23|Rh_@+*_p_qy(KXH*fF6!TXW5NBfU7L}8q40f zi?V@QUBP&2S5j8@6m%`R*TAn)?v8zB93zL%G?F)b35Vpe(*#!Lx7Ht~;a=tF|8b zKYT={7`6r|gI|BAyOlq42IvSpadZsyEQ%xmMBxxM&_Q7+c7U?bK!-uQVYa?)XC+

w2H+4tq5Ew^}qvo^S8njpENyh{l`re?H3rb(EczQn60T||m z^Ri397wf(i@WWC4UQ)k!!F|Ko!J@5x`Zi;Y;H!6@V5lh797t<^rpcMj-QUix2?n8y z6tsq^19(jS%(3c0YE5t&0*+Gmi|o}O)~b)~BggdiM=sC49`@r9LE=rsZ_}#fc*s0K zDtg2|7@*K+a3ff9y+d5|Xj720rwD33IiHg{9A zi^rw}L$qX8UA}L|PaZc?v7iVe)(;?4hh>_`$8rsTgQ-NyJwzBA^jI6hr$J5`=Z9)Y|G#4Kq8-V_Jh}S zd-2ZNL-$kJxAQwsU;`4=!+71{_;_lJIO9Z(y`bV%;mP*+qLf)?1*%R^2a4SkpP|8uC>_J#96eh1X1205ysn@`DeyS6laO}VD^VS>x@ilyTI8v};{UruP zTHMW%wCgtEi4{wW_5F2Q>|ijV<}N5g<3qnOQLFiUZ@`Z~bv`;@9-TwMwEdIyOUAU2 zPoA5fx*wBm6zc!k96YdLlTJ{XOiY>(UX&1>59;ff@;NFBbs*qu^Tjt*i~DW1qOmG| z87~TiC`uqLO96@c&vJI+vazkc#c#i!{)y@_QJ+Aaa|Ds}Kg^Wd$3?zjd_6&>Wg?gS zL0KZ>pyhp|JjM*J+)gQfRW&=9n{s)UWCf~t4KGA!D_--v)s@8YG1ge*dTh|LcucW$ z%}s<;!Ebs`%MqW?QGDgqWg(x3Rj;$EeiDA(E))_61)HKGA)(vF&Bi4N21Kt8q!bha zk`e@M{OIAsV|`t3^q*F%M%6xHYO=8VC0(|^t0>N5 z2i*W~0PXY9dG!SG@qq&WZAjQ->_WO4Xoa@VkTXA5iU~9 zR$zJE?cH$S@2fX zOmx|7U-q`A-pr&YAN*{7*)#yhm~*ji=1Ao9weq5K;4Mkf$9E&p2dxp#4mcwRLk19H zp7bMjl7r!IT`(0;|c&>+w-m=o&RZcs*qVLvvJyGvwwi3`r?3> zY=v}n>{B+RzG!nL#7>}NuLLmsUi%)%>K<1msqW)KBV?rrTJnNYPsMQ_o!LeTW@ObR z`=m3QKfp0M?(Lp@C{NH{T)vvBEZDD^Hfu7p!LF_~n!;UwzH)Y$8zcYJ@Qxbl_e?g8 zZ(Lx&YpwsvufWTqP#UH&N7+VPMhCctZwwE!TgJW=yU4~NXicCmQ9^9IVM!4TyUB`W zbuW7~$v9}yDe4lx8IO3eIV~5)P%{!Ff`^E#Ip+jK1-o@$%LirDawzoJe4d(iuO!g3 zc*OtKX3jWB6ELfY_04v##KSD>9r;}Sspa}5xi2F6`ivAh}HMlrwrlyhWlM0IFQ1awuyqY5BvdtV$GeJ!-(?YE^u1;bAvd9ST&a`PB#Fgj!zwXJcUIdn zB0&}kjk!5enBh-?eX{{OrDKvOWUx#y`C-B5st4CK`5(G_TN2qA$u!;pacRz*D-Dq& z+v2d{SwNX$5Ypo%vr`H>$K%i4yX!(xVr>nQIR~?wUXPy&rBhWl^R^?WrnaBc&t=m! zc!H3aMmB=yvO27_mrpy7MqLdpc1AzF@n9pR$udwTklm2-bD&bQf}^-o#zbCx;Q&~=tUu}{jfh#H?YNvgS%njRg> z=s2pmH69&AH3v?&#sos4_I1sB0jIx?Rxn_2dJPlL=lD0VMY=c`iv&X3`u>k;{{KCJ zp+mIpvkBUE171B}pdiDx9x{NRF+aLbhG}0^OgWo=9KZ>y zPjb8%-Kh4o?Xk@`;7zXbq?~I~9@@boeDB~g*K}4@vS`nMTrg}L4sqhtzFOhJhWbgx zAhONY`PJ6>gJ87h&=XJvA7oq-%l!O$TJYQN8Bj26=_v>{_14h;D zgt^0D@B;5guXbqP8#7Fx=gyW2CW$qui_YZ;b1Bg4xAc{P4oyB(okVC>kmmH^8nBSh zEB)7}Jh6@&=R8jvb>Fp+Oo{ci0VMdpMIen~?SNk+05!0&5)i9-1}&iPH2`KlOh8t; zK@a|#xbisJ0t7VrKMlTB(?O>+T^cSp7cGWNA^*4Z@67?|i97jVE`T0FmcRK6@J=Y8 zF*1U}(4A0Idh1onPwL}E`!RoCOu>c=SS~_C&x#cE&S|^fz-Xt#4SKmwKrK$5RuZF( z4~bBlJ7#Ew)#(C8YTkJc>g@*;&Z0-On=EN0DB-+TYf$b3ps zvp)dtd3+eKj0X=_*3(a|_Qo%g5{%5^%y7WM-c{B zi?`hP$oLh$Xd=wNbg2e(o<9`5P-jw7r%*f7m+URNKz9H0aK+oi3rbmFNqHj!#od`y ztlx)7TQd`Xr~0%h@;y_&6DCwQ(CK^_1I~W5rPIXU%R?e$3=ey0vQp+gCU6oJ{LtpC zk%mA#H2EqzX7V0EI9PVFua11qXn$&m;g3#dfVGeX2!8$*FoK@*Xh~BrqhYiI8P*~-oQRn zTE^umyVt#xWE27?wPfq&h0r=Fkd(d9oKI~&pO8U+as$>Sy`DZoaJ6*CZ(!j~wn;qj zawZ!7*=&6&a>?=OGZb&^5@Cg>CRM&*@!j!D!qj9ar()S(gE-?71VieJZ1pb3 z_e0ReVpgIo9n)XeP{CWh0cwZZ^h!hNeZ%|S+?8**-r!@4R>g}zr~*{%yG*y@oKRhQ zb{UKl=mqSSwpt)g;u4;vDK6KJeSEk4I12o>qCS_1$@i?6I20d;O5qXK=O z7#bCl@{ZwdA84!Qr&!$fK^j2K`AuaP25R=~_JnN3Nti9v6vW=oetbMGhUpK$G`{eH zZN$A(c2*Rqq^bc_JXAB6ko(^)2{e(7RASF(9ZdS6Q5&uIr!t&WiN6byocB@j#G{|H zf9(DPltN{rnwIcHU!0~B9GCwHxmm+H$yvVs5*Sa_lc$*3P%CBY?Cf07(4 z@!>K~P8^>; z>McXCYrrx+D}L|JD;scmc(BzS!4Y1mkBLTMulCCIr#((L6Z9IP(F%tj69(HR?_QkC z`fOws(!_nV<~o-yLX7`B_d*BARJ6GOqunG;oAegFB*5qb=q#K%jUAvc`IoWp)_vEd zt`Mg#cg<`@nU)aTB9hXg7eyprzXLdGX$0V%AIApR5Ak?21qi>H=msg0z?Txw`BJ=e z2IxwmlEyZj_81yo8LqXQdkzNLTL}qL4bpY~&DS|uh(TKLw7oCsz7A4&SwJ^KT8p__ zAOhO70v2Lh0I8OKF;7Xt}tn_P7iqxCJ+sN&6hGqH!qKMfrpcGP-moI*HUu^-8=IJ!u9%ggu6Y4P(9L7tQN6@e*>>1S~~NZ>wvHXu6AM zJD8FJib);sFM6_h{hs0+{7!cemhv1&w@~2O#6?x_HCP1(;9gI zmqQvy10gZd^x14DI;tIE63~WJtk?Lf2QZ-+#ooXMfFb_9u-plw;wiP2r55buFp5?YZJ(A|`*6uii6m*cvS_BK_Gk98rz zlbUKh#^`W10dWILU0v?ZXoMMsUACDWi}pYaR{TRZv;vs>X7}@Nsxh?dzS1#xz^s^S z`{ck4-3Ifdz*A=~?0CJY6x^b~HXQ-G**ir)5q+qtQkiqNtbX}JQZf{y>*5!{tz{1~ z?N;CI^pb7Fc142+%~DQ?K^7tfu^vl-EJFxQC^8H2Gu7x>&~UUsE}NP5Tcp_O5furr zc+W8TkG(>4s0~A(qwK;I!oXDXTnRnwD74JJK8C_~1Wow5_|&)Qkl7Y@zt^5~g|3>j zJA8%;9jL!V#gW;@Yr3DweAe{avZ{&3$!sh%gIBy`ctg7Ns z;k5+KwsrPO zs%@vt4B&P+*0)h#HDo6EC+V7i#MH?$i*3x4SJ9!=bDv)xn&2EsE2OcmBlr6VXYA13 zc74hJV93DR`Buq2E5KK(MI&P7s-r|B@~ZmtxuKDms-vR#Geoa~%t%7ma+H))i7!#8`E(+CLURnnIQes@o%h1u^@TL3dUgE zwaTu%*m2mpb_I?5>Dl0rs8p8(kqItKDD{{I6P&oJOz|Pkwi;w(`+j6`4qeeX16P%K zjjyjBZN8nGskZ$A3P_&mDy2FZW#C#GC7rJl-=B_fU?KVxyPrI~X#fOHGi!59>*{x8 z@PkF59{qCHL}*jZ)iI71uk}m{Mc1GfCGY(FGqc)3QRQ3iN8U_Jurq|$Uo@~vmld6S zfPtqM#5j!wHt_ynvPIZ zgxk4R92o|7!EA}vG)u?y^!E=2UItoL%dw}p3ODo)ZWt(=Kfo&cI!mFx?!qQ!e)F3u zD|=^KXjz7X9e|ibV;fdN3*A1Rof@TGZ!@*eF$^4zJMsi`v4fFJD5C47R9~PGC!%_N z3w|6LVnG#Zwhlw%@jjsv$dP@4j|CIP5$*HC31sGWcKalWdlYho;YC0FVTLazocwsb z-El6ANzh+n#*sWjzz3jb>R$liQM~u!;D>hyr^gKrZ}8MQ!Y>nj8u_xyi?H?8%D~v~ zA{}sBv1ILH$YC-NB<}=&0$uK~=f|z|)H&sXBI<+z67?da9`F64DJNhD`}2-&(%EMG zJ-Y8rVC-w>2r2o|m*(kqoKzmd>Yp8tTnQoUzp$yqf?MHgMl(nV@x^7EB9{2QOkiT{ z_dxc0NP9{R|K)q0cc>)%L_x1B1A^a0Ke=IdP>hZK!9c3`z4@m7C&y1@K6;!Y1JsZi zI70nMFM&9$QK3KXd2uqYzP~_uCB`UCdy>z{hNUXAF*N^4fBhF=Myfve$H(-)m4j<} z+wSoDWJuQa?P~W!YK&Y=Obia)D`M4($lC3~0mDcwydQKe0yw7W0g|lWFPsSn*WWug5GXvYg~jp2_!JoZtLL1+3DHT#loVD$jZcr>V-&+zC)sV!4(4;a z1oESw&YNFgc+6nNa(zVcT8q0YbuWF$?=;#mFS>TOo&gn&B_$f0CyXk=p7M}P!|?~_x6@)$ljJ)}f7sk8 zT`nLJX9kZ;4v`~xDpD}#4@7jU=pOdMf|n?y(HO24mtq2R2*;2Hj4r+#vN-JS_ez>@ zm|ld!YPMTY#h9f@W^2Gl0y3{%FW$S{h})lOW_0H$D{r?{gkLzHyY*>P3}c~pF|@+2 zbebCZ+4QRTd9zUjKI5I?ASXW7S<^DUJuDT&BJV4Ix?AcVdHqv=CLg2F{+}9v6j5{f zn#F{YIrAfeFlw4C((L763g(7aUe>_UzEA z{ISqX7BVT)^+d&{3^h7B`>cSBgeK` zbHdsGDd$_)?jWCw3yw7!LesPOxXAB;zr>K>1D^1;yHSy5mXrNJ$D4jWJy(!{<{U6) z%H8=S%_c7{3%A!0ndCkn>~FwzV)l2fKC8L{E{Yk{AQ=(F_D!KtxNUBA8lS)g6! z{%m8qhG^tdug-Pg0Z|vuFG4LAr0&y<|6djWjI3PMWtkIR7`7iXcCSiJhLpYoCE}M- zc5YB3WkbOLKUrnVsn3)S*tJ{aN!%u8LY&u#>3Jo)&+j%QWu4w-tcrffy{Uaq6`kW0 z_F3PmTLO1jHB5k*Rg#mK+ONLLvSJ!AIqpMj>){9VVFz%t?wx}EYsBsoNVCmwv|!R{ z>D(xXU!N_7FMhOkg-)sg&m;2VwPE*=kBUF6y0e{Ox$Uey z>jl>N%m9um(yrGidmU%x158k^PceR!L@pZtE_F50Pwpw2&tsszZ_h;|?Q$WyxWojU zex`GXPL9L0z?P$7-hD+Y=mJgdETP{I0HgKu`3M8U7&zfPB*&-6p@)@__Gwam{D^J3 zeeeEt`2_`@!jCYsBdbY*Xd?K(pGPde@*2cAiiy9~mxTFYp~6Iu6NjO#{;Ulgi(8CL z{qO_C6!7*kGn4fBFPCCUbe36=QUkWZnI#YU{kLAp(32+r$1JjZ7S z4i=!l#7 zOcG8O21a3AJlk)>^;T1r**%Q0QZh1^%&0B?;G?BLOgBqY{Jb$wq1eiq@h0oAj|+>K zu(MV@uA-I!cK3z5P|{vins;$A31aQnmV67JUfJY70>7og zvoY~r5rE+PnrBC2G8|?@m)+eFhbPwgg18~W3%`z>GmKT;8Dv&tA;Hfq;D|rkY_(CO z#j)BlzD>JBpK&!AH7!x1tae-4+;v}+(II>j761CalyRP_=o%LQkJ__Tr{k1CAv>I7NHnC?4|sy;_EwqVzg63 zgVC*=N!Z34aL%?}2@11*Ob`C(_h1exEfeFZCAy_*3oCHh2m7&(qg95~jyzT&eh0j$0qE@CkI4Dx}0} zPHX0+mSAg0vA5#lxK1>0>c2+jRk71^lJ!4#_QaL*|0CwyVAOp%mrtM`DQl0 z8jQu%Sr3V(mcj?3FSL@y`Rw^1D1J$K4DT-&i`30cDQrE>vtHR=V6iw}21DRfUJw(* zr(vW`(am-Xw_xJ+tHC6Ub&^;ntK{x{ZLr#n$(<0h@ojlt15Tvn=SDwCj?0H=q#4CD zIu5yO;zyb+|4zxM%fZ{433l)*OIZ73#>Z4zvQ#ibJ`St@u{HjcZm0o_>I)Uv6cIl2 zJk2>acXKw@;|OQ-Jp!3X!XUzJd$ge15O%L|gUF~zShT{rr|#*~;ghmq{q;)`4g6tBXnJgp|MP}gY+l~8pVybw zVlg!c5m%!8g2s6W`#BJ1c)o>k77@d*PjG;c(eRB|{p8Ywww5bTIKx%Lz&)b(_3rPd z_ieeh`k&u3LWrgA{{vBUg!@%;OM{i_0x;Ew?(B87L&M*0*&}(J(GicIVIN>S$T?4| zDe^d-GGH@ z5xNzBlG~fV>=xW{K@(7yKwmk|f%pRI$+`kvSp(FOa>&(o6TSfEwndOgtHcaP!zEu1 zY;F3$Y7+Pzg*K6b!?TyJL0}_FjQtlMWuiESH!nsyk*3N@;p1*9op3Z zmTUsX(`JY7Y`)9w!m<6^;a|eag1|}(A|%9u2Q-##XZI}dyg^Uuf5(PU#F(jg7!mrp#rPHXA=nmp09~;(ivc1*nj?;FD0j`%Y-?lEAMAeZV0(LgkOd zZu?bBFJfe~ziL8(md$`qbGcR^kN6PC<{SuhWV-|x*2yLjKtq{H9-t8AF3CNR@qK(;cB}7w{>gj}1Q!>9 z+kdnONS)$~qFgvUvxy-Gs93WP&`>UeQ;Uu>I+DjxmjD56N-|9zfGP*)6V49+9A0{6 zh-Xd~q(%=vEl8-t%BK5y?a4!H7bF6UEt4<`g+}y$9>8wlKto}9^5#_S_;L`8ADog9 zyuwn|{p=C^9rR$}Fr}c|(Ut$y{Q1@RZVPY|>T2h?^0<_jHli|BdL<|qPu%nf7L_X) zSLrkg^$X`ZJA?%d8F_-MrTW#3&X@|-({cuoS#c_6Q0Wyb54K!qaRcyr8ok!rdVbP4 z6-D!!<)fvp{5E)u9*zPU7|8s1_JG9gWJ2@eb~Y7E#P>jOx#qu<`_TT40c*>j&eIpD zKP7jd(MUfjq7i=l29ANQub-pQ&ewnPy1a6;U$CsdfeJn$Z*C6`HjnaIk?%j2lx>L{ zDz(K}_<=Pmp{w0a*I}qEb7uvnO6ktQMYOk!>n^>K;B$Qe<#ycgt!qEfdv<^EMSnxD z3~{dyWW}OkcTLQCl5hurM`xh4tI@^A4271S;(A@k;lb6xQr(^n5(aU`V1Q#1Nhol`@z(A13`WQ9X*$M^Hs}f<4q4 z8#`|eAkcDW74kCQrgKAe8lxQ1WCuo-W=jWtpA8n!W&ye*0_ADNXTW9iXO0pUPc+vT zi}+%Z+MIbO=pO7W+K&K&4o4^C~n#8p%MJ*~|t?AV;J~QV02cW!GeMfz7 zg~?fFzPY|Kt}h(KDvD_+++7s+>19m#3V6U;wr_4T9?uKNUR@}{EvnumqMP6u&SAsr z_ zbJOH^`>|#vB{VLE_l&4Yq4*%C`WaERlKO|JxI_ZS(6`xU6d$&GKl5xHOTB`Is_Q}q zUdUl>g-4LvP^@q1Ld-uaiTq&g4K19z1}^1!02{~hroR>M@dS5q;4X~i=ktx145+ud z^wG9}8n#Ge6=@Etr2|&b)CqgI(H(&a)&GaDw~mYI-Mha*q=yz5Kx#lndg$(uF6nM5 z=`QI;N=iDUK^jD)LlBS_kQR^@q!dJd*Z4i>{O;#|p7XrsPi1D$%$~ikYrWT6pIJF4 z<_JaiZ`H}~cP|wd--KCedu#A(nuZ5?>bcem1_Qngf zh|>)1BVe|=F2 z1IO*sp?C}CXS+qw_y*LLy+mj$QK5|q5ZTg4K!UtIp#>56bb$i7%G{TXAlQk1@4bd- zy)T#c&M>7T8z+2tBnO!c)cn4f$`LD_6~|Ne465VjCKsSA+hMAK?3AEqstJ%=4MQd$0YG{omsVk z*2EoDXY;~k5Q4s59yK$NmtV0W`Q=uahVJKPu!l*-l*&6gAl(wy0W5A9#Sl~X&oR2QvQ+x)r!4p?eTF|sDMhe#6Jh`Uar*XXqPO=ET zchEcET^FwwpU@^9=c3xI0LE;}CUyht+`aLkG@QjphOfbVgQ55b9;!PZtUgG0VAp@(f@$=anFV(*<$nvfKf==bG+81D9St^a`ot8@N{j*~J8D*!?x6>{r zEV$mL87!Lu7z2`_Wh&u77=Hl@PpIi?&w){3)y#X*W}dC3))ScQSk!)aNA+~hvT>;B z4c|&8K%7)hkCs7(-E#~!XQu(L?Gd#R$J$6$=9m%=VJ&2SNR^hvklOaQT0UDck}}t=cZhjGeQRl*Q*WTNWxZ zVucXFqxyL341Twt5o@}6kwzWg7Y;_5UqISg;8f7L)484>C05cCl-Xs=#D5%Q|3RXRE*u{f@>@i`>)#PKvN7~}u!q{cs`R*IUN z8(j54%JqSY3>^2m&(4uw&6Rz`C*c$xe;O5dwn<5>`-^TGx*rts?F?|P>Q-*owCpIP zMH{m0ll}lCmRydy!#uBwZ0Z=0>A3vJ%#ku{@5AuW1IruVbhHI4LL-@7>)yvW~pk zNRHl2Vp8oLNkH9P=!8e1iIF9|`FcJg+qNN#))=e7(Tt$rO?0Yb!{yAu!3#Gc5O^sn zcy#yWb`mev-ejfhRqA6Zlob=fHU$R_+kY+(M6nQ&O7p)GhXj24#;D?~Z$cjOqkmlol< zS=dbm>>cq^%`jC5$0gzG(imBcH5|JPT7K&G;vK>`WrB!g-C^vXNT0qbe_Xb~&Y(?~ zh6Nq5Zu5$^(EBAdy~sByFCwl<_mVdelAEcBA&IqhuqiP5tRV6;RDCm>fqyN~BYkHp zn`DJh&`qwE{%)zj3HQL&eMQtx(`FpxVF>Y8N@%gJOJ<=n@WMHrBL?{HzTeS4V2ajy zd1JmyS3|asv7m?jYDFdejykk)4=)XVAb&kj2%)~0^1dPrzk(-~Z?YC)qpc*QE|+-0 zN<3hYOrDwE6;~h1$lb@CTpapbRjf(PkgJm2uD3_qKw77QyV>&RkfV=fp~rJ4Yi-$w zNvI7{Mdj>UVB26DRoqduF@!giBw)U*(>|!63J{(k+ia4J5rZ6|c{1p3m-=YpG9L70lHixInf_SZpbQi5K@ zr|X{D!=mvVwMwPtUevGgLSh=K?^2i=3+jMX>6_e&Dxsz!Q?KpMbMQX>X>k(1o~j%T z`{2Au_{LSQC^MbgL#q9ZB}41nWO}RVA)Ahn&UVkGsscG<<0fkebm2-bqnYeQZd8cuNFO=x?*B0&(7Ug^DI zu)?bq1@BVlZfzieE({uAP(QR%;wO z#iq@#?-V1R9hHrPlS3-0MsYD35p~l*h=tbYnnkYS&sO-!$VE(tyy*Va_hf}=Wlb}M=A^EU67)kmS3i5PFTPzzdz50_O&1$^d|t?t9pWXt8EHt^16;fPA!B+i zdqdTMFBXk)15qSm$A(p_b>fR)*PEB?T`e+hNU6m=qqa}-+1e=W2UA%;8^^)YzTk+z zPeq^pNeNEe58)mk3i76kmq;VIVv9<1!Rb@;XcF%S#%hv$OLZCZbuTa%M8@D1O)-qo z!Ea+_TC_{eU(k>89K<3E@-KXYGb&M!wL9>NYJ6&k^4sy>dR?*nce@)Fti{Fey5OpPJP@X_N^IfU0-U=0o zM`03B1Mg&e6`bnUg{c|77V3~<{wNkgk0`F-gHqCEz7l+v)?c&KyaAM4)N#wqG-n>u{XsrE0 z#gm#Hmv1!!m52Tb=^t5MO(x#N;SjhDgLHzNg;4KzC~E%-m1XIU80wVQYUbec4v$S! zaod;CDm4yt?0FJV(nKpVqC{xH`l`cE$t};h_x42k#uWD{TwoX-6likV%68?kp*+qJ zz54BYeG2D|*(b2<4KBjC7(c_Ocdz1O;u$t$6@+ZKc4V*KxccdI_lWifMmxx5WHQaJ z6Y4z@i}0+-EX89W&@P8nJ=oImDWJ1tg=af#rHdDR)5u=W7YeE<0;pKF0 zdkUp?wOPSNcq0ha&6=W0y0ah42`hc6E({0n?Ve!<{(H2RCtcCaj}D*lwlgt_M~Gge zbhaasSdKMaENY!^2YwM&JuBju4$$|olBG;~R8jS^!+xb%no4uAmz3uWC(26Gh zzZ=J}@=g+0Qc*uj?nf-K1XMCkHk!teSQKjU8(#xTac+LaNQ+XQfO}*Uq?v|+ozs%y zTeMyM#Y>{4$@%W@KQX9rqCun-^ysf3yAsQe5DJIl;5V@E>vPMgqXvw{Y*RhzO zXzXh#amVq}_m6qt9m`*OViX(WSk>ojVGGL;P)8+$H%sNh=-1Q9ARnF{`ZBZ5z!*Hi z&)G$|)48k-!yXBAY=LR_UR(RoZd!2yq>B`><0fZ-@qH+E8@DMeF@S7q(B>5<)sO&G z1j}FybqHNzX(0X7dCj`(wMAC$=6>7CD)zzP)#5yEsq$+sb8mA_dTM7s^Xdpyc0ck+ z@QmMIdpJd1e6-Tt8jSSQ_Df2<#~-^vnfR+#9a9<8;1+}W)eY5B;V)3=!`)@g~XGcq?DyT~gBPfq03GvJ0}UKB{0g#-u$R9=40u6N}Wbbr+(^m(qfXN0FrIfbUE zt>JzQx3Jb;IqnoU0Isl$yVd*LB0}9@e<8dyU863G{vjSOWDIt;$!!)B`UVPxFfa)8 zOUd$=pfPr5v8Kc*$bf@-8b||015X3Vb!@nYh)ed4+MvBNc89T8mHW+HJHn(Bi3)xY zp(XzAv5rdox8gln0PP8CWNVbS6OFn??6AVh@Z2KsNODAbkcqX9YOlqYb`RT=XyPuh zAN@YW?vV4ws{`;idd<5mwI&y3ZrI8r0ywAyx0nO~y zl%LyWaHl*_x_K?l8GleDN}V$QOXeFe~d`PsPt zYlVVITH9ZoV)9^*JDO;LW`%;*4W%c$F++oMWEW#mPhLU8x8TLshK-3co$aYQho3)j zVKMKg<0t8O^#d>T#)V#SJKJsjhEHNbgNKpAtPf7i5%RMK zpS}ddHP!5{Q}~d`ZQsDdumYB8vZJ(m+67*@3K}%IYsSN*lYGO-j~hW3e9wjELqlPn zgcIpQJ@vxdg9a~skBlLQAU*utjMaRMZ5q}O4 z%3OpL6ede<4NF95;Qktl>Sng=>M%oFdwi%H_d!=o_2AI(QtxPB+vypfU@Jcf8q$zk z45lm4VO*kP47{o!c}*WQHNOBzOz@DTwe`8jx8c^mKtdE_K)qvs$~#c*rXp<9RQ)37 zrecJ8P2273;;B~xX$>vfW}V5=#jKeYTTvPpowL*mkYiRybP~Mc!N*d8f@CbH#8za; zULZkGOz87IlyV)UVJ`qA352UmZ;i8oj{WHdBt7Ha0zdN#Xf0dw zOONMspu*T(aH6Ub=_pjdq+Stga1V+>Dir-{NvhAm%kP>&);ICiE*Dnyftz%t`}f7` z-*WQN&7zlz(VnsziD10l{5a@paBf|+^#ExKwdS{k>tzMbUltC_SDjbq6)?x$NUQ)* zB1Qrw4NHlPe}K}YE#$E4=J*(hPIFqwktc1yvfcIusIxr6+D9*C%ZS_YZ(ePqi} z8_0d~Td$~kN)872Ijw?1$YWsh)?-?M#j_PB97Rn~ZuJAj_X~2Mpa4*=tAffw%)IaP zGl;PxXT^LQg5dCfLYI_M5OMuXo$7|HCAhghc%7aR3}oN8V4x+pB8kg26ixg;a{aKSIoS4J zHPXK>4MsK_W`4~3eF<=g()Yt=mES<64OpbRL3Sn}r3%wdgCET0xzo>pT_Rn_3yjn| zX|%6q><->d1MN?JABN^#Knvk-fMl)!mnts+1Gzg9xh%c(*<)Y~T>91nT$}NDx9><0 z@*%1_HBf{;4OE59CV|qsV8E14`v$CCM7LY*JyzK&C@f6V-UdB_Q?19HXA_DG z<}P67B*T$afSJ=byH%v)68)$5q?ArVf+M`kO0PD{eYM*xMfcFY!jyQftp@wBm}(XI~7bh%|IZ(KU_gb1OtzuoEa^>*qHkF zuxwlN1mcwYO>}upb?uutHqO6*kmYRd&KSF?x@JjNmGS=JK3{U=+ZzCp@*uuIv{`!t zGJM6+#=nB0qoF?0i;wIYw?}j-*Ggpg%y3$H5k_@z)5XJ5=sh zfSk6t>^;l!F=h9#FHT))=q+*8qh;(W`=)`Xa<{R~QB?)zJf(S)oI!WgrZ|Vma9JeW zuXjN5NJs8MmPB>T;>#l#{jm{oGEY&^dVyGzZv-l)RzPyU`de`v$tJEqMGt7VDbo9G z_zF#18#%nj`u~bJ~hw-!93q=~V6>a*I zDRrxvlMzZy{CC=6#cb4t(_A2y60oau2>k($w{4HP12Lwp)3a{@_=rZNth~f@=!Qh+ z_mz7_Ql^J$KS6XwdAL;3`o$|!)<^gzVpimorT5WBZSe~^f0%$E8$(5G2KXmd)3+pO znk}UwH|%ZmNJ}byAQ@f{asuf`aOv_q4v>Qlx~7p=AHR9soXR8+4y6DTZ~X%|H(_G> zW3D_jWQuK+D~{s;R2v;`-)s8b8E^Zr{P*uC5;xhjjx`OPx%c6(!3|*3lo2SyZeS!0 zD~HO{b-?*9Et3(7pGQ@Z;2|hX-`OswFr9xck7<_23^d|V4vbgtrZpxc;PEd=?n$ea zu(qtAno=-~AM$Sv&Mm@YepyxDzea4-W zMxOaoS}qhUMsKdbZBNPlFZd|Te?arB6M8C=H=(&@;n_x394AyM(P) zLoMQX5G+zWUDo(&g@h|ru=pvQz@p(g5Fl=UA`%@m1-8vWk5I~AFa|YMLFUgknI`g+ zMr4{Ye0?61QkXx1jQ#k74ObtJ8%lgLhyZ?~1%b)@87N&|6oTp4qCaX+u_A_pxYQMh zu69}a&7TyB)PmEA8FkgbYT1(tBaWMUQuXWBop;uU=7l651AF?omG$0`26lp~zTg$F zPZtRvd3)#{{82Nv))3fvu>TivXp&9}J(o-M9i6OVNRbxRqJpBlTIElA^?CmA4X|M6 z1xeF3ty_^yF^5=allA3J$6beR(uO;G8=A=#+_SLOpe0JX1oJzSi+6!^F(oWTez|fV zay1`6Of+ydh1UzE zMG~qol0A5M=x&JTf*P1BcpH+J18nyKhzIPiZ9gGtOQLG&png0(DKhyape?~!M{j{g za86#nzR6cgf5q)dxMbGnTc?O^6)1!^4y6DL3%mn-VM)V1u;O}0nb+#ggYjJKQlC0t zuYa&pFra%y4{{!dqhKlWAU;JiO4lw4*qbnzr^yi9$(J~<>ZSete{4j1L1LAR!s3v8 z@g9;d&QYi)a~eiW^n~OpILMhkyY=#Fiuz6OKeF4p;jRj~MD~b(j7>M6i+&OLdcR?` zGONQPEvfbk4M>NHX?KJ5o@*ugd)N@Q+W?Uolf(F9**5CqYI+V&# z?EG5Jt7iqAZB=VY&+Br9=XEcZQ+M+N=<@Cxlp zWrM|gf)*$?8H7umz3D7;)ys^vi{d>&wpa_z=3*h@VpjNVvF%pq7{zGQ@8uOQ)+61j zjxGEOTI8rF>l&D;xQ30Ljum7K-^W*%j9cU{JSMT{gR98HH-B1ayGuZYv5q(`G9%qE zu)MG0`0gf13qWop<$W$60x{1-JM}2yTCz~q&bPbWzkV(jt zOBOj^iOi4{E%Z*}P`sB4Cy^QGctohqFZ^*GwnSG7-??|%`bAbt=IA`REU($pEAA71 zpQK)+ndK`FF7qlz*4pOOHGplkzuw~`K;d$rm*@t25V&717_d$`gpG6GW3xf>xi3|& zrso&PSY(lb_cL(Yc<1!uoZ9$dk%!~zoj%@}x>QbhHcC00sE077`N!}lYSHUT(e`{& zzv7|0k0C&o@4>xm6;11WG9dsk=TIuR95x;)mf7$2$3xPB7WFYt7k{8|6dbsIaUfr0Y5ZCC11~0<^ zo2~9m_7}_bf^U(_g_juElQ2&@DygJQdPbgP^Paa#)f%#}5@33~_UOQ?jV+obdYMKp zAiarmNB={S?!Ar;vXZ#iCFOL_kS&rU`6^DlaYk+hy(s)R1#2L~%#x2#?s_9x6Zxd70OtD&k9w?T7F@&(!?jjW>4@6HLqMXd>*rS_0*)mRriTzZv-GwT}*Y zqs|+D%zipNC#~Lu@gIN+ZWXb`RP<(&hBrjhF)w4H7GqC9`$*MC-PSo=f!g7r;3RTE0yPaRY$W5hho6&|r{Pp^q) zOsr_Dl#Poy5pJ5~y#Bq!(b?|0Bm$bHg)|dAc5I6F<65iLPjI9Q5YK#w*M)FqjqE65vxZ-XlLRH%`&3)hp?Q329 zBg!1zQ(IoiK-1iJW^<&>grahE+16UETkQO*%d~%fJYr|6epdVENU5*JQ(-5{T&tt; zCtmnPen;}7tS4<#s28MB2}*4-)D-E4=G6E7SD{54CWJlLribMf=l6*{e=X>t_>!i| z;J^D=jC!E{HWk5|XG{2NF}K%;V*NHbf1xBM2y*Lvf@d#Kdsip1jXDgue@}j1(MVbB zQ?nRr-H)}{SA+7y7fM%#9uq1^iftnuwLw?ju%Dr!<~aL+*nUepGM>j4`zM{QGK~|C zxqnu>K^DfTj?3B_dNx2NMkw~asVTythKRPYYQZ$aLRG+8TjgSKD~7cwrrErd1rpituBo_Mh&w`o9r{+ zLrKT}Zep8lbKg-ge{eO{c|SWz#{98Ev_Wg=gRalJD7Ne#P^xELIrix(_2VnS1Yc0F zzJ~QqRfwk73o42ks7pKQO%Zo&%5Bn!V zVaqYsw?j|Ka<3v^h0R!;-;|%xVXi>Xz_Tipdy{K7GK&fp6O-)%qTSao(?cIN<(^bL zq~3oBo#kQOv7j{V!+MC}PxzIodvGuZU^*MG>^yuBIihVpj^SdOX zUsN$lnn0b{^C}Vg4v04JeP}B`O!Jp)>)Sf3P#}v0$YGl~Rhi~X*sB_r>V($(;LM4H+)OvfESFe`5gHm9Yb?vhm=eCGrAN88XC zDqEQ5(Db9=vXRB`PxkK+$=|o1?g?a!{;aHw#j2VpGmZR&+ zUzChURu!OxTc%lzIj`DvYP%7w8|n9M?d*;K#6U>Oi!`Y*^Xk@++s2o4!bqGWEK| zrV`UEQM|rOK(UMPi8C_pe-LjW%D*7$vSIw;QW4;X>jTR}t(BX|i--ON0%~lWS){vJ z|1ctM3xhT7u9j9^x_sKFn@YJs@dg4B7Va3^RAn@RRj>WsPEK*?dq0w2MS)2cwK^vr2aA&?e{1w{w_0Qo)q@r5Zp;M$b zCrw`wPbq{Sj=nEkX4wr1l%19|A^5^{k4o_Vj%6s_!Y9O8Vez{*4yO$9hg8qoe~Qob)-c4GNX}vpu~Z91B~BD*Sj|{gv0O-2;T#nn<0Ox% z5bRbw&g?-Qu^oLJ;0_tAAj0esUZLXqR^_GG%>jfuCum|mJv!9ijq^}y)l&vV->%F-9awmtvX_^ z%l0p1@PG-|a_DcLYnedfvEDA>zK?e_Q?^vJK}>?sCWdoLHYchD&O!SC4Mj3}IrgU6 zBP)~~yoL7)X#8dM7a@2|Xv^x~Iu7a_dbC6_gi{z@foC#9{_Ei4&FSBdEG9H%eTNrg zu>2ooIVKbYg7QPQw&WAH=S<-ICbog>)ocx+Q|7UG;}jvE=#P!~SYD?42t>v@8p1i~ z=QQkAE;yFph~hEa7cov(%^PnBuPh6gGrjwpZN9~yW8Yc~{h796{|20P^t=LvV!iPOH?HykHBGLnTuyCrVENab^5Gt04%9xA%Y3DmzIT<6*Adi$3qRM}w4Ta%cbotWSNv+}4 z3qCr?eYbY^n{Sk>y?A7w0;!GP>bH1XNG|ul`5!Ln*s_(MAwq7m+0b(H^k(!+kVnFe zJTC5q_-{y_^xq!Mq{yF;uIF&yKUoQ3wEt&Tf`T-z#kE0QI0*~7VbFTIDb*gw01ldBHPxB+*y_ ziHZFoU@%`AWzBK>|3eMz@g0V%&%lVE8gK0MHue&SfF>CAh-R_;2YB|$z`pn5Bm%zQOwNk z#(WJf3rBX4eLVzno%UDAt|iE5%=W z`E$GWXYOydA-FU}{=1P=gPhHriFqh`XRcQI#A~x_S$_84nccr^rs3{5)tcOR)pf|SmoHvrWX@7s|Uk0O)!8$tZ9*5 zpTBw5Psvm5EkBL9mt(l(^OqN-ci_uDu`E&eAOgfo!raFIKx)>{uaXuugP23dKJ>A?!07QPVJcj z>XpLYf*8R?v#L0gqBw{b#pbsoo3-YDF{9n5$M;3bqjS0|Cc-qsqTHpvpI= zUE5W*xsEnPTs)WCNcUT1MUeg){8WXdDbD%)zc*G=(AVYMu^Wz}a^Bs|`3EsHEqzvf zI$Fib+wW@xDsWT9b3lyR3;%_xQ9tV>RyUwsT65}IJWJTO)A02dr;+Sr+QC`RRPLA; z$1*uc{?xb{0Vm%Vj(6u;wIm>HQRa;tqt)&@!T<6Z=wE3bZ@m8>yx>;)44j|KCma3L z@EwJUlcRpg6QERoB{T7yBI~scG;DTEFNu&R#!t_vu`Md>AJiy!y6|9J=OoSK)Jm*}pq+1dfj*tH#;ME3>~q-k z=aj^Bxs)|vJ?=zsh?YycKCApz_x9LucR+t&_+8+=cPe$kfGC|8e>$`&+1VJ?LvQTS znLxnfVHw}#u2$o_Or0s3Rim0S72B&EAi}hZqIM>--L8{A)k=6E)_5h~suraxdJC1%%mjpIHM9FeO{A?enj zkVnbC$%eUIC|CEamhyvX2Hj!PPE%khSy}}Lt(F5HqYA>n1ozPVOc_Fn5ymt-=$A+m zPfhfbzF#w^jF^nS0o7F1=>M_#nf21XGbZdHph$KIpbh!lPMFY;Kgu4cN6 z!-Fo+FmMjoK9|xj?g=U{|N3_qfFs5!eyP+yK@J7Xc@YUyIX;zFJOlDke?W$Zul_K1 zN1{AVMseQ<=xB}${s*<05!);EcE#hxZC|$;<#5J562 z^?ecu=IXhRZZ$XlU&e9(*Ge#Dd{pC*ZVV{PEcN$I7UoVxra*>4?}RFg5oX8KxSz4& zVU<>EHu!Q_V3n{ZTD%(aDgdDJG#?Aon5U4S2}^6jlt-8YA4WRKKl3m9yY^pQfO`A6 zue!hg1y~58y#HFVT=ev*n~CR5Ac`zO)LyfiimnF24?n!G$iXiJWi4Ty?KS5|SXM#f z!a05@ws*#!pyl9V@I29{G0p*ZcH4%4S2mBu9lsHdPAg^Ub$$~^rcAFc44e~%#N?IC zK^ZX3#+Q#}5d5aS2TjReg^bN(^$U;zm0K_qXbaS>Pn6cwxOz?+?7CKsRKCd@LpI`? z&Jt)>-BH92N%K?d6S9$draMb0dSPLi3%d1F-P=PcxInw#Zq!{dPyTF$?0N%#KxaBD z;Jfz1@%K^k%$VAM%|fT(h_e}0@+Yin-)GT=e5Euh$4V{V4vjV)iDi(ra{iR*_#|F9 z?88usTs2J&ssMhC*;7Ew|FV$QG;V|DP~{WM5c2P@RQsdw&J>tkEeCBKK(6O;uF>0p zs!ndqWW)xV3)~3tWL;(E*=CUR1DZ)A#@8oXI2e6MyZ?40;)zEzBequ=TX^V+atH7i z^nL@0+9i2@$QEjv(~pylrD#w+X4^j$;ge9wxViK)ztscw=uhvWfZe`z$|MUry$(Zhf~o9M`sEBRHe;wA6%}i^ZBPJMU^(9Qp#69y zF{oP7l~LwH^y#vAsmSl|3`V_-KazmLKn8{Nm=$#Qf00KPjz5b5%s9m;~!% z*8vfCpW>T$Y8HUT`!SgSg}d~pk&HwkvN)#-PZ4^WE>s1zx?q?5mn!kVWA&1Ca~=l> z@3`@|v&m1nVEh4XZD#IOdjBFzn$ITRyd0uRd+E>h2#*XPr8l{q_5v#5gx@#&JiS)F z0a=r#Ox4hE2Kq732;zj__DyJ`hM*^N+%GUEC61R0(;y)M(4@c=sP(P1ME%e@6$$qP z#WYN?=>@WwLi|$z=V&Sgxe6C1BRbooB4o}r_-Z4@d!mR^p_aQm5Dr!3fAyL~b+nvE z)CA!{(U6GXxmZ`;U#JzenICMK&(CaC`VJ36NV|)wmHtTVi5sbFXGlhq_ z7C#4oBOavIJDS$q9oaJqNhX+cj)7cmHq+#1yzd|Ue^w8jxv5}| z1r$GKw?7u7rEK`b;sezLL0n~MtMqYAiQ}S5L~eb(A0O9D&5Xulvk(JG!+li>75$jd zGqzT8(el0JGsjknP!C8`L~P~=!IYk0yZ1hZxNiZkN(REau}|erxbP%?ok|6?&hku> z#%XtuKZ5+`ejM(Jx?sGhIhY|g{lt|nBkO`jhg9~WX1o|)XK#RRy#Ck-Yrdn+WfjwS*Qm)E$A@dke{pq2-)C5>}`c#p-bgZjGeEz*Q-S=Wk-4 z3@w=#E(%%%_S}DBDoxA=P9KB`_0=TSS{yG!X5--v%sV2r*rGYSz}1v@NE|}2yQj!ez61vrAI?jn{$aaf^ zA@=9Kmx&F-I}7-(Y+Y>BfVgU_Vj|ufwAIfStv$t4`wV9ERrLEGfw@0zJNtY9iEa=| zxGJDfm()QZwi5~hMHG2%uF)@Ejf+*hK=?G^M~+|vC&4)5Z!dPFLDlgsNB5=zJSJ2& z&q>g0gOSwj856BGD#~XkE^PYID9^jNm}pF2Y&TTs*fNA{!YoidP~Yi_kFpU9X-3mO+C7otW7uvPJfMz=?Yvd$H#=`Kg#V%JeEx)yqj4R0rqriN zTyjK26dTjr`GYYGEQa2jOFg&7)FLj*r@096Lz#e#-4Soc)Ho}u3q&!mcXh!vcGD^U zsLM$va!!@{Fz|dqcMI_ zJw_8VZX=YU^uxYUmQDm(0_pypx)3)1C%MT{ZhChyKD;;o#gHeLUG)A~(x$1Xd^wG5K8$^>Sx8GY{+pxJ3O1GPx$K;#ep27oeV-p7OH_^V>kFc=F{l+${mR7&aFF8Zu~J>om^*__SL~n_PunIy&zeH zjYmnoV1&VjETdV_^oO1K*oZJgO7c@7cmgiF%)mje)B9P+gs$$JE>f}O#5J$cGQNQcKiTVsP)W)sde_N~vO2P2 zK^o71+7|PfCFtXCSsS^t%*66E?9~zGXv4g(rex`AP-SP}M49nFdyeou*ZClT+s#N= zmR=Svj?!Pkww1?b$frU^i|=@0VE!$Xitezx)7$VJoZ1edyTmWR@Mu=H2o zkOP|4`00g@r@wu`jw7+BgU3((4Kz7qlIU>3VV(Q6k#VsvqDo8vlf<4%l#rcrU zcUi@{Rwqt0lzN$6F{-l?q4o1r6(!3|x~KZZI6BBG-f(Ero-NRqmw-mHeir_BoZM>f zW%037-LfZmk!Rsy6QcLxElfq{VqY%U_W==;Zz|uJu(^kUFKtxhUe-)RcFn4atgPAV zVx`ib>p>ANTCARQW2EpL#tQ|y1aEjW?*6HK*4azFzidj^<+_7nYmhIXeBz|TE>gH@ zh$L3qM1t!WGH@A2GN*ZAJgw@9vJ!V*YXsKDc?&6S#ll5-1^krmIX!IVvu|{6I+|^7kowXb z(+)+}Dy)unVp77V1XPqEst~&JD*x>g9R1+sCy^9QgLS32p+0@0F-^io!LYFE*C$R_ zt-UQz>e|_CPT}zCj(UbMD3)&2w!K$!+TGi%xX}m>HMu*|68G10e_KoqMQ6xW$L!ck zj4*3xJ*jr2>~=S-mD7MPIn#0-yKTd@;FKT32KEQak`rOasd%M@k-px{npp`pp zqGvUxkK0m^(Qm@!?>}dK8tymm`eP8slPN-;b5;#>hNNB`Quvz!2rhdiKn7%Z`GaBR2Na!Vmud; zxEBA^K2JMri{`kO+1TEReg#u}6;0qoV^KrZgMtoS!>|<9bvYVETl;-dMbJx21?gF} zkHlX%k7;o6IvRbu6ZM$U$G7G_$U?Ke_NC&k0eTau%W%{M zh-4|An}qDB>a#Zng0QbKlPR>Y!`*g^hiL(a5{2F{6^wBz9U^TR4HwCGcN;v>WM_!1 z9u1Rmxz<6~UyR2vNgbwhkEIH^i9XIp^=8~ctJvqLc%xxzS5M?c?D=y9jqB{h-{Xrwjy6EOb%t#Vk;~6@7=2;X?}cnEN6xqHiHT z1*@{UE9VPcaxj|0E!`@hBevQ)w0+Ic`C>LZbGl!!J4)Re;$D4`ux~E~$bQCDPl((; z$B9Rb&vwOCu4Lhm$iGHuG6*@H==7%SYVbfg5#Qd_yc?3?JEV}=E7>e7?8*|47w~E$ zPD=SZ#AJ~F;4^S+D%+cs@)5hh6U6A^SGmHXaq#_{$~a~;eAA*q1j^c?>QQrv&PNH0 zslNJCU;JWPil&$>Tn4yGu@#=1o2)bub2;0Pu(x9rWe?AfM=f`5mv{@C*l^W!Qef0U z8T|KhgW_r;;s4K-Zwhqp6C$po14ZrHGBHU)!-p7AXl2|}=y$Qs%^SB=8&4d zbU7PZ+}fNInHrQd99M_oBQf?&qo*WI&9k30(%lt3WlvpGhW^soiB*?Rq%A~C{f4v* z)6faq;|w>Ip<|5>jESd^w#=zfdoP*T#)w{#8|By7vZm#$y7Ebz8YzDF|Yu)T^&H zdqH;Hs&^-XmP8I~Acy{aXdg4C2>ynA^dNIbXsbetD54^>jgFqf+I1m7SFajwlhP(; zBwV+!ML6LLeX*QIaDj86#Q0M`KSPjpYU*IFnkq=8I z#6wp(J9djp)y-j6IU#tZ7mMag1{WfMX(tPkw6BVs3hvohBlLPZqbiO66+SD@PE0^r z1*;tA?_&flcIGwyPwcGuKpgic$gu734Y7+r*4oBe!LWk5Kx*}APM7kKH@M@&HvNN` zP!$N>s}P$XSnt9^dlB4K&SLq2$vc*3nHZvru2mVsr7GPsNB?BacK!u{r_KK_1dhSc z-5g;tasJO843mNEHNkl!*Z%~Jo*RQN3>)+7#hs5+fH^+?_HOED#!i3E) zY6$d2#U@gk1HIiF)~lIQ8ygjNvs+|WV4fq-XghoInyolbf9M;7Q%iYe?PV4rNauQ##6$B=Mt9x1kVEWTS`j* zN9;`CY#^OnFMz?n86|5U$}?=GvqD$*%49d_feFo;OJ_aG*vPNlfL61O`+2}Fz$1># zWBrN=eV9VT{BI^C$^ECHxafxFsJnH0vJ6V)EE$jl+HgdqEEc-^2r{6f zCUNQSgv9>;<&pVU`)K}R*~0LDID5;msM9vVT(Aw{|oWN46*1gYt5?b`~?W1yFy3bY}8eEx+-p2 zn^tjcqP;HZ?@)Q>;b{Akw^COG2s=!5jO(=ONE(Y=n%I2#MhR#NBO!}|7UPsVOFY0#2GJevhA;R z@ys+TVawN(&nnN3F`9)nj7?!Vs zj3#^LlHHVG5LY}_)3zCN2-fo@Fg+A^ZbZ;LTeh+;pKGyw47zNX4w^ zTq9}Hq{OdB7uoAKg9kvW(*8xRVhjiZ7N)BlKfpw=R~kHKW9IRcBSAClVy@42<{=pG z)?s?hwE%(+lE6Fx1WiWHZ#^c1c_~2iPcCKkPKn+Q{tW{XH-r8YH!y~t6&?o`Lu2_P z{zTKB;Kct*Ii?yQ2EeZJL5U)zmcb`VLY!}%ryFz`T!M(3LifDfjF6m?Ymhd$8awY> z^96jqT}5g;mToZP)zMqSq%i0i4zwg#oj}3&zjy#-kxgz9eaMKHTDIRCuOnH=(NFXZb7SuWQA9M zx-Y^Z;(){VxoC|+06>e7QuMATK=;sqncju;IQ|2dbJe?NdlhILODyJzIYe5TyTKrs z29MLjF?=%PAF~*rDj#2-?Ws}K)TNs`0(^l^(L_1tBS6U7CnQE@Zo~EmQv^D88+26j zK)w&BZ(^**SZej*5mrY@*PP{!$465_ZE>qWlA(jab5W{O!cD7-Purjq+^Rvjd@>|; zH=X2+6UxIr9!fR<4y#c*;3`76Jh_OX2bHt8hrs@+=lU+q^d9Mm!{!5q;@BulMc|V~ zN6&G01ir<+1Sh~OJfqw%Vk-Qj_|)!zxQQ27HBVT}dzDaJWVy3jVU?2{N-yx|7k{Qo z%EZHg2AC-5GIUcvLxI41J0>jJWJz@U?PC>(vIq z1#6(R*$0@w$}5HR^-P%QED@z25EYAb0jJZ-g-S0`Uyk!fnvP9UfoJ^idaq1CbKKRa zz%K=Vq!pHt%PZW_P~)H8H)a!2;I9X?lXFN1UQZ2!iU*p;r3;5yJzfQj@apbCaoi@d z#EoyW#Z=_6DTScnNHR>#fIDdE>kIm#=Q#uK++GedMeg`PkE=!=a=b~}D9^IzM2h+S zGEX0s7kV~|F1qz~MCGFJFvr)yo?e+!ybJ^jJO&UwuROt}Cg{8=--o2!@lVM$XtL5$ zd$$vN4bm$0)$0?)_bS{qkJ>-+1D97sJeOLg)i+ZPg@>#p)9QS&e^pNCRIQO)(}Npn zZ~F`y_>}3M19xqW&144X7yrOLa04J*%}Ms+J=_0;{DJu49a=vY)@5AtYgt!5-$R0r z_fDSm&yw;N)oz4ul-MD$;J+DwU;RSeqm@sEgsfi^#U)v5q4~Ima@THsuIke>sTwwI;*Z{A;n?gZ6Bgix*w`#9<; zW;ZB6=|LKM)1K9VLJp>;%P9{?FggQp76yyap)w^@~Q@6D& zf{($v-r?*w47QJe1{bZ%G|bMt200aSeOdGajOFEO6-ercHARGzpLQzzsi=+C z=ivI1UYg2M>^++biK=21;PfS^-{-<3Bqx&((`U1EEXv6f8)(D-eqWW~CBpC-#XX9B zOR|ECC>JWmh=dmNY4w)^91{4L_xcBLBlVIQucF&JT%MePsNNv=C}#GawD6chWLvfq zGUB$aRZuz=vn2r_H+gviT*_Un_|^^s$*2T$a6(KsZ5p*(;5C(grl%H0OHonD^~caq z59B;HVf{1A3#q87+~31TWt9 z@1!5e#K@dp79Crd-Y2d}d0IeL79RsHkvs8Kn#^yz$2h{t)S4v#V6Lec_ax4omo&t$ zDrD0M0MqaI#iTTW@IOV~*nio?bDa3>nB9r6AjXaLQ+KJ_R_yE>ghzqTlw;;J3nPXV z6ik{o5wapfgx?~WVD#f|-gysvF4b}`kY!bqe86770#0dlx-D2b-!%9TPAOzoHE31D z+X!_2KjMYC0d760*kVf>>{Y@ZpmF(qW+LkLAaREC#F;ZdWNx4~&|Md|L=75V@lx;t znLt{E*8h@g$|0vfWLQ)S63yJ^JQ4e%biC2-604}g2N{Tmc)+^U;EAG9)9@>Mac&xB zi^p6TOzXZwPQ+J(#>ooq_d=Ck zsr%^$yU*}@P`4xZLNzjx5dk_{vd?&Z;e9A`ik75j=8wN1qbyA+F7wDZq}{d79=BBk zVOAO?oozSZ#J041l#m}JYr0Y=Axnh3Bg-CU@AF-o2B`|@~VbYbM?qcsm_=F3* zUf#QJ#_c*fWLKBlJcgxG9r-;`h%y%B+#(KIXYunP9zdpJd(9rojsdIz%!P-7uv z{npcw0rv*N4Kw&N7YAvrqg)D-#Yt^qMMdNvHDwMi^Ixb+ilAm0MLO2b0t$}rkFun5 zRO@0#Hhol|^WL)|gq;T(8eG{6u|Qj8+#3(G|0hCR!rx$OP0pE`jqp##W8x=c4=sOGhmTV z$$a(Wo^2=*&!5K1rl(GNel4U&&ciU6fdZDN)uPzcP|dQb3?-d4Z7W^@rO1nkU;=c{ zmuC006xjI%`oxQ&k-R|_K~EpO{8Sfo`=Um|yh+}y9)uoUV>DPoo-7XSuqa@i^A!*c zBoSl;WvrWVMrxF)WAzUgm^!4jn}3V$XhoAB#Qig(Y++8sk{g5^TakZ)Z9Rk#i+)u0 zJb%j4(>0f} zu}MjkHox9o8)4VfNA!KkoJQ3@G3&o+0r}tT6Wnsxp;ngo5rk%DQ*6t zTO(|RHyypXdWo8%8>8=si!9`A!AF@Qcw=ckkaGCisX>?s8{C?{BtWXT@8*lzb}sGc z%ie_8K7_tR@d?*|Sfl-lH(Qa4+s`$^ zbz94Ama?E}^3zh<3ZC)O-hF_4U;k(Wm*(cWTp&d3z1G1sw+Rw=*UL%BKs3>(YdaXH^Tz2RXhYlozp(C2mK)pes z#L-{Wkj_Me^M8Di;IZXbw#q}F0;h@P{4=4K2Ay`{;_w}A zq~y)!Op&!khJ8t76UH1Screfz!OI&r%~(ZfL~&S$vRa2olr4e1neY+wv4#F2BPUx+ zIceahp%$?dR9=EEh+KMx`}Bqlpb;CBx}jC6;?$zx(e~_F{8~yS!tA+TJ!vo_ZSwBi zZo!Md5AKvlDML?&da|M<*=iU=9PGdANdFu&kL_sM=vBa}-7))W#(+Vmm=vhYW<#Pr zmq^vh3vY(?hVw%mNJVK!c0&ci9{7PGzhf>)#c>q3C)qya9d-SF+sm=cy(XrE(gn` zn>_LbO<5vj3jOEzVpSgo%sfrX8MLj3RL_5`ETtOdvWWL=l92>gQW_C^Zn1_$lpc4> zFa3e9`K_yKy(F$MtO-P7;J#0;;qX8YHJjPdM>B*yk3|?GKyYP!82^yjyKe}fFN4#` zh*m>$%Rd3my&`6}aXjS3OlR$C_*rjAd7)E|Dq;<9A5l+IKvcidV-Q*Bgo1wm>$NST zmZa|sefrC?F#UknQeBm_&rn)7rX%MVXowldlZDYdv+LJTf74-3h18)h^Nakf@RB%o zz^*Znm}#DJbcX@i`ooNCsMWrKlx!WXT4n&_3mZ|>29u$UTsl&7bsW*LeayHcW9vys z)MO9y2?}-~N@T!WeM6h3eBgI=w_rH;&ke_cf=KiF!`NkMoTy;j{@yW;60BmfF5m*F zipPRKYLE(fKyOyG*?2Vn<9DLJrVNQ(desUiI^3fnJgLCEXfYQ>_L}%nu~fV-`fm7( z0}_Jd5%rJLBsHwhD733Kfvn1_;Pa&59&v@68G-9X$1>|=M;^6pZ*3(!s7N1efKy#^*LUb{G5AgsBOfo_en=j+3Eh6dErSv%JI18S*j5$kBKGBvD2yh0K8M4N8&{N z7oR<5BuF`EbH=WjBAmN5xS;w_fHs_?i%Exsl)Sprs6MzB3c9-)*oKOYld5ugR{$f3 z=Xd05(jXo+Mhu9A)5cU?;lEHS7|)r$ms@x~{wzK~LT9S}BH|ro($&mybpiRr1Ed5D zNeKDz>s?x8=tbhA**{c}PnJ>t#Gf76t?qIr(}fIu$jM`^HIQRCE_vr=u&SB%*qDAX z-t1Tf{ZD;#`Ii*uv+wpknxBOXo^|BB^<3&qVOZ!i%uHkVX?SRl#ogGr3||{wS$@Mi zbo|YN(1MxZ>k@=!?&EQT`>y9r&_OQd9QViRi0rRSVj*AET)ey@3wqbqSczBHOn7U1 z+mU});?4U?ibHxQ81z`)ex`H%&|jjn$<$-=aNPZ(`Tg3gmWgie*5oxzd{|Bu7C6ct z9hxc{xc)0UQQA}i>!CSn;^f2Faj24K=A07Wx$7vdpNJ}aYz5pg>pebMOU)O2o+q-7 zKE9wrHhx^6ns*`~5LKM&ftK8{dIv9cyT7F%QS6NBcjcVd&c_a7cF$39KHKJgx3Zi{ zLqw$uJ{vvB`O&`Y1?4ngJuluAYr5HVkzWmUeW=MU!u$18V#l`_2C2i!&x`T=W2-Ka z+}yuTntmJ$;X1pLmc7sK)59HVH-5kM%jWS9D@$Vi>aM4dveQ)SWKLeiwCA+7x)-VS z<+U;PTzZ7tGy}@UMNbWHE=6Yuj|Bvj>UKPPa$@6|A>;fZ#W`l$M`EYk-C_xPU$jO0 zEt6kO3>^oqb#3`x$Mr5}rjl_Z0+Z8K=9G*p@8@@V5TW%a>Fyfj(xNK%khoxo6QeFA z%~|+sUfYWx-pR9R=_bo?ug%Tk3?%hnk0jO7l8hg{h4xMhk;hkM+J|Ca-Ixc%9#?f_ z8V(z?FW&Wtke-3WDGAIaR%h#TaWI(S-F))Kj9gEGHOZF%m!8=6!r2f65Um4 zsav1-Z!X+!Dv}YM<(Z1D)PXIn=zTBUd2U(vuxQsNy*SD{ZFLL-)6$-wF!dO)jQh7F zru>??DGaA7wg(PLxW}|ZNi=Fei!NKNn@4et+jqf~Eqxv*FE5NMI#e6WQ$M`l#}a4> z(u&MeDj?O2ch0lMWLKN~mrPq)?&3(=nh5Hf{$7A}wM2qT z7vEm2KaWq}RL>tz?66^Ycv#$YQ}yxSFhRPT87A9}{&mX>W5 z9YmXbmVXXH?LC9}b8cf>}V{RqpJN<&<~ijy zEZmzYd8IV;6KM=UfY3}rB${(-HUKu0?QCTG=bpD(_j>@=!T?yCdVjn81E&qHkS~hD z*9A7!DG?foUDO;MK&BY=ff9pRk8qpx8{om1#oPw(M+#Wx3?dFw5brf8%7wEJ0z+ZA zN`bq*j9;PJV*3}{;`qLtmy=Y;ksGRpmwj%1)EzLA_91irCQg7ewpJCN-t5goG7D*4 zYjON@$2>r}u6Pc?siij%_@BIxUb>aRfdc8`H~|%ih=W1fudeHqq$7~qw`-1zg@?z* z;+}KN1T)AtYnWy$%W)h14LEJs`ro^Y?bWpEccBaYgeOtX`v4RXBI9GlK(mGitq-sd z2@5)ZIMd4j!@7QuGgfgI_S}0Tynm`t&N$yty+M#fDd#`OkvK&N80Cxl0H#Vk$>4f( z^|@Qkl0_xWz&!dpfWuB=lb-PUVQ4H16p@6?w;uudoT7|)K#d>`9gqJGl2RhC=)mW{ zx&gB{0vzMIel$Gp*TcM;AL`0~oyq1R5k)ljWpZhnk;+P%l2FN3Q?}k*w5lghdsZE? zCuuv=S+)d|bm?IB2Y`NE+hUKt{v{s15|Iz*p#sBZGH}}t0K#9EBDKT2LLt@%^XFxZ)ZL6N&3lv(g1kxp9deN3^a1AGDtlCk zx|%Z6O0qenFy;GdVjCFY_1SxtKr)Pn3_RUN9@hk?|6u23d0P*^o$%AfuBTU5pnv88 zPBLR0tPh7Xq}QO|AUH-{wao;SvvI0Tibd|pG>u$27(NIGB-SvwI4Hw9%PuR|{nJM& zgM8_bNPMcIb*ft|Quoy16&Y3?-?8{R%2X(`gO^Mk#}xP&6(`TYV+@OE0jT|wt2_Uk z&}wdX-SPoPjJf#3r6}te@>)j8g+FNQ*rE#o#*>+kf@D`9ZnBDFcQ6US{bCu`k6i@R=jdxaPeJ%ucOTZtwSKNDyhTWTI}2$4U% z?2QQ5rSAaAvwgt!O!+17+A-h&oB_)B2-Jk8;r5il@?7F0+(suFK5IvZAitI>>H;{3 zaU1=LVwE{GgFU3sj&`vDgNZ9488ZE0#F?Lec!v^fNEDfsPX|Bx0eV|sjF4S z;RKtvm8;0Ovkn2MCGPtT8V7d_#%K%4&4EQA3U@xe&2bN2XcK8D{4kxW5ZhaLxT9r0B+ zNE(Bto0JNQMaP!yAn+8=qLe${l7Mlen{5J;45z%H>214`-1oi;^4s=GjAwj)qOU3{5M z7KMz*Ks^bk$KqI{?4vtrJB_~Bc|zQu8Vbp&(gP4WBAW~sz{avF9kDIMohM!bDu(Jp z_(2Ja&}|5Rx>MT*R_fkE&_;P^gPVCY&GOHGhj?+ zpXl*izJ=-Lz&WV;`Zmy;gyVsxj0SVIt51?Zm`{j|`Axg?$BSqad=~jQGfxqf+*3Lc zqcrHc%_Mq%W;=Se7-(g*&j1@+Tdulf{>ec>^58J^XTwh0PHdvYq1Zv_7*%XhD+TCS zEbNJ((<(jkFE(*3-8uI2KVt&7PFF5J7vI6LO$qe*HLX!c)rQcC9uXU8K-r>4F(uv@ zSig&=K!Cf5uffwi+3s4>ajgx%H+J|b>dM&q2x)SWDb&SycIctrOAYJbw5W@T>h*1S z<<)%cWu}tzeuOtfVi0oFZ;($COB{!C0K!bgdosPL?vw;xQ?h7!Gc>wafAj+1lNUZ5 zojaQLfrhmG_>6y3m`w|qO2V?4^_ z5ac45e7t!*70ihk#R!*Y#lsj??F?}+w|5LaCMG(Y#8`kwkF9W@+2P~+rMFHHS(}u0 z6im#1sd+q|=VLuYWG)-;4f-b!t2S$+C}@gt%jUrqxO}6kg>{cOn%wjEFrVdtI)l*- z_RHAgkX>Y^0jB5s3`Q6tOh%jND82^hjLE4a{JB~!wA5GSyU>{_Ic+SV(dJqjkhIW> zmwWX5wgWlY$~AAv_HuJAyN1*X)N07;Wqj|EV=>SDK31t;>h!eomv&2(T&fgDYyJe< zCY7nkT_1F*UzufWbEAMul&?w803xQVJl?HQ^SzijI77DleJfg{c1`$`M^W&L;I8(z zV8!xr4NR?Ap=S_dj_V+}(R~J@94MZ;SYb}k_w4mUYt`|ZjLrtEf?vcE&nvwomQ}La z)|(knsUGC`;)j6bhG+3#m4B)%nED;Sv9Ndw-O=nFo|Fi`L8`2x_Z`@wxrKvia9`#n zaKk}HQu)-9~@y2=! zPqD?egf+w16!NT?ax6cxcT7{OQFKS|_f)#V5GWPdv_t8`yc$sS>M|xgU14kXxKOyb zHUYYxf{zR7d?=jaYxMpNOXEtNfpTQcpPGmoZdu`{hHu#+MMb=fu#&g$Bbns(LTwP@ zm99!8NeecH1urh`kF>k&JrtMc_>W?!qXsR4`fjwm39(3#y7Qukyt)Tk3~WCUd9Z8RsQZAN(& zeOLt$3)K}LSdis@5hTJza5ke%M`enE1!QNjDGdu)&*_d# zVu!5{xkuoF8^+&gHm(aE4`8%5Kbc9Em)@U0^;?!wcx=(wQ5F=VJXh3gvcZNIHwR;F zi@Gv_0zvU*!9_C_!hwJ~0i~vvO!M1p;Ij-W;jOv~X@AjX^af!~Qmg7cmO9X4>_fw6 zyWWg>to~On-+*YOHn0z(_~`WItx9Uw1O)Gjq)Qp$Ff{3#$gi=qs`T^Kk4Gt=7uj#q zXk}`4HJz>Z8>Yn_K6_ z2~;}JHx$BDBI(S&Ej7ammQ0SNG{27?=_&TG3Y3T*2%BG+Vuip!KJ-p4R#9fuaICHm z52wWUov<-WSuZF_Au{9zz3N`u(#>$+-G8$H)bb9znPU=8u_SIQxTI;5!zVC2=}L+h z=EZba-a&NjO%ybpgL3|x;dJ>wzjWI+|I{1VbD_#ZW0#BnF zhsR)`JJRN}k7K50Oi_O4^@uM+nw>d^D@g++;UoGOWGC`7Flf!ux7 zUngG&)cEbG_iuU-3Nx65f^P)p>#e-<89GNRY%^F0W(bLAa4O!aO8)tNrD~`#R4-t3 zSM@PbNT#JjZn-B;7V1lr+@35tJQK@b8o*flWJPX9wgc+O+!!_G6%~3~iLR5^6Tv01 zrIelW&MDi4;LAh z(%D`s$-3WTDusVxWT}1qpenqAxy0L6@f1(VoN=VzDSBS`h>;_VI=QlDj?}BEfAJ`w z;efnLxTJdDuk3MS6SFFxhg=H=dRR??_2&_ADXmtRSpXU?z5C^5LgEc-5F)DB*9JvI zMN&fvWMPi9SMgs)lpg9YCNL6)2- z5Q;H(C~qcEQs)Hc6+LI-ZMo)`Q4UYD6>=}>jJ}9(*moW@5O6v;$&CLfP;fBR6tfIbi>Ed)v`M@fMxOL$s?Dc1f+w&fWDm|Q;Ed1M z-&c<Gq4Li6U0}8 zPHEM=WHhsZMW|!Fe=z1^uh4foNCYhHZDQ2=5W}_ti3sMV_lpnZ>jeY`kB{kZ@ecSX zenuWC2ACIPZC)2Y^B;pyd<$c6pdQ$>r>-yP)|Sd$bGs-R8BN2M<@6SD+ztjgi<_gK3z^OFKu6mVyd8#@>_*&RHuN z2VO7loWpx$fISq@a;elmYH2k3jkcw|%*_m=wqrT|5Tg zZ)8y}3FPF5s-WFog#5~KV?03bpUQx4ArNs;d9szK97MC@Hp?me>HFF5PA>!hI6cjZ zmB+P4Rd!Ba2CO3+ie^14hfW#GI=8@bebQ z5FgqAzKl>Q3*HmHZ3U!!baS=x0Oi}B;X!aKL5pA9{%bavt%%r2)WiE)4RP~IfhPx< zVSu`2WG_Wf&bTQ#nduX<`BY!W$>4oQHA)N?LMx}2m6rSsXS1;vmCb-uy|fmOyg$1S zK@Q-mzQy0six<8R&8z30OGb_kNqQrKo0VFe5yT^#Oi8^8YgSBI1=Va|bj`p=_Ru4p z@Bx$K7xIMWE>4ADjJj6Fz38ayNSsjF;WZ*4pOcE#deyGNfMfE6UigsL2 z9&ZLesE&Fgvg>9IsyA0$yMA0*6{<0sjFu^ zfrh8mw`6^KRT8FyU09CTLHp>#0|GLXR1#bYsj!b_I0%bAdQ?wIOV?a+i!oGVJm_uG zaFKwcD8>WlrgPGR#77nk0~J~(Uv19izT@=3S?o_AQ%RFOq!&q&_k(VZE!T$I6>DbJ z5G-dw@}-#5JR9e&STdTl2dT)NI$v#%}D- zyTX%`TQ8(LnV7vmd}b%wYDkiKKT%6|C4mrOE0QhokX=Lk47n=&Ys-d6RD#IcWf!Yi zzRHXe*HUf-FGGx{m*^kJ#2uIUkdp`7_qw&?6&nvd`n|1~{k^l`?@#ust(B5>;*l1( z&J~t4Gbyon+N`>uBFUgElm-$F%f$|>+199z#~)<+$(}iMU*_P3Fm^ad({*l!-7GnV zKbfCm1?RMKksvh27Q1D6*j7QJ0RMoNS-G1=NkmP{FYugaIrSmaz_Yl!;8rN>4bIqP%hJQ1-1`0D zK7LVL96V=E`c`AaVMPNm_UieiiRZADTluOsSvR|B7Q<)np$roQ3-s&EVAunggwS`q zN_2@ouP#Q2HrmUw&$Yt9`7IC&~9! z?U}0&PUHZ#t1(SOed;pzR{4I|mOY|r?^T;JWuyO*!vVV!o>FrC6KB^GwbIrwiGx%T zW$!WlxQB>6R+gki0-?2OqfMEZXg8+Zk7_R;V@NKR$&^r==#;!^C0-Ft!SiA%XDl&X zjNaB^o(#;Fog2(jKIegSEevk9!mq-Z6DurJ$vnaq#RBpU`qCmte62s)|IFS{Jwq7d$|lDE}tD2?`?gfygOi*wq7jq zk(aUaa376Gp<g~6eziNUJ>-xk+ z|DzWFF2yt&JM2XtS&#JMhfNQhC3;Nnzp0qV;jncm0e9nX)847M+q|t1@?2R>cqEuE zgLYqZ@Wflq+RDD9#(*~PKn+QAa?iHgJuzrQBxMTd6%?kYU`%0!A-9-6Xybh$ zA9MIoChGL-&R_yDgV1WV{Rhf%pU?5;M~8cyh@ii?#q1Hsy>P2WlXzn11oj2)IK=Pb zvbNo_Y(2k;wd^qInmGJ7kw@|-BZq$q+WDG1p;rk?XY3? zhC=$xkd6i(!M?L^5JLh6fa78mdY-CoW&Dy8z-6%Lh5@7&j{h@%pKbXtJ>A9&&t*5bM51&6y2#Rben4>}*H=}2y`3#CNFiR9CJf{4B9FY0G zbNXQU57GKAi_%|XxcR3-ae$PHHfcCfUeJ7N3tH4pdeK8p0&pfR-2@@yz^mm-51fL$ z9{$PwQK$&R6Z>Xf$~-N0#;@xL_Bq+>ldl$**FSq+POTt^rtf}!e)8`}oWS|6D-V+( zXZflcmxY)lhdJjCoDr}1kEB*$*W#fn%&;Oc`?wo3q5`c(xd?(2cUIcyqEM*iygbkci()({`b_3`t8xg`U1WA}ma z6(x**5fAJfhVbgz4$hm~UqM8mVE&~62y9NRG<08DY?lOChkd|4LX8X^jhQ|Pcy-W= z&G2lxn~e5)W5t1Dvc~?!#Apz$v(&p#0CU)ofjAprT#gHx)7%WKQg!=Y;qgNHwTEv( zzrpDU@c#CLoDWoZ-E<+`k&&l*ni-oX5sQX0O=mcoq`^{`6D{( zrex*!U!1Py*>E78O!Gck&BgP zTk%|((k<~4a_+vGuX}^+zbtGMKd|}_UCXKgk2-Q=9Y9i1>LkBP3oK65d;#&WYL%jr ziC80J=o`l998S$m{ee)J4cW4O@f_c}b+MSPU$?GfjnNgz1ANj5$f({)?b3(!m0m0w zhk}52sOJM@>O1cMoionXmIL+7AB0KRyc$7Dq}}^SS~n$S|L35L>=@V&*_HsAnZE@- z&8NuvK1=XlxNv_E-Npu2r=7y&env6`;_NpwR)tI606Qrq2oa4-;B4R)=mU4pbwid( z&po@Ql+%~ierlC3`*S*!FlrwqD1wd3R&qNZNJHY-z zx!+?A2#-D}4g*=9B0|MC;B4Xa8kLpS`)kPPfs+C?`n~UjJaWM%(}4Cp?-tC&sE7)x ziy9qb9A#lg4xJDa!k<;IiMyyuP%Wn^unCZbICpIM{%*Qbg^3QVXHRm2IV4UO&1JT1 zfOT%c754(1a`K<39MmR*Z->#fzCf4}yspwD9(+#_pm0y+s8!@IfV7p_s^RFI(hyWI zd2K=8U;sWnkX&A055Q1G*gaCNI3KX7oeY5Qtsh7TatDVd0B)pHlQCrOowOOFY{$lFm~J{z)_` z{0UlmM=pk!F56Q(3ixNW_Id#(l~y2mfQwhc-ItSrX@P}6JFtH;&)s`#($R-v&2*w$ zb#+f|eUq4f-4ggpXD%&!7OGG0MXx=vsj~yS4$%LSGWNK-vQkY^>3}l##!9}Yy zd6iGlE70-yLV|+1jMb_nfH{>Zc^j^S^#%Yd;X>!{eq?7Ma0kqkFoyj?9MIiXNmhS< z+N_4s5YC?dJh0uo3z*c(z{QR|Ud7TMC?~S`uAX^fKP_UPuq68O44gcT_!=3fX8x&f z`-;>hiOA7h)3jv27V$NW z(I<25p`26BJ)6BdAm}JPL}n0l;5KQmQ6C7-MBSEgk>HqQzWC(MhNcS5XpW^fhSFLQ za7i$Y+?;&MA3jvs?wmMH$<2a$>bg%gy2BIoBv{xwh*c@E8UdjieTCoFhZ8N)f{JSN zy{9Bz9_YQ}8ckn?$k4*_E%l+mTM<8s<-2MrDwsqE^Ke%9^YM4ywhVrcFi*Vi(eA|s zwUs3!wFE$$cDLKP_zSN-?6!=(xT@3Gh<@mexsL!Oz5%$frzD(PS{+ckQwp`MR$)v>S~2lm@6HcnOrk+diRdJp^N zPxaon%ego@>FenWdvm!s!?oD>RrSD2S6<}Z_!?Ir>0aOXlq{2g7ija0M7qx6{}wKw zGWD^>=DLh>l!sma>XzCEUt;^WPuQ}k8LBvoyec+}!-Bxe`$0=3B?ygYAV(b_c(cY$ zuD+EqM5ZPtBj3i)tswsW8$h$OE&|fK^LI)NeF6dsL3gL+QsMtNzjYs?C0;c6CpL)T zxVjz#F~_G08Z3N%?#N!L)lcF--v(brk`%@ES$%e6YE+OcJU&KDDT)7Z86Z)7kQU|x z*x{K;EK!3Yei@=!4U6Szy36Y=ynZ-@ri6F6n1o_25g4u~u#4JWbN9U34=jz?A}$Qo zFx(JbvP>3!7C7*$C(&0iU|<+7qAB`d2-5G+j5}@fS>RQ}er-wHu%$MEjHbdey}~i$ z@**JoWmY9`8^2W^CO$fj0*Yd2>%I;*TGZx@XK(&FPb(96gQ~@C5Cp5EZyt412S6X^ zoiRPCM<;lENt1ZDmH8{I3r84ht{FzE&>gbKxyKq+K9{JZ{UE8eJUfx6BV;V;{CuczD*}kb*C=f@BeoFUYbW=chlA~2*ZX)iG|4@J} z56IE>Oz(!o`XIr}l;5~4827juv#BB4akh9BwJs`X5EEd+uky6JlYee}<|x2km=E_i zEiq7uN!rpUt$)J6*&@8{T_G}k4!>f@(U$uml_T)+S!6rq3CZe1lc8n9CPpxVFykG_ z7<)7v)rFmkqtmGIBc5Z7kMMJX-*&_JNBK8uLli&BhM#;0P~h1@k=rg8Vc4eAevHjm zF&_}YwilEe8jOEm?Qs~&Gmy=6mE7B4K0^F6IYjnjHOYzm{rd@Qof=Vo$C90_Gt+G5 z`f}gu>HNO*zozee(#SYpKciW_!RskY@+oyv{u>MTW*Dd-R&@h8`t18yWET|14oQo= z3CdPzG*6g93uCVP8qzJUg`QjM#Ca{^$_j_S{{-^Nqjxs< zu3gTV=Gb22$lw#m$q!7ZG3r$Mf6s=^_`HBL@E2(DJgV0Y3xRsROe$f_Ie>3C|3T9? zM6vJcLEkj-ELoIEQFekVlI&dz;OYcje>2&{RA(N@{mCQM361i!*dft0-&F927=eM* zDOF|SvC!)oM($NlL;nhhY{j{hU-75n zBi;`r+V*jpk{u)tthrSwt|}4yE=%^+HKc|*x(@<8${&$Zf$!hw({@<>5=Ynrfm>FI zU#CHHn2r$*D4a!V$4ZvN1NyT+=vcl&)Q5@IjUMY9NNija4`!*{;0PA8>~VL$34ZEb z5N`&nn@OmT?{tH|$P)NQdpV3HyEoVtl})>q18a@qiN)v-7F}~szH?A5y&a3ju9{Ks z-bPgzmtWkH5BL~$kyHWYeo2;hqCp=Wrx%dj?7U4YvQ8qwVwco-1FCBLljj#~1yAw# z3q{7g$;f6<#?k+IY0*kAICaY_mRPHfUMku76VR8BT7*}2q};Yc^KRYNtnCLcrZF?43*&8 zQ?qfjM3*>c*ttXqWY~v4%`>nZ8bC3_r*P1IO)-9d*x_+KqoNn3)Do(Wl(;M#F_bl_ zAU{4|DX!vq>2dUFL_{x9fb;+(;*m7|oA>H>hB&T#68NLRz3a!Ap;)phS+GX*x8j?t zV`{BeA=sZxKgQwbeG?*!Qi3 z5RWZ<{LNRrSfMfD_y>i_5Gq&0hovER+zazV`6HC)-op}PTaR@3z@^IrZT5B7{eRL% zE!lPX%bXK&6?pK&GpH+*eL>jh<5;WOiih>}wW;>EYEg*|H91L$UCTd)8PGad5`uPs zhK^sZI8Pq;R?Gs&s+qz26;}X86?#eUO9z^8x58SjE+wm+?OV3>`w(KA@9_Pphmqqmjea3#1OhP|aV$m_k< zWY-w5&Zdo+i}CX1Az-*-#eDG*AbDZIYkflu2U9T|)kAicAy8U|Il4J2euewy3iK_! z?}a{)s`^cjee{gLYguh*Jep6fP>9vB8jlqhB0}dDM)Qc#3E_Ha;$j2kp*+-2Qm`#ld|s8xU~*Gu^Rn2Tx>pyxcI7YM~1<{ zMWhN&y)ia5F1N7a3%7-6K)h;(y(*Jsg_Yg%-n~UiNnaDp2xp=A7#D1`FhdiPyEwuf$k9dp}Tv6k!!5+ufSMrxZv^s$h!F-^K# zPN(*Fu*MK{qGv=(KerLg9#W%Z!%|O~ciSpqidQqF2Y&ZRMfs5RQvaA=Qs! z%zR>-B9Jm8y3rY5Z|H3BOgoGVb7=cJ-7ZfF^H&w>g0PktHyjNZQt80f6-;bP{CH2^DJ$)`Az8O15%Oon!gOx`Ovft`lsHh9@v1!F+Ou? zW^hmSs!>_V!d`L}AFWO#vV~KYlxVp@B=)9K0~;!k)smsVz2rOduSE4jubgb@DA zne*wsG~nEkQ;ZK!PLC>RN4d^Z_kJ!=ZnvTh___awu0DMvEQaTtL|$7iQ9Yb{dV2D? z*7jQ6-y1}IwV7>!t+Gl&%-%3QZ)i3HzKcD(Xcu~Iht5SI$7x0p)ZEF=(DVuiF;gqe zycq)d5>D`i&U)G(cV>yYRuao%$u_^REHwDv46x?ajxvt(oRZEF|`MC zdiRUq;ailA}_+$5-830xm0_Ka_P*fYYBHhke3GW~NBjY&B^RB4Y319v_cF&fYN5D~+RKX^ z>vD{mh_gtZ@RXU3%gW0tr;pO-uEsMw=2A4&N zKMlKLD_4v!!|k14DZH#iGF_0_)|4rBL@0Kr3kRq;l-Z&$F zSp96MAVF=~Kn&Lx(lKfgsa{Mr%k3!K)xY{NjB?39WZvDd@7eY0;p8XILa#GM9$-!i zm40yG5zXp%*r9rcx9G`TU1bGmW;Y&h?vMP`uPXD=W^nZgv@DCEqdA~AWO*+A(%w{E4nqF3Gg-phj1^ zm|@5_W$8P3-lEo?lVE}Vz2_I-S;?MQ+v>PJz4Gw1X7^GZcIqyF&A1Hml=CXCtf2e; z)H4aSsJP$l3$}xdoiiIEaY}V})!}r}^$9&?B`iGG6BMX^W>gzQouhWWJ@vaHZLchy z&Z(w#Nbbv&I`I?j3IQHnY4jH|QoDM)5;!{NYxau{Q&G%#2P=J%TGHr^@1T zVm$T2y;=@Bii#R+Os)0F!jUuT)UN+FSKnUTqH~v$D_?4iKbsI2swd&y>`G_+PnHhI z)pEOyO!j~R40uR=M96#|#z zE($tN-kg5i2z@V@yYilq?Hu);Wjq|u)!JFa3g^^_Y;RShJ+cgl#9-c<|L*_NGxxbL z@ROz4!q?B#za%^?KHb@BkrVlp5z1BwQQo_^(`D<)r~4yu!1ziqxqJdsjnBX$|4SyP zY?^Ho!P7+_kA|bGX?c&zB90oBJ}n$>PJgI=1PftmRkD19YZ|Tfmm&GKck}YWFlww^ z1_JyvbQ+nW!bctY4S|guKE+pD#FF2^zC3dF3|JKt`Y;_4$xpotju}%rF0!}>*eVC8 zJKJK-Ys+lL$_i`X?Lnn$kVoCo)GW!9RMd`c4Ar67*0BmQR~$v$ooUZoLIs|$<0o%| z7uqpkXCHO2ua-{!s@%aZgqpW^w9q>o8=w1v&N^84WUr+?@u3U}PQ?fZpEf#WW9H24 zGugH!Mtf%ERORBnbd1p0Bt2=)Qm)sw`TC^i-f#1dZ?V)1t}6{JtI~1ixaCVdqaufC z8}DaWx8h!5PF9^3jndiNFNA!qiXwc=8nmB^B8cwPOnuGWLyj!=6ePS!^R!B^noH0Q z&X%@(WH@}vx-MDy8N>HHcU`uBH6>b|FDSZe{^K?RRJ_cYKgj*Y#1ne){B82?Q)h$M zxmbXJ^lAC{g5Kn_A+ON?67SD|C4QjpG0Cz?joFD>1rs;*C-CP;JX6xP4P%a@P|p)E z?ZUn`dd|Qd$kX4x5G4cu;{Ofd_v?dUj!pN^p(zm zToCb5dA_Z_d&s+3^}qRMb0kFx-ceXvy_S47(4< zI1#+kOagn&jCM zO0ivRG2j(bSE95DSpj|AUaT62^ned*q6BiMkAZ`~$$vQLU`=q)XP-&lo)RGC6G{*l ze`y{#DpbHrLRhD_GMwM?{or4>2PjPRy%%o;PeI3woG0?b1_N~8AJjPLKlD-i3>r8F zD0&B>!Ev8de`x6?d{Qe=5!sw(^{(~t+X6U6`v*v0Czr4^SKfTQ8DoSA~;h{%0Ylg#vO0^}m7W0Ao5x?%(I0@-pji&#nI*oS*k3&CY6Ahby6 zj%OF+JOE47Aoe%VLY{|^wlsD)oNqK?3ZY$vtkARVZmZ+dr)`}kkT z(dNA4zx=;z*W-wqvu22ww_+aDShUF0aNu2dmpwrIQ{)X=B`GXmQLjvUJ{@|)kAR=j zQTNe`jnG(D94Iw0#wO+hu*R?9QR71(zwr_%y=eRn2$F_-SP(cV0Wsg($VGumn&w8f;ii%H~PFlVbPO~269RN|TFaT`vlM+NG=ngY-6($lA zIYkMHoCO|0sEP(UrX-=o6NmXEI18XpqLdC$OcbEG1a%Kci*zf1#)k6DBKZU-#m#L{ zrvO}DxDi8h!7g6fq|~9t<=B6%ASTs+7r>twbH}Fw*`UVpbrH z+Z5LFBRarsz>olp8V}GcF%tAH)GaIx0$LI4Jb=TrK%a0pA}EhQDxw3ZpqV%MP%eNt z4BrRtZ^B4x2Q>rRO$<1gvs?&%7xW2Lz52qTQBSgygB)tosd9 z+~?7^eYl=J(A984|IXaeYjLq;U|I?doe-qHN1MR6EVpctt#YR5$kuhXj=$X+m^IIg@VrA9rk7wZyl^+l zAX^9Y31p3#;?V}Z3QLoZ5Uj{CzHI2CnB55wc3qLdTXv8;bw!sN4UGH28B&J$8BAdi zT*1I}IuBeWjkJ+2I54vo=fRCk`{Cx5(z@J>ASLqHW7fTaj3p`D=gt9Qen*ZZD3J($ z7Yr7`M*z`t0BlLZxJwA%drSk`+@G2JiUV7TlD%q11Dby#q(Wi6+Wo&ic@L8X1HAR7 zB5y>qJ{g>|w$!`QZm;t9B!L(DtugW!7$1fOiv2$J0fnWiIn18Y;LysbS-bs(S0{4K z$WS-!Wai;60THs%3+pKz7#)FBCts(F2N59HQg4+RlcSZs=)_E>0c#z?}l8>XeMdw=Pv3qblB{JPppEk5!^4Em>dPoOiX>a z#5(wS$-+Qxxh?QFMQ?6{vP~L7h~*SPss$Oe77INQ4H3jiwV#L?n;W?hx6fySoVWcM zXZWL?mctJF6x|Zfc&QIs0r7u4Zp@+m%2koKpigkZk~-@9(w7nlArigPU)@> zv=q72saFK7_$k{M#C{-yc_Y6^xuyEEkeAs;P?qQLK5(BHEGA)a-R+{!b&@s`hOK=d zO&7ud?4r4TWOJ4PSRclzK~>*7*gE9QSEQ6#Ld4$*{2<0T*v$h4o?S~C1fXF?b{mW( z7@bCjSETy%!PPO~?SzYP8+kSofFtwr0waj<%KnxHffUiRY;KP-*|Vm@K(uW6K6?3; z^-Ex37o)rYUfyWnbCo%P>BKE1-JrP{X^uk&H#dQCz#oGS6pF-k#WZcT{`q~yC!&s& zgfLKCm5+u{elQ;IvHrdHL@J^Eer!_jTImCCam69!`xK2-g?itjPYOOqnP=;OoUe`U zw<#Q;L!wrsL1mEG76BdBtkIvKR*F#rm#4w_bkJhPTR7^cABl)=h^TGa*D&fdQn=w} z&kw$QU6b?-O;RS*cqH=oGMX_|q6AQsgYA;~x>dd*sj^@#Klab~z$3BN&4;h87 z$w2<%I^ky46Orz?*k>L#A9xh-F4l%dZx8T%&AgFv49J*Sf>5E$}OvS8q>YSINyJ*s6)=NvG@PX@UL&%cT<7*1nmiLZ|! zAjkWlm(ho^zp$^NBmMyL?cB!W0g(oyl9J+CEx1aW9x_H7FN(V+gbo2om{k=gS2Z-H zX*D_hiv+%Sc>P2gw{GKxxl6CKD%)`-Hr0HJ z*`|#@bYk(heMwf??)p(~UuCdF-y8-e>?#7$OD{q91l?u7e8TXXP@!^&r_}FnXB=IE zP$juCkj0PxVGk2k;}+v1K}rr{@7NtBE5$Pv1KWWpq~LB?-r&EaT!4X2P+uA_C{l|v=AW}9+TzO zNr(Omo8E&9{l!W^c&Ro#*)4xe)Kyg=?t%;p0`ZnVo7rb#cZQwf9z|pd0~Ni2`e=a7 zdqP14eMwQ5@m3~S$y7W@@gD=`>N9FCiF~uf2jSkGuRp8pw%so7u!+U&6lQ`@ z6^_Hf;q_8oZPs#)!hl)got|&>1{ZXbe&(OyGt3p1h+V{r-l1G;tMH!3L5BoqbNhMC zAp00}gzEcq8F@|Y6DkT0CQ*Y|CN148WU-xYckmkA&flt)WQnn9%vZ2!9C_Kd8}jBg zE(SNcp-}K?TsE2!9+i>J8$fd-n@rJ{_%|W9!SNMZp|7*oMv*V*vn@N$&gS6hgDTF7 zpE=)y+P-Qo#Ha`TWuJa?V+m$%CNt8GG%7*ekiyhpUO_+4<*CJSmuf#16=r2EBLn3@ z-AC_l_%pLqoyfR+Vb(+pJ@LZ0V`{a`gI)4vKHJxkTDJ8Yw7AgVJPNUc%h-&(dGb!u zb($Gk4gPY=VDY=VrPr5ysDrA&#f`xk_`pL|-v>Ua*K3L6po~!KF^~bMnLqX?@uyFyvi-ei^g>@(;F7L3nUEeG}96m6xKNo zE6k%Vi0A9}NsVO)Fe_;~$s>ST_c)HmWpv`+wp-0mNnARiT}@t9=W;FSsry3W)a7Bv zP7)61TwFhzg=Mos{EegO1}JSY&GEq_S@6@oVdd?QPf<7NYq;Kg)AZMy>QLoxf|j_dZ;hc4DB{*)ONst{xQkUHMUB$jpMhV1q5Xt0O*adl^5j zl{4Pi%WVxyf8$kgPUp8p`Q%RIk=b~vEn!6IE%LuOl945- z0wC!z_{!c|=vW?if^zAKoGl7cH=LXl&i_!&iy|&Cg&(U3DxJWZYXX+_$YCw3 zS5q>$<9L+(5q@nQAgScp>X`TIbLo8!F`_|w%=GImIYw&CPvu;*(*?s2hf0)oe3ah& z*`RB@t9#ILnkn+jA)97?9vxj_`uh5Hv(!u7j!97#Nq6fqZITM#*Z%oB==a(GV8S#) z2UaI`Igu#DK4)NZGmo(c7#RqDW8Zl{D_#4yv1%AT`}qJ}Z{S zLfPlka?tZF&*Db(1NV26;-O3|rOwlhA2t-A81?~;>M_t8kISAy+IP6A??({1(Y=}AkdY{beLM}P= zXgU10=}ilDrP__z+EbHzq(@H2)4!_TPJ&Hx!#g`55b?D92BqwZ7iv{SPZH`&(-J%L z^u+siy!iVAso49j6t$Mf`?lAw)~kk>(U2KHsXFpUy$)vb${so6?Coy9^gOdLull`3 zKrY!*OetDRYlY%<`&ZfcZNaIbef@@YtuP*s)O-Ziofe->U_q^ZG=wtY?54{wArzk) zg}NXyFIB;AhfdOuCSM|G&^6yhN@;Z0IsRsBzuVW(%#7k(+)#?jN5-1Rg%Qbfl|+(} zH0Z))EDujW$P88cMd*uizx`*ztk|#)T;Q`GOo&0bHuQXM81Xen%ABWj-bJQ5C~rRT zoAkdp0tWAu>QXMeJ!#<^(Sg`MfupCKZql0S zl@R?IblEX15FC0sti%425ZWly(Xt31j(+t`0>{2PN$qN!(|g~T?$sZ)%!@~wtm2-XppwZR;cT)t% zkqHUL)$_xT&hxTYawL&uEYsPAL3?)9{FZb5tpg`w)`nLe|3o&_k*?(J+lsp|%etqC zUqyZV9Lv$doji3CWJrm7L?h1T2g(jpcP$@)`jKG^RU^FbP%6&rmWu1%sP z(oUyT50%Z}E3lPfF=rxW`1_+dr52yZhAIT4S|=j}IV;|`kA_b*iIZktyaf7@&Ay^Z zn5x@cx^fOoVijj$<+iUoY2Z3}uMji^Ug63bL)?bas?;23(jTDR=o8yoboE-48oG?n zD~9bVcM;|)^$x01Q}8;~hUih2YaB;wbgz_sQ|eTAn>c->7TiId{be%cTk<_+&HP)? z-a-pCsIKPI9p@b1$-cX;<1O|QIJEr}3kJ z$xbC9m~tXkyHu*62FCCnazNKnV3lmjAp$T1w^TDyE}3;!joH5#Sq3)}Y-|XAEt0nT z1;HZL#xhGWb-T@kegnCGtPk}~)~t(^>Z90VGS)G?i*GThScbo96wi$J9McBLWLE+u z=kzZztQ0Sh$m}M{gGwPs1`1{Boq`W8npK%>ess)bIdqr$r?>4c#p?`gnYV!Jm@L7_Z*~Jeg7GZ^@qlyr^1FsERh`2q|H(Zx`F+*FM z(_1ZDRG(yu6k7QHPo34MR$Y}L4RRUDez^O2ryY8(9q&EWVyWF2nC|w#*rHO+aF}u= zTM8de?zpS{4@Vd$VLlu2tR_@*)xs}!LnHim7y%ndfP(yQ>s&uYXhG#Tl#%@G>AZ$u zWhb5q*^CJ+G|W=p7iN}Ond%L=4Bjo3X)XlY{|6e>qeo<&3~YQ&^yK4$W1`Lr$>?h? zkN-{X6aQ&jltSjmmwJ$6_EucDV!F2%Y#m$r7jyPwWbksg%-0PYSDnsorL%dHoh~X2 zyHXUzSJC5UZeF^zeB2lCexR58g=27*r&Ub`BLN9jHG!8b5r+hi3!8!z+3oTlQy03^ z-^_C|WSQ3roKp3)81QWozMWK@GXlQsu$MFeZi-Hk%S=oXwNP{+2}D-x#iApv34KUNcT1~E#A%rR1v07<~1Ak zAjnKN$?=;|KbS(0%S>z_jH>C8vlV}rOwE=ugb#UbH@IV2#ld~7Zf(8}DTlS5%72#y zP~l=cYnGqZ#kT!Ks%TnzGA+JT!*pwZvk-!a#LuFtU@WAWe;-oq5~j*G7W4xCtQ>xP zL_`FsyopdXQn0@GzH+0j@C%Ihfp7Q1OW?2&QKF5EUAcrb5JDfUq$K37h}AlG=C_@lRr%N)I=;!h&lr zlb!#NAk$su%_g(!Umy)N~X75in`=9-d9Q4)y9dCcUJd_gihm05tK}DKvhDdWHD{h50^)T}* zLnl7Iou+a#57re!BnlE4-W?Yv6*7^|T5?`bW{~b5W9W+;ua*e9ro556Z2C#l={T)t zeHd)30-Hw^H!sru&jzCk)J8~|cA6yq;Ykz*N0Gs!9Y%#q$!P$;srK zq>bmDrLKpxdP0`gI>kXdASq5<&&UKN=z-2=8%`xi>4kq_`lM6x3p0sVta?&m80pWP zZ1%8ry0+X@W*ZJz#;=Fmgt*k4IsK|Gm(Y z9DeoB75<+u9BH6zjK{vK3J`1j4=)HJs9?V~2E8}`e}4$X=ZO#wX}01p{6CzexfsHR y!^`)IJ^yx?f6u7O7hbR!{l7!_UpNbGe@K-I$$9&Vnl2H6e>c^Uh!<)$;r|7_fvc> + +(* The set of all correct nodes in a state *) +Corr == AllNodes \ Faulty + +(* APALACHE annotations *) +a <: b == a \* type annotation + +NT == STRING +NodeSet(S) == S <: {NT} +EmptyNodeSet == NodeSet({}) + +BT == [height |-> Int, time |-> Int, lastCommit |-> {NT}, VS |-> {NT}, NextVS |-> {NT}] + +LBT == [header |-> BT, Commits |-> {NT}] +(* end of APALACHE annotations *) + +(****************************** BLOCKCHAIN ************************************) + +(* the header is still within the trusting period *) +InTrustingPeriod(header) == + now <= header.time + TRUSTING_PERIOD + +(* + Given a function pVotingPower \in D -> Powers for some D \subseteq AllNodes + and pNodes \subseteq D, test whether the set pNodes \subseteq AllNodes has + more than 2/3 of voting power among the nodes in D. + *) +TwoThirds(pVS, pNodes) == + LET TP == Cardinality(pVS) + SP == Cardinality(pVS \intersect pNodes) + IN + 3 * SP > 2 * TP \* when thinking in real numbers, not integers: SP > 2.0 / 3.0 * TP + +(* + Given a set of FaultyNodes, test whether the voting power of the correct nodes in D + is more than 2/3 of the voting power of the faulty nodes in D. + *) +IsCorrectPower(pFaultyNodes, pVS) == + LET FN == pFaultyNodes \intersect pVS \* faulty nodes in pNodes + CN == pVS \ pFaultyNodes \* correct nodes in pNodes + CP == Cardinality(CN) \* power of the correct nodes + FP == Cardinality(FN) \* power of the faulty nodes + IN + \* CP + FP = TP is the total voting power, so we write CP > 2.0 / 3 * TP as follows: + CP > 2 * FP \* Note: when FP = 0, this implies CP > 0. + +(* This is what we believe is the assumption about failures in Tendermint *) +FaultAssumption(pFaultyNodes, pNow, pBlockchain) == + \A h \in Heights: + pBlockchain[h].time + TRUSTING_PERIOD > pNow => + IsCorrectPower(pFaultyNodes, pBlockchain[h].NextVS) + +(* Can a block be produced by a correct peer, or an authenticated Byzantine peer *) +IsLightBlockAllowedByDigitalSignatures(ht, block) == + \/ block.header = blockchain[ht] \* signed by correct and faulty (maybe) + \/ block.Commits \subseteq Faulty /\ block.header.height = ht \* signed only by faulty + +(* + Initialize the blockchain to the ultimate height right in the initial states. + We pick the faulty validators statically, but that should not affect the light client. + *) +InitToHeight == + /\ Faulty \in SUBSET AllNodes \* some nodes may fail + \* pick the validator sets and last commits + /\ \E vs, lastCommit \in [Heights -> SUBSET AllNodes]: + \E timestamp \in [Heights -> Int]: + \* now is at least as early as the timestamp in the last block + /\ \E tm \in Int: now = tm /\ tm >= timestamp[ULTIMATE_HEIGHT] + \* the genesis starts on day 1 + /\ timestamp[1] = 1 + /\ vs[1] = AllNodes + /\ lastCommit[1] = EmptyNodeSet + /\ \A h \in Heights \ {1}: + /\ lastCommit[h] \subseteq vs[h - 1] \* the non-validators cannot commit + /\ TwoThirds(vs[h - 1], lastCommit[h]) \* the commit has >2/3 of validator votes + /\ IsCorrectPower(Faulty, vs[h]) \* the correct validators have >2/3 of power + /\ timestamp[h] > timestamp[h - 1] \* the time grows monotonically + /\ timestamp[h] < timestamp[h - 1] + TRUSTING_PERIOD \* but not too fast + \* form the block chain out of validator sets and commits (this makes apalache faster) + /\ blockchain = [h \in Heights |-> + [height |-> h, + time |-> timestamp[h], + VS |-> vs[h], + NextVS |-> IF h < ULTIMATE_HEIGHT THEN vs[h + 1] ELSE AllNodes, + lastCommit |-> lastCommit[h]] + ] \****** + + +(* is the blockchain in the faulty zone where the Tendermint security model does not apply *) +InFaultyZone == + ~FaultAssumption(Faulty, now, blockchain) + +(********************* BLOCKCHAIN ACTIONS ********************************) +(* + Advance the clock by zero or more time units. + *) +AdvanceTime == + \E tm \in Int: tm >= now /\ now' = tm + /\ UNCHANGED <> + +(* + One more process fails. As a result, the blockchain may move into the faulty zone. + The light client is not using this action, as the faults are picked in the initial state. + However, this action may be useful when reasoning about fork detection. + *) +OneMoreFault == + /\ \E n \in AllNodes \ Faulty: + /\ Faulty' = Faulty \cup {n} + /\ Faulty' /= AllNodes \* at least process remains non-faulty + /\ UNCHANGED <> +============================================================================= +\* Modification History +\* Last modified Wed Jun 10 14:10:54 CEST 2020 by igor +\* Created Fri Oct 11 15:45:11 CEST 2019 by igor diff --git a/rust-spec/lightclient/verification/Lightclient_A_1.tla b/rust-spec/lightclient/verification/Lightclient_A_1.tla new file mode 100644 index 000000000..2be9b8788 --- /dev/null +++ b/rust-spec/lightclient/verification/Lightclient_A_1.tla @@ -0,0 +1,440 @@ +-------------------------- MODULE Lightclient_A_1 ---------------------------- +(** + * A state-machine specification of the lite client, following the English spec: + * + * https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/verification.md + *) + +EXTENDS Integers, FiniteSets + +\* the parameters of Light Client +CONSTANTS + TRUSTED_HEIGHT, + (* an index of the block header that the light client trusts by social consensus *) + TARGET_HEIGHT, + (* an index of the block header that the light client tries to verify *) + TRUSTING_PERIOD, + (* the period within which the validators are trusted *) + IS_PRIMARY_CORRECT + (* is primary correct? *) + +VARIABLES (* see TypeOK below for the variable types *) + state, (* the current state of the light client *) + nextHeight, (* the next height to explore by the light client *) + nprobes (* the lite client iteration, or the number of block tests *) + +(* the light store *) +VARIABLES + fetchedLightBlocks, (* a function from heights to LightBlocks *) + lightBlockStatus, (* a function from heights to block statuses *) + latestVerified (* the latest verified block *) + +(* the variables of the lite client *) +lcvars == <> + +(******************* Blockchain instance ***********************************) + +\* the parameters that are propagated into Blockchain +CONSTANTS + AllNodes + (* a set of all nodes that can act as validators (correct and faulty) *) + +\* the state variables of Blockchain, see Blockchain.tla for the details +VARIABLES now, blockchain, Faulty + +\* All the variables of Blockchain. For some reason, BC!vars does not work +bcvars == <> + +(* Create an instance of Blockchain. + We could write EXTENDS Blockchain, but then all the constants and state variables + would be hidden inside the Blockchain module. + *) +ULTIMATE_HEIGHT == TARGET_HEIGHT + 1 + +BC == INSTANCE Blockchain_A_1 WITH + now <- now, blockchain <- blockchain, Faulty <- Faulty + +(************************** Lite client ************************************) + +(* the heights on which the light client is working *) +HEIGHTS == TRUSTED_HEIGHT..TARGET_HEIGHT + +(* the control states of the lite client *) +States == { "working", "finishedSuccess", "finishedFailure" } + +(** + Check the precondition of ValidAndVerified. + + [LCV-FUNC-VALID.1::TLA-PRE.1] + *) +ValidAndVerifiedPre(trusted, untrusted) == + LET thdr == trusted.header + uhdr == untrusted.header + IN + /\ BC!InTrustingPeriod(thdr) + /\ thdr.height < uhdr.height + \* the trusted block has been created earlier (no drift here) + /\ thdr.time <= uhdr.time + /\ untrusted.Commits \subseteq uhdr.VS + /\ LET TP == Cardinality(uhdr.VS) + SP == Cardinality(untrusted.Commits) + IN + 3 * SP > 2 * TP + /\ thdr.height + 1 = uhdr.height => thdr.NextVS = uhdr.VS + (* As we do not have explicit hashes we ignore these three checks of the English spec: + + 1. "trusted.Commit is a commit is for the header trusted.Header, + i.e. it contains the correct hash of the header". + 2. untrusted.Validators = hash(untrusted.Header.Validators) + 3. untrusted.NextValidators = hash(untrusted.Header.NextValidators) + *) + +(** + * Check that the commits in an untrusted block form 1/3 of the next validators + * in a trusted header. + *) +SignedByOneThirdOfTrusted(trusted, untrusted) == + LET TP == Cardinality(trusted.header.NextVS) + SP == Cardinality(untrusted.Commits \intersect trusted.header.NextVS) + IN + 3 * SP > TP + +(** + Check, whether an untrusted block is valid and verifiable w.r.t. a trusted header. + + [LCV-FUNC-VALID.1::TLA.1] + *) +ValidAndVerified(trusted, untrusted) == + IF ~ValidAndVerifiedPre(trusted, untrusted) + THEN "FAILED_VERIFICATION" + ELSE IF ~BC!InTrustingPeriod(untrusted.header) + (* We leave the following test for the documentation purposes. + The implementation should do this test, as signature verification may be slow. + In the TLA+ specification, ValidAndVerified happens in no time. + *) + THEN "FAILED_TRUSTING_PERIOD" + ELSE IF untrusted.header.height = trusted.header.height + 1 + \/ SignedByOneThirdOfTrusted(trusted, untrusted) + THEN "OK" + ELSE "CANNOT_VERIFY" + +(* + Initial states of the light client. + Initially, only the trusted light block is present. + *) +LCInit == + /\ state = "working" + /\ nextHeight = TARGET_HEIGHT + /\ nprobes = 0 \* no tests have been done so far + /\ LET trustedBlock == blockchain[TRUSTED_HEIGHT] + trustedLightBlock == [header |-> trustedBlock, Commits |-> AllNodes] + IN + \* initially, fetchedLightBlocks is a function of one element, i.e., TRUSTED_HEIGHT + /\ fetchedLightBlocks = [h \in {TRUSTED_HEIGHT} |-> trustedLightBlock] + \* initially, lightBlockStatus is a function of one element, i.e., TRUSTED_HEIGHT + /\ lightBlockStatus = [h \in {TRUSTED_HEIGHT} |-> "StateVerified"] + \* the latest verified block the the trusted block + /\ latestVerified = trustedLightBlock + +\* block should contain a copy of the block from the reference chain, with a matching commit +CopyLightBlockFromChain(block, height) == + LET ref == blockchain[height] + lastCommit == + IF height < ULTIMATE_HEIGHT + THEN blockchain[height + 1].lastCommit + \* for the ultimate block, which we never use, as ULTIMATE_HEIGHT = TARGET_HEIGHT + 1 + ELSE blockchain[height].VS + IN + block = [header |-> ref, Commits |-> lastCommit] + +\* Either the primary is correct and the block comes from the reference chain, +\* or the block is produced by a faulty primary. +\* +\* [LCV-FUNC-FETCH.1::TLA.1] +FetchLightBlockInto(block, height) == + IF IS_PRIMARY_CORRECT + THEN CopyLightBlockFromChain(block, height) + ELSE BC!IsLightBlockAllowedByDigitalSignatures(height, block) + +\* add a block into the light store +\* +\* [LCV-FUNC-UPDATE.1::TLA.1] +LightStoreUpdateBlocks(lightBlocks, block) == + LET ht == block.header.height IN + [h \in DOMAIN lightBlocks \union {ht} |-> + IF h = ht THEN block ELSE lightBlocks[h]] + +\* update the state of a light block +\* +\* [LCV-FUNC-UPDATE.1::TLA.1] +LightStoreUpdateStates(statuses, ht, blockState) == + [h \in DOMAIN statuses \union {ht} |-> + IF h = ht THEN blockState ELSE statuses[h]] + +\* Check, whether newHeight is a possible next height for the light client. +\* +\* [LCV-FUNC-SCHEDULE.1::TLA.1] +CanScheduleTo(newHeight, pLatestVerified, pNextHeight, pTargetHeight) == + LET ht == pLatestVerified.header.height IN + \/ /\ ht = pNextHeight + /\ ht < pTargetHeight + /\ pNextHeight < newHeight + /\ newHeight <= pTargetHeight + \/ /\ ht < pNextHeight + /\ ht < pTargetHeight + /\ ht < newHeight + /\ newHeight < pNextHeight + \/ /\ ht = pTargetHeight + /\ newHeight = pTargetHeight + +\* The loop of VerifyToTarget. +\* +\* [LCV-FUNC-MAIN.1::TLA-LOOP.1] +VerifyToTargetLoop == + \* the loop condition is true + /\ latestVerified.header.height < TARGET_HEIGHT + \* pick a light block, which will be constrained later + /\ \E current \in BC!LightBlocks: + \* Get next LightBlock for verification + /\ IF nextHeight \in DOMAIN fetchedLightBlocks + THEN \* copy the block from the light store + /\ current = fetchedLightBlocks[nextHeight] + /\ UNCHANGED fetchedLightBlocks + ELSE \* retrieve a light block and save it in the light store + /\ FetchLightBlockInto(current, nextHeight) + /\ fetchedLightBlocks' = LightStoreUpdateBlocks(fetchedLightBlocks, current) + \* Record that one more probe has been done (for complexity and model checking) + /\ nprobes' = nprobes + 1 + \* Verify the current block + /\ LET verdict == ValidAndVerified(latestVerified, current) IN + \* Decide whether/how to continue + CASE verdict = "OK" -> + /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateVerified") + /\ latestVerified' = current + /\ state' = + IF latestVerified'.header.height < TARGET_HEIGHT + THEN "working" + ELSE "finishedSuccess" + /\ \E newHeight \in HEIGHTS: + /\ CanScheduleTo(newHeight, current, nextHeight, TARGET_HEIGHT) + /\ nextHeight' = newHeight + + [] verdict = "CANNOT_VERIFY" -> + (* + do nothing: the light block current passed validation, but the validator + set is too different to verify it. We keep the state of + current at StateUnverified. For a later iteration, Schedule + might decide to try verification of that light block again. + *) + /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateUnverified") + /\ \E newHeight \in HEIGHTS: + /\ CanScheduleTo(newHeight, latestVerified, nextHeight, TARGET_HEIGHT) + /\ nextHeight' = newHeight + /\ UNCHANGED <> + + [] OTHER -> + \* verdict is some error code + /\ lightBlockStatus' = LightStoreUpdateStates(lightBlockStatus, nextHeight, "StateFailed") + /\ state' = "finishedFailure" + /\ UNCHANGED <> + +\* The terminating condition of VerifyToTarget. +\* +\* [LCV-FUNC-MAIN.1::TLA-LOOPCOND.1] +VerifyToTargetDone == + /\ latestVerified.header.height >= TARGET_HEIGHT + /\ state' = "finishedSuccess" + /\ UNCHANGED <> + +(********************* Lite client + Blockchain *******************) +Init == + \* the blockchain is initialized immediately to the ULTIMATE_HEIGHT + /\ BC!InitToHeight + \* the light client starts + /\ LCInit + +(* + The system step is very simple. + The light client is either executing VerifyToTarget, or it has terminated. + (In the latter case, a model checker reports a deadlock.) + Simultaneously, the global clock may advance. + *) +Next == + /\ state = "working" + /\ VerifyToTargetLoop \/ VerifyToTargetDone + /\ BC!AdvanceTime \* the global clock is advanced by zero or more time units + +(************************* Types ******************************************) +TypeOK == + /\ state \in States + /\ nextHeight \in HEIGHTS + /\ latestVerified \in BC!LightBlocks + /\ \E HS \in SUBSET HEIGHTS: + /\ fetchedLightBlocks \in [HS -> BC!LightBlocks] + /\ lightBlockStatus + \in [HS -> {"StateVerified", "StateUnverified", "StateFailed"}] + +(************************* Properties ******************************************) + +(* The properties to check *) +\* this invariant candidate is false +NeverFinish == + state = "working" + +\* this invariant candidate is false +NeverFinishNegative == + state /= "finishedFailure" + +\* This invariant holds true, when the primary is correct. +\* This invariant candidate is false when the primary is faulty. +NeverFinishNegativeWhenTrusted == + (*(minTrustedHeight <= TRUSTED_HEIGHT)*) + BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) + => state /= "finishedFailure" + +\* this invariant candidate is false +NeverFinishPositive == + state /= "finishedSuccess" + +(** + Correctness states that all the obtained headers are exactly like in the blockchain. + + It is always the case that every verified header in LightStore was generated by + an instance of Tendermint consensus. + + [LCV-DIST-SAFE.1::CORRECTNESS-INV.1] + *) +CorrectnessInv == + \A h \in DOMAIN fetchedLightBlocks: + lightBlockStatus[h] = "StateVerified" => + fetchedLightBlocks[h].header = blockchain[h] + +(** + Check that the sequence of the headers in storedLightBlocks satisfies ValidAndVerified = "OK" pairwise + This property is easily violated, whenever a header cannot be trusted anymore. + *) +StoredHeadersAreVerifiedInv == + state = "finishedSuccess" + => + \A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers + \/ lh >= rh + \* either there is a header between them + \/ \E mh \in DOMAIN fetchedLightBlocks: + lh < mh /\ mh < rh + \* or we can verify the right one using the left one + \/ "OK" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh]) + +\* An improved version of StoredHeadersAreSound, assuming that a header may be not trusted. +\* This invariant candidate is also violated, +\* as there may be some unverified blocks left in the middle. +StoredHeadersAreVerifiedOrNotTrustedInv == + state = "finishedSuccess" + => + \A lh, rh \in DOMAIN fetchedLightBlocks: \* for every pair of different stored headers + \/ lh >= rh + \* either there is a header between them + \/ \E mh \in DOMAIN fetchedLightBlocks: + lh < mh /\ mh < rh + \* or we can verify the right one using the left one + \/ "OK" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh]) + \* or the left header is outside the trusting period, so no guarantees + \/ ~BC!InTrustingPeriod(fetchedLightBlocks[lh].header) + +(** + * An improved version of StoredHeadersAreSoundOrNotTrusted, + * checking the property only for the verified headers. + * This invariant holds true. + *) +ProofOfChainOfTrustInv == + state = "finishedSuccess" + => + \A lh, rh \in DOMAIN fetchedLightBlocks: + \* for every pair of stored headers that have been verified + \/ lh >= rh + \/ lightBlockStatus[lh] = "StateUnverified" + \/ lightBlockStatus[rh] = "StateUnverified" + \* either there is a header between them + \/ \E mh \in DOMAIN fetchedLightBlocks: + lh < mh /\ mh < rh /\ lightBlockStatus[mh] = "StateVerified" + \* or the left header is outside the trusting period, so no guarantees + \/ ~(BC!InTrustingPeriod(fetchedLightBlocks[lh].header)) + \* or we can verify the right one using the left one + \/ "OK" = ValidAndVerified(fetchedLightBlocks[lh], fetchedLightBlocks[rh]) + +(** + * When the light client terminates, there are no failed blocks. (Otherwise, someone lied to us.) + *) +NoFailedBlocksOnSuccessInv == + state = "finishedSuccess" => + \A h \in DOMAIN fetchedLightBlocks: + lightBlockStatus[h] /= "StateFailed" + +\* This property states that whenever the light client finishes with a positive outcome, +\* the trusted header is still within the trusting period. +\* We expect this property to be violated. And Apalache shows us a counterexample. +PositiveBeforeTrustedHeaderExpires == + (state = "finishedSuccess") => BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) + +\* If the primary is correct and the initial trusted block has not expired, +\* then whenever the algorithm terminates, it reports "success" +CorrectPrimaryAndTimeliness == + (BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) + /\ state /= "working" /\ IS_PRIMARY_CORRECT) => + state = "finishedSuccess" + +(** + If the primary is correct and there is a trusted block that has not expired, + then whenever the algorithm terminates, it reports "success". + + [LCV-DIST-LIVE.1::SUCCESS-CORR-PRIMARY-CHAIN-OF-TRUST.1] + *) +SuccessOnCorrectPrimaryAndChainOfTrust == + (\E h \in DOMAIN fetchedLightBlocks: + lightBlockStatus[h] = "StateVerified" /\ BC!InTrustingPeriod(blockchain[h]) + /\ state /= "working" /\ IS_PRIMARY_CORRECT) => + state = "finishedSuccess" + +\* Lite Client Completeness: If header h was correctly generated by an instance +\* of Tendermint consensus (and its age is less than the trusting period), +\* then the lite client should eventually set trust(h) to true. +\* +\* Note that Completeness assumes that the lite client communicates with a correct full node. +\* +\* We decompose completeness into Termination (liveness) and Precision (safety). +\* Once again, Precision is an inverse version of the safety property in Completeness, +\* as A => B is logically equivalent to ~B => ~A. +PrecisionInv == + (state = "finishedFailure") + => \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period + \/ \E h \in DOMAIN fetchedLightBlocks: + LET lightBlock == fetchedLightBlocks[h] IN + \* the full node lied to the lite client about the block header + \/ lightBlock.header /= blockchain[h] + \* the full node lied to the lite client about the commits + \/ lightBlock.Commits /= lightBlock.header.VS + +\* the old invariant that was found to be buggy by TLC +PrecisionBuggyInv == + (state = "finishedFailure") + => \/ ~BC!InTrustingPeriod(blockchain[TRUSTED_HEIGHT]) \* outside of the trusting period + \/ \E h \in DOMAIN fetchedLightBlocks: + LET lightBlock == fetchedLightBlocks[h] IN + \* the full node lied to the lite client about the block header + lightBlock.header /= blockchain[h] + +\* the worst complexity +Complexity == + LET N == TARGET_HEIGHT - TRUSTED_HEIGHT + 1 IN + state /= "working" => + (2 * nprobes <= N * (N - 1)) + +(* + We omit termination, as the algorithm deadlocks in the end. + So termination can be demonstrated by finding a deadlock. + Of course, one has to analyze the deadlocked state and see that + the algorithm has indeed terminated there. +*) +============================================================================= +\* Modification History +\* Last modified Fri Jun 26 12:08:28 CEST 2020 by igor +\* Created Wed Oct 02 16:39:42 CEST 2019 by igor diff --git a/rust-spec/lightclient/verification/MC4_3_correct.tla b/rust-spec/lightclient/verification/MC4_3_correct.tla new file mode 100644 index 000000000..951a471da --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_3_correct.tla @@ -0,0 +1,15 @@ +---------------------------- MODULE MC4_3_correct --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 3 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == TRUE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================== diff --git a/rust-spec/lightclient/verification/MC4_3_faulty.tla b/rust-spec/lightclient/verification/MC4_3_faulty.tla new file mode 100644 index 000000000..c711ee9b8 --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_3_faulty.tla @@ -0,0 +1,15 @@ +---------------------------- MODULE MC4_3_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 3 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================== diff --git a/rust-spec/lightclient/verification/MC4_4_faulty.tla b/rust-spec/lightclient/verification/MC4_4_faulty.tla new file mode 100644 index 000000000..8b8d25ece --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_4_faulty.tla @@ -0,0 +1,15 @@ +---------------------------- MODULE MC4_4_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 4 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================== diff --git a/rust-spec/lightclient/verification/MC4_5_correct.tla b/rust-spec/lightclient/verification/MC4_5_correct.tla new file mode 100644 index 000000000..04489ec7f --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_5_correct.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC4_5_correct --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 5 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == TRUE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/rust-spec/lightclient/verification/MC4_5_faulty.tla b/rust-spec/lightclient/verification/MC4_5_faulty.tla new file mode 100644 index 000000000..11dbd2ec6 --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_5_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC4_5_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 5 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/rust-spec/lightclient/verification/MC4_6_faulty.tla b/rust-spec/lightclient/verification/MC4_6_faulty.tla new file mode 100644 index 000000000..d0d98444f --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_6_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC4_6_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 6 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/rust-spec/lightclient/verification/MC4_7_faulty.tla b/rust-spec/lightclient/verification/MC4_7_faulty.tla new file mode 100644 index 000000000..60dcd3c5d --- /dev/null +++ b/rust-spec/lightclient/verification/MC4_7_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC4_7_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 7 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/rust-spec/lightclient/verification/MC5_5_correct.tla b/rust-spec/lightclient/verification/MC5_5_correct.tla new file mode 100644 index 000000000..926501761 --- /dev/null +++ b/rust-spec/lightclient/verification/MC5_5_correct.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC5_5_correct --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4", "n5"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 5 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == TRUE + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/rust-spec/lightclient/verification/MC5_5_faulty.tla b/rust-spec/lightclient/verification/MC5_5_faulty.tla new file mode 100644 index 000000000..abf5e8c72 --- /dev/null +++ b/rust-spec/lightclient/verification/MC5_5_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC5_5_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4", "n5"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 5 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/rust-spec/lightclient/verification/MC5_7_faulty.tla b/rust-spec/lightclient/verification/MC5_7_faulty.tla new file mode 100644 index 000000000..5d3d265ab --- /dev/null +++ b/rust-spec/lightclient/verification/MC5_7_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC5_7_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4", "n5"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 7 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/rust-spec/lightclient/verification/MC7_5_faulty.tla b/rust-spec/lightclient/verification/MC7_5_faulty.tla new file mode 100644 index 000000000..ae8af692a --- /dev/null +++ b/rust-spec/lightclient/verification/MC7_5_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC7_5_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4", "n5", "n6", "n7"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 5 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, nprobes, fetchedLightBlocks, lightBlockStatus, + latestVerified, nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/rust-spec/lightclient/verification/MC7_7_faulty.tla b/rust-spec/lightclient/verification/MC7_7_faulty.tla new file mode 100644 index 000000000..84065214e --- /dev/null +++ b/rust-spec/lightclient/verification/MC7_7_faulty.tla @@ -0,0 +1,15 @@ +------------------------- MODULE MC7_7_faulty --------------------------- + +AllNodes == {"n1", "n2", "n3", "n4", "n5", "n6", "n7"} +TRUSTED_HEIGHT == 1 +TARGET_HEIGHT == 7 +TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-) +IS_PRIMARY_CORRECT == FALSE + +VARIABLES + state, nextHeight, fetchedLightBlocks, lightBlockStatus, latestVerified, + nprobes, + now, blockchain, Faulty + +INSTANCE Lightclient_A_1 +============================================================================ diff --git a/rust-spec/lightclient/verification/verification.md b/rust-spec/lightclient/verification/verification.md new file mode 100644 index 000000000..db68c74db --- /dev/null +++ b/rust-spec/lightclient/verification/verification.md @@ -0,0 +1,1162 @@ +# Light Client Verification + +The light client implements a read operation of a +[header][TMBC-HEADER-link] from the [blockchain][TMBC-SEQ-link], by +communicating with full nodes. As some full nodes may be faulty, this +functionality must be implemented in a fault-tolerant way. + +In the Tendermint blockchain, the validator set may change with every +new block. The staking and unbonding mechanism induces a [security +model][TMBC-FM-2THIRDS-link]: starting at time *Time* of the +[header][TMBC-HEADER-link], +more than two-thirds of the next validators of a new block are correct +for the duration of *TrustedPeriod*. The fault-tolerant read +operation is designed for this security model. + +The challenge addressed here is that the light client might have a +block of height *h1* and needs to read the block of height *h2* +greater than *h1*. Checking all headers of heights from *h1* to *h2* +might be too costly (e.g., in terms of energy for mobile devices). +This specification tries to reduce the number of intermediate blocks +that need to be checked, by exploiting the guarantees provided by the +[security model][TMBC-FM-2THIRDS-link]. + +# Status + +This document is thoroughly reviewed, and the protocol has been +formalized in TLA+ and model checked. + +## Issues that need to be addressed + +As it is part of the larger light node, its data structures and +functions interact with the fork dectection functionality of the light +client. As a result of the work on +[Pull Request 479](https://github.com/informalsystems/tendermint-rs/pull/479) we +established the need for an update in the data structures in [Issue 499](https://github.com/informalsystems/tendermint-rs/issues/499). This +will not change the verification logic, but it will record information +about verification that can be used in fork detection (in particular +in computing more efficiently the proof of fork). + +# Outline + +- [Part I](#part-i---tendermint-blockchain): Introduction of + relevant terms of the Tendermint +blockchain. + +- [Part II](#part-ii---sequential-definition-of-the-verification-problem): Introduction +of the problem addressed by the Lightclient Verification protocol. + - [Verification Informal Problem + statement](#Verification-Informal-Problem-statement): For the general + audience, that is, engineers who want to get an overview over what + the component is doing from a bird's eye view. + - [Sequential Problem statement](#Sequential-Problem-statement): + Provides a mathematical definition of the problem statement in + its sequential form, that is, ignoring the distributed aspect of + the implementation of the blockchain. + +- [Part III](#part-iii---light-client-as-distributed-system): Distributed + aspects of the light client, system assumptions and temporal + logic specifications. + + - [Incentives](#incentives): how faulty full nodes may benefit from + misbehaving and how correct full nodes benefit from cooperating. + + - [Computational Model](#Computational-Model): + timing and correctness assumptions. + + - [Distributed Problem Statement](#Distributed-Problem-Statement): + temporal properties that formalize safety and liveness + properties in the distributed setting. + +- [Part IV](#part-iv---light-client-verification-protocol): + Specification of the protocols. + + - [Definitions](#Definitions): Describes inputs, outputs, + variables used by the protocol, auxiliary functions + + - [Core Verification](#core-verification): gives an outline of the solution, + and details of the functions used (with preconditions, + postconditions, error conditions). + + - [Liveness Scenarios](#liveness-scenarios): when the light + client makes progress depends heavily on the changes in the + validator sets of the blockchain. We discuss some typical scenarios. + +- [Part V](#part-v---supporting-the-ibc-relayer): The above parts + focus on a common case where the last verified block has height *h1* + and the + requested height *h2* satisfies *h2 > h1*. For IBC, there are + scenarios where this might not be the case. In this part, we provide + some preliminaries for supporting this. As not all details of the + IBC requirements are clear by now, we do not provide a complete + specification at this point. We mark with "Open Question" points + that need to be addressed in order to finalize this specification. + It should be noted that the technically + most challenging case is the one specified in Part IV. + +In this document we quite extensively use tags in order to be able to +reference assumptions, invariants, etc. in future communication. In +these tags we frequently use the following short forms: + +- TMBC: Tendermint blockchain +- SEQ: for sequential specifications +- LCV: Lightclient Verification +- LIVE: liveness +- SAFE: safety +- FUNC: function +- INV: invariant +- A: assumption + +# Part I - Tendermint Blockchain + +## Header Fields necessary for the Light Client + +#### **[TMBC-HEADER.1]** + +A set of blockchain transactions is stored in a data structure called +*block*, which contains a field called *header*. (The data structure +*block* is defined [here][block]). As the header contains hashes to +the relevant fields of the block, for the purpose of this +specification, we will assume that the blockchain is a list of +headers, rather than a list of blocks. + +#### **[TMBC-HASH-UNIQUENESS.1]** + +We assume that every hash in the header identifies the data it hashes. +Therefore, in this specification, we do not distinguish between hashes and the +data they represent. + +#### **[TMBC-HEADER-FIELDS.1]** + +A header contains the following fields: + +- `Height`: non-negative integer +- `Time`: time (integer) +- `LastBlockID`: Hashvalue +- `LastCommit` DomainCommit +- `Validators`: DomainVal +- `NextValidators`: DomainVal +- `Data`: DomainTX +- `AppState`: DomainApp +- `LastResults`: DomainRes + +#### **[TMBC-SEQ.1]** + +The Tendermint blockchain is a list *chain* of headers. + +#### **[TMBC-VALIDATOR-PAIR.1]** + +Given a full node, a +*validator pair* is a pair *(peerID, voting_power)*, where + +- *peerID* is the PeerID (public key) of a full node, +- *voting_power* is an integer (representing the full node's + voting power in a certain consensus instance). + +> In the Golang implementation the data type for *validator +pair* is called `Validator` + +#### **[TMBC-VALIDATOR-SET.1]** + +A *validator set* is a set of validator pairs. For a validator set +*vs*, we write *TotalVotingPower(vs)* for the sum of the voting powers +of its validator pairs. + +#### **[TMBC-VOTE.1]** + +A *vote* contains a `prevote` or `precommit` message sent and signed by +a validator node during the execution of [consensus][arXiv]. Each +message contains the following fields + +- `Type`: prevote or precommit +- `Height`: positive integer +- `Round` a positive integer +- `BlockID` a Hashvalue of a block (not necessarily a block of the chain) + +#### **[TMBC-COMMIT.1]** + +A commit is a set of `precommit` message. + +## Tendermint Failure Model + +#### **[TMBC-AUTH-BYZ.1]** + +We assume the authenticated Byzantine fault model in which no node (faulty or +correct) may break digital signatures, but otherwise, no additional +assumption is made about the internal behavior of faulty +nodes. That is, faulty nodes are only limited in that they cannot forge +messages. + +#### **[TMBC-TIME-PARAMS.1]** + +A Tendermint blockchain has the following configuration parameters: + +- *unbondingPeriod*: a time duration. +- *trustingPeriod*: a time duration smaller than *unbondingPeriod*. + +#### **[TMBC-CORRECT.1]** + +We define a predicate *correctUntil(n, t)*, where *n* is a node and *t* is a +time point. +The predicate *correctUntil(n, t)* is true if and only if the node *n* +follows all the protocols (at least) until time *t*. + +#### **[TMBC-FM-2THIRDS.1]** + +If a block *h* is in the chain, +then there exists a subset *CorrV* +of *h.NextValidators*, such that: + +- *TotalVotingPower(CorrV) > 2/3 + TotalVotingPower(h.NextValidators)*; cf. [TMBC-VALIDATOR-SET.1] +- For every validator pair *(n,p)* in *CorrV*, it holds *correctUntil(n, + h.Time + trustingPeriod)*; cf. [TMBC-CORRECT.1] + +> The definition of correct +> [**[TMBC-CORRECT.1]**][TMBC-CORRECT-link] refers to realtime, while it +> is used here with *Time* and *trustingPeriod*, which are "hardware +> times". We do not make a distinction here. + +#### **[TMBC-CORR-FULL.1]** + +Every correct full node locally stores a prefix of the +current list of headers from [**[TMBC-SEQ.1]**][TMBC-SEQ-link]. + +## What the Light Client Checks + +> From [TMBC-FM-2THIRDS.1] we directly derive the following observation: + +#### **[TMBC-VAL-CONTAINS-CORR.1]** + +Given a (trusted) block *tb* of the blockchain, a given set of full nodes +*N* contains a correct node at a real-time *t*, if + +- *t - trustingPeriod < tb.Time < t* +- the voting power in tb.NextValidators of nodes in *N* is more + than 1/3 of *TotalVotingPower(tb.NextValidators)* + +> The following describes how a commit for a given block *b* must look +> like. + +#### **[TMBC-SOUND-DISTR-POSS-COMMIT.1]** + +For a block *b*, each element *pc* of *PossibleCommit(b)* satisfies: + +- *pc* contains only votes (cf. [TMBC-VOTE.1]) + by validators from *b.Validators* +- the sum of the voting powers in *pc* is greater than 2/3 + *TotalVotingPower(b.Validators)* +- and there is an *r* such that each vote *v* in *pc* satisfies + - v.Type = precommit + - v.Height = b.Height + - v.Round = r + - v.blockID = hash(b) + +> The following property comes from the validity of the [consensus][arXiv]: A +> correct validator node only sends `prevote` or `precommit`, if +> `BlockID` of the new (to-be-decided) block is equal to the hash of +> the last block. + +#### **[TMBC-VAL-COMMIT.1]** + +If for a block *b*, a commit *c* + +- contains at least one validator pair *(v,p)* such that *v* is a + **correct** validator node, and +- is contained in *PossibleCommit(b)* + +then the block *b* is on the blockchain. + +## Context of this document + +In this document we specify the light client verification component, +called *Core Verification*. The *Core Verification* communicates with +a full node. As full nodes may be faulty, it cannot trust the +received information, but the light client has to check whether the +header it receives coincides with the one generated by Tendermint +consensus. + +The two + properties [[TMBC-VAL-CONTAINS-CORR.1]][TMBC-VAL-CONTAINS-CORR-link] and +[[TMBC-VAL-COMMIT]][TMBC-VAL-COMMIT-link] formalize the checks done + by this specification: +Given a trusted block *tb* and an untrusted block *ub* with a commit *cub*, +one has to check that *cub* is in *PossibleCommit(ub)*, and that *cub* +contains a correct node using *tb*. + +# Part II - Sequential Definition of the Verification Problem + +## Verification Informal Problem statement + +Given a height *targetHeight* as an input, the *Verifier* eventually +stores a header *h* of height *targetHeight* locally. This header *h* +is generated by the Tendermint [blockchain][block]. In +particular, a header that was not generated by the blockchain should +never be stored. + +## Sequential Problem statement + +#### **[LCV-SEQ-LIVE.1]** + +The *Verifier* gets as input a height *targetHeight*, and eventually stores the +header of height *targetHeight* of the blockchain. + +#### **[LCV-SEQ-SAFE.1]** + +The *Verifier* never stores a header which is not in the blockchain. + +# Part III - Light Client as Distributed System + +## Incentives + +Faulty full nodes may benefit from lying to the light client, by making the +light client accept a block that deviates (e.g., contains additional +transactions) from the one generated by Tendermint consensus. +Users using the light client might be harmed by accepting a forged header. + +The [fork detector][fork-detector] of the light client may help the +correct full nodes to understand whether their header is a good one. +Hence, in combination with the light client detector, the correct full +nodes have the incentive to respond. We can thus base liveness +arguments on the assumption that correct full nodes reliably talk to +the light client. + +## Computational Model + +#### **[LCV-A-PEER.1]** + +The verifier communicates with a full node called *primary*. No assumption is made about the full node (it may be correct or faulty). + +#### **[LCV-A-COMM.1]** + +Communication between the light client and a correct full node is +reliable and bounded in time. Reliable communication means that +messages are not lost, not duplicated, and eventually delivered. There +is a (known) end-to-end delay *Delta*, such that if a message is sent +at time *t* then it is received and processes by time *t + Delta*. +This implies that we need a timeout of at least *2 Delta* for remote +procedure calls to ensure that the response of a correct peer arrives +before the timeout expires. + +#### **[LCV-A-TFM.1]** + +The Tendermint blockchain satisfies the Tendermint failure model [**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link]. + +#### **[LCV-A-VAL.1]** + +The system satisfies [**[TMBC-AUTH-BYZ.1]**][TMBC-Auth-Byz-link] and +[**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link]. Thus, there is a +blockchain that satisfies the soundness requirements (that is, the +validation rules in [[block]]). + +## Distributed Problem Statement + +### Two Kinds of Termination + +We do not assume that *primary* is correct. Under this assumption no +protocol can guarantee the combination of the sequential +properties. Thus, in the (unreliable) distributed setting, we consider +two kinds of termination (successful and failure) and we will specify +below under what (favorable) conditions *Core Verification* ensures to +terminate successfully, and satisfy the requirements of the sequential +problem statement: + +#### **[LCV-DIST-TERM.1]** + +*Core Verification* either *terminates +successfully* or it *terminates with failure*. + +### Design choices + +#### **[LCV-DIST-STORE.1]** + +*Core Verification* has a local data structure called *LightStore* that +contains light blocks (that contain a header). For each light block we +record whether it is verified. + +#### **[LCV-DIST-PRIMARY.1]** + +*Core Verification* has a local variable *primary* that contains the PeerID of a full node. + +#### **[LCV-DIST-INIT.1]** + +*LightStore* is initialized with a header *trustedHeader* that was correctly +generated by the Tendermint consensus. We say *trustedHeader* is verified. + +### Temporal Properties + +#### **[LCV-DIST-SAFE.1]** + +It is always the case that every verified header in *LightStore* was +generated by an instance of Tendermint consensus. + +#### **[LCV-DIST-LIVE.1]** + +From time to time, a new instance of *Core Verification* is called with a +height *targetHeight* greater than the height of any header in *LightStore*. +Each instance must eventually terminate. + +- If + - the *primary* is correct (and locally has the block of + *targetHeight*), and + - *LightStore* always contains a verified header whose age is less than the + trusting period, + then *Core Verification* adds a verified header *hd* with height + *targetHeight* to *LightStore* and it **terminates successfully** + +> These definitions imply that if the primary is faulty, a header may or +> may not be added to *LightStore*. In any case, +> [**[LCV-DIST-SAFE.1]**](#lcv-vc-inv) must hold. +> The invariant [**[LCV-DIST-SAFE.1]**](#lcv-dist-safe) and the liveness +> requirement [**[LCV-DIST-LIVE.1]**](#lcv-dist-life) +> allow that verified headers are added to *LightStore* whose +> height was not passed +> to the verifier (e.g., intermediate headers used in bisection; see below). +> Note that for liveness, initially having a *trustedHeader* within +> the *trustinPeriod* is not sufficient. However, as this +> specification will leave some freedom with respect to the strategy +> in which order to download intermediate headers, we do not give a +> more precise liveness specification here. After giving the +> specification of the protocol, we will discuss some liveness +> scenarios [below](#liveness-scenarios). + +### Solving the sequential specification + +This specification provides a partial solution to the sequential specification. +The *Verifier* solves the invariant of the sequential part + +[**[LCV-DIST-SAFE.1]**](#lcv-vc-inv) => [**[LCV-SEQ-SAFE.1]**](#lcv-seq-inv) + +In the case the primary is correct, and there is a recent header in *LightStore*, the verifier satisfies the liveness requirements. + +⋀ *primary is correct* +⋀ always ∃ verified header in LightStore. *header.Time* > *now* - *trustingPeriod* +⋀ [**[LCV-A-Comm.1]**](#lcv-a-comm) ⋀ ( + ( [**[TMBC-CorrFull.1]**][TMBC-CorrFull-link] ⋀ + [**[LCV-DIST-LIVE.1]**](#lcv-vc-live) ) + ⟹ [**[LCV-SEQ-LIVE.1]**](#lcv-seq-live) +) + +# Part IV - Light Client Verification Protocol + +We provide a specification for Light Client Verification. The local +code for verification is presented by a sequential function +`VerifyToTarget` to highlight the control flow of this functionality. +We note that if a different concurrency model is considered for +an implementation, the sequential flow of the function may be +implemented with mutexes, etc. However, the light client verification +is partitioned into three blocks that can be implemented and tested +independently: + +- `FetchLightBlock` is called to download a light block (header) of a + given height from a peer. +- `ValidAndVerified` is a local code that checks the header. +- `Schedule` decides which height to try to verify next. We keep this + underspecified as different implementations (currently in Goland and + Rust) may implement different optimizations here. We just provide + necessary conditions on how the height may evolve. + + + + +## Definitions + +### Data Types + +The core data structure of the protocol is the LightBlock. + +#### **[LCV-DATA-LIGHTBLOCK.1]** + +```go +type LightBlock struct { + Header Header + Commit Commit + Validators ValidatorSet + NextValidators ValidatorSet + Provider PeerID +} +``` + +#### **[LCV-DATA-LIGHTSTORE.1]** + +LightBlocks are stored in a structure which stores all LightBlock from +initialization or received from peers. + +```go +type LightStore struct { + ... +} + +``` + +Each LightBlock is in one of the following states: + +```go +type VerifiedState int + +const ( + StateUnverified = iota + 1 + StateVerified + StateFailed + StateTrusted +) +``` + +> Only the detector module sets a lightBlock state to `StateTrusted` +> and only if it was `StateVerified` before. + +The LightStore exposes the following functions to query stored LightBlocks. + +```go +func (ls LightStore) Get(height Height) (LightBlock, bool) +``` + +- Expected postcondition + - returns a LightBlock at a given height or false in the second argument if + the LightStore does not contain the specified LightBlock. + +```go +func (ls LightStore) LatestVerified() LightBlock +``` + +- Expected postcondition + - returns the highest light block whose state is `StateVerified` + or `StateTrusted` + +#### **[LCV-FUNC-UPDATE.1]** + +```go +func (ls LightStore) Update(lightBlock LightBlock, verfiedState VerifiedState) +``` + +- Expected postcondition + - The state of the LightBlock is set to *verifiedState*. + +> The following function is used only in the detector specification +> listed here for completeness. + +```go +func (ls LightStore) LatestTrusted() LightBlock +``` + +- Expected postcondition + - returns the highest light block that has been verified and + checked by the detector. + +### Inputs + +- *lightStore*: stores light blocks that have been downloaded and that + passed verification. Initially it contains a light block with + *trustedHeader*. +- *primary*: peerID +- *targetHeight*: the height of the needed header + +### Configuration Parameters + +- *trustThreshold*: a float. Can be used if correctness should not be based on more voting power and 1/3. +- *trustingPeriod*: a time duration [**[TMBC-TIME_PARAMS.1]**][TMBC-TIME_PARAMS-link]. +- *clockDrift*: a time duration. Correction parameter dealing with only approximately synchronized clocks. + +### Variables + +- *nextHeight*: initially *targetHeight* + > *nextHeight* should be thought of the "height of the next header we need + > to download and verify" + +### Assumptions + +#### **[LCV-A-INIT.1]** + +- *trustedHeader* is from the blockchain + +- *targetHeight > LightStore.LatestVerified.Header.Height* + +### Invariants + +#### **[LCV-INV-TP.1]** + +It is always the case that *LightStore.LatestTrusted.Header.Time > now - trustingPeriod*. + +> If the invariant is violated, the light client does not have a +> header it can trust. A trusted header must be obtained externally, +> its trust can only be based on social consensus. + +### Used Remote Functions + +We use the functions `commit` and `validators` that are provided +by the [RPC client for Tendermint][RPC]. + +```go +func Commit(height int64) (SignedHeader, error) +``` + +- Implementation remark + - RPC to full node *n* + - JSON sent: + +```javascript +// POST /commit +{ + "jsonrpc": "2.0", + "id": "ccc84631-dfdb-4adc-b88c-5291ea3c2cfb", // UUID v4, unique per request + "method": "commit", + "params": { + "height": 1234 + } +} +``` + +- Expected precondition + - header of `height` exists on blockchain +- Expected postcondition + - if *n* is correct: Returns the signed header of height `height` + from the blockchain if communication is timely (no timeout) + - if *n* is faulty: Returns a signed header with arbitrary content +- Error condition + - if *n* is correct: precondition violated or timeout + - if *n* is faulty: arbitrary error + +---- + +```go +func Validators(height int64) (ValidatorSet, error) +``` + +- Implementation remark + - RPC to full node *n* + - JSON sent: + +```javascript +// POST /validators +{ + "jsonrpc": "2.0", + "id": "ccc84631-dfdb-4adc-b88c-5291ea3c2cfb", // UUID v4, unique per request + "method": "validators", + "params": { + "height": 1234 + } +} +``` + +- Expected precondition + - header of `height` exists on blockchain +- Expected postcondition + - if *n* is correct: Returns the validator set of height `height` + from the blockchain if communication is timely (no timeout) + - if *n* is faulty: Returns arbitrary validator set +- Error condition + - if *n* is correct: precondition violated or timeout + - if *n* is faulty: arbitrary error + +---- + +### Communicating Function + +#### **[LCV-FUNC-FETCH.1]** + + ```go +func FetchLightBlock(peer PeerID, height Height) LightBlock +``` + +- Implementation remark + - RPC to peer at *PeerID* + - calls `Commit` for *height* and `Validators` for *height* and *height+1* +- Expected precondition + - `height` is less than or equal to height of the peer **[LCV-IO-PRE-HEIGHT.1]** +- Expected postcondition: + - if *node* is correct: + - Returns the LightBlock *lb* of height `height` + that is consistent with the blockchain + - *lb.provider = peer* **[LCV-IO-POST-PROVIDER.1]** + - *lb.Header* is a header consistent with the blockchain + - *lb.Validators* is the validator set of the blockchain at height *nextHeight* + - *lb.NextValidators* is the validator set of the blockchain at height *nextHeight + 1* + - if *node* is faulty: Returns a LightBlock with arbitrary content + [**[TMBC-AUTH-BYZ.1]**][TMBC-Auth-Byz-link] +- Error condition + - if *n* is correct: precondition violated + - if *n* is faulty: arbitrary error + - if *lb.provider != peer* + - times out after 2 Delta (by assumption *n* is faulty) + +---- + +## Core Verification + +### Outline + +The `VerifyToTarget` is the main function and uses the following functions. + +- `FetchLightBlock` is called to download the next light block. It is + the only function that communicates with other nodes +- `ValidAndVerified` checks whether header is valid and checks if a + new lightBlock should be trusted + based on a previously verified lightBlock. +- `Schedule` decides which height to try to verify next + +In the following description of `VerifyToTarget` we do not deal with error +handling. If any of the above function returns an error, VerifyToTarget just +passes the error on. + +#### **[LCV-FUNC-MAIN.1]** + +```go +func VerifyToTarget(primary PeerID, lightStore LightStore, + targetHeight Height) (LightStore, Result) { + + nextHeight := targetHeight + + for lightStore.LatestVerified.height < targetHeight { + + // Get next LightBlock for verification + current, found := lightStore.Get(nextHeight) + if !found { + current = FetchLightBlock(primary, nextHeight) + lightStore.Update(current, StateUnverified) + } + + // Verify + verdict = ValidAndVerified(lightStore.LatestVerified, current) + + // Decide whether/how to continue + if verdict == OK { + lightStore.Update(current, StateVerified) + } + else if verdict == CANNOT_VERIFY { + // do nothing + // the light block current passed validation, but the validator + // set is too different to verify it. We keep the state of + // current at StateUnverified. For a later iteration, Schedule + // might decide to try verification of that light block again. + } + else { + // verdict is some error code + lightStore.Update(current, StateFailed) + // possibly remove all LightBlocks from primary + return (lightStore, ResultFailure) + } + nextHeight = Schedule(lightStore, nextHeight, targetHeight) + } + return (lightStore, ResultSuccess) +} +``` + +- Expected precondition + - *lightStore* contains a LightBlock within the *trustingPeriod* **[LCV-PRE-TP.1]** + - *targetHeight* is greater than the height of all the LightBlocks in *lightStore* +- Expected postcondition: + - returns *lightStore* that contains a LightBlock that corresponds to a block + of the blockchain of height *targetHeight* + (that is, the LightBlock has been added to *lightStore*) **[LCV-POST-LS.1]** +- Error conditions + - if the precondition is violated + - if `ValidAndVerified` or `FetchLightBlock` report an error + - if [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) is violated + +### Details of the Functions + +#### **[LCV-FUNC-VALID.1]** + +```go +func ValidAndVerified(trusted LightBlock, untrusted LightBlock) Result +``` + +- Expected precondition: + - *untrusted* is valid, that is, satisfies the soundness [checks][block] + - *untrusted* is **well-formed**, that is, + - *untrusted.Header.Time < now + clockDrift* + - *untrusted.Validators = hash(untrusted.Header.Validators)* + - *untrusted.NextValidators = hash(untrusted.Header.NextValidators)* + - *trusted.Header.Time > now - trustingPeriod* + - *trusted.Commit* is a commit for the header + *trusted.Header*, i.e., it contains + the correct hash of the header, and +2/3 of signatures + - the `Height` and `Time` of `trusted` are smaller than the Height and + `Time` of `untrusted`, respectively + - the *untrusted.Header* is well-formed (passes the tests from + [[block]]), and in particular + - if the untrusted header `unstrusted.Header` is the immediate + successor of `trusted.Header`, then it holds that + - *trusted.Header.NextValidators = + untrusted.Header.Validators*, and + moreover, + - *untrusted.Header.Commit* + - contains signatures by more than two-thirds of the validators + - contains no signature from nodes that are not in *trusted.Header.NextValidators* +- Expected postcondition: + - Returns `OK`: + - if *untrusted* is the immediate successor of *trusted*, or otherwise, + - if the signatures of a set of validators that have more than + *max(1/3,trustThreshold)* of voting power in + *trusted.Nextvalidators* is contained in + *untrusted.Commit* (that is, header passes the tests + [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] + and [**[TMBC-VAL-COMMIT.1]**][TMBC-VAL-COMMIT-link]) + - Returns `CANNOT_VERIFY` if: + - *untrusted* is *not* the immediate successor of + *trusted* + and the *max(1/3,trustThreshold)* threshold is not reached + (that is, if + [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] + fails and header is does not violate the soundness + checks [[block]]). +- Error condition: + - if precondition violated + +---- + +#### **[LCV-FUNC-SCHEDULE.1]** + +```go +func Schedule(lightStore, nextHeight, targetHeight) Height +``` + +- Implementation remark: If picks the next height to be verified. + We keep the precise choice of the next header under-specified. It is + subject to performance optimizations that do not influence the correctness +- Expected postcondition: **[LCV-SCHEDULE-POST.1]** + Return *H* s.t. + 1. if *lightStore.LatestVerified.Height = nextHeight* and + *lightStore.LatestVerified < targetHeight* then + *nextHeight < H <= targetHeight* + 2. if *lightStore.LatestVerified.Height < nextHeight* and + *lightStore.LatestVerified.Height < targetHeight* then + *lightStore.LatestVerified.Height < H < nextHeight* + 3. if *lightStore.LatestVerified.Height = targetHeight* then + *H = targetHeight* + +> Case i. captures the case where the light block at height *nextHeight* +> has been verified, and we can choose a height closer to the *targetHeight*. +> As we get the *lightStore* as parameter, the choice of the next height can +> depend on the *lightStore*, e.g., we can pick a height for which we have +> already downloaded a light block. +> In Case ii. the header of *nextHeight* could not be verified, and we need to pick a smaller height. +> In Case iii. is a special case when we have verified the *targetHeight*. + +### Solving the distributed specification + +*trustedStore* is implemented by the light blocks in lightStore that +have the state *StateVerified*. + +#### Argument for [**[LCV-DIST-SAFE.1]**](#lcv-dist-safe) + +- `ValidAndVerified` implements the soundness checks and the checks + [**[TMBC-VAL-CONTAINS-CORR.1]**][TMBC-VAL-CONTAINS-CORR-link] and + [**[TMBC-VAL-COMMIT.1]**][TMBC-VAL-COMMIT-link] under + the assumption [**[TMBC-FM-2THIRDS.1]**][TMBC-FM-2THIRDS-link] +- Only if `ValidAndVerified` returns with `OK`, the state of a light block is + set to *StateVerified*. + +#### Argument for [**[LCV-DIST-LIVE.1]**](#lcv-dist-life) + +- If *primary* is correct, + - `FetchLightBlock` will always return a light block consistent + with the blockchain + - `ValidAndVerified` either verifies the header using the trusting + period or falls back to sequential + verification + - If [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) holds, eventually every + header will be verified and core verification **terminates successfully**. + - successful termination depends on the age of *lightStore.LatestVerified* + (for instance, initially on the age of *trustedHeader*) and the + changes of the validator sets on the blockchain. + We will give some examples [below](#liveness-scenarios). +- If *primary* is faulty, + - it either provides headers that pass all the tests, and we + return with the header + - it provides one header that fails a test, core verification + **terminates with failure**. + - it times out and core verification + **terminates with failure**. + +## Liveness Scenarios + +The liveness argument above assumes [**[LCV-INV-TP.1]**](#LCV-INV-TP.1) + +which requires that there is a header that does not expire before the +target height is reached. Here we discuss scenarios to ensure this. + +Let *startHeader* be *LightStore.LatestVerified* when core +verification is called (*trustedHeader*) and *startTime* be the time +core verification is invoked. + +In order to ensure liveness, *LightStore* always needs to contain a +verified (or initially trusted) header whose time is within the +trusting period. To ensure this, core verification needs to add new +headers to *LightStore* and verify them, before all headers in +*LightStore* expire. + +#### Many changes in validator set + + Let's consider `Schedule` implements + bisection, that is, it halves the distance. + Assume the case where the validator set changes completely in each +block. Then the + method in this specification needs to +sequentially verify all headers. That is, for + +- *W = log_2 (targetHeight - startHeader.Height)*, + +*W* headers need to be downloaded and checked before the +header of height *startHeader.Height + 1* is added to *LightStore*. + +- Let *Comp* + be the local computation time needed to check headers and signatures + for one header. +- Then we need in the worst case *Comp + 2 Delta* to download and + check one header. +- Then the first time a verified header could be added to *LightStore* is + startTime + W * (Comp + 2 Delta) +- [TP.1] However, it can only be added if we still have a header in + *LightStore*, + which is not + expired, that is only the case if + - startHeader.Time > startTime + WCG * (Comp + 2 Delta) - + trustingPeriod, + - that is, if core verification is started at + startTime < startHeader.Time + trustingPeriod - WCG * (Comp + 2 Delta) + +- one may then do an inductive argument from this point on, depending + on the implementation of `Schedule`. We may have to account for the + headers that are already + downloaded, but they are checked against the new *LightStore.LatestVerified*. + +> We observe that +> the worst case time it needs to verify the header of height +> *targetHeight* depends mainly on how frequent the validator set on the +> blockchain changes. That core verification terminates successfully +> crucially depends on the check [TP.1], that is, that the headers in +> *LightStore* do not expire in the time needed to download more +> headers, which depends on the creation time of the headers in +> *LightStore*. That is, termination of core verification is highly +> depending on the data stored in the blockchain. +> The current light client core verification protocol exploits that, in +> practice, changes in the validator set are rare. For instance, +> consider the following scenario. + +#### No change in validator set + +If on the blockchain the validator set of the block at height +*targetHeight* is equal to *startHeader.NextValidators*: + +- there is one round trip in `FetchLightBlock` to download the light + block + of height + *targetHeight*, and *Comp* to check it. +- as the validator sets are equal, `Verify` returns `OK`, if + *startHeader.Time > now - trustingPeriod*. +- that is, if *startTime < startHeader.Header.Time + trustingPeriod - + 2 Delta - Comp*, then core verification terminates successfully + +# Part V - Supporting the IBC Relayer + +The above specification focuses on the most common case, which also +constitutes the most challenging task: using the Tendermint [security +model][TMBC-FM-2THIRDS-link] to verify light blocks without +downloading all intermediate blocks. To focus on this challenge, above +we have restricted ourselves to the case where *targetHeight* is +greater than the height of any trusted header. This simplified +presentation of the algorithm as initially +`lightStore.LatestVerified()` is less than *targetHeight*, and in the +process of verification `lightStore.LatestVerified()` increases until +*targetHeight* is reached. + +For [IBC][ibc-rs] it might be that some "older" header is +needed, that is, *targetHeight < lightStore.LatestVerified()*. In this section we present a preliminary design, and we mark some +remaining open questions. +If *targetHeight < lightStore.LatestVerified()* our design separates +the following cases: + +- A previous instance of `VerifyToTarget` has already downloaded the + light block of *targetHeight*. There are two cases + - the light block has been verified + - the light block has not been verified yet +- No light block of *targetHeight* had been downloaded before. There + are two cases: + - there exists a verified light block of height less than *targetHeight* + - otherwise. In this case we need to do "backwards verification" + using the hash of the previous block in the `LastBlockID` field + of a header. + +**Open Question:** what are the security assumptions for backward +verification. Should we check that the light block we verify from +(and/or the checked light block) is within the trusting period? + +The design just presents the above case +distinction as a function, and defines some auxiliary functions in the +same way the protocol was presented in +[Part IV](#part-iv---light-client-verification-protocol). + +```go +func (ls LightStore) LatestPrevious(height Height) (LightBlock, bool) +``` + +- Expected postcondition + - returns a light block *lb* that satisfies: + - *lb* is in lightStore + - *lb* is verified and not expired + - *lb.Header.Height < height* + - for all *b* in lightStore s.t. *b* is verified and not expired it + holds *lb.Header.Height >= b.Header.Height* + - *false* in the second argument if + the LightStore does not contain such an *lb*. + +```go +func (ls LightStore) MinVerified() (LightBlock, bool) +``` + +- Expected postcondition + - returns a light block *lb* that satisfies: + - *lb* is in lightStore + - *lb* is verified **Open Question:** replace by trusted? + - *lb.Header.Height* is minimal in the lightStore + - **Open Question:** according to this, it might be expired (outside the + trusting period). This approach appears safe. Are there reasons we + should not do that? + - *false* in the second argument if + the LightStore does not contain such an *lb*. + +If a height that is smaller than the smallest height in the lightstore +is required, we check the hashes backwards. This is done with the +following function: + +#### **[LCV-FUNC-BACKWARDS.1]** + +```go +func Backwards (primary PeerID, lightStore LightStore, targetHeight Height) + (LightStore, Result) { + + lb,res = lightStore.MinVerified() + if res = false { + return (lightStore, ResultFailure) + } + + latest := lb.Header + for i := lb.Header.height - 1; i >= targetHeight; i-- { + // here we download height-by-height. We might first download all + // headers down to targetHeight and then check them. + current := FetchLightBlock(primary,i) + if (hash(current) != latest.Header.LastBlockId) { + return (lightStore, ResultFailure) + } + else { + lightStore.Update(current, StateVerified) + // **Open Question:** Do we need a new state type for + // backwards verified light blocks? + } + latest = current + } + return (lightStore, ResultSuccess) +} +``` + +The following function just decided based on the required height which +method should be used. + +#### **[LCV-FUNC-IBCMAIN.1]** + +```go +func Main (primary PeerID, lightStore LightStore, targetHeight Height) + (LightStore, Result) { + + b1, r1 = lightStore.Get(targetHeight) + if r1 = true and b1.State = StateVerified { + // block already there + return (lightStore, ResultSuccess) + } + + if targetHeight > lightStore.LatestVerified.height { + // case of Part IV + return VerifyToTarget(primary, lightStore, targetHeight) + } + else { + b2, r2 = lightStore.LatestPrevious(targetHeight); + if r2 = true { + // make auxiliary lightStore auxLS to call VerifyToTarget. + // VerifyToTarget uses LatestVerified of the given lightStore + // For that we need: + // auxLS.LatestVerified = lightStore.LatestPrevious(targetHeight) + auxLS.Init; + auxLS.Update(b2,StateVerified); + if r1 = true { + // we need to verify a previously downloaded light block. + // we add it to the auxiliary store so that VerifyToTarget + // does not download it again + auxLS.Update(b1,b1.State); + } + auxLS, res2 = VerifyToTarget(primary, auxLS, targetHeight) + // move all lightblocks from auxLS to lightStore, + // maintain state + // we do that whether VerifyToTarget was successful or not + for i, s range auxLS { + lighStore.Update(s,s.State) + } + return (lightStore, res2) + } + else { + return Backwards(primary, lightStore, targetHeight) + } + } +} +``` + + + + + + + + + + + + + + + + + + + +# References + +[[block]] Specification of the block data structure. + +[[RPC]] RPC client for Tendermint + +[[fork-detector]] The specification of the light client fork detector. + +[[fullnode]] Specification of the full node API + +[[ibc-rs]] Rust implementation of IBC modules and relayer. + +[[lightclient]] The light client ADR [77d2651 on Dec 27, 2019]. + +[RPC]: https://docs.tendermint.com/master/rpc/ + +[block]: https://github.com/tendermint/spec/blob/d46cd7f573a2c6a2399fcab2cde981330aa63f37/spec/core/data_structures.md + +[TMBC-HEADER-link]: #tmbc-header1 +[TMBC-SEQ-link]: #tmbc-seq1 +[TMBC-CorrFull-link]: #tmbc-corr-full1 +[TMBC-Auth-Byz-link]: #tmbc-auth-byz1 +[TMBC-TIME_PARAMS-link]: #tmbc-time-params1 +[TMBC-FM-2THIRDS-link]: #tmbc-fm-2thirds1 +[TMBC-VAL-CONTAINS-CORR-link]: #tmbc-val-contains-corr1 +[TMBC-VAL-COMMIT-link]: #tmbc-val-commit1 +[TMBC-SOUND-DISTR-POSS-COMMIT-link]: #tmbc-sound-distr-poss-commit1 + +[lightclient]: https://github.com/interchainio/tendermint-rs/blob/e2cb9aca0b95430fca2eac154edddc9588038982/docs/architecture/adr-002-lite-client.md +[fork-detector]: https://github.com/informalsystems/tendermint-rs/blob/master/docs/spec/lightclient/detection.md +[fullnode]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md + +[ibc-rs]:https://github.com/informalsystems/ibc-rs + +[FN-LuckyCase-link]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md#fn-luckycase + +[blockchain-validator-set]: https://github.com/tendermint/spec/blob/master/spec/blockchain/blockchain.md#data-structures +[fullnode-data-structures]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md#data-structures + +[FN-ManifestFaulty-link]: https://github.com/tendermint/spec/blob/master/spec/blockchain/fullnode.md#fn-manifestfaulty + +[arXiv]: https://arxiv.org/abs/1807.04938