From c09933153d8fd76dfdab96802341cba03fcf2dee Mon Sep 17 00:00:00 2001
From: jbk <2634358021@qq.com>
Date: Sat, 24 Dec 2022 21:20:22 +0800
Subject: [PATCH 1/8] add articles/20221224-riscv-memory-consistency-model.md
---
...20221224-riscv-memory-consistency-model.md | 240 ++++++++++++++++++
1 file changed, 240 insertions(+)
create mode 100644 articles/20221224-riscv-memory-consistency-model.md
diff --git a/articles/20221224-riscv-memory-consistency-model.md b/articles/20221224-riscv-memory-consistency-model.md
new file mode 100644
index 0000000..4b6f866
--- /dev/null
+++ b/articles/20221224-riscv-memory-consistency-model.md
@@ -0,0 +1,240 @@
+> Corrector: [TinyCorrect](https://gitee.com/tinylab/tinycorrect) v0.1 - [codeblock]
+> Author: Kyrie jia bokai021013@gmail.com
+> Date: 2022/12/24
+> Revisor: Falcon falcon@tinylab.org
+> Project: [RISC-V Linux 内核剖析](https://gitee.com/tinylab/riscv-linux)
+> Proposal: [RISC-V Linux Synchronization 技术调研与分析](https://gitee.com/tinylab/riscv-linux/issues/I5MUAN)
+> Sponsor: PLCT Lab, ISCAS
+
+# RISC-V 架构内存一致性模型调研
+
+## 前言
+
+在进行单机并发编程操作时，计算机一般是通过内部互联总线，采用读写共享内存的方式完成对共享数据的访问。而为了提高处理性能，芯片厂商在硬件层面加了许多优化，并且不同的处理器架构采取的优化方法也不尽相同，这就导致可能会出现不同的内存乱序访问行为，因而会给软件程序员带来相当大的困扰。 下面给出一个示例：
+
+```c
+static int A = 0, B = 0, C = 0 ;
+static void thread_cpu1(void)
+{
+ C = 1;
+ A = 1;
+}
+static void thread_cpu2(void)
+{
+ while(A == 0) ;
+ B = 1 ;
+}
+static void thread_cpu3(void)
+{
+ while(B == 0) ;
+ printf("A = %d, C = %d\n", A, B);
+}
+
+```
+
+如上所示，三个处理器（P1，P2，P3）共享A，B，C三个初始化为0的变量，那么最终的输出结果会是什么呢？可能大多数人心中的答案是**A == 1 && C == 1**，这是最符合直觉的答案，但其实**A == 0 && C == 1，A == 1 && C == 0 ， A == 1 && C == 0**，这些答案都是有可能的。而这就跟处理器之间是否能**看见**变量的最新修改值有关了。
+
+>**看见** :当一个处理器（PA）对共享变量（V）的本地副本进行了修改，而另一个处理器（PB）用于保存相应变量的缓存行因此而失效或被更新，则称 PB 看见了 PA 对变量 V 的修改
+
+以 **A == 0 && C == 1** 为例，当 P1 上的赋值语句 C = 1 及 A = 1 完成之后，P2 看见 P1 对 A 的修改，从而跳出循环并执行 B = 1，接下来 P3 看见 P2 对 B 的修改，从而跳出循环并打印 A，C。在打印 A，C 时，存在这样的可能，也即 P3 看见了 P1 对 C 的修改，而没看见 P1 对 A 的修改，从而打印出 **A == 0 && C == 1**。
+
+也就是说，当你以为 C = 1 执行完之后，所有处理器都应该看见 C 的最新值，但实际可能并不是这样，有的处理器确实看不到最新值导致结果和预期不一样。而内存一致性模型就是为了解决这个问题的。
+
+## 内存一致性模型简介
+
+内存一致性模型（Memory Consistency Model）是用来描述多处理器（多线程）对共享存储器访问行为的规范，在不同的内存一致性模型里，多线程对共享存储器的访问行为有非常大的差别。这些差别会严重影响程序的执行逻辑，甚至会造成软件逻辑问题。
+
+### 内存一致性模型分类
+
+内存一致性关注对内存的读写操作访问，由此可得到4种不同的指令组合，依次为Store-Load、Store-Store、Load-Store、Load-Load，通过允许调整这些指令组合执行的顺序，可以获得不同的内存一致性模型。目前有多种内存一致性模型，从上到下模型的限制由强到弱，依次为:
+
+- 顺序一致性（Sequential Consistency，简写SC）模型
+- 完全存储定序（Total Store Order，简写TSO）模型
+- 部分存储定序（Part Store Order，简写PSO）模型
+- 宽松存储（Relax Memory Order，简写RMO）模型
+
+#### SC模型
+
+SC模型也称为强定序模型，CPU按照程序代码的指令次序来执行所有的Store与Load指令，并且从其它CPU和内存的角度来看，感知到的数据变化也完全是按照指令执行的次序。在这种模型下，程序不需要使用任何内存屏障，但是性能会比较差。为了提升系统的性能，不同处理器架构或多或少对这种强一致性模型进行了放松，允许对某些指令组合进行重排序。
+
+> **重排序**:是指编译器和处理器为了优化程序性能而对指令序列进行重新排序的一种手段。
+
+#### TSO模型
+
+TSO模型允许对Store-Load指令组合进行重排序，即如果第一条指令是Store指令，第二条指令是Load指令，那么在程序执行时，Load指令可能先于Store指令执行。TSO模型的硬件实现，通常是在CPU和Cache之间引入了Store Buffer，Store Buffer只有Store（即内存写）指令会使用到，并且Store Buffer以FIFO（先进先出）的方式处理写入的数据。这种情况下，Store-Store指令组合仍能按照顺序执行，但Load指令则可能会先于Store指令完成执行。x86架构采用的就是TSO模型。
+
+#### PSO模型
+
+PSO模型是在TSO模型的基础上，进一步放宽内存访问限制，允许对Store-Store指令组合进行重排序。从硬件实现的角度来看，就是允许了CPU以非FIFO的方式处理Store Buffer中的指令。
+
+#### RMO模型
+
+RMO模型是最为宽松的内存一致性模型，它在PSO模型的基础上进一步放宽了访存指令的执行限制，其不仅允许Store-Load、Store-Store指令组合重排序，还进一步允许了Load-Load、Load-Store指令组合重排序，只要是地址无关的指令，在读写访问的时候都可以打乱所有load/store的顺序。而我们接下来要研究的RISC-V架构采用的就是RMO模型。
+
+## RISC-V内存一致性模型
+
+2015年左右，普林斯顿团队发现RISC-V最初采用的内存一致性规范存在一定的缺陷，自2015年12月起，RISC-V 基金会一直与普林斯顿团队以及其他 MCM 专家合作，帮助加强 RISC-V ISA 规范。官方于2019年发布的[《The RISC-V Instruction Set Manual, Volume I: User-Level ISA》](https://github.com/riscv/riscv-isa-manual/releases/download/Ratified-IMAFDQC/riscv-spec-20191213.pdf)明确了RISC-V的内存一致性模型，将其称为“RVWMO” (RISC-V Weak Memory Ordering)。
+
+RVWMO主要遵循RMO模型，旨在提供可以灵活地构建高性能可扩展程序的设计，同时提供一个易于处理的编程模型，禁止过于复杂的重排序情况，方便软件程序员的开发利用。RVWMO明确了3条公理，规范了常规内存的一致性要求，但仍没有规范I/O内存，指令抓取，页表遍历等行为。下面我们来看一下官方的定义：
+
+### 定义
+
+RVWMO内存模型是根据全局内存序（ global memory order）定义的，即所有hart产生的内存操作的总顺序。一般来说，多线程程序有许多种可能的执行顺序，每个执行顺序都有自己相应的全局内存序，规定明确指出任何满足所有内存模型约束的执行都是合法的执行(就内存模型而言)。
+
+> RISC-V用hart（hardware thread）表示硬件执行线程或执行单元
+>
+> **全局序**即所有并发线程在内存系统中形成的最终内存访问顺序，各个线程对这个**全局序**的观察都是一致的（除了store buffer带来的“写后读”情况）
+
+#### 内存模型规则
+
+内存操作的程序序（program order）反映了生成每次加载和存储的指令在该hart的动态指令流中的逻辑布局顺序；内存访问指令会生成内存操作，即load/store/load&&store 操作。对于这些操作集合，RVWMO做出了这些规定：
+
+##### 遵守拷贝原子性
+
+RVWMO通过**全局序**定义内存访问顺序约束，对于不允许重排序的情况称为**保留程序序**（preserved program order，PPO）。store buffer是hart私有缓存，用于暂时存储要写入内存系统的数据，这里的数据对本hart可见，即写后再读可以读到这个写入的值，但对其它hart不可见（读不到写入的最新值），也因此双方可能观察到不一样的访问顺序。
+
+因此RVWMO为了形成一致的全局序，规定一个hart如果**看见**另一个hart的写，则必须所有的hart都**看见**这个写，否则会出现不一致（实际硬件实现并不一定有这种“同时**看见**”时间保证）。这个特性称为拷贝原子性。
+
+##### 存在保留程序序
+
+保留程序序的完整定义是：如果内存操作a，b都是常规主存访问（非I/O访问），且在程序序中a领先于b，并且满足以下任意一项条件，即满足在保留程序序中，a领先于b。
+
+- 地址重叠约束
+- 显式同步
+- 语法依赖
+- 流水线依赖
+
+下面分别介绍一下上述条件：
+
+###### 地址重叠约束
+
+对于指令地址部分交叉重叠，规则约束的是这些重叠的部分，第一个原则是：**写不超前**，即对于store指令来说，在全局序上不能超越前面的指令，否则前面读到或者写入的值就会混乱。
+
+第二个原则是：**读-读一致性**，对于同一地址的读操作来说，只要后一个读不到更老的值，就不约束两者内存序，也就是说仅当这两个读之间没有对同一地址的写操作且返回不同值时（读到了不同的写），才要保证读的顺序。
+
+第三个原则是：**原子操作不乱序**，原子指令因为含有store操作，因此当其位于程序序的后面时不会超越前面的指令。当其位于前面时，如果后面的是store指令不会乱序，如果是load指令，规范明确不允许乱序，主要是为了保证原子指令的操作语义。需要注意的是，对于LR/SC原子指令对，成功的SC才代表这个原子指令的执行，失败的SC不产生任何内存操作，自然也不对内存序约束产生任何贡献。
+
+###### 显式同步
+
+RISC-V中定义了一个FENCE 指令用于提供相同硬件线程上写指令内存与指令获取之间的显式同步，约束了可以乱序执行的指令范围，一般来说，fence指令前后的指令不能交换顺序。
+
+```
+格式：fence [iorw], [iorw]
+
+逗号前后的iorw分别表示fence指令要约束的前后指令的类型，i表示设备输入，o表示设备输出，r表示内存读，w表示内存写。
+```
+
+对于常规内存访问规范只推荐了5种组合：
+
+- FENCE RW,RW
+- FENCE RW,W
+- FENCE R,RW
+- FENCE R,R
+- FENCE W,W
+
+当需要跨越内存种类明确约束访问顺序时，只能使用fence指令。特别地，访问time、cycle、mcycle控制状态寄存器（CSR）时可能需要fence指令，因为CSRs通常为弱内存序的内存映射I/O单元，与常规内存也无必然的顺序约束；在使用时用i表示CSR读，o表示CSR写。
+
+###### 语法依赖
+
+语法依赖（syntactic dependency）是指一条指令的源操作数与前面指令（不一定紧邻）的目的操作数是同一个寄存器，前面不出结果后面没法执行，这种逻辑上的限制“自然而然”地约束指令顺序。
+
+这里需要与语义依赖区别开，语法依赖是同一寄存器的限制，而语义依赖是变量值的依赖；并且不是所有指令都有目的操作数和源操作数的，因此没有指令会语法依赖一条store语句，因为它没有目的操作数，也没有一条load指令语法依赖其他指令，因为它没有源操作数。下面给出一个示例：
+
+```assembly
+(a) ld a1,0(s0)
+(b) xor a2,a1,a1
+(c) add s1,s1,a2
+(d) ld a5,0(s1)
+```
+
+这里(b)指令的源操作数在a1寄存器里，而(a)指令的目的操作数也在a1寄存器里，所以(b)指令语法依赖(a)指令，同理，(c)语法依赖(b)，(d)语法依赖(c)，这个指令序列自上而下地构成了一个依赖链，因此两条不相关的内存读指令(a)和(d)，被强制地保证了执行顺序。
+
+对于内存访问操作，语法依赖按寄存器用途分为三类并保证有序：
+
+- **地址依赖**。前一条指令的结果是后一条访存指令的操作地址。如：`lw t1, (s0); lw t2, (t1)`。
+
+- **数据依赖**。前一条指令的结果是后一条指令的操作数。如：`lw t1, (s0); sw t1, (s1)`。
+
+- **控制依赖**。两条指令间存在一个依赖于第一条指令的分支或间接跳转指令。用C语言的if语句比拟：条件语句对后续的所有指令（包括语句块之外的指令）构成控制依赖。但RVWMO仅保证对后续的store指令有序。如下所示：
+
+ ```
+ (a) lw x1,0(x2)
+ (b) bne x1,x0,next
+ (c) next: sw x3,0(x4)
+ ```
+
+ (b)依赖于(a)且是一个分支跳转语句，因此使(a)和(c) 语句执行有序，这就是控制依赖。
+
+###### 流水线依赖
+
+如果多条指令之间可能存在依赖关系，那么它们不能随意地同时在处理器的多个流水线单元上同时执行，这称为指令流水线依赖，也就是说要保证指令流水线的执行有序。如下所示：
+
+```
+ 代码1 代码2 代码3 代码4
+-------------------------------------------------------------
+(a) lw t0, (s0) lw t0, (s0) lw, t0, (s0) lw, t0, (s0)
+(b) sw t1, (t0) sw t0, (t1) sw, t1, (t0) lw, t1, (t0)
+(c) lw t2, (t0) lw t2, (t1) sw, t2, (s1) sw, t2, (s1)
+```
+
+这四段特殊的代码范例都是前两条指令构成语法依赖，第三条指令进行相关的读或不知是否相关的写，RISC-V根据“几乎所有真实CPU流水线执行机构的行为”，将这种范例中(a)和(c)的关系称为**流水线依赖**，并明确规定不能乱序。约束代码1和2的出发点是“在写地址或值未知时不能读这个写”，即(b)地址或值未确定时(c)不能执行，又因为(b)地址或数据依赖(a)，因此(c)在**全局序**上不能超越(a)。约束代码3和4的出发点是“前面地址未知时不能写”，即(b)地址未确定时(c)不能执行，以防止地址冲突，又因为(b)地址依赖(a)，因此(c)在全局序上也不能超越(a)。也就是说这个流水线必须保证指令有序执行。
+
+##### 提供内存模型原语
+
+RVWMO指令集为加载(load)和存储(store)等内存操作提供了一组内存模型原语, 用于对相关指令进行标注，其实也算是显式同步的一种方法。这里原语如下：
+
+```
+ 与处理器一致 顺序一致
+ 加载 acquire-RCpc acquire-RCsc
+ 释放 release-RCpc release-RCsc
+```
+
+同时标准扩展A(atomic)也提供了原子操作指令，用于构建线程同步操作，同时提供了可选的单向内存序约束标记如下：
+
+- .aq，约束为acquire内存序，后续的不论是读还是写指令都不超前于本指令执行，如：`amoswap.w.aq`。.aq不约束前面的指令。注意：只有aq标记而没有rl标记的sc指令是不合适的。
+- .rl，约束为release内存序，前面的不论是读还是写指令都在本指令前完成，如：`sc.rl`。.rl不约束后面的指令，但RISC-V规定如果后面的指令有aq标记，则约束其不能超越rl标记指令，也就是同一hart的acquire-release标记保护的关键区不交叉、不乱序（这种RC模型称为RCsc，相应允许交叉的称为RCpc）。注意：没有aq标记而只有rl标记的lr指令也是不合适的。
+- .aqrl，约束为顺序一致（Sequential Consistency，SC）内存序，前面的读写指令发生在本指令之前，后面的发生在本指令之后。对于lr/sc原子指令对来说，SC内存序约束应采用`lr.aq/sc.aqrl`序列，因为该原子指令执行的标志是成功的sc操作，sc.aqrl确保了前后指令均不越界；反过来如`lr.aqrl/sc.rl`，其它hart可能观察到sc后的指令发生在sc之前；当然`lr.aqrl/sc.aqrl`是可以的，但一般没必要。
+- 全省略时，没有约束。
+
+#### 内存模型公理
+
+RISC-V程序的执行遵循RVWMO内存一致性模型，前提是存在一个符合保留程序序的全局内存序，并且满足返回值公理、原子性公理和进度公理。下面我们分别介绍这三个公理。
+
+##### 返回值公理
+
+每个load i操作的每个字节都需要返回由store操作（保证在以下store操作中的全局内存序是最新的）写入该字节的值，即读操作返回最近的对同一个地址写操作的值。
+
+> 1.存储了写入字节并且全局内存序在i之前
+>
+> 2.存储了写入字节并且程序序在i之前
+
+##### 原子性公理
+
+如果r和w是由对齐的LR和SC指令在一个hart h中生成的成对的load和store操作，s是一个store x字节的指令，r返回一个由s写入的值，那么s必须在全局内存序中位于w之前，并且在全局内存序中，在s后面和w前面不能有除h以外的hart store 这x字节的指令。
+
+> AMO和LR/SC 的原子性：
+>
+> AMOs在内存中获取一个旧值，执行算术操作(交换除外)，并将新值写入内存，所有这些都在一个原子操作中完成。
+>
+> LR 获取一个预定，如果预定有效SC会 执行store操作，然后释放预定；预定可以以任何理由被取消，但如果预定地址范围与任何其他hart之间存在store，则必须终止该预定。
+
+##### 进度公理
+
+在全局内存序中，任何内存操作之前都不能有无限序列的其他内存操作。
+
+> 意味着更强的公平性，一致性模型保证序列都可以得到执行。
+
+### 总结
+
+RVWMO模型提供了硬件与软件之间的一层接口，使软件程序员能根据这个模型实现并发编程，得益于它的宽松内存序。而RISC-V还提供了一种比RVWMO更严格的内存一致性模型，用于支持“全存储排序”，即“Ztso” 扩展，主要是为了便于从x86体系结构向RISC-V迁移，提供了完全兼容x86架构的RVTSO（RISC-V Total Store Ordering）内存模型。可以看出RISC-V正处在发展的黄金时期，与其他架构相比，具有强大的竞争力。
+
+## 参考资料
+
+- https://riscv.org/wp-content/uploads/2018/05/14.25-15.00-RISCVMemoryModelTutorial.pdf
+- https://github.com/riscv/riscv-isa-manual
+- https://riscv.org/technical/specifications/
+- https://zhuanlan.zhihu.com/p/422848235
+- https://gitee.com/laokz/OS-kernel-test/tree/master/memorder
+
+
+
--
Gitee
From f3de227b37f46d76daaa44f0fc501e555d412aab Mon Sep 17 00:00:00 2001
From: jbk <2634358021@qq.com>
Date: Sun, 25 Dec 2022 21:29:34 +0800
Subject: [PATCH 2/8] check the rules of RVWMO
---
...20221224-riscv-memory-consistency-model.md | 197 ++++++++++--------
...3\351\241\271\346\235\241\344\273\266.png" | Bin 0 -> 84299 bytes
2 files changed, 111 insertions(+), 86 deletions(-)
create mode 100644 "articles/images/20221224-riscv-consistency-memory-model/13\351\241\271\346\235\241\344\273\266.png"
diff --git a/articles/20221224-riscv-memory-consistency-model.md b/articles/20221224-riscv-memory-consistency-model.md
index 4b6f866..96557ef 100644
--- a/articles/20221224-riscv-memory-consistency-model.md
+++ b/articles/20221224-riscv-memory-consistency-model.md
@@ -10,7 +10,7 @@
## 前言
-在进行单机并发编程操作时，计算机一般是通过内部互联总线，采用读写共享内存的方式完成对共享数据的访问。而为了提高处理性能，芯片厂商在硬件层面加了许多优化，并且不同的处理器架构采取的优化方法也不尽相同，这就导致可能会出现不同的内存乱序访问行为，因而会给软件程序员带来相当大的困扰。 下面给出一个示例：
+在进行单机并发编程操作时，计算机一般是通过内部互联总线，采用读写共享内存的方式完成对共享数据的访问。而为了提高处理性能，芯片厂商在硬件层面加了许多优化，然而不同的处理器架构采取的优化方法也不尽相同，这就导致可能会出现不同的内存乱序访问行为，对编译器的处理会造成很大影响，同时也会给软件程序员带来相当大的困扰。 下面给出一个示例：
```c
static int A = 0, B = 0, C = 0 ;
@@ -75,156 +75,181 @@ RMO模型是最为宽松的内存一致性模型，它在PSO模型的基础上
2015年左右，普林斯顿团队发现RISC-V最初采用的内存一致性规范存在一定的缺陷，自2015年12月起，RISC-V 基金会一直与普林斯顿团队以及其他 MCM 专家合作，帮助加强 RISC-V ISA 规范。官方于2019年发布的[《The RISC-V Instruction Set Manual, Volume I: User-Level ISA》](https://github.com/riscv/riscv-isa-manual/releases/download/Ratified-IMAFDQC/riscv-spec-20191213.pdf)明确了RISC-V的内存一致性模型，将其称为“RVWMO” (RISC-V Weak Memory Ordering)。
-RVWMO主要遵循RMO模型，旨在提供可以灵活地构建高性能可扩展程序的设计，同时提供一个易于处理的编程模型，禁止过于复杂的重排序情况，方便软件程序员的开发利用。RVWMO明确了3条公理，规范了常规内存的一致性要求，但仍没有规范I/O内存，指令抓取，页表遍历等行为。下面我们来看一下官方的定义：
+RVWMO主要遵循RMO模型，旨在提供可以灵活地构建高性能可扩展程序的设计，同时提供一个易于处理的编程模型，禁止过于复杂的重排序情况，方便软件程序员的开发利用。RVWMO明确规定了13条规则和3条公理，下面我们来看一下官方的定义：
-### 定义
+### 定义与规则
-RVWMO内存模型是根据全局内存序（ global memory order）定义的，即所有hart产生的内存操作的总顺序。一般来说，多线程程序有许多种可能的执行顺序，每个执行顺序都有自己相应的全局内存序，规定明确指出任何满足所有内存模型约束的执行都是合法的执行(就内存模型而言)。
+RVWMO内存模型是根据全局内存序（ global memory order）定义的，一般来说，多线程程序有许多种可能的执行顺序，每个执行顺序都有自己相应的全局内存序，规定明确指出任何满足所有内存模型约束的执行都是合法的执行(就内存模型而言)。
> RISC-V用hart（hardware thread）表示硬件执行线程或执行单元
>
> **全局序**即所有并发线程在内存系统中形成的最终内存访问顺序，各个线程对这个**全局序**的观察都是一致的（除了store buffer带来的“写后读”情况）
-#### 内存模型规则
+内存操作的**程序序**（program order）反映了生成每次加载和存储的指令在该hart的动态指令流中的逻辑布局顺序；内存访问指令会生成内存操作，即load/store/load&&store 操作。**保留程序序**（preserved program order）指在全局程序序下的符合规定程序序的子集。如果内存操作a，b都是常规内存访问（非I/O访问），且在**程序序**中a领先于b，并且满足RVWMO指出的13项条件之一，即满足在**保留程序序**中，a领先于b。下面我们来分析这13项条件：
-内存操作的程序序（program order）反映了生成每次加载和存储的指令在该hart的动态指令流中的逻辑布局顺序；内存访问指令会生成内存操作，即load/store/load&&store 操作。对于这些操作集合，RVWMO做出了这些规定：
+
-##### 遵守拷贝原子性
+#### RULE 1
-RVWMO通过**全局序**定义内存访问顺序约束，对于不允许重排序的情况称为**保留程序序**（preserved program order，PPO）。store buffer是hart私有缓存，用于暂时存储要写入内存系统的数据，这里的数据对本hart可见，即写后再读可以读到这个写入的值，但对其它hart不可见（读不到写入的最新值），也因此双方可能观察到不一样的访问顺序。
+定义：如果指令A，B(store指令)访问相同地址（或者有地址重叠），那么A必须在全局内存序上领先于B。示例如下：
-因此RVWMO为了形成一致的全局序，规定一个hart如果**看见**另一个hart的写，则必须所有的hart都**看见**这个写，否则会出现不一致（实际硬件实现并不一定有这种“同时**看见**”时间保证）。这个特性称为拷贝原子性。
+```
+ hart1 hart2
+A1: lw t1,0(s0) B1: sw t2,0(s0)
+A2: sw t1,0(s1) B2: sw t3,0(s1)
+```
+
+因为B指令进行的是内存写（store）操作，那么对于并行的A，B来说，如果A指令不能在B指令的结果被所有处理器看见之前读入该地址(s0)的值，那么A指令读到的值，就可能与B写入相同地址(s0)的值发生冲突。同理，A指令进行的内存写操作，也必须先于B指令被看见，否则写入时也会发生冲突。
+
+因此这条规则也可以称之为**写不超前**规则，对所有的store指令来说，程序序在它们之前的指令在全局序上也要在它们之前，否则就会产生冲突。
-##### 存在保留程序序
+#### RULE 2
-保留程序序的完整定义是：如果内存操作a，b都是常规主存访问（非I/O访问），且在程序序中a领先于b，并且满足以下任意一项条件，即满足在保留程序序中，a领先于b。
+定义：对同一地址（或者有地址重叠）的两个内存读（load指令）A，B指令也需要保证顺序，但是有两个例外：
-- 地址重叠约束
-- 显式同步
-- 语法依赖
-- 流水线依赖
+1.都是读同一个写操作返回的值
-下面分别介绍一下上述条件：
+2.B指令读的是在A，B程序序之间的一条写指令写入的值（这条写指令将数据存在了store buffer 里）
-###### 地址重叠约束
+示例如下：
-对于指令地址部分交叉重叠，规则约束的是这些重叠的部分，第一个原则是：**写不超前**，即对于store指令来说，在全局序上不能超越前面的指令，否则前面读到或者写入的值就会混乱。
+```
+ hart1 hart2
+E: li s0,1 F: li s0,2
+A: lw t1,0(s0) B: lw t2,0(s0)
+C: sw t1,0(s1) D: sw t3,0(s1)
+```
-第二个原则是：**读-读一致性**，对于同一地址的读操作来说，只要后一个读不到更老的值，就不约束两者内存序，也就是说仅当这两个读之间没有对同一地址的写操作且返回不同值时（读到了不同的写），才要保证读的顺序。
+当两个hart对同一个地址写入数据时，如果不保证顺序，则A，B指令读到的结果有4种可能，这无疑是糟糕的，所以需要保持指令在程序中的顺序。但是如果我们将F指令修改为与E指令相同，那这时A，B指令其实读的都是同一个写操作的值，所以不会发生混乱，也就不需要保持A，B的顺序，这就是规定中的第一种特例。又或者我们在A指令之后（程序序），B指令之前加入F，这时B可以从store buffer里确定自己读的值，并且经过检查后这个值也会被写入内存，不会造成冲突，于是B也可以在全局内存序上领先于A，这就是第二种特例。除这两种特例以外，其他的同一地址读都需要保证全局内存有序。
-第三个原则是：**原子操作不乱序**，原子指令因为含有store操作，因此当其位于程序序的后面时不会超越前面的指令。当其位于前面时，如果后面的是store指令不会乱序，如果是load指令，规范明确不允许乱序，主要是为了保证原子指令的操作语义。需要注意的是，对于LR/SC原子指令对，成功的SC才代表这个原子指令的执行，失败的SC不产生任何内存操作，自然也不对内存序约束产生任何贡献。
+#### RULE 3
-###### 显式同步
+定义:A指令执行**原子内存操作**（AMO）或**条件写**（SC）操作，与B指令（load）访问的地址有重叠，那么A，B必须在全局内存序上有序。
-RISC-V中定义了一个FENCE 指令用于提供相同硬件线程上写指令内存与指令获取之间的显式同步，约束了可以乱序执行的指令范围，一般来说，fence指令前后的指令不能交换顺序。
+这里A指令执行的**原子内存操作**，即**一系列的内存读，并且后面也可能有内存写操作，不可被打断**，因此如果与B指令有地址重叠，那么必须要保证全局内存顺序，否则原子性就可能被破坏掉，B读到的值也就没办法确定。而对于**条件写**（SC指令），通常和LL（Load-linked）一起出现，LL运算返回目的地址的当前变量值，之后进行判断，**只有当上一次加载的值在此期间没有更新时，SC指令才会在该内存位置保存新值**，否则SC指令失败，这同样也是一种原子操作，所以若B指令在该操作期间读，也将不能确定读到的值。
-```
-格式：fence [iorw], [iorw]
+所以对于原子操作来说，如果两条指令有地址重叠，那么一定要保证全局内存有序。
+
+#### RULE 4
+
+定义：fence指令前的A指令在全局内存序上领先于fence指令后的B指令。
+
+这里规则定义了前趋集和后继集，分别包括了常规内存读写和I/O读写，也就是说：
-逗号前后的iorw分别表示fence指令要约束的前后指令的类型，i表示设备输入，o表示设备输出，r表示内存读，w表示内存写。
+```
+fence [r],[w]
```
-对于常规内存访问规范只推荐了5种组合：
+意味着r指令（read）在全局序领先于w指令（write）。
-- FENCE RW,RW
-- FENCE RW,W
-- FENCE R,RW
-- FENCE R,R
-- FENCE W,W
+fence指令用于提供相同硬件线程上写指令内存与指令获取之间的显式同步，约束了可以乱序执行的指令范围，便于跨越内存种类明确约束访问顺序。
-当需要跨越内存种类明确约束访问顺序时，只能使用fence指令。特别地，访问time、cycle、mcycle控制状态寄存器（CSR）时可能需要fence指令，因为CSRs通常为弱内存序的内存映射I/O单元，与常规内存也无必然的顺序约束；在使用时用i表示CSR读，o表示CSR写。
+#### RULE 5-7
-###### 语法依赖
+定义：为了保证宽松一致性，原子内存操作（AMOs）和LR/SC操作可以选择使用原语。
-语法依赖（syntactic dependency）是指一条指令的源操作数与前面指令（不一定紧邻）的目的操作数是同一个寄存器，前面不出结果后面没法执行，这种逻辑上的限制“自然而然”地约束指令顺序。
+**原语**，一般是指由若干条指令组成的程序段，用来实现某个特定功能，在执行过程中不可被中断。这里规定的原语有两个：acquire和release，分别用.aq和.rl来表示。所有程序序在acquire之后的操作在全局序中也在其后，所有程序序在release之前的操作在全局序中也在其之前，且程序序acquire在release之前，全局序中也应保持acquire在release之前。
-这里需要与语义依赖区别开，语法依赖是同一寄存器的限制，而语义依赖是变量值的依赖；并且不是所有指令都有目的操作数和源操作数的，因此没有指令会语法依赖一条store语句，因为它没有目的操作数，也没有一条load指令语法依赖其他指令，因为它没有源操作数。下面给出一个示例：
+前两个规定指出了分别利用.aq和.rl进行内存顺序约束的方法，即.aq约束指令在其后执行，.rl约束指令在其之前执行，但是二者同时出现时，也就是说一个程序段出现了两个原语保护区段，为了保证不会出现重叠冲突，规定了.aq必须在.rl之前执行。
-```assembly
-(a) ld a1,0(s0)
-(b) xor a2,a1,a1
-(c) add s1,s1,a2
-(d) ld a5,0(s1)
+```
+A: .aq
+B: li s0,1
+C: lw t1,0(s0)
+D: sw t1,0(s1)
+E: .rl
```
-这里(b)指令的源操作数在a1寄存器里，而(a)指令的目的操作数也在a1寄存器里，所以(b)指令语法依赖(a)指令，同理，(c)语法依赖(b)，(d)语法依赖(c)，这个指令序列自上而下地构成了一个依赖链，因此两条不相关的内存读指令(a)和(d)，被强制地保证了执行顺序。
+上述示例就是利用.aq和.rl进行顺序约束，整个指令的执行顺序就是程序序，因此.aqrl的约束是顺序一致（Sequential Consistency，SC）内存序。
-对于内存访问操作，语法依赖按寄存器用途分为三类并保证有序：
+#### RULE 8
-- **地址依赖**。前一条指令的结果是后一条访存指令的操作地址。如：`lw t1, (s0); lw t2, (t1)`。
+定义：一个LR（load-reserve）操作必须在与之成对的SC操作全局可见之前确定值。
+
+```
+LR: rd,(rs1) SC: rd,rs2,(rs1)
+```
-- **数据依赖**。前一条指令的结果是后一条指令的操作数。如：`lw t1, (s0); sw t1, (s1)`。
+LR 指令是从内存地址 rs1 中加载内容到 rd 寄存器，然后在 rs1 对应地址上设置**保留标记**(reservation set)，SC 指令在把 rs2 值写到 rs1 地址之前，会先判断 rs1 内存地址是否有设置保留标记，如果设置了，则把 rs2 值正常写入到 rs1 内存地址里，并把 rd 寄存器设置成 0，表示保存成功。如果 rs1 内存地址没有设置保留标记，则不保存，并把 rd 寄存器设置成 1 表示保存失败。
-- **控制依赖**。两条指令间存在一个依赖于第一条指令的分支或间接跳转指令。用C语言的if语句比拟：条件语句对后续的所有指令（包括语句块之外的指令）构成控制依赖。但RVWMO仅保证对后续的store指令有序。如下所示：
+因此SC操作需要前置的LR操作结果，这就构成了全局内存顺序约束。
- ```
- (a) lw x1,0(x2)
- (b) bne x1,x0,next
- (c) next: sw x3,0(x4)
- ```
+#### RULE 9-11
- (b)依赖于(a)且是一个分支跳转语句，因此使(a)和(c) 语句执行有序，这就是控制依赖。
+定义：如果B指令对A指令存在**语法依赖**（地址，数据，控制依赖），那么在全局内存序上，A领先于B。
-###### 流水线依赖
+**语法依赖**是指一个指令的源操作数和前一条指令的目的操作数在同一个寄存器里，因此这条指令必须等前一条指令执行完，将寄存器清空后才能装入自己需要的操作数。这就保证了A，B指令在全局内存有序。
-如果多条指令之间可能存在依赖关系，那么它们不能随意地同时在处理器的多个流水线单元上同时执行，这称为指令流水线依赖，也就是说要保证指令流水线的执行有序。如下所示：
+根据寄存器存取内容，又可以将语法依赖分为地址依赖，数据依赖和控制依赖。如下所示：
```
- 代码1 代码2 代码3 代码4
--------------------------------------------------------------
-(a) lw t0, (s0) lw t0, (s0) lw, t0, (s0) lw, t0, (s0)
-(b) sw t1, (t0) sw t0, (t1) sw, t1, (t0) lw, t1, (t0)
-(c) lw t2, (t0) lw t2, (t1) sw, t2, (s1) sw, t2, (s1)
+A:lw t0,0(s0) B:lw t1,(t0)
```
-这四段特殊的代码范例都是前两条指令构成语法依赖，第三条指令进行相关的读或不知是否相关的写，RISC-V根据“几乎所有真实CPU流水线执行机构的行为”，将这种范例中(a)和(c)的关系称为**流水线依赖**，并明确规定不能乱序。约束代码1和2的出发点是“在写地址或值未知时不能读这个写”，即(b)地址或值未确定时(c)不能执行，又因为(b)地址或数据依赖(a)，因此(c)在**全局序**上不能超越(a)。约束代码3和4的出发点是“前面地址未知时不能写”，即(b)地址未确定时(c)不能执行，以防止地址冲突，又因为(b)地址依赖(a)，因此(c)在全局序上也不能超越(a)。也就是说这个流水线必须保证指令有序执行。
+A指令要把s0寄存器的值传给t0，而B指令则要将t0这个**地址**里的内容传给t1，这就构成了地址依赖。
-##### 提供内存模型原语
+倘若B指令改为`lw t1,t0`,可知B指令将t0（A指令的目的操作数寄存器）存的数据传给了t1，这就是数据依赖。
-RVWMO指令集为加载(load)和存储(store)等内存操作提供了一组内存模型原语, 用于对相关指令进行标注，其实也算是显式同步的一种方法。这里原语如下：
+而控制依赖，则是在B指令中存在分支转换语句，例如`bne t0,t1 Exit`，并且对于`Exit`里的语句，也应该等A指令执行完成才能执行。
+
+#### RULE 12-13
+
+定义：对于A，B指令来说，如果在程序序中，B在M指令后且M指令地址依赖A或者在同一hart下，B返回的值是在它之前的写操作M写入的值且M指令地址或数据依赖于A，那么全局内存序下，A领先于B。
+
+也就是说，多条指令之间可能存在依赖关系，如果乱序的话，可能会破坏这些依赖，因此要保证多条指令的顺序，也可以称之为**流水线依赖**。
```
- 与处理器一致 顺序一致
- 加载 acquire-RCpc acquire-RCsc
- 释放 release-RCpc release-RCsc
+A: lw t0, (s0)
+M: sw t1, (t0)
+B: lw t2, (t0)
```
-同时标准扩展A(atomic)也提供了原子操作指令，用于构建线程同步操作，同时提供了可选的单向内存序约束标记如下：
+如上所示，M地址依赖A，所以M全局内存序在A之后，而B读的值是由M指令写入的，那么它应该等待M写入完毕，否则会造成冲突，因此B全局内存序在M之后，也就一定在A之后了。
-- .aq，约束为acquire内存序，后续的不论是读还是写指令都不超前于本指令执行，如：`amoswap.w.aq`。.aq不约束前面的指令。注意：只有aq标记而没有rl标记的sc指令是不合适的。
-- .rl，约束为release内存序，前面的不论是读还是写指令都在本指令前完成，如：`sc.rl`。.rl不约束后面的指令，但RISC-V规定如果后面的指令有aq标记，则约束其不能超越rl标记指令，也就是同一hart的acquire-release标记保护的关键区不交叉、不乱序（这种RC模型称为RCsc，相应允许交叉的称为RCpc）。注意：没有aq标记而只有rl标记的lr指令也是不合适的。
-- .aqrl，约束为顺序一致（Sequential Consistency，SC）内存序，前面的读写指令发生在本指令之前，后面的发生在本指令之后。对于lr/sc原子指令对来说，SC内存序约束应采用`lr.aq/sc.aqrl`序列，因为该原子指令执行的标志是成功的sc操作，sc.aqrl确保了前后指令均不越界；反过来如`lr.aqrl/sc.rl`，其它hart可能观察到sc后的指令发生在sc之前；当然`lr.aqrl/sc.aqrl`是可以的，但一般没必要。
-- 全省略时，没有约束。
+其实最经常使用的规则是rule1(写不超前)和rule4-8定义的fence指令，原子操作保证内存顺序执行，偶尔会使用rule9-11的语法依赖，而rule12-13几乎不怎么用，是为了保证操作和原子模型的合法。
-#### 内存模型公理
+### 内存模型公理
RISC-V程序的执行遵循RVWMO内存一致性模型，前提是存在一个符合保留程序序的全局内存序，并且满足返回值公理、原子性公理和进度公理。下面我们分别介绍这三个公理。
-##### 返回值公理
+#### 返回值公理
-每个load i操作的每个字节都需要返回由store操作（保证在以下store操作中的全局内存序是最新的）写入该字节的值，即读操作返回最近的对同一个地址写操作的值。
+定义：每个load操作读取到的每个字节都需要返回最新的store操作写入该字节的值，即读操作返回最近的对同一个地址写操作的值。
-> 1.存储了写入字节并且全局内存序在i之前
->
-> 2.存储了写入字节并且程序序在i之前
+```
+ li t0,1
+ li t1,2
+A: sw t0,s0
+B: sw t1,s0
+C: lw t2,s0
+```
-##### 原子性公理
+由上述公理和规则可知，这段代码为顺序执行，那么t2的值就应该是2，也就是B指令由t1写入的值，如果这时另一个hart又对s0写入新的值，那t2就是新写入的值，这就是返回值公理的体现。
-如果r和w是由对齐的LR和SC指令在一个hart h中生成的成对的load和store操作，s是一个store x字节的指令，r返回一个由s写入的值，那么s必须在全局内存序中位于w之前，并且在全局内存序中，在s后面和w前面不能有除h以外的hart store 这x字节的指令。
+#### 原子性公理
-> AMO和LR/SC 的原子性：
->
-> AMOs在内存中获取一个旧值，执行算术操作(交换除外)，并将新值写入内存，所有这些都在一个原子操作中完成。
->
-> LR 获取一个预定，如果预定有效SC会 执行store操作，然后释放预定；预定可以以任何理由被取消，但如果预定地址范围与任何其他hart之间存在store，则必须终止该预定。
+定义：如果在同一hart下执行的原子内存操作（AMOs）读取了内存中的旧值，并且向内存中写入新值，这些操作之间不允许有其他hart对同一地址的操作；而对于成对的LR/SC操作来说，只有当LR设置了保留标记后，SC才能继续内存操作，否则直接失败。
-##### 进度公理
+对于AMO来说，它本身就是原子的内存操作，而对于LR/SC来说，它的原子性体现在当目前这个hart保留有标记时，不允许其他hart对标记进行修改，只有执行完这对LR/SC，才能执行其他的操作。
+
+这条公理其实就是rule5-8的体现，是为了保证**多拷贝原子性**（multi-copy atomicity)，有了这个保证，不同hart之间就不会发生数据冲突了，便于我们进行并发编程。
+
+#### 进度公理
+
+定义：在全局内存序中，任何内存操作之前都不能有来自其他hart的无限序列的内存操作。
+
+也就是说，一个hart写入的值必须在有限的时间内被其他hart看见，并且来自其他hart对这个值的load最终也能返回给它们。
+
+```
+ hart0 hart1 hart2
+ spinlock(operations on s0) sw t1,s0 lw t0,s0
+```
-在全局内存序中，任何内存操作之前都不能有无限序列的其他内存操作。
+当hart0持有spinlock并且一直不释放时，由于hart1要向s0写入数据，它会等待spinlock的释放，这时根据进度公理，hart0的操作必须在有限时间内结束，并且把资源释放，供给其他hart使用。如果hart0向s0写入了值，并且hart2需要load这个值时，公理保证了hart0会及时释放锁，然后将值保存在s0中，保证hart2可以进行内存读。
-> 意味着更强的公平性，一致性模型保证序列都可以得到执行。
+这条公理意味着更强的公平性，可以保证不同hart的序列都可以得到执行。
-### 总结
+## 总结
RVWMO模型提供了硬件与软件之间的一层接口，使软件程序员能根据这个模型实现并发编程，得益于它的宽松内存序。而RISC-V还提供了一种比RVWMO更严格的内存一致性模型，用于支持“全存储排序”，即“Ztso” 扩展，主要是为了便于从x86体系结构向RISC-V迁移，提供了完全兼容x86架构的RVTSO（RISC-V Total Store Ordering）内存模型。可以看出RISC-V正处在发展的黄金时期，与其他架构相比，具有强大的竞争力。
diff --git "a/articles/images/20221224-riscv-consistency-memory-model/13\351\241\271\346\235\241\344\273\266.png" "b/articles/images/20221224-riscv-consistency-memory-model/13\351\241\271\346\235\241\344\273\266.png"
new file mode 100644
index 0000000000000000000000000000000000000000..304f04cf23d205d96051ce8d91a03d47c044feb0
GIT binary patch
literal 84299
zcmeFZbySq$*ER}*Akrc+q%=rL*8l?2B_JtX1JWf!r-XD%4WfjIG$JWIG($)?L-)|l
zdHB8Wch38r^Z)tlTZ>t&dDigEJ^S8s?Y*!2x`=wKu7LlP@+le`8orX^8!a@n$1pTB
zbgw5^z!m0wlWyP_y1SNw3|iR`^%n316C$l9jfPekk9%YO7B5T2M(CrVmtp6iy}^!o(X@kGx)-o>kdTs$bo&$};knl3d(K>|dB48t|JE-`rm%?URZ%i{qbIuNT^!#XO!<_SQ%KQ$b{&5mQ#9jdG@f?Xe1aewU7U8^
zg`P=<^gL-^mU?sJPFr+u7#XYgS9uK5Y)<_CeVKpsQsm;{tFzDlCW+suqcqz6jr^PN
z?;Ay_`w@TIzAeGOc&*b6i0Nqm%lZZ`MMMU5g
zW>|N2d*z{lzV8+;r|2YJ3#>GLx@aM3<#QK#bTuixBe91&W|_jijDuGGjZ-`IM-3{{
zKwNsl3A5`{x_n=64u8*Lp~ePr3YC+aur9oavcZ*$(6Yhl=!JwBYy|hp
zfN8YoUW(ZM^`4)~F5WGOoX+X>NsE`=+(ur7WZbFeFNCE(-Sw?u+=i-TTZGnP@6~V%
z(pjsCh&vVqTdJi%*jFOu1ADRgTUgC*nRkQ@?&~i<&{5hqh**J3FdKQBj-VVL7cP{j
zzcxkWT_3Nc-+ND&CSpe`lG6!&slQ!)Vr&Mc{%HB^>ioW9<33ywW4;w5V6LuLH5mJ;
z@&P2*9eL0!@PjcS;f8Q%-jp8y-A4A$Pi@kF=cam9f0bLVFPu?Ht+aQXUTEBx-{52B
zaqjw1khwp)c8(>+J}7;)?!xY*I`d7b+XTKHox5y1JJQ;JU
z74kMgSlEVdER4~*a$5$Q8Yk;>x9jAZ#yRJd^NGzr^et&3{#^xXw$9R$0Re}=fZnia
zQZb@Q1~278SW#=)VBmtOU6W9Bs7plo;Pp}Df)x9aq0P%(Xiuf8qUUuKvm1ZPM23dt4y-`@3$X*|==hE2e+)
z;so|WUe_@?C~ep7EJkAxcEiGEInE?z%g&S2oQd~wefj*>P-J$ZBs>KFhFkCLDsKGj
zZ%qG5W+qCDV7`y**3yg>Swh6}3U=C*@`Xk_+02tnkXPzRIe=KpZ^wsMElFK(_Nkdz
zy89r@k`>r74h6a2ODcCsvvm4w3i*>KXcU`;gjdq^@JD`6^D^9BlI(DMwk^G&b83Fc
zW#dpiUXFN1*9WZdnZr1)3hC0OD%7{@%4~vsET52pHA<1w}#ZM;ABLk3-;8&uHH3+#^Q3=
zE~L<18eSb*VSvuLK}jWY7$VUqxV))SN8+z4Dc+uHF52?XunJN>s
zV{cu`*{{i5?rW)Bja@c6m69E)uS~L9meN=uOeR_7_pjkLlv8yFC#KQwRJtt7r~0CN
zH4uFe1rbJvj-K7jt&9x)r*CV22EX_hF3~iw74d_mGUMKXQN3OC1#%jFDrt6+$8P}t
zFgx`He&N*D&n^;ERqus-a~5kwIgr16&fk;mvR5>HGnj^|si{fo;&@rA_d}G4b67aghknfLM;yl%{@vzrKgViL9C`5wf5?t)hx`sjf~mH(S2=uw1QE6$zv9T2Gg7l
zkPY~vZ}!EE5%Dr_(JKF`gT4=L?J`|C%uQ?8u=7Zz8h;OGBiQlnjuBz9R@aq7=ArZt
z^nO{yXyfYY_8WVPk~-wQFGDVSqILqxfpwr2-E=w(a}u3m#s^-VU+&++e#ZMAl3!?N93
z@gE|Pm#m~E18e>1>eqkghcmqfomcxUccQGhywX-VKz*{fiuy1IbtkKgXvzz`*LZj>
z5PE_kdCoPgD*n%0j~SDP1_?(=QCIrmukOPe{gjn$&6ZF
zrfw0>qM{mlS(}JMW&3Ohmp{k2ZIwT2P{4B?zw=8*mNAtbL}x$*-@8Ir(tV?qw0tl+
zgv!@y8(*)1wvu^mH<&2V-3VHzzU>a(LpoUai>M^OAu?D~KN)eD72w}_mjAB)&CqLj
zb!^28Pj~?aD2i*o>G~wb=utb!ym1RM88@XImBaI%R#}9nOr%0EY5;=h8drrR_xOD@
z(ck_&sCVr$JDAbs7S+unnWnM~u23^Kh6LF?S5a`;8j-KZ6piLE&5{`OlLYYANkXJr
zU(#IYIH4y1s4z^Yf=wS?bt`?zXH-*qo;q}$Roq_Iq1Jx6!LdhSk3a~a){rqBm{}pI
z1iF{WRI-g;hG2@WLp`6P)^c{;QR@T~U#zUqsY}E~^k_?}u9pbk8
z8qIqMMGb81wx#VHe*ZG7?{&xFw78;daqE4tNI%Dysj|0I$U*o@&7!z{
zN|I|D-=4~=K?ossMZf?vN?qYTva3^ZjI@glOokQQq!EOvBhzM61st4-jRGsA3RG1!
zklD_UKZ&>M1~ts|jn`1tN=cO_u_`$jk3_SomyO0bdx^3>$-p)O(C=VUJB
z24yd8B*%8?J@a;4d_1!<$OG@)^~&h2&8u0B{e$eDy)W$={bWUc&&>L5vdLmj$esMw
z)uGPFaB}ThZmr(hoz-7bE>vZ?MoUvk-|0PMv0_5EQu1!Oy5Ft$NxPT><5(g#t~;`4
zypxtvv+Q^`GzP*^!R-2-kaPp9xa7lKhR-OAco_0ka@2flsn`jL(&G%L1ZOF{H2b;w
zDSxMMkAUEkZ5KrDssUdY$1=shu-j>d3|LJ>i!7=av8weyUU(`VOyXU^}GuMcO2Qhz%v{?V#m-@B6GF5OuvbF>-_Do8CjqWOE1
zWn{rnQXy$|lgKwG3D@b;Lf^u_?`39+JfVQ?@Sb}(I^ER$gwqnVw%kjkswn=ziTzSq
zv9Cq${&xM^zuT?M82r{7*>bZX@6p
zUB$bjZ=D-{9OFpWfA1zWv^c|_nivCFn{wNG4XWHb_FvReT_#_MyD8!L=AoB2B%oC5o>_s#hwk26)=jc`X>BgvC#$Hi
z;TT77Y4$?{p8F1R=`nrr*y*LO&)H+vqL6}Tu^?Kebw-y404+mK>zm`ezw
z7ss}>gd4a=872r3=XyW=*zP;e!f9`g!2Tibio~a5r?l;#!=6*m1Y;mxM(SC*B=Kpo
zT5j1!7HiW$+l95uSLosbL3&R$Os?t~B~Rrm7XN2O3HkBl*KtR4l3m6E8z-})fw&6cWPL#3%6pA%wUG5Ov+M?AHEjc2)3P#9prm@knN+1v
zl;;hrafX5QSw?O$?7%)nQNpVmxr@|F_9g=pRDN+zGI}ZH9^k;;5zLQ(PD?vr{8Zn+
z^7}giJ{ZpXsQ_fR$8Dtew&K*g`c6!ApbA7#vF;b{DtD|E1Mh+LUbhEV#_RcP?1_|r
zh>=^n?*E9!SqH7pQJK>IugJg@MDtGXLlg>PAwo#V)Scg){zoYs=#ldmBR6X^{tgzp
z5+?t@tP}_dGAcc-28KWh{Ir><)DDuEjnMS8o^ql%qFZMXtUC?MiNLz@@O=bF0WQOn
zT0XYJAUa|7IZe)jCwT-`;H=71LsKWThLXFc7AbSL?41N3O@!K<$BlMvYF$+(6uBEjQ%~RD+di;n1O*YFV8MrdZWt5P~S2R
z{CFF=*bA)VVaUqAsg;msJs3(>QHSzD?hM;w3BAVSs4!NONR(ya)v6Y5oIo?!ivQY+
zw0}`y3L76f{wW61o(fc6$vJOXSWKsoWz_valo9S5-MpO&W@SnQ?83$NU)wiDA*MdT
z1kV8RMZUFaiC*Z(-^_i#G=v;ey8g3EZZ3@vabJHUTT`X1<1Ud*#BG;h!2g
zL@er!Fv5}&P@L_s^#PGfG2z2GW2$mL=E+CqxN&$;eB$@K-xP#Bb|&y8fA0-4vZ1Lgz32xwdf%0S9&!qxZVgz%EmFy_goDDgGSidMCkK6>O&
z_lsZ6cKrn7N_Bw_#8?4mv?g2`gkr(Ji_uEU=^p+3r*IvhUAg9_IuSFwTB6Upq=Gsh
z#`s?QKAIGR0m0qT`kWBeUu8VNSyHd`q69Y+;UwX1IIW{@!WcltdsFOFUg{D}Bq?z!v9`>k`_{k?*WN{=#S-
za75cdBLW#L^B(nu3gO@mZVy<`^%j2E5{F~8c6WoodJbXkIb(PA@g)18x6k-sa_yGt
zuA$uG0w=0c)XjGU;cjk+1}E6?gC{@{edo2JY5FU;8|ux@Q5_uL$b41!}IDk*%hTxQAkuP$HEQm27k%=9&IUy-zhQ7;H@S
z1i{G7{*swSv$h{+ALs6BBio21Obf{Ksy!bmr`F)a!+R+Hx3%>8$j|{|!KoM8
z(N&Ao6@P!}(uM2frlvwfsF*J<=)YPB{`;Yc&yzkt=v>|6jU$$F2L;LO3FVTw)|q-k
ztI@})g6k6Y|Cqi07YAc2=O^gFG{*V2PZn9vF=;;N?9N-b$Ow
zBRUW9$wUo!9Bdg}KG|4{?>9Bf=I4kw1|h02ol`#WlBZXjNoG+Yel>CG;>=E82g-7-
zFki1y`!hBQ5y85rBMauBZ%v1Y&&8c@m?kmvo?C&V2gHrjsa!tTFO3A$rQT3OX+ulW
zRm@&&eAyia=#PFuX)7!c0t}>Xbd#+BYqoQKA+x!71L>q9DxZChc*k;e
zQgl<6HLnc3qo?Qm)X81%iWRwCgLODYVVRQAe0qH!w-m8n=Eg@G;n4b{HZ=iZwfXe&
z@NColY%MZoG1{cycM`FY{hVOFIL)n2jPLBEK5M3oE#Hpe6+$B*Mq6dwTmiGZ*22}o
zR;_nH7-q?x;>e4)GbAA+77ylqrbm$D23;2dn$p=wm8&e@yGshaM(Rn_CCMF
z2vpMB3+5Mg%m>h7WE%s0iQ4e$gaewJIzPsbyVKDU;=-1DqZt$^W8Z&Id#sztllHBT
zkj=%DV~hOLiiSwh5<&xTEb~UDL8r=DujrNhN5>c7_=j-~DeW(+FvlZu{r4gDp-rd(
zH|{DAlBOVSy@fBXI~tn>gBH1r?Azio8?;4#Q~De?a1u}hz{gWi6qzF=)$hY8UckJV
z$O)qoig|f5318t7g*6Gtjo2aiFL~^Em-ctVd$_VHGG%hj8Cg?nmKXSHxE%zlng!&B
zp;yd1HdXY`uCe|p^5zOY&N5q|nT?RCoNfG`qDyVN=0mRSTo9PMd`B&iqU~Ud;bZY9
zCv>H=xT~N~N2k_A)JnD^*eV
z)3A3DOF%=wtPDc%tH0ZT|C*unuwY`q8y$QFV?F4eV5Ho4{a_DplcO-6xGJ_f*9OGN
z8{}nt|NI(bcJlqnec`NgP%2|l3`8wYeQKb8joKZHgz|ZK_&lQG0P09FBrX!5Xb6&GluVsoW87ddVMC+e@p0xAs^_>riD?4s=
zhT}tUrvmNq&S#R1fv}0(Dc48c(h1QGWn}3W4!7L1=3p-at;zduVW^v2N%YW=rh49z
zGPmW)!>nR{(Ogyr&Kj+_QnVO=nUy5IHd}w*pObZV3?6~PK7RY@7v}CJyk66F$yezn
zl7r$*q6TB?tQ`=!`3HSUJfhoWDn$*%{QCvALNR^2Z_eU2sZtmk6RyG*+zrNG7Tv_Z
zHwPFSVcLJG?(-yX;GgS;`F@-?(%s?Xrsl5B
z<(tTu9wh)Rmt8q&CTQrIba1SdFTQ^@)oi-xo3%x)x!im_%JV$t*&+_P{}P_t5D+F-
zo+j5T^H_7Zg~H^QK1rUY}Pk%{u;DGc#$vGKW7IG*U8R
zaz${dPfwW1qs;$7N$gWDhcDHA8GA7Idxt1Y3|da7;73)Lr6oeow{9G0HA_&g^eDfu
zn+vmLf0Xv<_ZCqc&$Y$Rg>Qr%kg5Gouf+LBUi<;iPB()8N|<$L(S!k8d9mlmvG2+1
zyBd9Io@XOmiBsqPT_$e6leSJmU6Qz6vkC!KZ~wj|^=hxE?Bd5z3ETTBqNijh3YFv>
z-)z2Xpl)j%>uglgi{m?|b-s_342u6SOjrr8etdwqf@Y@#z6EF_X{YqGg9e9!-sKSZS4CiH>%$&K*8p$SaB_THvKV1dO%
z2!mxKEH*0=_1!gNSZ^_?b7sj)KQzZ^-31(S=u+y;3p__dVkAD#^IRn)4E(AzL>nSsXf#t`)3Y`$)~aZNu9aCkHJ*fKl^)E
zBv;!gFTqck51~j=h!7cPuoP{#B0O3$K)9^?jx{G*(ur?0y
z=DZ*A=c#Yekck>&TjQ$__jRORV++YFrk$NW0mJzN32Oj4rArydlz^CaVjJs-a+{MD
zEyA6CVs84a8g&7Ud=Ra0(L}nI*^`D36h2qfj}~7|BrU
zz#%6vq&UWi8h!Si?GU}q>nSAE
zd*s$~!%hZqL8&&}V*f4C>2!0~tv=sT{u@tAW0G8k-LTz3yz;uGAPkkwPlfy8)zy*E
zO+Sk{g%i?eRR@W|(BVlfxz{0T;xC$cEwtKZxW7^C4BUUTClekqB4bkXo;ajyuP=Yv
zNH5}N=nw_n2S_Mt;5k`ot0cwCwtj11987_`pJ@596%ms7QCa>Ct?z)s`5j-`Qi)bq
zemy>oElX(3c^j8Ktv`IZ63`uszKi$d6R^wP3mIN@!G(obv@}7pob|`Y_lHYovtK-S
zns_IVkHtlZv!kzRf6Gzf&B&iUNSh|ng~
za*0^qCqhYt{32ZB3GveVDlEy}GsZ{VYHc;emWS?>SkPX9WSN_}%;2`U=~^W{@~=8U
zy(eT+Meo#V_9QSZSvBBOxs6`~GUjZ;ML>v*BtHUKQ%m`3v|K|=R~;Tg>gm^-R6+Z*
z^-=sWOf((wq_O-do;p-{(n>a?A5bfkzUHC|Ew(y
zO6sK~G&0PnNd`r#YTGcGZKN0eV>V2=v}y6rq7{1rtngT41!G^3)wk2h;!lror5DlF
zpQgNm<(C9&!)m(#Q(nRUqU!a>L8!VId8BaXPRY{yXM&Qu;dB_?=6yBA6vys*0?^(I
zw6}b@_E-#G#uT=kdAeDxRSB&h+a9IM-Xg9n>Y(^AF>{Kmn$lnku}ezMm#ncH_aj`3V%w-yCt1AZzY4}c9;M-{d*`M%!>f6IPWaGxKjykI
zas1?r!D?}HxNuQnLp30@Hr&U8ytKW*yJQ16jsEP^4p8hyorLMKTEjDX-k#^(Z
z5m_ThYte|BlS|6yKc=2Z@rZwln834@#k3JlKq$nt!H?;pMoJ~Ez>p!+`)s6%dzHdk
z<*iZ^6qiH(x*GL`W1({){ShNb(`yltn5Cb_k=R2yZ4Hhl*KnXBk38MtfxUV|2j>x7
zjVPPZy5QUE(hekX&${THl*2!2xx*J)P~YJO5qbZRT1e1~U(H7~0aAxKsE&51dTbZQ
z$AfDyj@SKx4j$gm@UMY)$pPizVb&LpQuqEJK3qjj#*kXDmhc3?Z<`zhVHudtm^F8#
z>7}5)X)Ex-(_1;ozDo+vANmc))@v?8$Y~-^ictGX?6Y6S$H?0);rwekg(VQeifKk(
z-JxMS#veHV#1ZxuGhP_hP5rVLUtqkZoLC)R{XSyj
z;-HuCOOFZe&k%qO4%AoLsn~vVF@ES}dC=Vkmj
z^udCw1*wLZCv(<~!I5mg95@K$nmH_5aoiz@pvVHQWyGl9E6b`Oifn*6`#Sj8k(Dyg
z4=yxCg6)4P)f)0-ns(f@W6Dr+6ixQf{*$$Cnl=m8X%eJm^R4dm=Ts|KM%VLwtGmsySJnl)WpaiU3OQP_XwM7;~Y6}sSZR@B$0M3Kr53}ly{8?)
z_85}gbQ4+zyj8u>1wd5emvYSO5P0XY(f?nQ*tz3L#vi18Z!S9;w3I-ofD>dROS0mtrK7IOZgkVQp)DT(Oa+^vIbSE)NiP_g6_>xcT(
z8N7?XLQFpKLiY+?q9e8h{Rm6JQ1!NjUop)jzHPjpxym2;y{k^Pen`d?oEwmv+iwU46*A!;om^&{7ldcOt-&ZgR6{iK~_{l_Z_CYsF~$#&UVv5%tl
zD*S8jz@f(LF$+WM+)Ht1@crI?u3(L11f?s0X5S$v$vD1uqOUCfl_z=A6KjL3S{*z_
zftcUphmmK25V0E)DW)4=TS9o9d9{s!HfFRCvls2wGTTH9jZXI{bfP`ztPNMKd&MQi
z0G~OxyJAum?vCSE4~(0T<@;}EuH~ZJ9OPtk&0LF}v~6)ISyS#uY7R^?Zc8j_?DUs(
z#ZFJUd)Sc%_q*IOal37`_J*DO28iy2e3PDV8?D{BA+#qwwlBwkj3Qf(4H>E`ACNPxnB{|>vGxhr7@z(Cil+aP~K{EM1XQC*>&+)6&!!tp&
zQ;y^P05>EQvtA`|tglU-BLwd$ry7Y+moc{M{f)NRkSubUMp98~uZi6CFqTkFv>EO)
zFUof6XtW5Vh748Tkrn>4lrIkoDNUyu-0P9E
zf_Yrtsm9RhHc!z_@r4P*?oCtw_eFE;!rjg9L{&mWbb80a{9gqRonMirs}kzxgOF7y
z&Wk)`IA=`ZUQo=&Ks{}JmhYgZG4>47uTRav82|+HI#y$Q{1r8aKMpNX)}K|b-v6X(
z=LLXMUA{AK`eHq_kIgDAKI1fll5R0&r`WmrlVZKkwzGwnalKR@C-&cD3PiPfb8oDU
zXMWpMNn_%R`6GGcQNcHxWG<7o{Vz;gl9%2`0S*#LKDpU6ZXOBsuj+`;kAeH2$sKo1
zc)d;NVL^J&7jPeG4s{)GAjWbyNH`SY2BBmgha+~eS#m0Swkcmr!eCTR(*dSw=wPJx
zbS_ub#ZP^PZ3lBN_)l_Wp
zh8g7El+mHcReu(B6+W?VraB9al8D5ij$QTZ1HFKDr4oLW;|tM8*Yd)$LA^I4&*f)R
z3!l?zROEjGi<`!@U5#~Ut>~-uK!>ukG_mU@sXYtYzHl_gWIdIPCw8`o&Y17ig~I@#
zc;PU#4iFZdR#ZoWM7q5|4R@hy#F~)hb)J54#2xAO`~6qT^YY9>c9tkP&qv`5Y($#`+f$ZZbIGF=)EWn)ar=!&CJY~xIvZS
zl`bA3hVP=Rwe9>cz3`g!du6LmK*t9Z3S&_qI}SXIAF{*D+(j1XLK!z6&_Y@9ztO^y
z5ZeVq&HK`9D5oUBFJ~igc_7z&?8Z1+NjR=o>eoGyYl#?^!Huyom(*fr4k!_4`U6;j
z`!&BQ^124y)LcV8S#A)E#H3-8*p{*xp4;_f=5dU0Wo8Jpd4n%Ze^=f1Z(DW&D!Z=S
ztIughQf(dLa;yTc=IY!N+EXu+n>GvTBDAeZ#@q|bEXr|F1rv!M}Jzsr5KIy>QA%ej{G~j#q}bJ&iWe9NPQmm&inv0;;2bAZR3SX4uR%GFxZG<)-N85vMHr
z`rK{kfk0zK3VxO{2E8X;_gFSp52|~;ig6%V>#Nt|F9gK_hp6D
z^NP0CisJhl-ak=IdspWGOeib`hina{r*;?!k^fsX30nWOHXgTNJ>qX~l}49;9J3)v
zF5U|OghgMa9;bzznyC9?PmE%_d(RMlM2_e_D?s4qP~;KOI)gRD41=j`KidboXRE);
zWw1?cOP7gelOYbg<~_QR67DEPa>Ydnw*
zp&}p1Z{<8c-+Y+S!HJ|d%t|~b{mue|HowvLw-cC^W-H>TioMsSH{37>Uj^>I{>J>Y
z`%^3-nnTKeNDGHoNq!$+{Zw|%m)nxO9y}6(n|G(fJ*XNc16mJ1-mRQJ>6vvv-!H21
z;u|7NJ{I-WgCmNpRK%S)8pwnRT$%)!M?6bTQ$WQOMD^cdn~KxOoBGc?%sKcoNY2is
z4N56m9LVmNtp|i|$19;KcM{%ucLo8Z(1x1L_EtHS5mEn0fw-!uw@u154txwvzk5VA
zY6>o;LMXAm`kJ)mb3+C<`t5`Ap!^R~yCQYG*Sbbq_CW{yu!!Y3y*sP!=5!$gE#(5ZP-?IsYLb>*UmOvyLHBk0m*hV<*ptAF>
z$Vg+?FX``nB{mGTJK$ZH69ovpDk4cwSLgg03v5uFQ=gxhP_yxD#9bG6b5uJsKW|3@
zr&z_bJi{pyJ<(J|thW{ptCuv{Plmc~IR$Gr?y>q!Rju9t8>>`w=x#l>^jnCkZ!oy&ic@P9y+m@8RNBjJn?)lq*NCha5_N3>HWAV
z`w591(uC0F{}c_)`d95Tt|rnlTqtKh^~|{7_Qmv1r5c%)JxAMgXjc5&k+hX`UBlCVJN?)Gm*>kH}d-L2fx;3H#yJw
z?1^9c;%Jy{#OBty0++!1(*w>jq5xg6KqD4OW!v`?ul7wBC3d~g_wKRCGz$1Fc+C?~
z#$EbG#q{VRL9SC1zr*~H8RTjk3i=dL#gU<_1zehM)uj@Odi}n8fAOR3SZhMa+-X$A
ziMLibff-RmS82)Vxb`Y}JG%Cv5MXFx0i}00J*F%6Z_+I5c>c?<8q5Bdt@pjxYEwVu
z^GlB$@YE|6W_ribbeqqva|C_{%1#`bGW+3QXq-S?S0$E*h0h}lQ?@I`t>GRwZ3l0q
zVbeoto*$<#T9vbTlU&`G71&r1oMaw4yqh(tTSFScNL-;TLx6NBTqI*u1FeMkC{_QM
zKKIoFF}3tXb}cMe7i28%I#agzQ22{ggXVe_heE{F0J70)wvVAOl*YAfC~N9RBYxE$
zOIn&RgyuAM!z!DOyPSyl2uX6+HP(P~NSihB`8xT59r8Od2I$k;i2LhNKYs~O1Uk|^
z+iL`c)0=|=W)aumwcqz=`j_wbklRSdIfT0;@{&(JBW7dHv4Rg*w3v?%Hmyt!`2@1H
zLjb5-90N(r$3?#FuG!Yq!|^|#{el~dfq?!+otr%D=&R5Lu#?<$fe
z%v0r@luu6p;rNz#R7|f45)?T*i)+o4tQJ(}CPlrPPxuOq(=MFq0iV{P46HF^p^6B9
zrCM^p=wF^*Mg})V>IdTJy*lW4R%Ngeid8*0xc7$oy7C(sO1AX=H(kg#=ywQ4dr^x5
zyjt+tpwP;3S>#=JDaCKT@avXub|&5x%ac$0^#k5^U<^1iIfK7kV{m>>AylU)m~Bi?
zn$>(=b`Hs3#N!LV{mb?toA_6WAQ}7eSHkY3G`Up+#L9~wivD!(*|UFJaIDty>Yc(4@9-Sk|b7LZXpR@hS=G<j=v*LcS?1L+a^vB@b*)pXDT%gXT%M0
zQz2P%1#%xL5#hdHreFW%IVlUvRk!k!N+O}`Gr1*>aOe$(2SdQ!%(q
z({jdaAPStB_~=W3Q{p1bm%7CvFF`-WW(Jxp{HpJS$Z8YRq@|-*P6OfF$MIH-TsZNF
z(oRCp=pOMM+@52b7ej?}tt^a8hxp!%La63gd3rV@+7t>4*Xt$liBBV2Q$Y*A_ru)J
zsVXLW!B>+us4V2p5x5r5>vId5i%wRU!Z~;Gn?@60W2RaJ2(C}gj4#^EUD
z?o6wOy*PFD?M-9Z6BGMe{70;au68+hUT=NpnqmW)g^L6wYRuGwxY%N)d@f!v{IgJi
z#oSZ2VT(!{xYINBdo9qy%C(1_iQIQYOLwH*afM48XUuIS#==W_9#irHlyl7V)+l0=
z`0o{eN+Ld8G3U%9wtExS6FLdfV=^vyIX~ROEI#drX1ndGubs-bJ!f-jOLlkQ1V0w=
z8q`hFc9Fj8YRj5Z46_hpG%2L|4Sgll3)
zlspCLa{}b}SkTlgHgEalEZcU@3<9cmL94*Y4Lh&gwj7f+M)~^nuY}T>^XjA79nkeMvWW^2CQ5-O?q+NWHzet`nDc
zkJr|%RN8`V&kTI&C>ZsJA>q}~d!Z^8w~Vs-5W=5$%GJviVL9;X3mk<&sHnA2Kyc=5
z1}F@HNvxUY)77uQ!e$qDj{wPsa+!<9p#Z&%n3N3YfkO}9iNttG
zAaeev)4*F>nnK2vY0N0e0X~6#!+Kwl^zCmKblLx{_Fr=mv?d_Xp=qlj!EEkODnx
zdeqEMH$v4d{aO+@(9q>nw|*#pJ^l7JI-v8=1^aJtX7@J@QUOV}w>9}Fcg%iC;PeH8
z#dBWj))&9Xpz1G_6{abitVFSLu%>7__fJLYEm&hAf=fYQ4w>>`lu%w=V*^Zr>gO48
zR0x#*m}IWOZshp~uCy2a`7`$5Xn*AI4BJge=GzzWd?B8`z{c)<`>%pX@BZJ;fZBp&
zL6%H6?iU53ws&`7K^N$|&U(<^p?FV4%PkLk2WCaM0BxOudxr1Jfgi&0Fnn%iO&kD7utnM9oh!YrD?l^
zg|l1BEDiTvm7|2nYI3q)!9d{(3cR<`nQS&f$zx1yvxKR$ah+u@e+xi?)}RKR<79|j
zRX5C-viMg3$6yZ0v*kHtirtxELxIQ5Q=a&kWY2J0w{ob*imF6R!maV)~y
zJ&^4SLhhy}(>4Sv|DPPt)o|1gOG?|#4`w|v>TC>aI%o2!(vVISfp~p~9o=X3A2iSc
z>69_{2S1n%2y$I~-t#aGkVwrxoTr$r#QNO3=*TXFdns50s-Yz3R~58vofnPGU(3s6
zps5&w(YPity0{p6{o}~d3wUM0PPUVpdER}H&iCH=Lu+!i%5b@X+(pKqvT7=t+5)*|
z(U`5n-+gG33ZTkk1k_UJ8wF
ziS_}S@=^an0JhKxC%okCv>V6{&}vMHhYT_-TTla%*UNXB7e8bqFU3lvmw9Skw1%u=
z1d-FEZf!#n#Sc#P)LaiU7a>OzS!eW0$8uK2x
zEpOb@uT0oebV{g$H18;9dq;!x(4Xz+cJJ#P^IFfb#ZdC&R0qy}PByQsnodGjiYKb_
zXD4=R|JdPM9sO
zbqftF{iZpeGkSHcDAIy;e0GRcbe4E=$Z%HrJ`6+xH~Y7V`Xc5mDn$49v!X)bWAPA4
ztUv1etp~?NmMc@d6vEbIWTo@b$LA}2@t(MNk&War^Y&zY)}V;qYBI|`nAu$H?}KD0
z04m}S0x6Tg6s-wo3zE*Psn0(bI-LOhznBDrz15}IufWJLdx&M!2jCZ=FH1cyUO{3uzQ{lxi{qPWCZgWR>VAgy@FS8se^m&9J*zLAAbll?K^M(
zzW<(o%$Ne4IwU$MecjKe^!!1Qgs*HEv9G31h1e$mA;LI-%CJX`o7>fl#m+cc7lj`$
z%A7-&C^)w*w)+OouY&RYqq+iQ{B8|VYJPp}S}qIwYEZP0Z{+$ESnz`YF2-^4
z+7&rDU+`{d7VxS9&h4?7jRb7_wH7g{bU*lt0r`&!;=x3ko_%Ol
zCbn0wd1|aD3q(^4BFazCdF0g-Yy(&l_9Z{3mHdS9w|WI$y>Lhe*p-$5(~8~ZU$B-BUO@)n
z``!FVkLf2(bgskURlkI#_PqbDewbA^hp?R;s=;Odwh_U&N|XcxUY{H_dR=Q
zx^%UO`(yxXR*Db|luqZk4yXQFH`&v
z%SyLdNwhrm;f6`>oKm&=cs@w>
z<$Tb}>>OMw#Kid#6*_8x??dwPNPK<@3fSuC?n5(d{FQ$KQAER_k>~W;#FPu0W0;O)
z2k!r&CyMD*vn|H7=xJ824+26cZE}Jt$)gG-2{BlAY)>xGqN_Vsoqln#%#c^(U
zAp|A^g9Q}`O`?D$LI1&LokyKY|DzbL&WeP+MlwQ`k{ep`)%tzM8D5z~(8QxO3WCr$h;?|tHuJ9G+6(<
z8lb;B+?jvW-&F&`_`(r}aEN^^uMTTBdtUbd1ppcO18x$Frm7(LI~NN9J!&iO)}Lf8
zpH)dJ{))XR%$f@Gi?fZ%_~S0-<|J}?CkF+39?S7-0rrnb)1qbH?xQNWuhr0T2aPXl
zuRPCJocHZ+*yCHlx&cc7=)LeiQ@oq1azM2DrjRcN;DehrDs?tn{hlYRlFVt1L?g!2
z0_#Z=cQ#BRbY*1@d_a7OP_xG2Z&$Nb6#0-yDqEWWAuO^G>KgSv
zL}oC>9#FU?FF&`KM=+1K1@sDwvzAi*X^NZtGz-V6hh;?l*)nw;NnWqt1t~Ge0?a*u
z+>6GL>p?{`ejK{VkkU@?KhaIJGha{c;_WHpV>DJ^%|+o@oRmGf$qEUgUG(pq7Wy-)
z3{>3et4cA-bPj(SgZ+{f6d95C)OAFU*!C8*C{=K3PFN9f1L9vz;}s~y8d;OWdtU+(
zB><2;hqWOg*Guf}8)ZD(BSSM0baNsl_S#^f
zcY@v_19pnl`I7)-;0$l($naw
zajgadY+Y?kncj6!>VH+(Ybf8VD^ygRsIBdo8EC3^S=ryM{f*=MXQDd?q}Y0J6a`3W
z`{?Ksf^BH`f3f_~${fCN4J=Rgdqrt5UXfhyu(59xFF&`gM(yO%W(ce{mH#>OYduDq2I)-ztLQu&1R~HcuWMP`EQh$xOwt|0IWzQVuhkcEs)M-=)`y
zfUP;+=-vwDCOyoN^@YB>9?ZZ_qVZTXlwbhXj*si3*^&iDkqc{_W>
zImtJ;1%MY5FJ{Q-*D}R*=|vg#IxBgWMORzi{Uwb-m+g0i56imp
zFLX30vS{E+P||#c{BX}9BWB!z57=#}rml8bshExZ78g$#j<+YDeT$fEMh1`oj#?!^
z`5&>CCri3fNe{{Z)XKv5E=du(Ru&U_Gpp0_LF1SldY^@ZP>^@*kB6TF^4kp_SG~1w
zImfplvGp7F1Z`^{oLzfQM{TCJ3!N4cMfNrci&+7hdqYkI&JZY7SUq(
zg7R=q;+unRu{*nK2s-s%x!39xp*S3tR=GV>d2SKv_Yx2qAeBozB_%7Dc*argBySxN
zTd+*kz->+CcvB{=EP!LU)tSURq4;qoM3mE*P)F}}vq~ehDmSAl!nu5Jf3=(mz=;Q<
z)6!pmzINC^Xk06zgV&b-LX7}+!J_MsTm{|9ZQaKI=hVJ$O?ai)
zpKo{pOxjk&tacMxDy2}d_}r`!*HnOhi?TSM)PPz_lbPBq)duERFroNnCak2K$fKOI
zHo6iVm|(OGXjHvTOT!#O^`(^Oe(MA3>aRDLVCwVveKIC;P0v>sZv#q)cIpAjIG{)E
zEvem~j{I7aFf!NY@!CsiH{Sgq`H!}J%~L=Sz>-NU@v~NLlxrg%le;z>%BgN&J35comXtasFUjd^~(VJ4v?S{&grv(A(^HLey7#
z4nP4}0ptnHyUfsq3(KgI*M>|l%;D-C8k*u=H@WGH;V!!fu*2%A=QRY)&0n#4mO9ZDJa1%-_8)T_%{kM
z2iH6ZbC1;OUCDAWi@zmYYV#y|UccC;87NytKJVtDQ#TsiPZWB!Zfbh+@YnD72_R*7
zwqmLP)pp2x`IvZLgQgX*0#E=YVaj*-7z(gjZ=wTkF0UH1^J3=j4LwTT56WuHci2}M
zi^VYkHRr;qIFHj;lgoQXOVS9!d^Zz({sFL|a$NYtR?+hPyzhCOdU*s5D;6t<*wiZp?0yQI
zSHnPVf6;mS^e0`1(@J%#HZ=%U@3x37Q1zLfbs=2`&q{T(wxgT7iH5=p^XI0JXl5?lReG_
znk2e=MILa>f9Arn@6T$Y7F#_{ljAS84lZ|>!X&hru$fZJ2*9F8&l?z(NA~mwq9yFN
zY`9RQ$7x*^I-b|J!3}oLdug*9kBD^q#e)H;-U
zjlbvu?Frlwz^JxDv}Fz5#h?6ZCjK=o(m3*MQEb35l%^W6!r{xZLCZe!)kJk0+?e(v
zh3a+NyR!nP6
z6X{?nn5QNS0w-JcWoTAivh>lW*W_Ul?C&U3Gf~H1dvl!pCbQ^||N1(N2CT6%nwLjQ
zdOoCGW{r1rD@V+7wW&b_C0$1YV>e8w5-mjs{uV2^-bxZ{v^1cpr%l+@YI*aIlsGYC(CEVk*uwvZJT9i+Zd+$9hczQ7-5SW`DlCH=_jc~qPNO>-kh*JUu__3Y>0%IfkXahW2AzoP(2!D5dIJE@&C{NFCA^x
zsUED`7^QigsYPu{33EGw3}-YN4ni5Pr5D2I1StN9L>(RQqj=?Do)q;PhQH{Zn<%i~
z+?As3FB2kEaWF7)t2h+SUFaouH#fs){2&JAgkr_U8co;n)uphu`V&3pAPLHQgMQLF
z@hv!9Lo1lv*$IR)vQyo<2yUbU;?Go+{?(%CoDqkJi*HznCJ2~
zZwEuFiT>QGSJ}=HWVED3!SfGCzlL8uAF$&Gy}HdWEg5TAaNm#j)j_YTE9RK5-SwyR
zYc&G(J_VGthVB9{{+r*e>bSddi{L9hjLFXR(c;hVLT{Z$M|&{z^u&IOiz@m~5n$Gd
z7rgOq>bks{>^bAii{5%ib_k|e(pzF&J}P$tFjLv@%d@h@A{^V6Ds5PesZuE?LX8OP
z@Wr4b{ef7cbJ?}`yisvxf?PT5clVZSJsH>#RIOu7GkRZt&wK2FzZy@}MRtA}yT6aT
z9qNG^3vJu6zAbP|HC!K~y~h8{xiWSKTeFi3+wCOJ{ABxH(O+~q6>4sM`|IWWa4V)&
z?DOA}gV_N;Q}mHIB*N~bqjFWx_3gi9lmn=!@5k3m9z|s}@^Ok3OY0f|S
z4u#JmZpR9$G;W$LBHiL+D}m*z?*AYFCGbG;?5}QYIb8c>UMQjvgc=
zR~EGJdKg+o84n0H%`qUs;4T6GTkoB4@1B70K3_6aTsp(0x49W*oAe0)*F;?2mlorr
z`uewjJujGo9QP1%nm8#OUe@IR$vDY<`KVv}uC*-g>yO@NO|O;zTm{|gmeN1g3rik#
zIe?eWGa$PR;I4{2W-^{yx0R&1lrA9Ub=^Ls6IkWSatYNxAG=>67X2?$`67BZWUJuw
zXdW$(anp+KHDUU2&e(b}%xNFMpGQ3B;TRolwer-2JO{G+eZMU-@!?v9
zCqmT##SueP-hyiTmr)xRKf6*#VWxhZsYmi&J>JgmN?NiWm9m?xE5bCyM_)PI#Xs)8
z4VaYIk@xK^;%0O1rW^Xxzo||pNrDvQ?+@Q$UYceH#6DRLb!zj;|9Xe1Vl+N{tI`qi
z6o0h@>uqcXEM+vb2V;~q*?;k94t6VV_jDkw4QerHLa^
ziP)V}zu8Gk>^d=bciZ1T;&ig1+z`$Cm)%LI1Fykmk^+6ee5E(mv*md={f>9k%fFcO
zvCUt!1d0|2#eY#Y9R_nh!YN5L!I`1N-8oeo$A2WeFiXz_3lMj&Nk#C3LW#R_*-idX
z@#8iV4f$wkInBFklzJ=MfC?sSpJb-eIB*F)B^AF6lPTtCZ+zAwZglvK8
zsILp;E)^n10(RqQzsmH?Rwz*3zBzva(IN{@o8HvyUTQn6ml`YhZ00?7Dhv5sk6}!z
z%@uDWG<{6e{u#V_$rt9pAVeVGI@rdc?-QV`duz0+rEZBvQ$swmX0{KF%JylkOKht@|Nhx!aV5Wgap%
z05;m_Pt0NGQK4(R=t%UU@zbb&0y{h7>7Bn>^5xkwEno`=$H_6u!(*RJ~RiR
zE-x}C9?VWHZ-CLv;5Yg`KlrKPT3YThvHwNM?Iwu}*P@IpJlYJULL0TL#%ZcT+pg#=
zRYHk3qPB+{p|St*4i_}No3#cpyrEx1VGq^m7z%UXoV5Xw;!t{^f+g8kZkoSCoW{ho
zf>d5uQC&^92k-GW)JKffdEGx74$)~p=s~R2I`n=+3<~+l0!VGY8FB$XG=A7%cCWrm
z5dUjyyW-;bo`cWLEhCk?MDHi0fUQC8Hk_C_tkbunfMPdlaidR=@(RU!*6TT&_vxmr
zZ3dN(X$y06g|zajAvKdTazoQM@Li*O6AabkR}Kc@=V+v0?DWrI{s&A;d^J8T>VQgPnl)xGx@6jAY_yZV(8Uv26n0KOA3Z
z>#q-Gk_sc-j_B5<5|=(3FuSfTl_3I?x~uZMNrn<*E6N^-^Pu{4Ns^tHl=HRAJ>TfIch&^KyVDSGd3n8E!|6mbZa9X~
zIX%S{iiy&e-B>K`>fp+Z>JL+K>nKiG&}uv2jPQY=WGlFBF|+0oLWudPRD@VC@-6)EW`)@lbjMZAuT}2%Uq>4Xt
zmj0D((;D-$)c9|W5r{O$!PY{bw`84TLnCpCWn1-!_UE%bP4Wik(74|C=&Mpaw#i@T
zFFlLvqGqj%M$6h2dJE!O7aF;JD^l^={CirfLo=zUF1;okM5Ofj(cQ2IB{MgtRH
z_4s1gUk&r@h=vw`%X1W@uh5pP%1k-#TrVn|4-vJs
zIesO9qnd+&5N~>%a?GyXaM6Q4kwm4e_-%5e7*3Nu4Etm=B$Q#s-ujkm(u4;(;2rAW
zbz!*N;v;A;MxCc;T`G<@HgNpGwu0?Nluwk_aQu1^&)Cm$f=fhKm}C@sWx
ziM8WJSx(XjGsCED$pCz(0}d4Isz{Hk6W~X$9Ds$PLdSCdt94j!1A;8p$ERO%kB&+u
zD5cKFjGts3cO?%YwYL$=&1rmASG!~N(XdAzR{W%0MBv5iUMxHQAT@rgdRXNH1;39j
zvWFU`+0&(ZjI6h|c4+xC-^Yn$LS;|KG*hKZq)L2qNBRB9%R=m0ypN~QdUfr7yTni1
zQ(~lT5yp;0!JLk?Ig(d#FR*+FrRVlP?tq?~`+St1Q{5#06aOZ0H=^uoK2T+Z)%Oq?fl-^Sm3BkkWtJkea*B
zi|HAxT*LwUh0?vi-XnS%$yco&nPNRsK}`?Wg2ZbKXo9pDXy7R}i(vgba?8ltZpQ(R
zYA!&Xf$K!l0hS+g6mo&JAPGSyW-^J-w@?;9CB6?E2e!<}nps(UnqoN93I?PAbKz
zZlT9>=HF%gRkM%@9LApz$#o4?8s%=!_o0&!<>wHfUJH
zbj1!sDHwtL!p;a6PX9=HV-^2_gM+6S(3Tu({_rcJ$i~~VSGV~=QoB}vt6!#5YkL5ek751p}p#C|7F&f!gDYG-E1x1iWt?aNJ2gVY?pSm1hs~B_n
zz}(O5K1gswky_@BD-qV}_bKttFT`8d*kIKhVw#LD{3%~k;q}ppFR0-{VL;?D0Os}Q
zQvmrR0e-C00uVUT$o7Z-qHm=Pa3!bpyRT|}-nd(+u0;(o!J^-+fq4fQ{5Nz;g-+Cj
zY4~>B{XU*ue0$LIG3Rt2M)GrNrzJbm$6Xq9pZe4@YH%o0V#{tWW-RCz)!qB$n>q81
z6%lvf3(D~FKY%^89gwEZ^!VcjqX+0rp@?no+805o-g
znN_g*TNqC^3Se7l3H*qQ2axZVpj=tDdJ&*6OXn60R<4#7L@8qjT4!dg_cF)p?mcuUq4G=!I__ql-%ScVh?;@Ed
znE>BRH1C5z0mHQ<)zWAMSzSg2Q-+8MH44iD(E#gf>)0ucSh&GIXT$=upz$~(WFroH
zViFQ>e8?D3u_ZoL411Ffg@nkaPYX`zw{Ht{f5-QuX$~6yUtcJr5opiBE>}J`o-3)
z+gM6gJXd0G2G>uMYp@RHbcf=6#q`c`96se2+GKlP5
zFU4Aoe+K3XO$jX)`-Ry-?6vRPaz%0km_i3t{Xt{#07U?iRwU7gqtyJc+kS{)h4jZLyBt$qjK(GmsuT1#%-?{v5>ScXUszU?6}TroRZ
zo%(j&rJSPcj%@C8kE5C=Hh-BG$(C%q2xC=j;Z<8QmwdbAT2!*AQ~wfJPBQ%IsgOoO
z%z2gNd=blV=GpIdjkv&gn|O0DX17bA7kIb1C$%ft5>4uK4GrGPa;43F1XwhA^sQ7x;bk
zVf0%a&dVci8ir`I&jV%*hejY8LqgAlamn5(vZ$fTf-dB2H!XyVt_3gUZz9rKn+`j?
zR#;;m1pfXF*hevb=tF1orz_gGAdTa8j3b|Dhp1`8y`*KX^92<5xOUSq-
zeO)Am?yrHfa@yf_<+(^*ywHH$s&Y?&rFVuq5T9yE!~RpC-x7ISUZCe|H)(~CDuJwQhbNP@a5K
zTaq{7y#U}6X~+%$i|j$Uu*yOoo8*^#GCEblqi>1<@KpHU^(>5mTxVEGB2S8Ta>T-#
z$8icXlT-x1KU
z{i&qGXdhzov?MZKs118&2Jp&59vQbUw2zVzogYp=WIc^TmCgC^gvV4XEgVsNE|sXl
zV0d`R_hYVAT1*dX;^EuK@UTP=7$ZMM0C1Q2RU=&q?)GwZ;?e5bG*0A(0_+nbjn$RFQTlklk?Y<%lIvau!k%|J(Kto1W$0kCH?lTQLdERlwf#^WC+
ztiZ$kBd1hz0dq(l?$+7t9}m%@vyAr$?mA!dID|EZ78mr~&uX+l#|4>I;+A}-FR0BM<6(6kQOrNhtC*?nC
zYl#Qji%;(hSUBC&tqx`}k8b#q8nd~2BzQECm7J_gcWS-7QBr;abSl1iy8u1aiVc1v
zGsbPz9ACdXio4MqBn1MI5Ukw!oL37QN#t8}RLcvw4$AEXR&&6IlJboYE<_A2;PcN6
z?Z)7Fkk9h{yNr7`O8xs-@C%YmbxE){lM2e|>cQBSj<6paVC1n{4oo@z1j&^I&82k1
ztMjqHmj;@l)5gKpL?JbakhGBZT;GpuAg&wAK)OtRGXSe}lXli`nlRd7(f4v#OH$Li
z2Vwk&8kmd=iWlo0n>?2vIIh@xI!&q5Q!ItbL>?x%X(vp1`K2|Yxi#?27b~(#2f`WC
z+RX>;j{6gL#L|}b2W}pjwXwz-bNwp|ac9lako0;)|B@sWI
zQRMr&z`9D`rGW-1$FkgO4>WqbYclCJXj=KU4Xtn0`Sk%*E^T4FLQO&5T;$}2)<#|uIC6;)6l2`ijIZARf?o)c2-is
zHRK-%XPw`>1AzM2?uq61K{F)@-V`^6)0kx~K!d9O8|af9vPtcAoFHK#P;wDx3e!Vh
zq-Za&e#RMzS-s$IZxUfA)dJ2K4uq(umr2z!hSve1`R@TW(~?C*b~QHA<2kWj@TZ_A
zW3d6)K`1NfNJA=-kMvx?b3=6Ek=-^P&&mHARj$Va{Kr%(@)YFYb^4dW&xX{V|JXwJ
zwX;fJf3yB*j@d6Ta%1)Vq|{r#gvo!#i@p1rv66IeJxov-fs~M-sN)1rX?A(Bl<4zZ
zDPU&IX~#pe<(!e;S9M(QR1jEupWVbT{=&^F5_-`jm$Wmw+_jkh0Bab#S{<^}Sd*-(
zzfBJhH*Q@^i$yga;kl-hapVmB$g|XF5n0{Uk!Gp~(aUs%0uO}xrMLRDCh9!*mA8%H
z<*NUmjY_0iz?T>k*Dq^eU<1(&lLZ)nArJG`RX+E+m_pl;@damS`tu}t`nMEbnLm6|
zb9)Z($yEzawyq8uFjO${05%oMw-IbvmkIhnWKv`0)ORa8a_^3hNsbdSB`Ye6_@B3z
z3iHzgkB02A?D2I!Pf&V}0VM0x;w6%Zb|Ssb8Fw0*ZB?81<>v**%D@Ly^N$cj(OHzn
zkINbkbFww_JWU}2k@0zN_$q_3q;#q$fP`fNID=pRhc;V>9(?ZDfJwW*DBY#ZtR@2b
zG}g~5y|l=I5Lq&>2v(Q!N(P4#Hj>U37+`ZsungZ&c#D@j!{u!O7V@mluEH@m^%LM(E$3
zbyB)rWhku;@d*AEEO~R_350DXIl*%$6Zkhm4lH@+xo4-S?$ewgO$Y(w36;tcwK><{()6tm*=K;-BKU4!vqI{qPMG^o#f@x1x%XAF`GbaZlja~c
z@_poLH+V^MLRs8+7@B6a-?lDRs&wU~7s(k`J}yX$|8
zX|jb^ha;N{UF*Mj>ujrvpQn}bBC$=OY)W>)j@}5q@f~w_z%?BPIMw~bXw&$e`ZL{{
z+1Fa`<#izl6j|@g(s@<5RP=WAwze?kNjTzL?R$*D)-(wvx_#MY`RhF6Q)K5Z%hTeE
zSDql@YO>B&>zG>RmT)6qqQDCFOk@Y^G
zv!@60R*ts9jPi=Ih6WYJl~QbAPOm7C{{~oyyL8LC=t<9g3sEi45|3=w#N{LPi99N>
z2|6DYj!g_O(un}>?3ghJs@HzgHf*k1UG*_vl1{I~>U?1>ErQfRh<-0_LlMTa@ILEz
zRo4hc>MLD?&*q|SYru0Ol_UR!#V0lyzBG%UcN%f83THxlE1S<><|A(K1}`zbk_
zfa2Ft@s7fcPK3#6ttz71=$M5O))iH@Qj(u>e3~x05|$+FlQe7b<|@|Ws&G&C=c%Pu
z0_#T{!P1=k@<{Y-b?JcM^BiqYyABdGZ|ML-5=mZgP8z9b`J-0J7@
z1*zhqJF(VdP@Kq32Uc=lj+r5Mzw(HXII=&+NiwSK(tRwMc&3Z`H}c-C__>M^nnvu)
zu5gFF^(mEzx=J%nABycIpA@lNE
zeZ@$lH<0FX7~5y1Ox>~jO9FLd8KA5F+qP)=2+-->oOFx(%&lUxK-qC@kE`9wlh9lQ
zEbVyG-W-mCn2Om)B)cFk*60?TF#$8(5uClz6mhHmZ
zYA7wU%e$ePIZZ5UJ;pHk$`L`8wy6zK)!cF&*#_b7=BWo=wYy$I6&=_-PhUT{r#55dYr0^&*5~
z)^OFIcJ(6kNVTYZ17<+*>Lkm1!9via;w~f(qCjIs!lCiM%{YlNmGhhaX~%gAUNBgr
z)lU!i^fgt{7kcH`3Q-}{#}C`G@Q5^_BzEGhz)+dc_@sVHR1mlFnPiB8OsWAN&2^0x
zXdB-MPJXi$Y|29XeO?nbO~%VBx_WNoKc^;HA^7~9*;vPsc3rZWNuWfpIMe1J^4mC`
z8Jiw}Q;q8=G(=-9JJ`M$q+MryP}}Z4Rb)VF2&A=zhZdcGS!Lm=zq1
zM6WE0GcmmE4wJ>Z*NW2f7*vv1X)I_k5HjUP>Q(X{!kHS+ycGm`f{j&vpBZ#|K+Hr-
zV~b4gqP;9u{`SqEHO@M6Q5h+BCM1%yV40FSO?4w@gNaK%f+b5mzZ*4AbWE3?jK4d;
z*fyMdO!H5draO%E2d7x#H-Ds2_4&f0(wK^7Olaxl~Ueg@@ilA;vEeXXSygSyb)AN5Su
znn$k1PZRgfpa{ZR!h{yi{3bIE{%AIRCaJ(Jg_x}(;|o~{kqo@NpYR&U&m?nQQ;8A
zOo(V0jy0X54a4qgfi_pL50Fxb9rniBRVZe6ER6%tZPX{e2Iq=5v5q86=Qtnvz>?#G
zxT;bSed$?Vc)2CCWRcpZ5nSR$SyG7s1<|3A@3?K*{yxuBDip8s{dp&WeaCJ3B43##
z;z5@rOVT$Uy;veHztW*Qr*4xz=HGgNVgZir4&R2~9Ai6s?vN*c(sE1Ie@Awt
zsz9#$k#+GgK{nGAeYNFx@#9R7_mqf`h}Gvb?ffvc&d$Q!4JF&6PVL@{oAHhn($2U|LwRccjxWOKKQ+m
zIQ%R-(GsMv^@AmH*QTXAyl;ZbWYFMjN0o8|<9kwD1*lhv^Y#}!ZUY2!BAa$Qjvp`?
zfCPN}7V|)5m*3$!afoGXPDkTz&S$I>-l}qH5=`)}q@6*n#gXgb7iO@DIa?3I5T?FbCZA|X9?no*kIEpw`m~{=$j}o7+ewCR&52n_(2qBB)<5C
zpX?v`Bi;nA<%inp=FL=H#-fQE-FVRxj*iD=>n`rCCw|_rk;fE@y{T6T2}o#>ep{N%
zEI(ts{EBa^W<(W|!ATJ08o8KZGlw$+#FgjO@wg9WE+sZ6A0{nJw6VEu!ek)E
zYR+5W)G9J%4Qr;D$rt$QWM{DgwtC_!{UeGsxO6u#^2FLIS|5XzccjsPfJHIT?TPkZ
z&pFFO(=;_3A`0V$y0^uxaV@TxV_^sdtokOv;?+?$)p!tMW)orh-I<&D58l-eFE7rY
zrA=}uY2=HJa{V!r7i+vgKH<-wj9-xG4Rft=(*|~Bkn*vJNSpQbn5W{a>Y8yPUC;$5
zCRal9{I7A4=Z=8)%B>)EsBT8T^9%(R4c7GgXw}C41G_}EcvtNM)P@bF9~ENCBs#fW
zscCN0S=V;{o>Cj-9pwWu-};HAf=|R*wh1@1nsLnfm2&=3mA%~v)#SN=4cTsNlEPtL
zl=x>VxR5B*Jw&tYQ(Be8LXA!RF6RS|Sza(}j+SCA=>9O{6jqA|i?r
zf6=0bL{Lt{wAbv4casMkn1&$hR~T@FtuOpG1Qg9RlVdCgn<_lY&2oMjI4jNvo27|W
z^W$OK#`U;Iq0o9B^K8ow^*?|s|3YEt&FuGw&xr88lsoO!uFHISE-ZEZDKXZeY=jpzkmODD+K7L
zg4b~X?^g%^LZ&6Gg@f>0hN#qn!N^k!ZhhZRn9;HWV>0}-O)L-L#ui2rl>8W2C*@Cb
zQ9|ZRIZ2&i1`5e)Fy|MkM&^}+o-x~Xx%Ys*%xZzC3UtC0lxovs%uA3Tr)dF|B#pHlasX_VQ?CEsri&_9Yt;YwQvR
z&B;Yxg+)}Q%{13ce36U|n=e62!0y7JB$)FUjkN~Sy5S}?A7{SQJ%L1=3t){UaAgGM
zYm%~7ruGWFl)Y`G9`QYw_#>BHcwk@%vcf&SrtB50`rT4*Fxg-8`zcM5TN^q{<*Vi_
z0LQn~CcQ5aGH2~6SW!pCD-|KoQU<)z!vIye{6Q8|jO~Sswz)0$q<5-8OW`ROsN;nH
zw*<$Ak;06Hp+*pBTETVE0jo}X_In<&IHKY`)%U(DYOi%`
zQtw~p3S?KN%PWjFLzcYui7;6l{$nixY`XRc@fEX%_KIFTRNpab_|e9^zXoNlc7-<_
zUlv7Bx`}a8{CK|h-PPBa(*2RXiFS!1hVK8f&hD#nfQ;rolcTC^4S~?raT366wWb!S4<<3P?l%xoQpB
z4MjiaZ!&J^`N$#ldM}0b!Z9lUfl%~ld_ZC5m}}xju>)zeSs&HS#Cvp^zdo}_P;!cNui?2%Wuf6UyZ?7xigTVEODU8KM4?t6PJ64GRDHD@tr
z4vOk3?krHd!A0me3Ursf{6{g$ke4}jl|Ak?G}a`fUm|;`GE??@FTAjfW%U|GDq8nAC;Y|e;DE&l4$C35v(zZ94hf(sa>Gu+x>-z!mc}cV>Xx_>rQ-`kutgR
z@m+cJ)S$syY}!|@#uXFgo02)y7}%JJrp>rQFMD7Av6^wp=JPI!-5_V_aNs-t(s`Vy
zrfRvc+nn?!uIy4z0mTea(#jIcSHj>p)Ge_iLzy~@UMt(RtDNgKhLb&w^3E=~7{TB<
zz_6h|WL>B9_w#6MZzWQyYyQrT_t#jjYDh;mEuK_u+)(4`PcRREv!ro0BCjXkSE|O1
z*z9^3U_!E--_i{b
z$N1xJ@yVAmJY{3z-;v!M(i!`uY2E#h%08_HXiNW=dhsug2D02@2t^+6nq~zv3YqZ)
z?Kk^fvrRMiT%D1Oor!W&Icrn4*k_56BH)!`e-Uu&(
zW{j>45q=%18cR}9zq71RTyljIBZ|h9Z86%*X!yT4?oQh$4IyVn9$3sjkq3JJphKeWW3Lc&N$RXK@;l_@j7amJJm{B0m2%ZU0Nb}c5qh>Y8abGu1riSE5yh?^;pV$
zIxza`Rz(Q>Tlbas7;oN$TJDHZb~Ogl9)3{m;^7kVK(=dC%=W`46=zEXy3Ys`@Qy`$2-R+C*OX|Q?YP>;_j0X?W5q_|BHcqSE-(@C&K+@$-2|%YsrEk
zi>)ta!IJ;);wGSnc%&kGw$b4E&H2@{jK*^qM?4rl8N>@sUF8a_E$uk6dI?u{WVPM@
z9-!ZH^DLv`qPwG#7!r`9#A1tlHAxl`)rUTNRnOI(OI7k+>7L@hW)z=)@~IFg_c~NP
z+nFZTKfA+)YaDjWhH4CcA&ub!y@XAFYBe5O6?sn(yUYbA^gfqna6V|nfl<@bc+Wid
zo`9nc3RwcXbu_r(6oE@SYECb4T@A!S!%emqs|kHm%b)ceA{ZFDLl3(HaqmarQN!EQ
zw}gs%J})eaG7x87oRj@qVK?y{QD#)%yir-iUi#ZzmzDFx3w@qL1|Xt1XA&g+L?y9k
zN-@3Dj}KDxL=*@$TPk}E2w?Jwa3
zJPttJ@^0QhsOadbdHYl95NImP{`ONjX32Y2bNbqVe5$28BTj*saVsKv+s!R^4H&>@
zoBL4x;jOj?JM3;xw1Sm(J_ku)`Hn{cc6##?ww&Y6em!620FXM+3s75_#m~muj^KQ2
zWrGBm?wqaYj&kQz({m#6Y)W5nrMe`mzWN5OZPjS8Pr2PK>A}drW!L$_(L_6?*rUIY%{Ul?YSnQntO|Nb6+*iQ*oR$LheaG^jwb+7Cu?dKPVTkL6o}
zW_hs?ie^#%CT1rYs91lOa4~dUB#u~0!JP8D46SC?WP&6y6Ta!z=I3|!K9O2~Q57e^
zdV0bh>l-GtOx%o{5m{;ceBJ7T<*?ftMo2f?TFtm1!l=6&GW*FUPK7&!mvPb}o?Iwk
z=)-K+SeT)0{2h$4(9OcTVl^NS(WTn&9;4%*Pmfph&TZem_!)o@$Si6&C(i4$#^=*E
z*j6+BezYl0r~J4-+JA{8UL~9@C?c~To_6nv&6U>r7X8A`M(gaQJfW866o2Mq=s0GR
z(o2ov4p^m_HGAs1fGcb%ueB|-3XF%F2ifXHR#K=`*qVX{=kzDXD#_B$0oJ5Za
zNg99TNjRlZiSH>O+a)|0Ni~q-yF$2Ol_`BcnF0>~S=jYB0H%~KCzxl&XD(XY(4mob
z%1paKS}2?9_8s7{|8Kc95&L{l<8nK1H|N7e;yk=M>@atOU@S7=yCTztk$CkFd<>zFnG;~~|*PVl4*Xzawb
z3-8RZGE7n4*@c=x|SW1DIIxf
z_;yNX&Eq!Pv~1b_g6sA($ky&4RvVcw306toLlSMa>2;koc^fcGPJu18NUnnsukhU)
zpNAAbRAcl_R;T;>ajl@T-DZ*t;y!m@|wCESjR~eHk#bg3&K{h
zG+INJ+S?9lY4tgUxQP@RngSOCQRu|auCw!p+_wMIk%IJSE*H6IRf)%BD519n0T6juZ$d1NzdZq0lIGsTpt
zZ-6ytl*#h32iM&8MB7nrH;loAIJ-5V@Z1F6t`J4&b+D2413hds+2zh?E9tfw_xo&;
z%`yGk%Nu*3{Xv_4llL1Wr4dF#!!E?jqpSs=^AE#F?JG2Kc6S>5R9asE0oXuD%SlRo
z^*7VAR>VXR(+&XrdA|y{;Di*GxOdg;9Xd1ReRSbZJ9(BLKDfd-_Leng1ibqMQzVl(T;R2uUAJ;0Q%5_FfScKf+;SmOUtHUfJi@Gtg|)$r;!
zDc??JvbSy@650DHOTnQ8V&`0_~DoftD52R;HOi<%~*D@egPs*@_1lBJLcTC++1{JnMOlz+jA
zl_h7)efp}lgWG9qCVkyJI85g432cayWCZZXAF$|iR&K`$5f|fNn$E+vjBRCye&C(<
z(SAw>Daf3s>JJsAL%EFxKGs;VjG1Lua#JEHN&a(3pklF!u=%
zuF=Hr&^)01dMS^mV@j(}7LYm~YNx&4Z=xe?;F5fM_2+6Ac|t~aigUgAp7hh4-I@-J
zF+L)`5lbUqE-T*KSMb-srs0FiG$PZK$q3YAs82Z&s<`y?xbs7iODgfOF{pC%X4rhK
z;^v$^ik(!52d4fWHWWgc2Lh-ISEv~^BwBTXlGbK5@1)Z(>b*4~8`7O~hDjO8ig$-)
z$AK2`eoLtpP4hVmkUmAC5opV{Qmx55B_49xSv25~N|{*<_xld8$QH%UJmmOMn^`o)
z*s75VxS`$pYwbr6>}t(>&*X!^Xks^Q&8xVbH{nD`pHSO9&2_ubDl+ouH0mAO!@4z>
zLcb3kRh8cs5vuY3f5g3YK$LI0E-EV0(p@4_(%m3Z(jeU>4ALbGEz&L0HFS3h(nCoO
z-QiH9&QKXZrx&nwz7^Q(mEzmK2tI
ztsbQk%qt!L@3WHS9)AgdYCiH-l;R*z>djZA=eiv`Y*Nz)fZ3aIAl6iVRk&+zGl)}b_3FGE8s
zvRk4!K6Crc^+;Cg^Oi~{gtF&U+W;VS*?ho~*meq{$>F%w|{QaH&Qa$>6E
z?V;w~=V>_GLJ3FMenQC&Y{0Ti#)(Sf;5RhR(G|tbH3jtz1+rzVoa~C9j55r_Kc4`al0A5gj9*{j8oH6uo5eocy1n_)q$~qSSa^?AXv`H*&xMC+Aq<
zU!kPVn-Y~uQr%o;ktDlY4|_y^+A3rZiM1O&{!}P!pCKHx*&x{u<5)CjuLzq3P~W%`
zy_Wo_J7&RWs!G_EVaZo;hQ$4Py=+mHw(hU@RplWrx2jkt5^QvmzmF9>>#d>y(z8Ug
zscns~&0gClu!CNW9>EQen2H17yM+#%pfc;)>fyYj=wQp=rV-+8<_LAX!*B#1{R0d2
z(YkOdXOianzjf6ZDT0uVFI>pVZ$JC2-D5k}$J+~j07W_ypd&FrA=o%eBnKL^o>v&~
z?;T!UZ+C7lJ;o}cf;k|47<>2!!ex=CBw#5j-Rq~*-3ZB;zEkpziB4J6LGbfS+qemE
za*QEow%i{aWP^2`_&{XACfM;rGyrP#>;vGLsIOLSZ052+d#36
zYr@ZRdl)-!*7uu*t=+I+)Dv=9V=RlP?
zhvh^{Ec)WlUEbuL@(}h6(T4udn8^JB%iXP##313rs**!1G#C#VQ0Br`hN{N?fVEBeEQ>4(4qf
zyyP)8^iCoMr)Tq)zoYT|et`q7Lr`jc!+C2Rs&y!ax>PMw=pG$9@0@8M_$<5AgpAX-
ziKG3GL-7%tai&SKE`beZj&)}YkTAVz>(+S^9xzAZ6s#cyKfa>G^SODkedbLm+ZVg0
z$7C<}=K^?@mfO3Z#`yaKPJO^WenRiuD7o+JZJBM-r4Edrt$Z(7pn^Tm90gnBjyQ5U
z1bwroe_R^-^mk-i=psRdl
z))}?_S5&-l3c4S3GQPW?hg7|4{|`lRN4)nyAlAa#G;mp&5>H`p;o`Uf_SLC08^U%y
z1fWEH-2h?{aSHH7bn>c)%Z}I}J^7<6N8gq^Yu$ya{UlH_V3NuTSp@;!SYgS}-F949gBo6zcP5nhY0hH0Qr!8y6va^g0Ic3-|3}%{Z1gl+1d~5%t&qq
za$`Aca5owNjQ)B0<(sn=z61-*
z@&a>wl1j#Rv5pmbw6OUFr-S=%_IPz}6E9LsT@slyDM;T|J$g!nA0WDS2(%{KnfYdN
zxOu~r3EaIjnq^#whKhswZ#^rHr1#CkgzFs~2Ckw(a@eZTPQe7$&)T&k?xYIGh5?vU
zpScsK#{?ngJ-^(Glkp#4WU~|HIqF47+uVAp^%RIMV3y1AdfvvL4-GBN$PE-P^w}B&
z@^6%mpYWc0s&HHqa|S|LTVPdeV(4c<31Bvu?D~0o#ySpM(+_{v{e=KsEmUgse|W(g;g_lA&mG&l3o@w(N?O2>
zBer97tD}E!x3yys1!OYI&Ea2_1dq5>+fv=)F!*E)y4dI*!G8ErCSFL5
z9UZ!aCx+ll$l^IohQeFrUK}Irmf#HBjouqWpJ;@P7)B>Y`$hi>Uq-H#A`fJ>H57}q
zYW=(igqbqv4;*q;=*N$=%+#wi1FpCkmR&3QIKNm|Ta#~Hi;oz9Wqf#wTlzYd+z;UI
zSlLdx1Fcp}xlWc?;)cQrQD&9I!oLhM9U1Bk{W#I7)sVOxS%7--^{e}0v;4OMhv-&_
z^;h%eD198?zFIp4-_BNs
zqf%Mru^IOi<|x{8-w_(K5##*^^|Z7fpkVH|)6_|kHIdGcDmOQ^LA89xPkk(yhPL!}
z__Mq`D9>mA8w;=2Cr)_=Qw|`%{eNnQ@c0nVj^ut
zqxDtwA<-}6n#UBUnW27vMA-SS*+>kA$14r4Q}NtGH14J_gz#K&Gkn@#I}wyiMI4B}
zU(L1^^T}7v3N6X3IwX{oPaw6TIPE)T^Z1KJV%i1HbyJ7q>*{LFUa@V{px$AgBtxtZ_dq_E_R2
zkfYPYsj~O{f~`sy=CzD4cGf5eqLeH+qR*PDw6ZAt7i*kPK|aX0usmO<(m<|#g)A`a
zJ(KL42lV1(oPN-u_S*>~>x36i*^i%1%e2z%#vicmb>qdjDc$6KWC*BNkXk3p`%7+T
zJ{-0j1;=)VWNnD#JEq;15?=Ol>m3lxjOQKtQu(BwKWD)xW@?aesLgCNj2$?To|?EC
zT`w&U=sP^Co_{1>w2uH&F9a3abEG<7`n2t_cOhbOg)F(hip1pdr=l1<&JrBL*wEsK
zBsfQ={rW$0vo=XLBGQ`rO@oj0vMvq&;dl9#n1MgH#EksIaFreTOD{jCmCW&4xj5>}
zG>a0is33=hGD%&A7XF%gmb0WIK%v$JKQtv7-U$*6h161YLTDl>I)IXjNRQTj6%gph
ze!IjYy{PQTBPZmtp0W*Rr5w{AH_9qgMpD
zinoS++C5Mq10X2CpsJQPk;18B9@zb==`n>Fu`l=*hkmZ2021s1@&Bz{Ip)AyrMOm~
zzIib#&kyjUEkC_hXGX>tYWAicHa7iETsjh*GOFv}ltOJTEY@mi5e|ZrvLrMi_5+iD
zHn_b<8bjXwJ9Eh|Q5NeWft?IFh>wLKkhPX5CiqpXavZ{&@c0UW5R%
z@a?cy42UoS40fTNWls;pu#_`Dy)3oJt|t$xmK!4dC_1s$XTmM8k6Ss=+~&kiGL{)!
zo8RY=+W2($B1G?;STSB9o58~XeW8PBY9OvZ6=SN_Y?LPR`(A_d#k4gWKI~I}(>T!v
zmqRRK6J##b?uWXqOcTXzAt~nbhmi^+W}7VL9I$|kADm1F$$v^$)YpFo}Bcp
zZRbWc84b^f2mG7<7odH7b|C=YeSJ(rllQb~z2ptb=DDh|L+=N3G0K-U4N0AuUsQbK
zX3@OvZojS#e89sRC;1pmo-!gH39dL)?^@?&FE|=NP-?QXNcX;PI2NotCzOOSao*k@
z_Y5?6>y78V%O|h7#59~(>nW-(|LL<{1G6Zv{LAe>oCY#bDxgrqj4r)HtdRDb&c;up
ztNM}e=zEmwWQVA$l#%^LnZ3KkX5p5v!?gEaz21|*zgC<1Z}L=wq{2ug(qq2vwE?qI
zi8j(kYm6si3p0p!f50zN8@;ibs?tLIaUQ>_pY4QW8}Z}RXaPN3(rHSozUGM}$5^^3
zL5roLHLjywPYp!_FU}XbcORSCaXYXtbl?e(D#@}X!0`5JZpR4``;}wSBLAgFoOKHR
z)_)TdYumr03rs96tsm#U@u}c;gTw#>Q0`F<^DmlZ^*XHxbw(~R986eVoa0asISP;p
zDkB0sQ5S2qDt?fTBX9Ke+O1e;M|Q%Vp@LYrGMU#?2IVem$Mihu!q
zFFH6eSL;A*zCgUh>h$mFqXqo%Tirpo7jBhuo
zc7U*BPms6O5!nU+rX)KN0j5Yh&FWZW)t^t3bg}L;ZrCL1`;^;@_25MW(NogBu=>>e
zsM7RbL^-;94t`nW(ayUov!e#sKkU2o{fVLw)0rll^Rh9hvh}=o1$(IgBr79udxVc;
z9%Xm*IS&Plg2*=)8&ko$<*4bjlgrs{>I*apQ1
z%T%G_N3ED935*@EkCU)YL5jqMAqfP1PH?}eqk--QrW1EXG}(E~P^xp!sES7%xq`jkjw<)sHb
zyn5WVb_?ZCc}JwXqZXXlXGhE%`iv4UpQ3r%LyH`4oCU;Y$I!?W&AX;*>d_Z}kc;Am
zy!f)E1L|Fqb{-d?dah!LMhRIzFBPA!bKyPD{1KBH{mkKV;1FlE?MW20p$ko~VEWw8;;IPm{shSoQSpvBw6$K#G4MX8^2Y
z2mm0T00!@W2|~62K&vjN)xX)(zW>;f#viFCv|ltDe>XXG)9km;Qxzh=F<9o&Pu};V
zjEo?&AM)vgn^eRrvGxGUISx~4@F`)1Ehw|JvRvfp$4;n-g3xN`%eKA?j2}B>L!5j8
zZc=v+%H^>4&%@8O-H0j<+^9MU#UH1#I4EDQ@|<7ZWSz1rjU0yYz1GK;ldoKdz)M*;7M1!I^M+h-Zz{R(JKAJ(
z1yI7m`0i-LJ{2y0Xjl6@cB
zbQQx}h{b=48kNG{!vjfHg%%U1<{qN1ktmrp?AUWd`ldtyRk%Ti_kQ5>^m^bSiJgAe
z&5kgW
zol7+09S`J^ekbGIY>)vv^_EBeSfZpK8VL`~5?!YhhL82z@$H$F^?8Th5qhJBC)F?TL
zy>@^w$okHo-v@X?zrKM9L1U660mOfRDF=WSfIRmLj$@jG)%K{?3z|av;2eM};e#G3
zB(qAmp%`8169*}^ea`a}d`^Y!65l*T^9jEq5Setpx%;S{OYboZ3aw1t3`clvPN_dMQy9sp`d
zrpNWy9Z`+D#ogMT1HuvJf)Ox0V)BsR&GuYvnRx$u%28M3Ft71rLDp=5qKN};%fq?-
zVA*mrTjE|%S8osaPD@!z$pyWG*h-B*9o^g;3-;ROG?-BDThHu*=QdL(8~(HQi<194Vd(A+>&zyI?23J^M7X&3;;{~e<#6_n|Ku6
zOMhvy`czG`fPo~;C3)B_2Jv)nPh-;N`WaGXx)&PfStzbF)b;lZ%D$?Z6)+qUG<
z0ne%-6j!wEwQNAY^yVA@$3n}_@9U11DgWB62%%#?RB+Vc3BV*6?laGv4$+AQ)h?rT
zvO4)zpUe7o+)MpPTb-@#2FHp
z#GH`k@3w#f>p#jXGOBO?t@Y(SZ5G%v-n8VkZ|7r10wa&bX|1e#88_e)5tlgyF3Hti
zWiiMFoUew9VqA}CIXfMiYW1k99**dDNVpwu2doeL+XP}%(y5~9W}@q3`TGnk;3~Yd
z($#|gope<7l$!#MG-OEb4R|)b2yeg1gA*anp=1o+spMJa
z=vZq)GhmYAxxO0uI5sznFjRBpDAL>nYtdbGuPzNG=~ZXa&VcJLw-;?CivgYM+r0lD
zek505+TA+C$bHV!hHqDUs8R`N4{NJlpXD|D95Pq!+HqaDn<-sUv3QCMpyhw3v@Lwq+s@
z0fuwclcDQKKbxFUU5dsa(}CUUj&RVI+f7*;(U*>F&;IUeX%Tu
zUWw_d!upW}=Mp4axOhy6DgT?JS4W!o@_tx(a;^BkSG$Bn7L33oVj?{F?5vxrBp*XQ
z`r>O<63ZQkMV*;S7H_h0e4b_1d^OD_V|Mrblg2xed8(b(+O^kWI9s-1e@O
z27~Bvll6i3i=iTatItM(PY5uVDT@<0Arqsj`hZe
zmByjn5s%nw%ro2C-Kuv?_4AR)HPB+hg6BhZF=2$WexC;^m&V(sWvKDCZQ#Nm29?SN
z^1Z^+c9M95LA9ohmXl&@666T_wE#5|h<>N>Tn9v7u|tvwLLHSpzQK0lK0UUeza3GM
zRa_r4AGX-&p6o^NoD@P#a6mP1*m?h@l#t1C8~RDenO$Uqs^3M>*?E*onMM*t(_cSy
zEpAojSZGaX8Qm}pb*k9B2emQj@-$qm9yO{+r8jtx7df0aGw*Rpa8Ud+fXZ{@#q3C0
z^bujvuN14!jo&Ku@x7BrJ+tgxrynVEyu+j4H3w~UK17-psrGKBVbvaV@ymd~lZ*r|
z4|}Q=nS#^_jLN+YEyJ~2&O$V$_Y$(Ph)c3%p*jpDYgOoF#1xm)jA~{}O7|P+rQLix
zn9;ggyNJ_?$t`k)1;$k
zc_XCx4x3^Vp5Rma0Dp=#zmGjA8_4sD^OKNx^gWN`H9yp?+2x_(cBCYWcl6Uv)B
zsn@bb&77gEpD-FNTQW*l0zerC!pjqx+SNuVE{?W{J;frO@0nJ%129LzJ4zQe+qZG`
zBU2ipAYc`F9*{8s3tHQ`N&RgFb+Cs#vsec5RSX@g^5}OD;G?sXJFK*omDGB=ON24U
zc-F;BfR86XqM1JEtdGHy&-weoy`t)^7ytbxrQi$Hxk%+b=}K|8Wc;}h&w=g|@kjsv
ze$K?kbyFIdpfz^?=yK>TN2*IKwB9an79uFg-xG
zcc@=>v8K-$%M`05mT^-{s(sj5zi)o4Qus7@zTfgLK!|`Fmk@XMeWl@89oB_l53)BW
z@e7y&_r5h&g)~6D{bH<+Riky2lo`@*=_eK|H=-*J0_p#bVR<(${$BCd{RiE(+h3iO
ziWuSiz2dRZ1G{{!>caZH%`D<^N_Rz!Wy*gom)$+|>8+PtysghR+fsnv%k@tWuNhuc
zJquQB%O3fAy@7CUg}^CR&Bvmy?C6eb`#BLgjgrMCU3T
z4stV=M#K}|k
zbkr@DUst@dg6oKiP2>nA?;cB6QDz$NOaG6Pl?f*wj+x!x_LLm}OZjtn>xC>4B!V{w
zxkrJXZMJrXK~~qAYAd>JPgz4xD`2`a8tBgP4A`pkhB=wsVSr8}6x28>MldpgNdsL;
zJxO&hY1;7{vn8a*I_%HXRFqpL=T@{v%-~hIQlccfR7_I}d62!t-9{aY>G_pY#{guf06d$d2fWc*phK
z)p|=laeKF~ooAL^2)6DGIG`Li5XY8znjZ9-bS2h!|NX1OLAKKi5s9}fEOc@*lC0Lo
zrz_j#22OQTz0qF@zo*nyf0DK!q~FpQv%TOKRl&Bv3nE{}(0B-Wvk)LpGvhYIvD-ST
z=0Esa&ZtG?Wo2mj`RLnuU$Teq@82KFDU*`sBfKAS6+UIvP05(L?~ExHCLW;vYdf@1
zCcM(7-maI8=dW9pd-41Amm%>*KeKX?_VjPN(%eg8ZTmck2{pGY2p=>Qm6uVtw>)Pj
zipnmgw3QR%uDn*T@WF>T4+~o+)&&h;vjTlT%6)4lbepxZ_A3D8RmUi_RVSu5i;x~X
za1=9Xwx(2>S#b5xrl1XR8XINFV|a2M!oF+4dbE|Jp(OdW#`s4sO)IcAuKnCls@1sN
zZzfn$(m&-}E2;TKKF~;NDelpzgBiy@L*33__`*>K)-)Zmjrw|(R&Q!k5(yIaK11tq
zjAED59E98L8{s~RbgvK6-@C34EqlB3EV&9V+2&EE1(L8lpQ@TzKb73orT0V7r^P<7jC3$}RF|8=ELd-%YXQO?9T0Ibf^
zVrRCOVJ!Ma?W5h;r}LqXg?ZW*In2apV=Nqhi8zUc4?YDX>kNn^9>)0o`lO^$OWC`{?+LR^Y4}YjH@r
zh%f8A3y}AL4ttDcK?xeZ9xBgQGIPB!2ore+{d?I&Jh8Y`7$=3TF7kp7
z*hDf$40{oP9W{~wW`7EBG`zMTIA8&-|F})LM8AQt_pkC|Ew9c}Q%5`LZuid(yEbRt
z)rg>HJW!Q;n;h6ORXb?glDjazyeleaYqBkmAe}UF=i1FhW}@W1j~pu1`MA>8OX(aR
z7uWp!09bEf#PI{+O^T~rFER4z#KH%n>~=Iy(kvBgqUS!)>z+xpBw*xD61z%7
zEw~*}n58R^%>KCh-QX&xAH@_t#(3g>bhQ|C=P202Ul=2aY-{`a+C`#2tvp2QFsPLb
z^p4Q*O7K2etXZQ{q9qDgk1}m~qdHg>tv07OCrhd!A3M6*OwR7MwsG$jIdcqv8r|GG^IC_n8MgX!rxt_k_)`=!d-CnKB)~BMB%{sPbVBk*}Pd0qrlVy7)WF5dT|#5%_LpkAe~zt7l+?pW#vl8FH|5iP^U
zb`M>`KUqTaK?PwYv{-5lT9uLqwi~!wDIf-X#0Ea}WR4f2>Plgw??kW5uX_-T;B{8;
zo3VT2Rv{|`(XDFsgw+*XjE+#_`6Aj4)c*k$7kZ+URi%v?8avi
zSayP7nf1(|bre7DSfE@O?WUa4It*i)ugI^q{$tZ1fmNmnZX&>hB?AE!JF}Q*aw|7N
z{IzUqOGMjuh~{Wt^MYi7lhB{;8(+?vWcDH`S`+Ovh8_5SRfYtV2J66St1eu`9S!*t?Q4E
zez=~~n`msER#J$Cc>wJF*lY`WVC%`q8^8*^g)b0z5101O$rWf_`I1@Vr^o<2bbLHRuN19s|gl_FGJgYqO=S1da
zE?##rT)?pyi!e{C$B-eeB>+G1caaE@93}1r4sh=|SR9U$UE5
zvHC(R?)FaB3agfQLN0nyw>yve+&#npl6Y$`LXh|7_k-4MSaCYp3cG6y;ea$;81=f@
zMl3v5+G5*Ry*d!ei%+(mkMH#$aj+IA2Qc>94
z9_P;2e?rQIN$Gj72cEL$0daFQw@gJ(PORy#D9(;I1KG11$phMqPhK*j^+<++J#Hu5
z%kEU!LqLXKt8RWs{brsi=j`|$o;|yE+~zTa7dY5`|M!