From dce891963eec89a8527683dc5fcf47feff3d1d62 Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Thu, 14 Jun 2018 10:29:22 +0200
Subject: [PATCH] Hillel challenge: solution for the third problem

---
 examples/hillel_challenge.mlw             |  79 +++++++++++++++++++++-
 examples/hillel_challenge/why3session.xml |  78 +++++++++++++++++++++
 examples/hillel_challenge/why3shapes.gz   | Bin 2204 -> 3483 bytes
 3 files changed, 156 insertions(+), 1 deletion(-)

diff --git a/examples/hillel_challenge.mlw b/examples/hillel_challenge.mlw
index c85242042e..c288679a53 100644
--- a/examples/hillel_challenge.mlw
+++ b/examples/hillel_challenge.mlw
@@ -1,8 +1,25 @@
 
 (** {1 Hillel challenge}
 
-    See https://www.hillelwayne.com/post/theorem-prover-showdown/
+  See https://www.hillelwayne.com/post/theorem-prover-showdown/
 
+  The challenge proposed by Hillel Wayne was to provide purely functional
+  implementations and proofs for three imperative programs he proved using
+  Dafny (as an attempt to understand whether the proof of FP code is easier
+  than the proof of imperative programs).
+
+  Below are imperative implementations and proofs for the three Hillel
+  challenges. Thus it is not really a response to the challenge, but rather
+  an alternative to the Dafny proofs.
+
+  Author: Jean-Christophe Filliâtre (CNRS)
+*)
+
+(** {2 Challenge 1: Lefpad}
+
+  Takes a padding character, a string, and a total length, returns the
+  string padded to that length with that character. If length is less
+  than the length of the string, does nothing.
 *)
 
 module Leftpad
@@ -26,6 +43,14 @@ module Leftpad
 
 end
 
+(** {2 Challenge 2: Unique}
+
+  Takes a sequence of integers, returns the unique elements of that
+  list. There is no requirement on the ordering of the returned
+  values.
+
+*)
+
 module Unique
 
   use import int.Int
@@ -60,3 +85,55 @@ module Unique
     Array.sub res 0 !len
 
 end
+
+(** {2 Challenge 3: Fulcrum}
+
+  Given a sequence of integers, returns the index `i` that minimizes
+  `|sum(seq[..i]) - sum(seq[i..])|`. Does this in O(n) time and O(n)
+  memory.
+
+  We do it in O(n) time and O(1) space. A first loop computes the sum
+  of the array. A second scans the array from left to right, while
+  maintaining the left and right sums in two variables. Updating these
+  variables is simply of matter of adding `a[i]` to `left` and subtracting
+  `a[i]` to `right`.
+
+*)
+
+module Fulcrum
+
+  use import int.Int
+  use import int.Abs
+  use import ref.Refint
+  use import array.Array
+  use import array.ArraySum
+
+  function diff (a: array int) (i: int) : int =
+    abs (sum a 0 i - sum a i (length a))
+
+  let fulcrum (a: array int) : int
+    ensures { 0 <= result <= length a }
+    ensures { forall i. 0 <= i <= length a -> diff a result <= diff a i }
+  = let n = length a in
+    let right = ref 0 in
+    for i = 0 to n - 1 do
+      invariant { !right = sum a 0 i }
+      right += a[i]
+     done;
+    let left = ref 0 in
+    let besti = ref 0 in
+    let bestd = ref (abs !right) in
+    for i = 0 to n - 1 do
+      invariant { !left = sum a 0 i }
+      invariant { !right = sum a i n }
+      invariant { 0 <= !besti <= i }
+      invariant { !bestd = diff a !besti }
+      invariant { forall j. 0 <= j <= i -> !bestd <= diff a j }
+      left += a[i];
+      right -= a[i];
+      let d = abs (!left - !right) in
+      if d < !bestd then begin bestd := d; besti := i+1 end
+    done;
+    !besti
+
+end
diff --git a/examples/hillel_challenge/why3session.xml b/examples/hillel_challenge/why3session.xml
index c73fc7d0ad..b1be653dc8 100644
--- a/examples/hillel_challenge/why3session.xml
+++ b/examples/hillel_challenge/why3session.xml
@@ -122,5 +122,83 @@
  </transf>
  </goal>
 </theory>
+<theory name="Fulcrum" proved="true">
+ <goal name="VC fulcrum" expl="VC for fulcrum" proved="true">
+ <transf name="split_vc" proved="true" >
+  <goal name="VC fulcrum.0" expl="loop invariant init" proved="true">
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="VC fulcrum.1" expl="index in array bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC fulcrum.2" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="VC fulcrum.3" expl="loop invariant init" proved="true">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="VC fulcrum.4" expl="loop invariant init" proved="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC fulcrum.5" expl="loop invariant init" proved="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC fulcrum.6" expl="loop invariant init" proved="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC fulcrum.7" expl="loop invariant init" proved="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC fulcrum.8" expl="index in array bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC fulcrum.9" expl="index in array bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC fulcrum.10" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="VC fulcrum.11" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="VC fulcrum.12" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="VC fulcrum.13" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="VC fulcrum.14" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="VC fulcrum.15" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="VC fulcrum.16" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  </goal>
+  <goal name="VC fulcrum.17" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="VC fulcrum.18" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC fulcrum.19" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.37"/></proof>
+  </goal>
+  <goal name="VC fulcrum.20" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="VC fulcrum.21" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="VC fulcrum.22" expl="out of loop bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC fulcrum.23" expl="out of loop bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.03"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
 </file>
 </why3session>
diff --git a/examples/hillel_challenge/why3shapes.gz b/examples/hillel_challenge/why3shapes.gz
index f3f6c9565b7a58c267341e479a54009554019289..52f734457823957f4de07d569e717668c48d44d5 100644
GIT binary patch
literal 3483
zcmb2|=3oGW|8HZx^Y2&)?Ry^nrBJ+^L1)rYb^-nbo`eGq6ZY!-+H`|?{^WC3?|S5$
z-~9WfyLG9U=0@v#UyhUs#R^SabfT&zRLARSmY{6Elhyl8;n%7(Wk2_v)R4R`S+MnA
z>D2A!t5;8XZ@2S>+4aiLm8H+@^6bjR|Nprj^}Tle_y6%rU*CUsZ+&UQR!z1~&dinO
zA2z+Obw1DY_qp@^$b{_T!h2D*xz}@QuAS@1@K5VL`Ayk=*ZJ%l{rhv)vAyANuU|Z~
zaqU$Pe%|-_Yp+VV3$0*%!{E%|8XUBFMxOsXx#wEp3k2)+-PVU5H9c_j>72L!oZ_}D
zzjJ^6vY^iguXN{TCg0?G^HyQo)*Joxw<rAG@F8joi|eF^OJA*2&C2_EH2TuZ{g<QG
z+$?xLee>2A8Y@a`KXOTA&7LEENqc(f2S3Zxi%xUSWt+)ny<`8qKXvo(nZ7u<byZZA
zO0NFnKmnD=SnerD{u|cD%r=#F+kF4`yuA@07qxn+-00U0d~sN8n&6G;It<L&2@5XY
zFmSrkwI=#-)czL1FGdF{y(1K^DX8b_l<a&iaZL3k=dQrj5#NHCO@*aP8zq)!daa8N
zo1UwoyYqrV$+UR=wa=N}EX(fRP|R{zVa4;AUK=&_BARDz;lA6XyL{ooE5Z6nRhEU@
zs<(*?Zq*9CxZwNlI;lgy6%C{}eNPN{U3uv0GX~`tpIb#KEvLH#^;RsOHNCr0aE-*l
zCa-hcepgO(&g#$Hc<Jt}51XDp3H6Cum~h8p?UHB5q>eg9oODUjP>$a@Tl)L_&>f!d
z@;2{{yPNlK_P2S*W8dp8p3td$WLNoY?N5#|$1<i|@~PBYlXx%ft&Ou_tJ~x7@Y`>f
zUw!tAzkGAy_41OfJFS!YU6T{e<udy?yw1C{c6Z(c*T1h1t-3ET_4?G98?KWjU(D=`
zVmaGcm+$;cMOTF5P&5CrLd{ucO00_K-~B!J*o#A<F?)2_YA38XvHDcs!Hh{FU-+LK
zFj>%d$V{>(p*xIk&6C3R&}*N4#jliq%$01PR5-(cFZb9_=EqTyy?iR(l5;NVc?&fc
z3oKPR;B_x)&qMCAC%I~G`I#l(9X_Gf`zv7M9q&w$#|oR~$|O!uwrP~9)O5F-sGNT~
z(B_1pQ(6j7*vUD$7ar6;vg9;zyUn3A@j=orpa0+dj^@8#|2S81$~>F$xQ~SnSF+7q
z9ah%Q$|~8-(y&tYjm!%_0h3MNm!I3|t6yZ;5o1&G&fG!Dw?*v9TdQxk7vH{CmCLbj
zhfQqsrYqCtWO#4e+RA?`Npaz|JJl&74s25cRo?S5+PQiDuUWb+%3JKZ%Gtc1uFLPc
zEcdkFym!lGmFdRY(-aED43r<sEcq{78nv=3DtU%``8HoI&k6hU*5}`~e`g=7YPPdj
zC@1075ijwugKTQ*mOEZ31|D=1*)Wkg=gH|d-f0^Sa^`H{mHx^wJ3;kmca-CnEuBjq
z7_xO;R7yH0_-1;H<MHnv4=SToxGU-cKDfM>nS5(Qjxh5&)2f9s>gFt52hJ>7?!P5&
z*U#kgIWtZyUS1nKKU_;->f;x?9&Ad^S9pK+bv>_<)`f}d-sP3w-TpE!=Sp%PXGP-&
zey+szdmn~z=T2ylX=M)K*~50rXtT*Pjh1xxJwnI14~RGHXK0A-ym>sK^qI{fgGdcW
z!=z1`Tq03&tUvyB>=(b!^K|p$y2^5`i|<cyEXWgeWAM*osktPkEaQ^Pa#^4K&m#7U
zRF+K!Ofpm2^>1^8WU^!>v8>8v*=5djj>qk}?-j4;{A4kY+>pRGap7y;<-NPCC6E_Z
zZ<)kjAIp<u*dc#NfyqVBDC+ed|63~Ec8dJhmLvqO+H>mNtFnz9N0sWNx;tJRs5-u7
zi(t+)C04y&4<94(J-n+0Z*iXzpHjbE!@TR<7O9Eu^OCQukd$Tb39-`7YkYb1y}sDT
z;>eaO_dJfDJo$M|fM;sY^<zg5=n8wv)G~e%jc@XHl>I4Yvnn~wZ1ej=_C28=cZEiX
z))%c7np`&VhI005p~*Q;g%_iJmb&Sz@!~xdtbcn|NoHtOQs}PS&}HXW3pjZ^WIZLo
znl`cWl#Gj?Ui$n%`)>#KM%+kB>~7tv)5H2MCq?h`iKcM19RkA77tC-~m#i*P**@b&
zQc`#4Rv#UO?`OExO&-f^6>E!rQ<SqN&}_wqs_oX_a>}zJdXf$M=AX3axp0#)`9;g~
z0~Hr!G<GC+u^vomNc|t_lViAXvX728bBeF!PnYK!ip?pKJ)L*Mz5CSuYQ7BBy{j9!
z+kfiT*Hc40C;gvj79g_zVw2m#P2Y4<&wS*()Gx+hqt0;R;U^#Wo$sWD=RR5UaN}=j
zWoEydDThD)*}S}(y<W*<n#{V%MLRAWpOGRqDV=ko;;RJ)mLd(2E=%JQew|{P@tnoy
zgId(P*1*`V`N=1ZpY^_2^m)n7C;A_a?>EhO?$T2txkc<y+mYTP&t)Bks`<V?R+V2v
zUh;Eu%@bx-n)r%W{MM`qYZ=ck4ZM3=Z=TO50kQoX6_&a6Op+63|B&Gj;FGl0_XO`}
zMTzXb|C|@T|9SS@<%+JSw7P1pijQK-d7I$7-R^>_8P3bo4#tRx2$dUf-+sMgWqj+G
zmTz<VRs5z#Z)3JzayY-}ldS7a8|LZTX9wIBQ~&?d`qcEYU%gh+J=fG<w>n8qWfq$>
zJ@!qakI8EP+qZWIPCTr4N%(1<{Pvl@SMP4Rw(hFRv^<}$W{Z+yub!XrV8NONf%+u}
zq-!>xO=X){HM_D?z%sGfFs@Q~iN~bmF9(BSv>F<>dwDA^TBlg#AZTrKX1AL3X&xK)
z?K3!8<jv+vvP9Q>m1t>}uzBHn?p2an|FH+=H?z_t)|k(o-f>WPo3ub%VfM_#1Ot|7
zmD5Wfp3GHUrt*08+rM|SX3HndZQnm3KV$K2wpG`zNWbB#lP%_aUacN**k6S8@T{!|
zPw>mL#QY3Q3kvr=ce-h#{?*Xg@0PQ_y7K3f&N&s0vn8h-jYH18?TXd>q<QhFjPQ-x
z)IBxzqIvJ^`)ZE)o|Aq5*Hv-L=63(ct?#lP@(RrF&AdKSICYDq&Wbkf=ruXFwQp~d
znvvBXc+|w=4DXs3t;`~CS9SCrkeDBKbyfSk(8rUH-Mv>I6Mnj<@sgzE{deD7jAo17
zjkwhN`y)f}p^qP1&dcd(up27wm5#Z@SL0S=zGOks`TzsfkIy(hx?a8T>F1(vN#Tqi
zK79UF!lrke@vE2kQQ50kjb!f5h<P0S{Lh2pxbmyIjxp1=@Ra+!)$QI?=DPEO=i5V*
z)b=g+tiS8CK4@Cp@^wXOlbbwe^BkF@`C@~mQTE}9yGrLyoqT4OQ*8B0U-LELhrAz7
zdC2DA+R-2s5hS6(kanigYOBxrv(L7FFK3oKn)&|1$2>O$f4d1BN#8vuMV}41er(N!
z8w!^eXH}h9@nZS?DVc)11rN_{538;EciBSespRqw>4&<?SJf6yW>Q>iFmK{>`@p5~
z2~|Qbr?jvxkoB11&?T-J+%s_x^SqhforNwIZZ}f4zE)S1So3<H^-PtS+xjHaLmB27
zq^UdcZH{8<*M9ZGXHUjy%^qQnV_au7b}aU2C|v8DqT{^z)BU=w=VsfkxncS6_|&o*
zHM5J>@|%pq1Q%Y?a-7FLQL%(ocd^x~O_KAEX0Fi5x}p2)p|uEK<ZRYH$;pY5Q&T5u
z>KV8G^opMOBlFyhlqZ+p#=beaL9ba`s`SNEr=Mrm8P3cPuHIGTqRJ!{Cb#O7rrnp<
zt~z_&Z~1I05K+D1QfIM*r7I=3=0e}xUH9KgNQ>PujoN);QCD92_gG$@rHh0D)BM)W
z@o<~IyG41~#|qUMW?y@I_lg|)<9BEJ-FoM6e%rMZ9(=txAtCVB;;DXWVl9g*oB~4x
z_bimvYcdWzsU!F`xrjqOMs!we!pFUbl%%HyJyTTXQaCP<tkz)hv?sx>x+W&;rO(Re
z{UQgO7Roa?cbyB~vX}k%1w%%Oke;9gCrc8_%+7SRna7@1cG+~`_41Z*zgd;<cO6mD
zV>XVty=Ky~y*foxpDllUSWj!4pFXdv|2ac$6Y-2~3ng0;{T4m)X<ZXM$#90w)+;wz
zjy>Gs@$2rQ)9R(hv0iJA&WQ9mvG`TdbPIRq<)PBe1@|o+;<o(VV%Qyi!FBJ%$h6#J
z0s)hc2E|{{S^2m=@8gks^^M0aJ2`WSPC3goGx?&im7r_hn#GeRdFA~JHqbYj6C3b(
z$%;azC0r%bzOC4@Y;N<qH6nbh{2cTCvIM?r+M&*8xAu}oYs;O#VlzK+F4|(H@^0~4
zyF*tkCky+{UVmBI$WrC;#0kPn?xuY@U2&&QvcH}6`&XgqBG0S++XIDmx6a`$7m-|~
z@>4xK#X{wy7hCOOr&9}h%o4<UYquT~I$G?JzL{sv!hV~ej^%S%S0224(AQk(+p;X~
zHM-}gSzTK*^>t|f&EN`+&u{<pM{JsOl0h~?;kJTs>n1ft#!cEk`{m}ho;+<f{rTmo
z*K2lY6mQ?K*Jv7N?jGAV@yiDc%4a@ZcI(R*`|#V@i8WKgz2&N=^!uL@`*QsDqNTTt
zX6NoN`lx&|{pk7~W&0g%Pli{S+})hcy(`zZ+<eQD+dePv@k+eB{aWzU9FGa@C#R|2
zeEit;-NzY1*D7M>xcz#%qin0k%mc@E^BhmS_%3|ILcav#WU*&Ae;D5l?OPlDTIs3J
gcEi>B+)?aNN5ansHFlhNb@e~PxnB%Hg0&0`0KUqcE&u=k

literal 2204
zcmb2|=3oGW|8HZw^Y2&)?K{8z#bZ4-<_!@wOr8wM4Qxy-Gfz8BKPvNMPRX^GWpBP6
z*uB5bJ9nk4*DF5*Ir~X3l2&WXN~!%?>l(DE_2S2lLzUC_Zo0<(a7Mb1%fTJz6vEH0
zU%h8{T<o$v`-?8-ZmTTbUiH>4_uZ}T`v3P{ta~&4@%z(T{wDulc#%;mIONH4txww?
z-Cp-a^sjGx-Nos9`PLY|?%sJ%`u2v0`EOGMKKI^Sv@!Xt|GRaK$$z(R-pgqH_~Q91
zMjPCCA1{1$cdeUgkpxrZ0Y3|tfEi6^7VUie;md`vo6J{#tX*+;#i{IuueVp;zS|mc
z-n?>8yy?<qQ&)zZTdeD?y`kJThga_P{@DljzTa`sash{AT-!XIHG7}FE*H7{e+irP
zwfmKycO5KaDP42jo^kRmwda8qPdD-1(@c*nvGiQ-xFn8!`|Y#OZ-1#vv)L3lb!q!T
zSwp!7g_KfWjf4L+YqNX~|GM?2IJ~GOblvj^&CYMlt*$mX3wsXiTf!iDgNOZA$5+!0
zd?~qKYxi<8zjSTrw%ouVEub7Nw$Y}F$9eh}@sh=S8(#!4n>O}#F|?<pP0ZeXbt&)C
zN!=VytN-lEwq@Orn<sb3Oz_Lp1$pT`k91-#G)Ufb%{e&jY(S{iN^3(|zd5r1wl#OG
z(FzH9d3fQRRUg)I`K*#Dmbg+VSGm>lA;<BFx@_({R>(Z`Pz~KJQ|+Gev_r@3WaYz7
zDVxB{R>kYKY<JryWBXH6ZLNw?-kdO};^f{(4Pgd8K3ylm-~GDvw_J4H<lFgWx38Xk
zR{wHF<(+RUdYFXWdrIG%PoL7fqvN8+(wU!R)+XLdduuaUBGCJB`1IX(uV!ujdpS1$
zPMLrB?7xz>Vs7u}+-8-ScrA9h^!B-uVpGjqSH)k{*e<G<WBZz?<eW>dW3kl!?TW=t
z-iuhiJZLVAd9cPf_spHSzY97fVt1VCp8j+JzmwLfRf|duW~of5bKvu7z9RT`P4oA>
z!1Ik$?c{cxvfBT$>D0CU*A`Ry4xcETQ9kFs^}4B7FEu7;HXGkcbu_SG59Cl<^Psrz
z{FA1`AIy}0C)@LUFD#gxRl6qUU4T@=8%65}9JYNQSS&sXx!WC@c>Zz6cMG=@Jx3Cz
zp18@zdry6yuvhYy-iFSG?w5UaWu8ah=WYMEjA5ztyxlAQSTL3zKE|W**x#2ob2^8?
zwS$U{at#Y+#oCpg%e6YOv0dgpcfYX0)n$!hhpk0qmb-6X{n(1Rrts&7j83DdBoSRh
zdEH8RU9m}5W>xD;>MAs!5}N$IjYEF%0{MEwsNz_$>n&-w{|a4p@62>kKM*}zV~g6h
z%R(yWn$Aor<U91g*Kn<q>$MGM7F+MW87MSi|GRDG@8Y+IPw(t~XVYP3;FpxjwK{`&
z@m!fT)?Oi74mO!BTHaf6bIU~4+$SAoMf1#F%`-d56{VlWdhwFVq^9YH7o>E(W)`#j
zUK(=Ymo3kSB)LhgHup6v7nS#M=0<GmWV{|#719?h#l)JRwtBhtEB)C2l{fr)KD;=#
zZ{>Gw(auv<C9xGZcU|Xye^r0~cL~uq9@Br%cK+yli{CBwxy%9X*8Ra;)o*#XOKqL#
z@}z@rNzwz;3sYvc8m4R7+<Y|ECXQpDz#mqDJ6tnsdBW1qEq0k4sJK>evag_OR^hY<
z$94Y+?&CbIe*5pIcM=!#y;uUGTR9$_bUom1##eG6isi96d(B<JJwlBdE(*UNoSd%9
z6x!v`>$2dP>jG=Rg0z&9doF9Yd^Jm(lHx7;@xzX!t^4=+u6EcH`S)>;+`pY1NrFep
z6+0LvCQrL&^?tJ1Nw4`T{MVKwEDflfdiUwsMIEk!_B~3AN)q-aN8R8s<MwIfZtmoK
z*0ep*G@v^1=b=yeQ=YnAoEPSOQu(}L)=J4-_MQMM?Yzd9s_*r?eryy`++u#H(Cd?p
z_R1EcW7&_B9!yI-w3)x*-=WzLgjN{8Z)z{_NinX}|8sXm*Y&W4TK}G`Iy5m>=8fRi
zRRtxp1g_6bT4iv`DRdS8ysDe4E-hX4#Ur#TE_9i7cw+~Xt(TzEsh*k3&oCAjS^n1f
zdOdH4c&jc~w20Yq1F;>OC+<9>%pEuLfs@ai=A<yIgEzw0KN0KH6^d3dQ{SktGhI$L
z>)6gKQoP$Y*(N9VZgOnB`up&<^m2~FN`0;}_LD4lUcG5Be0iZb!6t)m%Z}tO))b`!
zM*nq$qE)^rbfzXYT$wW2e@nlUAj|0lpPc(qMVXiG7wyT?D?7dN?sBWGucroh2K*B=
zyPy^4%^kJq)UC}^Qv3W1{$wZ~C>ClE(mTIpYW97@i+<;%<Zk~rG<q<_*KCe`{kM|y
z59B>2J>|LHe6GM#K3PbT^*oc(<REs{$&)#Zl0#mx%Ed==e4f+7dC%pvt<+VykHtEb
z$Mzg7E1hQ|{zrA+vuKIWb9w~zny+=3spL)ZR&tdL{&elglF8xzrGF9=4;F7?5N^F!
zaOGM{4sV5CPnLYy$COF!8=myG8k#0g`CwGYpwFwY)^p8P&!WRM9LHvT{?GJ9*Zyav
z!s}_y()?CiCZ=#HRzI7WC2x}?vViyPtcg22wy5M~ik02ou~NRZg!!$Fe47PdUM72)
zR$Kq3&$0{V+-07=J$>aa?XrKD)2Ha?ewQvaGm4tO#$DAlgfGG)Zc8?Q@}kJtw|U>3
z6@Eu9k)HC~#>aU3^xsKq)|y&J>@w`TeV}XEuexI$>`%o_UiJB<G`r7^Q4?9YeCBkI
ziR?ZG$F%dC4yf$tv5SbBu4M2bEVEIf)OVtAqs52BD3e(cYELXJkM?L(*uV7Auy`JR
z+|lCX!O4+NO8**8UjOXDVjojszH5`uc|Uo;yiD5R@Q$r#3=E7|rd3wIIuv}%%ZKw=
z`0m?(v!=hlZuR}YqP=i$nbe9kg=Q8tA700J?XXa5oK+W5W03RhcEXf)f1!0Xn#RA@
j&6-gs)>Hd(ch=*dUyhV#-LvsF`f2Yh)?1_$#J~UmVAwJP

-- 
GitLab