From 7994c06bcd726b7b1534577e187a8520a878ee52 Mon Sep 17 00:00:00 2001 From: Martin Clochard Date: Fri, 4 Sep 2015 11:27:28 +0200 Subject: [PATCH] (wip) example: formalization of Why3 term API --- examples/in_progress/why3_logic/term.mlw | 183 +++++++++++++++++- .../why3_logic/term/why3session.xml | 2 +- .../in_progress/why3_logic/term/why3shapes.gz | Bin 1362 -> 1363 bytes examples/in_progress/why3_logic/ty.mlw | 2 +- .../in_progress/why3_logic/ty/why3session.xml | 6 +- .../in_progress/why3_logic/ty/why3shapes.gz | Bin 997 -> 952 bytes 6 files changed, 180 insertions(+), 13 deletions(-) diff --git a/examples/in_progress/why3_logic/term.mlw b/examples/in_progress/why3_logic/term.mlw index ffa323653..0e3ebb2b6 100644 --- a/examples/in_progress/why3_logic/term.mlw +++ b/examples/in_progress/why3_logic/term.mlw @@ -264,7 +264,7 @@ module Term function ct_d (t_ctx 'vs) : term -> bool function ct_m (t_ctx 'vs) : term -> D.term 'vs axiom t_ctx_inv : forall c,x:'vs. c.ct_vs.c_ldom x -> - ty_vars_in c.ct_ty.cty_tv.c_ldom c.ct_ty.cty_sym.d_tys (c.ct_vty x) + ty_vars_in c.ct_ty.cty_tv.c_ldom c.ct_ty.cty_sym.d_tys (c.ct_vty x) function ct_tv (ct:t_ctx 'vs) : context ident_name int = ct.ct_ty.cty_tv function ct_sym (ct:t_ctx 'vs) : sym_ctx = ct.ct_ty.cty_sym @@ -287,6 +287,11 @@ module Term function ctp_mty (ctp:pat_ctx) : pattern -> D.ty = \p. ctp.ct_ty.cty_m p.pat_ty + (* Type of variable symbols in contexts. *) + val ghost ct_vs_tys (ct:t_ctx 'vs) (vs:vsymbol) : unit + requires { ct.ct_vs.c_pdom vs.vs_idn } + ensures { ct.ct_ty.cty_d vs.vs_ty } + ensures { ct.ct_vty (ct.ct_vs.c_ptl vs.vs_idn) = ct.ct_ty.cty_m vs.vs_ty } (* Contexts bounds. *) val ghost ct_ubounds (ct:t_ctx 'vs) : unit ensures { subset ct.ct_vs.c_pdom ids.ids } @@ -551,6 +556,10 @@ module Term type trigger = list (list term) + predicate br_ty_are (ct:t_ctx 'vs) (bty:D.ty) (oty:D.ty) (tbr:term_branch) = + ct.ct_ty.cty_m tbr.tbr_bty = bty /\ + ct.ct_ty.cty_m tbr.tbr_ty = oty + (* Binding predicates. *) predicate bound_env (x:vsymbol) (c:t_ctx unit) = c.ct_vs.c_ldom = all /\ @@ -611,6 +620,7 @@ module Term ensures { co.ctb_d result } ensures { co.ctb_m result = ct.ct_m t } ensures { co.ct_ty.cty_m result.tb_ty = ct.ct_mty t } + ensures { ct.ct_ty.cty_d vs.vs_ty } ensures { co.ct_ty.cty_m result.tb_bty = ct.ct_ty.cty_m vs.vs_ty = ct.ct_vty (ct.ct_vs.c_ptl vs.vs_idn) } @@ -650,6 +660,7 @@ module Term let vs = r.tbo_vs in let cb = r.tbo_cb in cn.ct_d t /\ fused ct cb cn /\ bound_env vs cb /\ cn.ct_m t = ct.ctb_m tb /\ cn.ct_mty t = ct.ct_ty.cty_m tb.tb_ty /\ + cn.ct_ty.cty_d vs.vs_ty /\ cn.ct_ty.cty_m vs.vs_ty = cn.ct_vty (cn.ct_vs.c_ptl vs.vs_idn) = ct.ct_ty.cty_m tb.tb_bty } @@ -688,23 +699,179 @@ module Term ct.ctq_m tq = D.TImplies (trigger cn tr) (cn.ct_m t) /\ tq.tq_qty = map vs_ty vsl /\ vsl <> Nil /\ cn.ct_ty.cty_m t.t_ty = ty_prop } - (* + val t_node (ghost ct:t_ctx 'vs) (t:term) : term_node requires { ct.ct_d t } returns { Tvar vs -> ct.ct_m t = D.TVar (ct.ct_vs.c_ptl vs.vs_idn) /\ ct.ct_vs.c_pdom vs.vs_idn /\ + ct.ct_ty.cty_d vs.vs_ty /\ ct.ct_mty t = ct.ct_ty.cty_m vs.vs_ty - = ct.ct_vty (ct.ct_vs.ct_ptl vs.vs_idn) + = ct.ct_vty (ct.ct_vs.c_ptl vs.vs_idn) | Tconst cst -> ct.ct_m t = D.TApp cst.cst_m Nil Nil /\ ct.ct_mty t = ty_ret global_sig.sig_m cst.cst_m Nil - | Tapp f tyl tl -> for_all ct.ct_d tl /\ + | Tapp f tyl tl -> for_all ct.ct_d tl /\ ct.ct_sym.d_ls f.ls_m /\ ct.ct_m t = D.TApp f.ls_m tyl (map ct.ct_m tl) /\ - ct.ct_mty t = ty_subst_ret f.ls_args tyl /\ - map ct.ct_mty tl = ty_subst_args f.ls_ret tyl + ct.ct_mty t = ty_subst_ret tyl f.ls_ret /\ + map ct.ct_mty tl = ty_subst_args tyl f.ls_args | Tif b th el -> ct.ct_d b /\ ct.ct_d th /\ ct.ct_d el /\ ct.ct_m t = D.TIf (ct.ct_m b) (ct.ct_m th) (ct.ct_m el) /\ - ct.ct_mty b = ty_prop /\ ct.ct_mty th = ct.ct_mty - }*) + ct.ct_mty b = ty_prop /\ ct.ct_mty th = ct.ct_mty el = ct.ct_mty t + | Tlet u v -> ct.ct_d u /\ ct.ctb_d v /\ + ct.ct_m t = D.TLet (ct.ct_m u) (ct.ctb_m v) /\ + ct.ct_ty.cty_m v.tb_bty = ct.ct_mty u /\ + ct.ct_ty.cty_m v.tb_ty = ct.ct_mty t + | Tcase u brl -> ct.ct_d u /\ for_all ct.ctbr_d brl /\ + for_all (br_ty_are ct (ct.ct_mty u) (ct.ct_mty t)) brl /\ + ct.ct_m t = D.TCase (ct.ct_m u) (map ct.ctbr_m brl) + | Teps u -> ct.ctb_d u /\ ct.ct_m t = D.TEps (ct.ct_mty t) (ct.ctb_m u) /\ + ct.ct_ty.cty_m u.tb_bty = ct.ct_mty t /\ + ct.ct_ty.cty_m u.tb_ty = ty_prop + | Tquant q tq -> ct.ctq_d tq /\ ct.ct_mty t = ty_prop /\ + tq.tq_qty <> Nil /\ let tyl = map ct.ct_ty.cty_m tq.tq_qty in + match q with + | Tforall -> ct.ct_m t = D.TForall tyl (ct.ctq_m tq) + | Texists -> ct.ct_m t = D.TExists tyl (ct.ctq_m tq) + end + | Tbinop bp a b -> ct.ct_d a /\ ct.ct_d b /\ + ct.ct_mty a = ct.ct_mty b = ct.ct_mty t = ty_prop /\ + let tm = ct.ct_m t in let am = ct.ct_m a in let bm = ct.ct_m b in + match bp with + | Tand -> tm = D.TAnd am bm + | Tor -> tm = D.TOr am bm + | Timplies -> tm = D.TImplies am bm + | Tiff -> tm = D.TIff am bm + end + | Tnot u -> ct.ct_d u /\ ct.ct_mty t = ct.ct_mty u = ty_prop /\ + ct.ct_m t = D.TNot (ct.ct_m u) + | Ttrue -> ct.ct_m t = D.TTrue /\ ct.ct_mty t = ty_prop + | Tfalse -> ct.ct_m t = D.TFalse /\ ct.ct_mty t = ty_prop + } + + val t_var (ghost ct:t_ctx 'vs) (vs:vsymbol) : term + requires { ct.ct_vs.c_pdom vs.vs_idn } + ensures { ct.ct_d result } + ensures { ct.ct_m result = D.TVar (ct.ct_vs.c_ptl vs.vs_idn) } + ensures { ct.ct_ty.cty_d vs.vs_ty } + ensures { ct.ct_mty result = ct.ct_ty.cty_m vs.vs_ty + = ct.ct_vty (ct.ct_vs.c_ptl vs.vs_idn) } + + val t_const (ghost ct:t_ctx 'vs) (cst:const) : term + ensures { ct.ct_d result /\ ct.ct_m result = D.TApp cst.cst_m Nil Nil } + ensures { ct.ct_mty result = ty_ret global_sig.sig_m cst.cst_m Nil } + + val t_app (ghost ct:t_ctx 'vs) (ls:lsymbol) (ghost tyl:list D.ty) + (tl:list term) (tyo:option ty) : term + requires { for_all ct.ct_d tl /\ ct.ct_sym.d_ls ls.ls_m } + requires { map ct.ct_mty tl = ty_subst_args tyl ls.ls_args } + requires { match tyo with + | None -> ty_subst_ret tyl ls.ls_ret = ty_prop + | Some u -> ty_subst_ret tyl ls.ls_ret = ct.ct_ty.cty_m u + end } + ensures { ct.ct_d result } + ensures { ct.ct_m result = D.TApp ls.ls_m tyl (map ct.ct_m tl) } + ensures { ct.ct_mty result = ty_subst_ret tyl ls.ls_ret } + + val t_if (ghost ct:t_ctx 'vs) (b:term) (th:term) (el:term) : term + requires { ct.ct_d b /\ ct.ct_d th /\ ct.ct_d el } + requires { ct.ct_mty th = ct.ct_mty el /\ ct.ct_mty b = ty_prop } + ensures { ct.ct_d result } + ensures { ct.ct_m result = D.TIf (ct.ct_m b) (ct.ct_m th) (ct.ct_m el) } + ensures { ct.ct_mty result = ct.ct_mty th } + + val t_let (ghost ct:t_ctx 'vs) (u:term) (v:term_bound) : term + requires { ct.ct_d u /\ ct.ctb_d v } + requires { ct.ct_ty.cty_m v.tb_bty = ct.ct_mty u } + ensures { ct.ct_d result } + ensures { ct.ct_m result = D.TLet (ct.ct_m u) (ct.ctb_m v) } + ensures { ct.ct_mty result = ct.ct_ty.cty_m v.tb_ty } + + val t_case (ghost ct:t_ctx 'vs) (ghost oty:D.ty) + (u:term) (brl:list term_branch) : term + requires { ct.ct_d u /\ for_all ct.ctbr_d brl } + requires { for_all (br_ty_are ct (ct.ct_mty u) oty) brl } + ensures { ct.ct_d result } + ensures { ct.ct_m result = D.TCase (ct.ct_m u) (map ct.ctbr_m brl) } + ensures { ct.ct_mty result = oty } + + val t_eps (ghost ct:t_ctx 'vs) (u:term_bound) : term + requires { ct.ctb_d u /\ ct.ct_ty.cty_m u.tb_ty = ty_prop } + ensures { ct.ct_d result } + ensures { ct.ct_m result = D.TEps (ct.ct_mty result) (ct.ctb_m u) } + ensures { ct.ct_mty result = ct.ct_ty.cty_m u.tb_bty } + + val t_quant (ghost ct:t_ctx 'vs) (q:quant) (tq:term_quant) : term + requires { ct.ctq_d tq } + ensures { ct.ct_d result } + ensures { let tyl = map ct.ct_ty.cty_m tq.tq_qty in + match q with + | Tforall -> ct.ct_m result = D.TForall tyl (ct.ctq_m tq) + | Texists -> ct.ct_m result = D.TExists tyl (ct.ctq_m tq) + end } + ensures { ct.ct_mty result = ty_prop } + + val t_forall (ghost ct:t_ctx 'vs) (tq:term_quant) : term + requires { ct.ctq_d tq } + ensures { ct.ct_d result } + ensures { let tyl = map ct.ct_ty.cty_m tq.tq_qty in + ct.ct_m result = D.TForall tyl (ct.ctq_m tq) } + ensures { ct.ct_mty result = ty_prop } + + val t_exists (ghost ct:t_ctx 'vs) (tq:term_quant) : term + requires { ct.ctq_d tq } + ensures { ct.ct_d result } + ensures { let tyl = map ct.ct_ty.cty_m tq.tq_qty in + ct.ct_m result = D.TExists tyl (ct.ctq_m tq) } + ensures { ct.ct_mty result = ty_prop } + + val t_binary (ghost ct:t_ctx 'vs) (bp:binop) (a b:term) : term + requires { ct.ct_d a /\ ct.ct_d b } + requires { ct.ct_mty a = ty_prop = ct.ct_mty b } + ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop } + ensures { + let am = ct.ct_m a in let bm = ct.ct_m b in let rm = ct.ct_m result in + match bp with + | Tand -> rm = D.TAnd am bm + | Tor -> rm = D.TOr am bm + | Timplies -> rm = D.TImplies am bm + | Tiff -> rm = D.TIff am bm + end } + + val t_and (ghost ct:t_ctx 'vs) (a b:term) : term + requires { ct.ct_d a /\ ct.ct_d b } + requires { ct.ct_mty a = ty_prop = ct.ct_mty b } + ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop } + ensures { ct.ct_m result = D.TAnd (ct.ct_m a) (ct.ct_m b) } + + val t_or (ghost ct:t_ctx 'vs) (a b:term) : term + requires { ct.ct_d a /\ ct.ct_d b } + requires { ct.ct_mty a = ty_prop = ct.ct_mty b } + ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop } + ensures { ct.ct_m result = D.TOr (ct.ct_m a) (ct.ct_m b) } + + val t_implies (ghost ct:t_ctx 'vs) (a b:term) : term + requires { ct.ct_d a /\ ct.ct_d b } + requires { ct.ct_mty a = ty_prop = ct.ct_mty b } + ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop } + ensures { ct.ct_m result = D.TImplies (ct.ct_m a) (ct.ct_m b) } + + val t_iff (ghost ct:t_ctx 'vs) (a b:term) : term + requires { ct.ct_d a /\ ct.ct_d b } + requires { ct.ct_mty a = ty_prop = ct.ct_mty b } + ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop } + ensures { ct.ct_m result = D.TIff (ct.ct_m a) (ct.ct_m b) } + + val t_not (ghost ct:t_ctx 'vs) (a:term) : term + requires { ct.ct_d a /\ ct.ct_mty a = ty_prop } + ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop } + ensures { ct.ct_m result = D.TNot (ct.ct_m a) } + + val t_true (ghost ct:t_ctx 'vs) : term + ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop } + ensures { ct.ct_m result = D.TTrue } + + val t_false (ghost ct:t_ctx 'vs) : term + ensures { ct.ct_d result /\ ct.ct_mty result = ty_prop } + ensures { ct.ct_m result = D.TFalse } end diff --git a/examples/in_progress/why3_logic/term/why3session.xml b/examples/in_progress/why3_logic/term/why3session.xml index 0d6fc7f64..720c8b5cd 100644 --- a/examples/in_progress/why3_logic/term/why3session.xml +++ b/examples/in_progress/why3_logic/term/why3session.xml @@ -9,7 +9,7 @@ - + diff --git a/examples/in_progress/why3_logic/term/why3shapes.gz b/examples/in_progress/why3_logic/term/why3shapes.gz index 513ee53d37b177ed87e377b33cf14b1834bad399..e15287a322b4f137edce3673d82286b15b46aa81 100644 GIT binary patch literal 1363 zcmV-Z1+4lXiwFP!00000|Lt1aZW}oaeeYM~6G&Ys@nL~20t5)KXkQldYDl8A>uxTE z?WWzoUydE8@omQ4jZq|PAi-!X4u?FXjwp@5gP0852(1knEfn$zumCwjQ7*d6i*`S| zXkX@4Ch2C8o?0Dr*qQ6q538H^?R}cwwduEuUmmZ&rZTx%eC~X@n$`KAUFc}9h}_?P zmr1|RzSQdvd*nVZZaUx5TJX26F4xiZzNdQa+PBnuHDu(+8|k=<112sd#te)rv2F8g z7Y~}JedFe>+(zsWMo~mu>U)yYXSVb?mDxoQVZUQb-Mx~f?}t%-lo*8>ZHHzAXtdit zm@QqZ#O}h3X3z&S?1NoP^gdkfcjHmcZ`jthHaP^L( zsg@HGQ}H%BZ@g()d~G$yC~}eJ^Ez8h@9$phl?@Y63&_bxPV56Ua)8{N1Tofsf907n z&y;zl%rj-a1Z7^o7=L9~D@c+YatX?q91>?%E+gOL zLu#mSH~@}0SSg_zMMlfynh|#q8BeV(m)<&rwY5}jwnWK-F|9-lhFbwCE`}D5NGjWf zz2-l{+0#b2+9z?2Kpz3jkt`R_kgK9kF6y6Q@5p1Z6vmU-u4|2Rh)xqC)(9c{oW%ws zp(ZGhg0tBr4@uIq%JCqG=OCRpNRf+a$(91mHt|I=7>8IT@d~{iBRVgGtOmhbeNoj^dE!dLy4ABvMp1J#&~epZ#HV+8W^m{ zu-Q3GCl6C2>yy=jz-T#}n+_!9H!W+O3#}T7&%-phybD`vr9Jb`=-Muh=;$R5EbR8~ zWt>CYhu9dMt9))wxa!R1D6#`A8PKwD;p2+$-Hn3*P!8NDmRt^s8Z(Gx>5!jQ8OS1W3%NLq^=K|)Vo zNCt+|8%2-7S>T?ntz!-;2eh^@+6<6V@<$QT{}?~(`hge(GO@9SIU6v|A_}x1&Hi9* zF!bqdDYlQQe_CB+#JHL$L(0WeVXQ7zD<*(g@$k~q|LX#W#8z(=5{bmkcwGcR;M`jE zP1*@&_*VrFH$}te6frS^&fb=4!&p715VQ{Z;R)?jAFWU1e_>y3jNtpP8CuOWT~DEN z1X-#pe9YMSVb*V4 zHft!dc(-}BczX9K&A;Ty{O{XIS$yl&XtRTL1K%&ZA79`9x_DUi>J^{c^=WNF-F973 zam%!DS8KyJeD8M*m6O?lkIb=@YPmGYCW@~i literal 1362 zcmV-Y1+DrYiwFP!00000|Lt1ajvF@&ea~0;6G+|lP@usA1{NrimttNGN|aisUOTXz zP5Src__A5wW}J47V7CM8Vl)A%+{Y9OXFo({n_}&ofYB5!*?0_ zefg!_e>fxec|B`vM-z2hz;KhC&`P3SOjBhhDI*oqySr<-um zJn8ERJRX$FVXsNcixSioISSBoZ7c_<+2)q%=M|+$ZX?!l5A)?P&^gxd)2vT zE~9Do8b5ZRX}a-#vTA%tCX^TRb@{fQOy`e{J-juCw~_;SJ$YO;YTv+p1IF)SP(?>V z7hSeG7^|$RiEXJRg}^+b)v7Gl)5ZM7URjaARgaMrCyLg)>I`74hCM57zrS*z%z-io z${Z;3B`EX$#rP|kQh*25P>!Vn1a(W+X$%$`pyLTQ_&h{F>B}hlUVO-jUhz02~m^?VYDf+_KJNW z$UxrcWXJ+BJ*ylqf;a@}#z6`(t4ca&sJgPvoIn}G!afCdwp_tvraJ<=a(#%w#Ta;n zOw}dBCdhokAtr;N1R#eppQwH=GrhxP2-1HHlJz-gN2F_V6qK@Hu-$Bwz*SIKu3@tw zOg9fxb=s1afX;WsI3jq$Z84$s5XxxDj7Yo#;uPVd?-^yp|ME-dWM?qv)i zZbPh;%vCm3!?DQBWn72`FegAAIp%m>@qM~+&;iN`#+N|3mCxE*n<1g)8rdZusaiyb z7Gq(f>6$g$rWES0rd}5?RHGx8B?XLvfXZ@#8ZohV989d;z&ve8`OX3NCXoY`iwoAX z*ClYaDB~#BL=Hm0e8`joc1KmS;w%}L6GblUG+3#cIg-*&<*cuvAai~P```O)Ze0M$ z04v%0SfZ+mlJ?+}amvX66bibcN>2a3NA$-tcyU3Bc!C*l!8(!I;lmjAfcx( zBppNPjiML9XoxLaYZIfVU#jaKvIl(X2eMW(zMp{l6}79P47WK*GVrs;n%6z{gZ; zv6br$X82bHPppE5O%#wKg3R99m5QO*NZv~w^urU{tv*`c$p0K|(IJ3szh+1^Q)NAc z#yCh^Ope!#ogZf1*9MWbQV)XzUD^%0nyoNu4oOH>a>e6qrlwa0lHppj(ge;p$MUbV zWl)L8WN!&ZpBJmOsN?A-m%5JK-4AC-hBG9?8InW$hBG8T`wWQ`2hJMdGOTiuatbJi z7^+q-M7HMeZ1HsdiB@0IWcByMB(J}i9pc758LP>x*} zRLmwV%y@73f$!sYm_y-qJ5*C89ZD7_tgP7yQncXn-sbgk`o|w-Ihih(WmX<(zP_V6 zSrxHUH9@FqCm`cehWq{HJ}s$EAEvWsnbD5FyTyF - ty1.cty_d (result.Mtv.bindings x) } + cty1.cty_d (result.Mtv.bindings x) } (* Failure. *) raises { TypeMismatch _ -> forall f. (forall x. s.Mtv.domain x -> diff --git a/examples/in_progress/why3_logic/ty/why3session.xml b/examples/in_progress/why3_logic/ty/why3session.xml index bd50b6548..71594df2d 100644 --- a/examples/in_progress/why3_logic/ty/why3session.xml +++ b/examples/in_progress/why3_logic/ty/why3session.xml @@ -7,7 +7,7 @@ - + @@ -29,10 +29,10 @@ - + - + diff --git a/examples/in_progress/why3_logic/ty/why3shapes.gz b/examples/in_progress/why3_logic/ty/why3shapes.gz index 0d35003c4de3b23997d11007989861b61b7135da..3253cc0d7c311f93739d35b14035c966549f4d07 100644 GIT binary patch literal 952 zcmV;p14sNHiwFP!00000|Lt1KZrd;ryyq+Y30%H;DA1sQfn3^4p{uccs4<$@jx7gG zzrIrJIF3Y#Qlh#^;hSwPm)zOm?2@pP)FaP1SVc5v3_*a?f~vstpao8{FOz(^o)izW zTP)o5Y_na5{OT*t7y10x0O)vwR)G>>k%$IK6}bNM!G`Rkhxc&Etl?wd1h2xNDDT zZ}B3iy-}#|K7-ODZ#sL*C(xb6&SNCjTl^Vj2jW1rJUrw5JODi@b(G(y$;~xhOV2K< zfJkv=Z*d~B$R1>oNwUZ!S>zD1n2eGRvgn<~5VEKkS=2uu%Mf8<8HH}P94y-1W;;5y zjaQp|xx^tT+B2kv>uP44Zj{!iN28|0K%z;I=r|xvFO*{{7~!}G7>JS@ys%7aX(&kN z^klUTZdq=vm@gL}A|H2Ye0MBE6XYaOikb*&?RXkXnM#CW1!__YqGELK@NK+;K&^jJz}taXH2i!4Y*SE2y<9vO4Px?B&P&q*lR0pqs5Kxt90OP?0fvA*ec^Vo~5Y8>ixkWj*DF1zn zB0PY1LNenNV<5HRfvX(3v6K)y*)G-r-8I^qP-@P6QGB@nD-0rN@?JaAwe~dhG<`6P a$z?l0i9d9(XJLFRHU9u?{g|#!BLD#8;ndUs literal 997 zcmV279@uQ{rYg`Z%J$cH#x?kY6uk2b6yoD?YCF`-Jb>o6 z)%6Zq-PN;YclPmryI7Ws<=0KY3fX(0DOWf3-_4l$vfldlJwUxqgSod*gS)zlAZth& zTUZr(H)(M710cQn9#=2!e{9Y5;^AgynAaBZV>tE}@gS%c|%1L)iRn#*ZncvJ8CyRp>ty1J=?lZ(oRU&?IR*1 zKX69*gqRQRZipsNaWti%K&MEks84+(63X|8355VGc8X&!Uqq8u26A7@a3V8vCJ|Lx zA{u-9kFcqdY^q!~)u}`jmG}9<$I<-!{_cGS%j? zdveH-&O}lUfLxz<9^KTrSG*%^>J*!iOX6Y8Y%WYkG!yoSDVj-Qnn_;1X1+YDbSBLd zS(@2@uL6w>*=RzCNUCqAe;j8&M{3q5!8dT!5Z+K4;s&LJ-D2fFQ?__60OT= z`M*CcD<)m(X-TZ1ObFB{lr4o)P>P`Rz#ZT-NYTZn1CqWWa zN*QGWv6dTetz?GJw#&6Q?whgKzE;J>vifhoKAO}T$?J>BQu`YELg(ZpCg{UNCO+e0 T(?8>SYD@e9v104PlqUcHcoFJR -- GitLab