From dfa620fa83e44a1c502f473a196a327ffb080ac8 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 22 Apr 2026 11:21:11 -0700 Subject: [PATCH 1/3] Update CI to TLAPS 1.6.0-pre and adapt proofs accordingly Bump tlapm from v1.4.5 to 1.6.0-pre: fetch CommunityModules and tlapm on each run (the bundled TLAPS.tla and CommunityModules.jar were present to make the repo self-contained (drop actions/cache and the .bin installer). Adapt BlockingQueueFair.tla to the new toolchain: * Switch from CommunityModules' SequencesExtTheorems to TLAPS' SequenceTheorems. TailTransitivityIsInjective and AppendTransitivityIsInjective have graduated in TLAPM as TailInjectiveSeq and AppendInjectiveSeq; see tlaplus/CommunityModules@9017c0d. * Strengthen TypeInv with `buffer \in Seq(Producers)`. See also lemmy/lets-prove-blocking-queue@f5c7db2. * Decompose the Wait branches of the refinement proof (`Spec => BQS!Spec`). Signed-off-by: Markus Alexander Kuppe --- .github/workflows/main.yml | 18 +-- BlockingQueueFair.tla | 32 ++-- CommunityModules.jar | Bin 27793 -> 0 bytes TLAPS.tla | 311 ------------------------------------- 4 files changed, 28 insertions(+), 333 deletions(-) delete mode 100644 CommunityModules.jar delete mode 100644 TLAPS.tla diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 5e44c46..f290eb3 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -9,24 +9,16 @@ jobs: steps: - uses: actions/checkout@v1 - # Do not download and install TLAPS over and over again. - - uses: actions/cache@v1 - id: cache - with: - path: tlaps/ - key: tlaps1.4.5 + - name: Get CommunityModules + run: wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules.jar - name: Extract CommunityModules for TLAPS run: unzip CommunityModules.jar -d CommunityModules/ - name: Get TLAPS - if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above - run: wget https://github.com/tlaplus/tlapm/releases/download/v1.4.5/tlaps-1.4.5-x86_64-linux-gnu-inst.bin + run: wget https://github.com/tlaplus/tlapm/releases/download/1.6.0-pre/tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz - name: Install TLAPS - if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above - run: | - chmod +x tlaps-1.4.5-x86_64-linux-gnu-inst.bin - ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin -d tlaps + run: tar -xzf tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz - name: Run TLAPS - run: tlaps/bin/tlapm --cleanfp -I tlaps/ -I CommunityModules/ BlockingQueue.tla BlockingQueueSplit.tla BlockingQueueFair.tla + run: tlapm/bin/tlapm --cleanfp -I CommunityModules/ BlockingQueue.tla BlockingQueueSplit.tla BlockingQueueFair.tla - name: Get (nightly) TLC run: wget https://nightly.tlapl.us/dist/tla2tools.jar - name: Run TLC diff --git a/BlockingQueueFair.tla b/BlockingQueueFair.tla index 4c6fc6e..e137251 100644 --- a/BlockingQueueFair.tla +++ b/BlockingQueueFair.tla @@ -1,5 +1,5 @@ ------------------------- MODULE BlockingQueueFair ------------------------- -EXTENDS Naturals, Sequences, FiniteSets, Functions, SequencesExt, SequencesExtTheorems +EXTENDS Naturals, Sequences, FiniteSets, Functions, SequencesExt, SequenceTheorems CONSTANTS Producers, (* the (nonempty) set of producers *) Consumers, (* the (nonempty) set of consumers *) @@ -85,7 +85,8 @@ BQSStarvation == BQS!A!Starvation THEOREM FairSpec => BQSStarvation ----------------------------------------------------------------------------- -TypeInv == /\ Len(buffer) \in 0..BufCapacity +TypeInv == /\ buffer \in Seq(Producers) + /\ Len(buffer) \in 0..BufCapacity \* Producers /\ waitSeqP \in Seq(Producers) /\ IsInjective(waitSeqP) \* no duplicates (thread is either asleep or not)! @@ -112,13 +113,13 @@ THEOREM ITypeInv == Spec => []TypeInv /\ buffer' = Append(buffer, p) /\ NotifyOther(waitSeqC) /\ UNCHANGED waitSeqP - BY <3>1, <2>1, TailTransitivityIsInjective + BY <3>1, <2>1, TailInjectiveSeq DEF NotifyOther, IsInjective <3>2. CASE /\ Len(buffer) = BufCapacity /\ Wait(waitSeqP, p) /\ UNCHANGED waitSeqC \* Put below so TLAPS knows about t \notin Range(waitSeqP) - BY <3>2, <2>1, AppendTransitivityIsInjective + BY <3>2, <2>1, AppendInjectiveSeq DEF Wait, IsInjective, Put <3>3. QED BY <2>1, <3>1, <3>2 DEF Put @@ -129,13 +130,13 @@ THEOREM ITypeInv == Spec => []TypeInv /\ buffer' = Tail(buffer) /\ NotifyOther(waitSeqP) /\ UNCHANGED waitSeqC - BY <3>1, <2>2, TailTransitivityIsInjective + BY <3>1, <2>2, TailInjectiveSeq, HeadTailProperties DEF NotifyOther, IsInjective <3>2. CASE /\ buffer = <<>> /\ Wait(waitSeqC, c) /\ UNCHANGED waitSeqP \* Get below so TLAPS knows about t \notin Range(waitSeqC) - BY <3>2, <2>2, AppendTransitivityIsInjective + BY <3>2, <2>2, AppendInjectiveSeq DEF Wait, IsInjective, Get <3>3. QED BY <2>2, <3>1, <3>2 DEF Get @@ -193,8 +194,14 @@ THEOREM Spec => BQS!Spec <3>2. CASE /\ Len(buffer) = BufCapacity /\ Wait(waitSeqP, p) /\ UNCHANGED waitSeqC - BY <2>1, <3>2 - DEF Wait, BQS!Next, BQS!vars, BQS!Put, BQS!Wait + <4>1. waitSeqP \in Seq(Producers) /\ waitSeqP' = Append(waitSeqP, p) + BY <3>2 DEF Wait, TypeInv + <4>2. Range(Append(waitSeqP, p)) = Range(waitSeqP) \cup {p} + BY <4>1, AppendProperties + <4>3. BQS!Put(p, p) + BY <2>1, <3>2, <4>1, <4>2 DEF Put, Wait, BQS!Put, BQS!Wait + <4>. QED + BY <2>1, <3>2, <4>3 DEF BQS!Next, BQS!vars, Wait <3>3. QED BY <2>1, <3>1, <3>2 DEF Put <2>2. ASSUME NEW c \in Consumers, @@ -217,7 +224,14 @@ THEOREM Spec => BQS!Spec <3>2. CASE /\ buffer = <<>> /\ Wait(waitSeqC, c) /\ UNCHANGED waitSeqP - BY <2>2, <3>2 DEF Wait, BQS!Next, BQS!vars, BQS!Get, BQS!Wait + <4>1. waitSeqC \in Seq(Consumers) /\ waitSeqC' = Append(waitSeqC, c) + BY <3>2 DEF Wait, TypeInv + <4>2. Range(Append(waitSeqC, c)) = Range(waitSeqC) \cup {c} + BY <4>1, AppendProperties + <4>3. BQS!Get(c) + BY <2>2, <3>2, <4>1, <4>2 DEF Get, Wait, BQS!Get, BQS!Wait + <4>. QED + BY <2>2, <3>2, <4>3 DEF BQS!Next, BQS!vars, Wait <3>3. QED BY <2>2, <3>1, <3>2 DEF Get <2>3. CASE UNCHANGED vars diff --git a/CommunityModules.jar b/CommunityModules.jar deleted file mode 100644 index 1476eb32008cc70c73834176eea5ac197dab1cf2..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 27793 zcmZsCb8siowsowDZQFJxw)2Z^+qUhAZQHhOV`4iK&6oS`yZ3wQI{imi?W#UqXZ1d7 zud}v-G$cCpn<@EWJQ$)=_KXE7``TefE4~S6bgv!J9KL|Zb0ih z+~oU4{l5PlDk~@_DJBX~rk53ake!;8k*1@chm)qGo|&3$RAO9W**kKa5=M5Qm5`Z{ zPyvbrCWC`}l<{cKic&(6RsuL@Q&*$XKEXatJ;64^p|RptN;#nh(nLusIYqgk@;)R! zv3j(-xBq)GK>snB|1xbL@b3p_Ya?ccf6e!Qhamhb#Lm^k(b2-##OdF`|NJ;eiHTi3 zU?8AD5FjAj{~au3;p}GNWI}IbZQ$fotu!kQB8d7mqO-lV!YsWw;k&g2|6{%ysw#<) z5*fdv`r4f2qUv(yoQ(Sk5)Di=?92bF?9>7g`IIPQf7;7#$D80LGd*s$)eWeWlM!iD z6l{04E32A`4 zkM{1m2YF`Yi7&DsW~adzyZ8-AF&l~A=xFOTW-K%vB)SQz)va1ToM15@6lm)QHKS>#)5;8`U5 zPX7~#c<4P3;uZUl*-<8>A9o-~L|qC)QMU(TU0@7wNRetB2k>3wV4)nhJ2>E7l6~34 zst5F652nC&NO!7TvO}A9@JI$-0Ma7zU)$4uJ7fpj?s5Jv5c6?|AUhNX*j@bo2w=B@ zJs-lr-f67_&N|jiZH1aC$hk1Sj0S$9@5iPoyve>lkPuV zw&TyNgDSDQJ~B+ODRm=Cpxv9z1zg$+udWG2B9i z?iBSx)ZJmmBscjId5BP|wB2myhJ$~T5P(m@Z-?v~KyoTZ5ooYN*__hd6qSiE>~mTu zLbI;|vN8x1Mo?omhcSgU@ z$|OC!8?yAb2_!jrHQrN09#^ozMioS~@Yza(W-@2swIk;Q;$Wq!;u_?}k6}cj)2aQ& z4KlV;cv?eO0g!HmwFST5IrO}sc)v>Sye9|CAF_b_q}g|BBiw&*7Z|{3yPvd5LBOcS zx5OscjlX+E?&}9XsR-Cra_W@ z!1va=irP3ry#@vI9}ofiCEl8SgxtJW2KVk0LHmvJgM9!7dT;BZ67i(OI2u}zp*Q38 zp*ly1S6`uy{56iJos!mx_IF`TG33$g^^oi;>w;S)+WTKov3LP6Mu09#qW#&XRO$xwJkzUn@v z;Blw1ujEMWw9+C<=rFO@MAt1cUPHc-nt;L=0-{4xZA;re-_Ds~KTZKpTqj?DkdesZ zQC+BXVyd%93*H?{M3CR?yN;_MOI=f0m=c-Id0k$V#Bli3u6aNju7mSSwf;uJ$RtDL z*i0xUd)Z7mQsl7_h)a+jwTT2)O_d6t?wExa!bocZPfj}9DPk8FAsTL8nz}456Vko_ zet-}GLCqL73vCZfx^>-D{RF1a(IqnqrA_#PbK6Xlxfg3tWn8VMjQ8LeYCHgyQpIiK z;B2~!aZ2t{c_pfXC*DlCw&V$~-W|+~YU2$`%2}QuY-o8DPMD+Q*N-sc<&6TI=gIhr ztHcddqW4La(MI|Fg@$MrT{}etzsa_4ftMu@#b{1mG}dJg!KtJ9PYr=ucxlx?I1Uy^ zC10Nn3AB27d^XBM-jPYp(&xZ=uvp76Su&$`&RjjdD=MHFdR29gDI!v8_>9{k#(FdQJx?5fILyRf_A^|Mvu+zFvv(6&X{B+B4k2Y& zf?s?pt3{jKw51HSaF52%1tEH0OIG`&>;if}9>0oqfw9>DlVwlM^8VX{ zy<~{}grTR>sqzHDabKrVZZL3XRPGB`rF(S!9Ke2~R8S~Tu&%Kr>VfJ)hYDuUN~;mJ z40a?t50BlOfy<|PpLnMYTA>DSa6vjn`QieV{#PK?Mj$znc%1FUbT& zc$+28dJaY>TilsDFy2_z9Y~ZENklQ{+Vv&i6X%vv=Z=_^H^Lgk(gw~NNr7AHjC@Ju zn1k$#?5C=dag)1kG(uA@;zk?h4gz;( z8_E?uiyh=GX9qR2;W}$4R>xYlXhQOYH{{EW{>i6EwYOQ3s!MF?k zv=Y9MQum_}8|bM4xFbh&wyovd=M0B7g+&ea82xNXP3GQ6Oj=9h{c4NAq~ zhTK{Th5wd}K}XKsou8F3U(%X0@@hy;>n4tne9NXT$o#M8=tFKHrdS-P5l+t}3M8ir zbooi1`68RKAJn~&KJ!t_*y^M|4yv7I_#2xzuB%lC=d|N z|7N^WPIk7WO#kFn*@;?qivoxtv*fYaMf7aR3ktRY8SMMV$cnm=@rn8s$wPvYFhV{C zMhr1QR%$Icdl+}H5>P}-YNWoXhArB}MLqt;xh%PCEV|Q|tv9&{z+3&ANIy6MeX!_1 zP*X^Amg`9OvyvZ_=q1`Ij}k*0LTO-eO#i0jb`-+za%`K=diN(O57oYaI8AN;l0?nG zm;W<|z{e8JYhXK15f<2=>C+#-Zo%~Xrage*?aU|Cy7(CLJsBmntuBv~@0gZ;+)In&Jnwq0(x-N)M&pSAHlFrT!}?oO{1N;A7mgxMT5a^$jjmyL+{g->B?Uz8-xzhv0tC z9Hj}nd2_8H6BH)vN^bC4QLJ#&X456?=M!XiYNO{3tH$ zeUgY?LNOF#ZXbLvDnH?a?$7l&h2(23%D7ksvME_b66Mk~ilq{D!YTQB3G?32epJz!iQ=@+$% zCa@ea{}B9lb*gk@HX7ENggp<18b6jU;xhcp9BJ)}i3QGR0W0 zD>4!RpAa)~$y{;{k&j4HS{Jz#5K4=Q!&4RuOf0|Ko&pz(bArIJj>+jH&M9enE~Mrp z3*9Wd|5PH(Ue_57Cq!%J@l|Wim{z{vL0Sy{jI3pS|huPw^fmv-fAtr@)TpPL*Bg}jG{|jIzH50f{dDj-c;7sf_EXAx~Oa|c+^Bt zgA1RqHj*0`AfZyGJ-l30-WEyjfs_YhF`>LAkrMbN4I`^sA5&7ME=SM60Z_>hTkLMj zu2}PA6)t8e(=1w&U;&snD%0j^dQ<}D$*1f}SSC+tA(GBb>|0n*Bv?9e;}nBfPpBU| z9Jd61hG4IcEs=uu3QfZ_Q?ja=G=soQ15SBEG@&)cSuKY)Nj!-SNTG_O2IuV^srrws zwj}IZM};5&N%hhw^_2O`tLf2TTA(~n5))9)*2%VtM)Y*NoT$)`q=);b>{h9HHCuSB zp^5wI$>2-Y5~4}_f<{K1NITd}sp5t8MYglcTG56)G48y$%*X*dGe;LBckF5pSh zejC{B)McqK9vJW;_smf8zO@;#a{~#dEhQ}ltva6xcXJb{=08BE5FaFJ&+KHq#8CWV zwr${GLuDdo9*k6{OZ?tkuKLDdQ|32a+v!a!@ zyGA98sLQj6+XjU;#WjjrQm)H$pbQ|lDg z13(aYJZ%xUd3Lw{r9C0aHFQ*NT&2UFjuL}|rkOV{)D^-wZBQzPu^@_lo%~0GqP-dW zXMnurl30{G6Wz)!B7y_KPs!WdgVPnb{Z}T^yBQ_o6j*VP5(1Y{6xnAABXMay(n46CLrmm;*Kn*Bx2vU##5r9nn9C>9EK z>imiM7*rT(j-|rpG-$oIPSbdn{m^gEkU-1I%n>a zZ^)GKY1ARl;k)h)S#?0FYY!YZiE=LU)G*^w8w?&yg+EQuV*2eWX`!rRs-FP0A)VCo z@zWhD;BBvO1kWwhNV6#sM2ohANUmhQZ=M6@MJ&xJ(dDs;qLg#DSd5pfoXNU%^D9|9 zH0fjHwAf%8d?-m{0?gR3^QJ-WfZ=ind;`M!bC_MjR!<|YyqnoJ$fH^TX^gFyZey~U zCm4-HC<1C{f;9!t;Xkh8kFjHjS=De&;^p;VORe7$uM~UyPyyx=wr|bY!&Lc-iApe6 zOXe6?E4NVi%ePp#3+4z2XWSjSg&Yc{VjPI2fyaPD9}D@H4%n^jN3j@N)Sq?*nXDb@ zw)5t-j9x6;85lTNi=ip=##ujj2GTjhpDjl^F?U5%y(g(ft*Bj&0T4ZlbKbhF^HU9Rr5_18*g8Rv*C|271IVQsZGP%V>UHuWQa_0Ggg<(%WB z|3fb2<_JqwxpLv~6`1hQfMQ%XMM#*-yc#@k7yJjfg$e>S8K=X?0yW9u1<0VsZjs7H zxy>)(EI{@6VCy8a&HkyOP}5_aI&vC8D}V_DE{T$W9-Q>OQi33vVcedzJ;{EBQ_`bc zB#RPxb9k~ftkuRWDA+K_Gp)9j13L;~BUiKd*p}%`A=2(91pe!IPgic|$n=sO9T3A4 z;-e)&Zmk}RdNfG>8{V07=Ny1>QkqDLG>OW#xNeFQvqu~TL&Y-s?j3`oLp4wknxnIC ztgv7XO0yBK($ufoL{w-VM7a^K*z^kklW)w@>C*m5WSwyQ9_cirEmk$!wYWW4GooU~ zN!_1d$9=Isk8-KWyJ1@QcPT=UoEm3%_9@thpA?3)2$3!v1m0H}6MPGLkza$@&K5ml zcywkVpbiPT{$grOySnRRkS6)c(=faI7muaupLCLorD9s&>VAV3;*=zOQspU!XiK?t z~OU?%gPE@w+$zUiLpTZ-I}W`=Q%Cq7GUZ;x=_q z905@W&-uKz1S8_swzI;5STAm|1zmoankSUx4tn!!krQ8vGRJ08ev3phvPK(>B?yI< zm@F%bnVn=YEE~LRIi(6WwRc5|+o~Jd0Pety!8DD)pH`lKBXU>Tw8R*#dYjv(bq={U zO4OUMk4`Bq-!paM3a=SwX#1J6*rMNps@8e6f$_*pdxM%6k(j&&#M^CxPr%Uglmo;C z+XFk%l&L8d?Mdu$&1(1EJib6(40*4|2M>+fR!0uOM}+skuKt`{Tgn|?vd*003|og5 z8Q{{Mz#qDRL|FxtP8{+FbBSMzI!#h~!LLR+jPVEdB$LcSb8YxxkM+UA(149#6ixS=6;fg5#(Sn#X z6e*k4hVRHbg9dxf?>fT-AxU$K4{Khja|JsYpKC-=DKx(_OQZmu{=>}VXKnaJq|L}) zuTM}CYnU%X%NhJ5%ppNx^Ep3|$|kJN94soNVFd<^Cp+)fBrlzZ7iftxkL$nwsAPj=JdAMr~h^shS$) zTHVn)ophHa`Knfi{GokWcFUxRQ0qDU8L#3_-gTlY=vnch zGkK4oZTAN22IO;!1~kvqY4tI8Wx<>~Ry;r+WvAIig;+;ls`kxU*P zX-ga26$!n~j+$ZTZBIYx6*~_@>FTZ3!M25vpFL^5@aDA)gg0~sWB543DpilmpVtPb zUk28EX)2Boyc;wiyP%KEGinNMxQk%j-o*q>DJvdgU+MEXwdV0?e4`8u&DE)<`9f$p znd;zhWVHflaIsF|V;J6j=v~9;-|V_hq>h_^b0%Iee+nZi$wMw@Dy%{7A@Pb;4~IZ> zq^oFmT>9-V!nG$?S4!;aM?UST+D0BjlDAa>UvvQOZ>tZkGHD?;#lORpEk^}C-9RpK zL2fMPX6R7UTTy9r&fQy4ol{=@9EyQK)x)W{bS=hBYmV5OGJ#P#z8Q_!2%DC{mlx|Z z1%p1c2IAPOX(3^Hzug=t9~y75rg5i6NTo^NZEAiW^Ny!bdZ4l4R?x05do=LJ1hrhg ztjD@-7lzlp_Oli^5$xTWkdr{u_O*Yo-l6Q7<)4nra~PrVj7`S_xn4mXTq4+fe&k?^ z-REgU6(=MLMc?z9lpayhnyck!y5~fcr9rca3gdm!@%3AYR(G+0bsCMBd%L26vOTxh}{dL9fs68n09 z*8AgZY<*$B7<4H@aK!G(rm{~9bxN9Zn6Yj79gHi2$voNCFK=e5y|stl9fLTjrZ?mL z{n^4QzH3?3=<-3T&TqVOo22rGBb2W>I*xR2nT;=m`mX_^Lu~fO@{r0eEB-F@BP89+ z(2t9rA#`mBHH=?UCiwWf{fFhePMzajupIU>nSk@p|4{~N$9p!!fB^w@d>Rt?7l)i>083KE4f--4(5K)oNrT(TeABu_=Ez8a#8R905;A|BTH)R;Uw zU181bhUF5Z31_K^J{xGJDaq3TJk#xzTPj=V zR~dm&gKv#Q$zHIpz~77Z$O%{)q=7c$&_Pc?cL)eyqAi#K3>A#`cRejp2m`qH@Szp_ zyu~8>Cl0RA_&#sgZ54o-^U?I7^@O%C%c-HqYQqY*hMc8GB}>BQRCQS*{U|bJg2lpCyt*T&*D0K%yIQ(2!p;c~b%I zZKdCwS&IS12q!igCg+}z9BKPSM|0y8bQ@5~uGM+YV>w@M;qwJ7=*ZS?K|QK^D0tGB zFs)-Y?ZZs(fEXEPA+lO$qP%W6(~3NyLX$eb$8yi_`9_-?(;a|@RoFHq$ZE4`?=(^} z+r;@B&ZB4;5Z0-yt-%r56K%Fu^rr;yD3-w7kz$SCS^rU{=v%QGC65yjX$c zE-7)6%45lOz#}cH8IX8c^-`u=j>%4@BWbGXwP3a&$gfOUh4occ?B(qEIbImyLP7S} z(#CnK+#mpwr;$jJk5%G#dq%!7KhDyuOud30b|;tny!|&VOPdRT4Y-CTx9{#j<23o4i4mZLgp!_?*uAuq|-B=2>-I zPLZ#OSWEw>vOHosC6eKO4L_171K&;bM`+CrQOpveXG}j{@DHAF)E1mYmIDYad70ZYn+7cg zO!kL}d_SVmRfriJR1eX7Ip~5H425K%7;dWvD2AYAEtjYjD7ZKYWdI$Lm=wAFx^$W;%;i&dJa!PnN=tZ7-6>}0R&>YP4!khyWHBY~z3+->6 zp`;#=F3TvA=sdet(3BgCxW*4 zM}%$SlKsdYW5A>ht}*^$K$hVXLL_S|G%>x8x#m#2HiP5GvDHVMHVCF!C^PLx>NCGB z&^t@`SoZE7Oc}?7ufuD|s}ultNdkXnoM)?jBvI$L-`Ts~3v~})_gg*87`+zfP;i-) zyv!p_BKQtp1G=FmVQu$C;>iMmU~e!iIoJ>Qzbjd1E`RV5zx7YIZwtYW>AK;`4Bof-;qA^Rh5C6Hz<5dtazv=IH^RB7 zIUgS_3F&ep-{x|NPA5%8r$c?xKE&-?3o0Nh2LS%;?wz_<8;I2#FOjS;|rOG zfWn+HM`xf1!DP)ZL02O9Z6p!!_I|g=xurJQS8G5)s z3k^*{mSrdbryff-!#LEOLlrs{ueA@G8Rp~MCdqqX&%djVx{vHAuNV>(rMne#+&X6Yclh)LaibAC|HWem`2)2o|``sj@x#38rR& zw&0^!0AdKFi7wo)0%um$Kqg;31%g-5nMJw!B~m!tAfPsO|gg>LQlD%6pD;z;J9ID zWE>%Y7%(3o^A+RM}}`N z3JZc-xVU#>IbC0seM{qX*7$<>;s-Uf&t1}L22ELgfVGf8E55Fwm33s5?>jR5BC6wv z_{3emkc{O0e0*X@QZ$(lq9p252_%%Zp2F_1nL_RO2x{w}$|7(|c?Qa2D4$|IS1{{+ zquP3_4rYkk!!fl)LXX1vX#;lu`|pGYf$l5z?Ja^s`#+Bqlx2kf{UZ&lLp!6aqIDCD ze=WFMM`H+(`}=byv{G^gKtvSpr7aCX1mcxBwA8b)2Gsor5!B;A=mt$q zOf=FvbZ}wLygkAlY!QT=68#@L^u{-cac+^L`9M2lJ1>!=ouKYe;S)FpBYha7WuT)A$vh|=6dId_(ecr7(oDKANwDb4@H9)^^t zXy(ai=RZHSn0Ag4X>!sV*)g@7v~CJ(O)PF}Rd~CslTq6}8Huufa&dd?$f*34?1Bc3 zvQlPiHOP(Su!YZ@70KbTSg1)|>6PaiNfe?id4b~P*(8(8o>rhQ#M2N=SAD~Z8w7?U zyGRTfYQha0#Y;2LWkc#hu|Wkpq0vx8`b3m~|0c?{uAY^2-;^>1b8!UL=9DX4zFE0m z5*H2|7|(?4<=Ge!e9f6UeFq-P;K)04M;6QA27x?UZ3PPHG&R2D*(X+txONQ;kALT|Q)OO%w59ZFIw zB&B3hnKxRTv#0Pt(OYf!<<%@39Yx!XsGLqh9d!?J=TD4xaMSBjL4H#lRX3>gcf#zI-58nBUJAIDOB3jl+Yku zQgYoJzk^+`q|6;x9;&KW>CWmyY}oFOCw8~;74&ON;pi%$N;)Lm)s^v*kg_8k7U7&^ zqs(ADy2ROO4G)@wd%qi^yZQEB%*MZ>ELrzX94l0$$Nhyx-)LZ-nNS(g@HhA})-aho#hgd+a@H~tEGerB zEYDJ@sEV8}-l43=Qf;!@G=9=xs{yR@sunhA-baLO{ zC7JP5qQrTkky!Uc!rB_C0}?S&Hai4hv^LTQphJgQ&f@2->8d+BWNGz(tO=!rh%j<| zQZN`^)iG6MCZUIGt}7>Ybq>Myvz%wpdoata5-S@|ON5#%TV(Q0V4L&Ti4yljiFikG zX%#dS(@rtkjYtlyGpEp*(F8vahgi$G9tp)&(>cI1X@5A&5#Mtk(i)bfum3gX&-~mY zB9@o4lW{i_ws9bN3cjO?e$gC3T?{5lXtvpQ9(U?#XTVK+Ql?pD#@a}NwMn=>b1m1I zT`)RaeC*D46a4hILYrF=HKk4z3z^Da)jQLd3ilD+q-*E|V{|A*{?q^W zs==gUiiNVdyDed_UwOz}X66dxPn!*zkuzU!N@TmT zzjz!M%_iAdNctiQ#gdaDGRKjrR1+7i;8-+n_X!rFmuT_JT&-Kf77v?(7nBn(2Ch{n zVq_rBs$-^>Is`U~6r^0wBVLnzG~$&ommIaH5gE~wyJo_(!fBGb2*zn_)biKI`Z~(I z2M-SVO$u7zpjTYcoOo*mq1vFr-*RBvjXx*CXnCsV;ne}e9-#7Oi^HYa-F%y8;gfSy zqzq7cXA@vD6RxcWiLtpw&fABfi|I3M?o~*3DFdaT{7T%}#Xz$ukws3j6WGa@RT2Q%`>+czln_e!C zI%-9n$q`cJ=Jd{oB{0?)8u1C%=>wsGT+B>Wkiy7RPovzi)TpDp%WOCqq1ojtt};iY+P%k zDd<)71LUxYF$A_0k?;I)hCdcql6^*h)YLee4^tfab_gSTonSi0uDHo-56Mt7fR|fY zEa+iUam_cOOrD~6lz$vsBEE=XJ76!GLG!uI)p{Vd;^kF&z+U>^xrCBG79cqNe#|by zFM5%s>v>*GbHeTUVtTcjaHOP={PrIT4B`eJDr9JVTvgi;`T1yslcIIPA1+|pkvFfj z;8M%yQ=>zH#~Rp%pD1Jxc7g7RD?0tAw2VUxMr#A9%wIV5gm#>v4C?^lITPoDcIyu_ z<2fC*g#>Lg;IJjl;y|-+Kxrz7+~M&0A{Q8P56>0b78HS*yMV40V9ecN`$2vXPecoQ z2PoqSRlvuN0?%+V4+j_SPpU-QJ&$~g^gPmK4GVliyJBkQDpE3zGEB*zi02QBf){`; zukSMeyQ$C*o8{-VvuZPy`~yvU^^&0Ljyvi3{z)XYcE9u0ppfT=OEcndr^tG2A90&7 zSj;5?U!Vz_X*uR1jW0oYI+@?R!4+(3&{SQe|H!OK68-idJp0?=a-voOUkI)m>W?G` zwb{y%*`u(!1M08bfe9mXjEmZ_eW{9cWPp$qd}Y*DMi^M+21(ego}Av2jWy_Iu*x4H zotOz0^;x7!?l{XbTn?wLfqVzp1%g9~Ib88X;Zi#k?KjeinY<*Uu~uf0ipmKedByz_ z6%Ti*6!Ef&pW`DJNb%NP6QJ~wUa+&_;FN8Z@Ok^3E06E;gex~ZvF?7Gm@Ch*2HOcO z@e1nvv2fzQ#SrUg`eq7ZjL5r@2d5- z9Pf35H8FmW(nW2?Lu!CH1?a`#-9=Z~7_!FZcI9t2q}X zEqRo0BR7Op=@M~WvpcXumtfQy+XzQAf+{OEJ$V#qjQr+xll6LbdE+9;Unw62qk^9I z!f3OoaC&Y8r{k?2mXoZT_qbU-VBWrN;u44Ya1eS2?c=rqrrG*FhZLiPL+r4$A(t)6 zJyWDs`%I$1{kXF;BvQIg@L-cD)S-BG7Up z`&U1W(q^%bG6R%t(xdApux_G6DjU)8!=4Fc%36mP$F5II0f2^T=H$yBb>Jd_XV=ePr zIr#Cd9Q><6z}ecMSy|C8lM&JPM9q7l30hNvP^o}U34bBEJOL^t(OG_;xE0foZ4EXH zRq3jCmOR?nr|dZ%U#KDOX6EGPdeC8qZR*;N0EB=;rl&6Oz^BOw>?O&;-=a-Db}%B2 z>KALihXH0Kjdjsfq(Q5+$4LlZW3*Vbvq+BfQ_W^p9Xi%@gmIu>22y)|xh8+YRmRsw zJ>R+#{STvSdHmz3GXw%7{B)~M->PHlE9$F>V^>Q9*1&)f5I<;5(~Z^lajh5Dp+_F2 z=)Ih}iBvaVsF$rn$RE8k_TY=O^^t43c68oivlZFPS|=XvR;#7hwR}8$BagI$ly~4N zT8$nqT#XsgHUy*lbRw`xKd$XFC=*|ngrEmVR06T)(;Tpg(7A+&>peG2++F;%vX9|y zMxdp?r>B!gtA=uZN86WI+MWWUvtxwn4eGNppGaA)Y|RSlex}X|kb3^S z8!G}3OuB=xwc3>*xmV>)%rh(=>Ig()r!^Xr$OjipJLa_yu*7m=Sio&BsJog)W&Smv zgKUu)7u735lc`QF%(ILz&yS#FMqqn_tOf&r{#q8Q=q;DQ9;-HjPvXg09@|fgMT6YT9Ol^SI(TP?#H4j{Z4s?EQ*)7h>QF>G7WP`ZKU(`alfwP z$Mocr`4~p#TYaza%1Qk2P&=KIl#5UnWJz%lqjm>%|IB~4Df9OehA<=Y`*%kR6wp5q zg_mS>0`!e2uWv;C!&N0>VQOmPXkzPZVPGxl;9}rxVQ1?^|BbKeBze0`0mR{(gnPUl zBvgsZN)xRHSVdYSz_J{J6?_}*HT6n|h6KG$kC$00KRmQDmvKDjWsk?yhw1I-PM;4h zuLu!H%E^L+PQ@eUPrlM(?lX{2t{y)Rq~S@?;APK7ovL3%J(G{>-kjTGrDo-R6VJz+ z<@#i%EFVm3R5mC~0sXjzt77PXQ$35NEp!(OlRVct*$dq>6AU9kICwl|>+Jxm?|SJ* zycR4SVk5usr&63Zxudj9BAMgGx;ZtjiB75}e=G?eYuNTu1-|;$Ym$WVw}O-6E!zfE zWU8|FYbbzQ6fLvDlHZ`w!X&te5_oI2Mv86Q9UF>E=y~Z}*gGnc-X{D=YU6;H#Tens zH1@s@xXS`o`7TP)H>N|!>Ofg+}Hg`g-9MgzyaKq-w zjj6+koQOq0Pi5}+61MP;84*`PHSb5W>>y?I8q8Y$2Djfb2?Yi*VczQs6(=ks- zX2Wijhig123lCC&?iC-W@Nm=-`g15!#QK~Hw+`#u^X3Fm@pqOR5@fMFeYT!Qu!)cJ z&GPbq!9{1)!2EApvLcJZU5Q?0Wr&v;>-)rB$o|QHIfeO;L= zF$-G@XA^*l^M8nz|9}fX*6x52vHM-EOAAzX{<;|%5~e0Hc_1>_ve-r?eF)KtNbJi$ zui~%IXnt@_69I-;f}#A!&Q#ZladE@i=|C-6i`b1a5uFHlcZwLN%^oXEOtCHoy4R7^ z6`oW*V42$cUe$0U>_LOu_keEfd2LNl{eolYSZcrSmztPi?ewhw5|4!tT7A6LvMQkC z+$?HmrL z!Q4jPJ|&c(FLu16-ke0aT#yX29xT%!5MflL8rHjgU4z zaAKfeWsFu9Xy(W1wX~jcA2j_ILY9*E%Q;Jx>A849`nPev5Cltz&Mw@6rh~=l43z!gK$J_GOTT#yXmvcb#n}{b)_lWz|(5QoGj@#S~3*kOi zDnD(GN{F-XuZ2{(t~qgDH^J=*nvR?O?bB8ynv^7I+GzfsFi`@#n=$-X(s*`@oT9G% zYS77B1MXsP9n3YW(G7w#$o8?$zPrV>|H7-od*p0X@pO^gx-v**48`(qT--2AuB>!#36d;L?+* z4Z$$hyQ@jlsXb6F#+jqd!~$*1C?c4#Hd4Va6)ae8`4WSDggZR=#7PA7R-(n)xD$>u z9XZmp5&Sh;O0G-9@Tk=vDQZ6!oO8e++ygIbU+1uR%e6vlyVp-AptBP%DP-bKqkB*& z-=q!<9b_UMXnaXZA6f;e-ngW1Xd~WzqeR;zm`Itn z5k3Q~gU0IH{iV+xsB!YCl2oj`bO77S=$fd2#m*iT@S2JETEWzx`t)CMjfEtR+2qCR z<#9@%QbD6*V=o_;jF``Y#*r;VpKbk$G}EYIW_5JktjTnF3nbx(a*$U-A8$OiGtEU_+G`b@fmuKp}oMCmBvzxnGNosmO5 zY#8e5eiB;N`>~h`4EXN!C1Qbq__ibDIpew zX)+Zrz?r@(>cCX^N%Mf_I>ZiVDK1W&VK5|>4;X1Akm-$>m$NyJ`%f zilQmox!tfyu-Cay00}#HqV%8Rq+IuWP3WU0L;?~KDF4fX;b$7@(}R1_rLQu6>`k7_V2W5_r2SG zE7m~bjt2JT|FOL`C&@|=3Lu8w1bl>HbXnJxFB#PZs7q^>smMeLEei9mV9&{J6+tTg z?QG0Murj0xyw0DVF+TBmNsq80&~EGMNQ-^DJtFpyaCkMrDPih3_aK2C?H|HJ7Rf&+Ov{1%99KJ|-l*aa zE8GTp@`9r^aZqSY^YZ10A-MgrrK$qd?;x~Dc25Q4w~;H%IorFAn3XzpyjQWfZD(f% z{wY@))Uf}6ZwV^t40w8ht-;VZBA>T4zmLq(P$`@cb(6OjX$`qx2LzKXka1tJ<2dvq zPhP8M$T3HS!++whzIM?FL%|;dZi?A<(drNNW`dA&lGd5N5A;`Kj_qMoFy8|cMimX{3k*G zSEJ}Z2zs)O-G%_{=2Pp&~->XsfTrkUilh4>JY{BP^3wWUd zph#h&T0}bY$1eA?Q)HehNdBR6^9+;xL2D&+@ApC3a>k7KFF@K9`sC!gIqc-wX}i?{ zCJXEm$Z3zw#0)iC+S(Q*`5v55V7Y5Xvm2PjZHuF3E-FMhWMv@HokY!`eR2Q%n&a4*l^Q}eH>3Ev@JO=sc?wc3$&ll-WyN|N^P^PMZm^fNkcPGfM6C2?x{3en@_9H&i%vJ{anZ0B@HfSXF zDK5AJ&O58~_q-K|cO|C}VH-4qkD52cN^P~AHOgPZxi5Ggdge*`r*>-@B^th2^8qbD zyG=p0ZHphG=^)^ITzh;L&Id=~aQgLK=~F+I;bHS#y=$?yTdgD5IU?^QR`0qY+Y`C+ zqC>DLuD@*!0l|ymuY#d}xo`1HPl$H}ES1Uoma_0#7lCDqq3TV!CZV^iG;~aB2Ilmk z7f{$F2jts(ysX7bM`ZPbIF885pgsMBU$UxJgH*=!_j`lxB0mWj=i(?}hI9%nZpwHl zh*U%)OcGhRPqCp9^S1VR;X)B~Ny3ds*Lub*-q*tTb&~8>r4~LLn>CXWd#8i(3tYGI zq*HnjX|?NX#gQP z0D#DrPRh}|dCtEOgv^-3+G<*2n4RzHKb^P|Hc1HWA+un!!yT=I`kDNGFvxw)a(PUU z^2w(?EQp259-Pt0T(z{%8bE;fM>pS2Sy&qCURM?N&+tuU$UB{hH({FVU|6@pRDWyE z3;jVH;?b{xEs7bq)JdqH{#q$|YNoOU=gUpbHe(qxW5xg_iP&ipvj!^OSR=KH+Bc=* zbGOIm#p6q~U!NxtJ;b0+_(R&j_E!jRgt7{7m6 z_zZiP7&u$S>?La+DloK}$z(GBaqWPU#wo&Sm>~S?D{({6B9PIm+G*eHb`b_-WhV~Z zz+a^L!>|cY1F%3z34O+2l^F5c0J%_H*qBu5m;#)KM_p1Jh9#G7SVXYb0`!i#hskuR6@JAF=l zWG-yE%(#@2w5a&bc$@_p+7%r+X|LO;kBkW2hNA|ZUq0y=T}hx<1Yw*R@7sb<7|st$ z$S&fLru=%>Y{s!{jMEPdWncGY2>VYXKP)tXHOAOuClH~@X~AL>MjgjXu<*m9Q*so) zZCjNr1g8vA>Bm>giX9Ly6c$Qkg8BKWMD1&@59(Q(44KbXl1oJ8vMj$`EL7M%b`Ct? z@`r)QSbgBce7=xNh9Cij6m_cS>U?QnTq9b|Kymfbg>siAx43z+SS*eI^o}qFZ5pa> zH{1D_sNiq)T02@_7n?tx*@i~&>5dd&P}KNV?5W-K?6O3(86QJryoZc)z$1FcpKu@x z?CNdc*r25miJ#^yLO9pzKVBrA-InN092IZV(Y3W}Jqv+CBt#}NO%OnJelR&nm9ep3 z9;~NkK0p3C%zcZ?#(w@;Wl!JZS5{gwjvm?1g%kS><#lERhhSD0Lb=h1S83&YSvT6d zH|Q`0akJQrtfI+=Nj#YYoH&^3QKhbK9v$tgJ21yL`&-qGH_$PA2dk9k0!)ycJee-v z)z9M*>!$hNY9*jAopI|{X~+Bwk#;^Bz9NYmY)!a~z3n>a#b_iKzXLC4B)n7YdyHz| z^t4>G!@qh1PU_n?N%s>$My)y@8?J6_qK5Y{mhf)FO!|ONSEP6H7UX_4>cp+ah6VsG z@c@A5bp+tIrt$Z4UdzsbloRD~v=ZkO%97J+ee+HDdo+gR2=d8b8``bh1Z{#DGi`_G zRkn(sw}tI7esGK4vu^=@UVkyxVmr0k!rSRA5xVh8^V2sn_v;6|c8;Tb_FHF`<`z$X zUUQaS6T(i2C*Doz{)5=OXt*^>X75o<-%nAD5blg<#@7&>&C~mjF5@$zLf4&}A8DKV zh|TjSPj1b@km-zVy#2Tdy6H8YSJWQ>Q`s;(JL9=f$W1z95Y365pDCz`WZ1tKRn`Z? z@F|r69I^tsYS&H?wbGnIGQuGXC&hyM!BWDgE+A;JEC{j^^+Y5ud0(^9xmzpP_`@`; zyR!w93A}Rw`ti1YftYr)Rc^tX;)Ql}wrC;3KEVa2#ImqfZPfXFUD8hJ!K-E}oeFppyM^cSmaG`?ah^{k;Dk?XO^q}^j=G2= zY*bBDmC0i;vqAm7+C&&xE6OatoYz9xiqH9t(xKJo98uv3xNK7her0U_a5<^&%pm+dIC4_LS{5(=1$5(b&% z*x&iW^~bkHtbC=-AZ1@CgeP)ln-!Dtwi2@=!O-;*5;e99T_flqy&aOvri30q3zx8% zpTR2+LR!+Q`7mxK3`>cg(f%U}!+q4`z{r*TS^vYQvioYY=_8mHj>%E5#2b&d)>+)< zv%A))bgXvcpWbv0#gD^AeF@Y+-hI`!_QhjUt4LZ&;P5{X*M5DK@ zbiX;PFhX_H9(S{2C*CWx)4C9`nGmQGY&dM)Vm9J|kX*@IZs5Wh1-z z%~f;%Cl~=^Zu>&%gPFNK+uORWAHUpKPjnTih+QJuPzjA<@XbZiQ%=mb_mmO9+R~8i zocvwgmzsL)NQpmx&mHg-R>x!0X=i6!6?9>p6Cu0^Y6I~P7KDHe*j%^}QFX0CRD zvLNvlwpc?SaK*Rkz@Ulp;9N4=PBk^YrOap%r=8(l|CYt-A>4Qiy=X?z`f6vr(CXZ= zHo2c^6))|Wur!-n?eH~AU6LnmBJt_{9%-!9CXfHFd`dpMHcMvF|36@E?+`Yx+4$IDWB| zOgDeCCOg!4UhoPv=-0G6+nQZ2tiDl2)7<{VacO`cCtc(nnXbdbu)B>Syj|B*R#}ep z*-3i1wF$BG$jf{9hJ>O#|5qHcY3k>u8aSV}j0+&{x0Ie+Eo^R2Z7gP)Mn$)|pS*St zc4$=u*&F?stZeK1Rdj$a6uQy2%(20(>0iV-@7v+Jhy&QL;{q81}=vy!m# z42M)F{gS{}LiTE0d+=-=EYPbU!fY0cb`(u_TG}x8wqi8bHVac5kdiy}5y{{L1Jcb3 zx)*W)kbj0I#D0<}pSdAf1hFuPapHLgK2I9EF+@`5hp+yI{JT6R40B4Ni^Lc8af8vpR#XJs54pc8hzcS9v zJ+#JwH8kvt)U3Zn~#HoMn2&<~rT1_9}g8Ox0VT$1AVGf?{k9s-gc$4hf zA%20y^b?&`o^T^%SlaHdok4l;J^}8bxAhp-0OWd7P{d;b(Ue6-Yl6Z|%;>=2p6|MJ zMj;xGk7qzcCv~G%acq(D&mY8e3rGgPYlVEx4H&^=g>0GdXQnI;+W}@k#ibFN3%$*H zzzLYH>S@L_Q0ye33*SeFN}Cxq%Bu|v%r&=b3_5u98Bo@-*`7O7P1A9Q$lTK%X2BH~ z`@Y3LT+}B-WTxeZ+6ewt3+G%29|maCbB@7k4E!~vW=1C5GJ|THuaEtR1{au{EF9^^ z6A|qSrdG1u5|J`p2*X%6L+-^W@!HGr^0gyU_9poLhmCz};kVp@G5NK$XhNhYwY!C^ zHUeohgVy2|wLSJhN#PDIDv`7;Sg!awq%oQJWlCo%nzQtyh@^F={FW@^5IMOp)!ID@ zR_na>mN?!PN7p;GwevU{NRQ|1MoO_7B29jftXK`rQRV#z&hcP;y1?BT&upC&F-+Ah z5&mo5vXFpC!=dCS5~Q?cVu(T3Zn|^oDw{5;wS|uW2){T1-Irtxm1uwWl+2C z>WUbk)~P6AN`W7@j?6u$rPA+F6{B_87$nw|-XLr{P##TOPpcJ?$GOhcqmMjviw$0yA#&CuTw%eqdM9K)(^lGaO=gvAVXAC$-*7Nr!dJz7qovNN>QC8Y`8wd$kgrvXG0ksaMp^G*&}Oj3ziFR5bDhsc^$m z<7bowahM|0o6Q_0Au#J=qKyv3D)02nypfS(|gKvJpU8a}d zVe$YLV$D}TMpaEYG|7>ko$_)&YR)gX;nH4xmfi|r;bu% zjo2hjYb~z&)Q=%+Qr1r~0%P}j(9b%zfPs&NbELu%P_TV*>yIlZ#9n@j#E%L0M@fS} zD6rc<_9o;ymSUOemh^unuUJM8=SZ!?n)Yw@GAmZZ(ME!rHz%dVVyP#fTuOmcvGYEV zar32}F1V{}PCdI)i|xPawhL8!fVm9PIka51fw#{LA-<9zt)JnM=rSXUla> ztrfs*pZs<;teozlP6@V8amVyCzEIh1FMW76y~TCAA8XmNF-p6^L;nX_gV%#kiye8h zcKby$Ke@oKQ2nNHa!jd`q!rr^ic+k_@;#3`f?u?$FkfZaDwMCo8ICPwbV^VVqx|@Z z{Ia@v6h?4vH= zq|NLA6K9lVla)BMSFqJ_$mpdVO^t2$5;!x4o<$&lluqR5FvX(YEPvFJ)py)Oo?Btr zuf*hR>c91Pk2+Euye^cUAe>`p{Lp|C zZ`BW@sL}#-_G?Y}rg+~71(xF7tJ@!0x&T+b?(^y{$0*^sonu>diztq?TUWaYIPuHF7+9Y`5jbCN0d~>!V z=X(xu7TL^woW^r1eoM2`c-(l%SFEXEf1TBM|JdDpS`KRfcH+PKY6qTliHZ<-4QCaJ z?t5}h1m@>@a3W_kPmJ|sqqI-3w`R;f`88cXXt=yBbsLLmQrwG<1!bzc0=#h0gT`!X&y#?vOjSwHT^F(YJf!Ry(@L?aETP zL=%xrwi6{!BCt?T3H|B{P*`ws-pE@TdO@Scn>*e=6tqmJodiDtW5bBKbLb|}JifU8 z`mkip8E-NwSnaDlJrjXmihpnoM+!{Z0KhsfU~HN3kWDqJF+5+PZpzp-kokJQLK#W( z*&|T(Y}or9&i3bgt!8QF;ACd^ANRY8yy90Ol(s8PxeX{pF`=kArFdxB*H!`Jxyc4t zJcBg0IW6pHn|_Tg_y|&Q2+me4$EGWbbvpD!Clax$vtY!WZ)&)mc2pq|qR{o;apjcY z9TnTOFyY(=@c$%=P&DxiFc{np{1$~Da^Rlz>X&CU9X#4sF3gLdh(mwmIehca$ZSF} zW&wwHs$&5;=ZL=IK3w*%^W_X^Znh%KkIcvNKPtznTB7LN$ZWmROp+vD7Jv4*kTbYAv4MQ%B8JErq8l5s0KmUk{7|F;rHS>ieJJK%9mQ+ zBWS%rA%n$wbKwXb?NvNGvY0ggxqA*dTiIsHs390rdPS81xC|NoAp)a*gMln{1g3U| zM&%yFdJk|*$HafW5V_BpABq1T7sJre$-%+=Ki5QK(SAV)#pg;h>La#gG(J8RIqU~L zrU-TW=u8RB?7_}L?X;Ah7P0WsN3W~ELv~jYH6ZbfiN*HtWmNIB3=(2rTUh{tfag-K zWq8<~T##;E_yqsWDT)IJC*jk4FAoN=FeJ3vP98fv<3o7q}{pLx<$;zsPYy_vW zFbZNuc%>DD8<$I`hr7@OO;~rBQN$-EpVKhxa#U6y5vDu9Y|4rZI@7DgDnXHg7>&Lm z%u?%4#gksW_gZ*6C!9cG0xO zksxdCIu<0&ug`msVNGkP8_GjQUVClkY)0ec%GtDC zH4%GzQm1Zk*WI}BGg=SmrNnZ4cAGSDjz7`*0Y@Nf5wT8|;(X1Pu+}nL?>*9aZ~OtE z1$~grEELz@oO!=iUy@pYb(zr{Ws41|Jj2>sGd0Rlv(Y*v&RRYEeV?r3V z`#yIC@-g+Bv~Yh$!9sw{upg}v5gc&+rrwD&%Ehw?USNs`{&>3*Oh(`^dvwa_t@Pz^!kPaf*XDuP=)Of|{XUVTs;V|2iiCBn=)tIc>*>Lg>bCbnYs59*ea9-f7Koq;h2Ptkh4kdZix|t~pv|+r z5l=|KIl;5VN_UmJJLPSV#*%SJI1%08+Tl$;)@yzD$-t3&&kxQ!g<)Rv7k*Zp>%Bvc z;E|$n52pUO9>-cOMk`njiZ-3^I^{0+D67t+1NZ199AdB<%6GXXu!IjaHyPU>X_dgI z;=!dc&dklQ z2RMqwzUuvWojC9Gny zh=UdUDHaQfJ&vIzhVtueXU>)8!0$AA!_g2?ti4j^(HxmZlf1}Ao$^e}6+vP`YoS#= z$6@MUu8D4q70`HSdoD^d32dfmd6->Fzs!;=U*MVQkoqwf5WMM3!3l}ZnsyNypq!mA zUkv-uA@+F&G6CU^$8CPrst7Kz<~32%0sDG^jpEL!De)_RVQfCw&_^7DFGpo($;3v> zYfq%esLpNL=-T@lF&6>Os}^}flo%xb;wDWaxZ$kUDO)1KHRRsH-?zb*aD0n-k@)rq zjLHt$n+{8TR)ImdMBhBQuC)N{hwjVoT%nq2r(umXMOc;xu-^UTHo+$w5OY%91lrA4 z->g5Kq4UeZaK62NCn!8r#lK;;GaqjQ7+@*W1y7=>Lp%uCwE*TK*id_{vAV}!wBel? zkXtWVj=;nJFjvQCTg(0NTBeK$DM~enI&*!kxlLUy# zcsjDi>M{JGi84bl)aPo?ypNTul{B;=K=tclsF?NDqOb?A{rU<87lq?U>O&tYy0D z9P_M%hN6HDk;q*B6v$^W738z5^Y;+>Z`9iJj=f$(-eHpirR_jdZZfDKI1hZU+!AR; zOd8R>Jhn+oELm9(l0h57~_^EIO z24H@5PE;5(J<_}jJ>%K+7zin_O+hYbUt0lSxuYad#wgayC*nDUo!12`n@A%UZ8>df z@C_1Z4fguO{&Mw}!r1Tm--RU*ed^%w;?FQ*&4gsO&g^aBJ>jA~ zmpr?|KI8C+NwN=}tzvJ2C)|Pd>OfT`yHy^PAn2Q)!`YW`^|DQ zFQ;EgX`a{336Nr%u1S7p^>FkarX4eiZkw$Hi`_ZWGNmSTC)6zbG%$8Vjp<+bDTgPS+NFWU!y z-ZhV~z>`qD9q!%QZ(uZ-)q13^vwU^rSIfsYlDKC=a3Q23600MZxt7JhTKi?+|THaVBt8bdmFW z7bOZm+a^NBPYjebx9WF!_{ifzk>H3_rm<{Y$D0MIbVzRF@7Hu^UlY5u^AjK9q)T~v zan1qUsvE0{9m0Aa=qBgQjqD-!+Zxt3OpeD;De*Uc=xj)JMjtvJ^>^ENIZC>zzP`@j zVIt>;krNU?=eiv|+_TxyDmu4!%u&pC7Hi{`q=TjzJ&>jDvk(-n>hAo|m2=E}(9+@& z^7)fx&S^ugP@?Q{EOA0p=dT?rF=<{?o>6x%Iw32`JzNaaiZ9 zT_0mJYxQDzZo@Pxv33DPS7j?YISwIUuD=?Xrg|?qo_bQH1jP7SZJ@bstY+>6w;}c` zp{A_Ovc6!wwkfXjj8E-1>ay`>L~~CvFXw=E6gi)?6)yKr*1di+L2z z`y|y%`P*oJ7tzqcgv$exij0tl(e@?=YrG<62qe2$nc9d(Vd--IQ3@xAY8Xm9XZX*X zvbRXwG~{{j1bn_DpSMo{6>(uPd2t52w~1;KF^e21-m{vvhMo-v2`k7_0aI3S2o*wc zc(4(o0eSg}Jt?G^@iiMA$8=`guJ1g;jJuP*ETv{GdkCfhjE1GlXSG?3 zxj2!%@h+RJB8N4dKS-&7EDH@VorBNU1avE!+3f4{;~~MSFjJ(oM#@E><7V*%2hc9V zmh=c$cq6EDP-ZA7Q4zMh-{KZ?8lj)=VH>NtvX7@VHJW5@>F_n14@Kpq<;>W%z*7Un z(jF~dJl~z8V?`OANjzAu>Z0kyUKccU`q-Sv?i+Tm7Cjov)ky$ zBihF~a$~F>;a>X$^h4CVeX_Ue^o(eau}NH1KtO8F7v>&GGl`UK+hTHLcG6E&%S*+S z<^ED7>Jb{mQ_AJiS3&DpU^M)N>PD2Kiy2u@+l*w35#7gzrVL$zh0<1f+85zc?~WAT zC7ji+RVrWiO=KN_RVODW-?@$NJX%%U%ahzv_2vq>hMK;{nn`)z86}ej|`A=4Xq9{N4zT{~#aR~hE{)ybQ4$po=vH^pFG~7+V zgrhznCRCO7kW{5)X>$6cpYN(h6td|t(;j66!BBfuV^+Fd9V#)0u$K#rgFcRF###*E zl?o|-P0}TT$V|!-P+=vZOL6*o>8NJRHhnqf(KNxlMpbg4b8^w3%0ORl?}X*pjeP;Q zHbl9QYm_RUP0Xcg2_<&A!E1|M@^*ta4z7s0w@A3ViXngGO+A-7kAqT|YkdrD`M&egBqFjt3wK)swQ0Q?L=`E^jlMXNE~+ewc-nfT#GQ{Q(o?V5 zRATvx)HDSsK2sW#Xow}b?Lejb*jy@(we%6|lINP5F1^p|%T)sod2lrx{1jA@1p~)` zcwSjPZ^8bp0?YG=eLheChr+)<|5s$?KlNDthW>j+mfwKiM}7e9^ZWmxf7ECBv+>_G zUHU=NH{SGo{@eK?WmW!z`3+h88}gDt<)yuUFSGLB2A_Kj`)qpq ztGyTS-!WBx6ESWpzG^MVsF{NDx#6a>2Dd;xto{$l~EBn$N{ru$vTi2!i-eCBWV``iBkRaTHO diff --git a/TLAPS.tla b/TLAPS.tla deleted file mode 100644 index d5f0473..0000000 --- a/TLAPS.tla +++ /dev/null @@ -1,311 +0,0 @@ -------------------------------- MODULE TLAPS -------------------------------- - -(* Backend pragmas. *) - - -(***************************************************************************) -(* Each of these pragmas can be cited with a BY or a USE. The pragma that *) -(* is added to the context of an obligation most recently is the one whose *) -(* effects are triggered. *) -(***************************************************************************) - -(***************************************************************************) -(* The following pragmas should be used only as a last resource. They are *) -(* dependent upon the particular backend provers, and are unlikely to have *) -(* any effect if the set of backend provers changes. Moreover, they are *) -(* meaningless to a reader of the proof. *) -(***************************************************************************) - - -(**************************************************************************) -(* Backend pragma: use the SMT solver for arithmetic. *) -(* *) -(* This method exists under this name for historical reasons. *) -(**************************************************************************) - -SimpleArithmetic == TRUE (*{ by (prover:"smt3") }*) - - -(**************************************************************************) -(* Backend pragma: SMT solver *) -(* *) -(* This method translates the proof obligation to SMTLIB2. The supported *) -(* fragment includes first-order logic, set theory, functions and *) -(* records. *) -(* SMT calls the smt-solver with the default timeout of 5 seconds *) -(* while SMTT(n) calls the smt-solver with a timeout of n seconds. *) -(**************************************************************************) - -SMT == TRUE (*{ by (prover:"smt3") }*) -SMTT(X) == TRUE (*{ by (prover:"smt3"; timeout:@) }*) - - -(**************************************************************************) -(* Backend pragma: CVC3 SMT solver *) -(* *) -(* CVC3 is used by default but you can also explicitly call it. *) -(**************************************************************************) - -CVC3 == TRUE (*{ by (prover: "cvc33") }*) -CVC3T(X) == TRUE (*{ by (prover:"cvc33"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: Yices SMT solver *) -(* *) -(* This method translates the proof obligation to Yices native language. *) -(**************************************************************************) - -Yices == TRUE (*{ by (prover: "yices3") }*) -YicesT(X) == TRUE (*{ by (prover:"yices3"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: veriT SMT solver *) -(* *) -(* This method translates the proof obligation to SMTLIB2 and calls veriT.*) -(**************************************************************************) - -veriT == TRUE (*{ by (prover: "verit") }*) -veriTT(X) == TRUE (*{ by (prover:"verit"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: Z3 SMT solver *) -(* *) -(* This method translates the proof obligation to SMTLIB2 and calls Z3. *) -(**************************************************************************) - -Z3 == TRUE (*{ by (prover: "z33") }*) -Z3T(X) == TRUE (*{ by (prover:"z33"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: SPASS superposition prover *) -(* *) -(* This method translates the proof obligation to the DFG format language *) -(* supported by the ATP SPASS. The translation is based on the SMT one. *) -(**************************************************************************) - -Spass == TRUE (*{ by (prover: "spass") }*) -SpassT(X) == TRUE (*{ by (prover:"spass"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: The PTL propositional linear time temporal logic *) -(* prover. It currently is the LS4 backend. *) -(* *) -(* This method translates the negetation of the proof obligation to *) -(* Seperated Normal Form (TRP++ format) and checks for unsatisfiability *) -(**************************************************************************) - -LS4 == TRUE (*{ by (prover: "ls4") }*) -PTL == TRUE (*{ by (prover: "ls4") }*) - -(**************************************************************************) -(* Backend pragma: Zenon with different timeouts (default is 10 seconds) *) -(* *) -(**************************************************************************) - -Zenon == TRUE (*{ by (prover:"zenon") }*) -ZenonT(X) == TRUE (*{ by (prover:"zenon"; timeout:@) }*) - -(********************************************************************) -(* Backend pragma: Isabelle with different timeouts and tactics *) -(* (default is 30 seconds/auto) *) -(********************************************************************) - -Isa == TRUE (*{ by (prover:"isabelle") }*) -IsaT(X) == TRUE (*{ by (prover:"isabelle"; timeout:@) }*) -IsaM(X) == TRUE (*{ by (prover:"isabelle"; tactic:@) }*) -IsaMT(X,Y) == TRUE (*{ by (prover:"isabelle"; tactic:@; timeout:@) }*) - -(***************************************************************************) -(* The following theorem expresses the (useful implication of the) law of *) -(* set extensionality, which can be written as *) -(* *) -(* THEOREM \A S, T : (S = T) <=> (\A x : (x \in S) <=> (x \in T)) *) -(* *) -(* Theorem SetExtensionality is sometimes required by the SMT backend for *) -(* reasoning about sets. It is usually counterproductive to include *) -(* theorem SetExtensionality in a BY clause for the Zenon or Isabelle *) -(* backends. Instead, use the pragma IsaWithSetExtensionality to instruct *) -(* the Isabelle backend to use the rule of set extensionality. *) -(***************************************************************************) -IsaWithSetExtensionality == TRUE - (*{ by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")}*) - -THEOREM SetExtensionality == \A S,T : (\A x : x \in S <=> x \in T) => S = T -OBVIOUS - -(***************************************************************************) -(* The following theorem is needed to deduce NotInSetS \notin SetS from *) -(* the definition *) -(* *) -(* NotInSetS == CHOOSE v : v \notin SetS *) -(***************************************************************************) -THEOREM NoSetContainsEverything == \A S : \E x : x \notin S -OBVIOUS (*{by (isabelle "(auto intro: inIrrefl)")}*) ------------------------------------------------------------------------------ - - - -(********************************************************************) -(********************************************************************) -(********************************************************************) - - -(********************************************************************) -(* Old versions of Zenon and Isabelle pragmas below *) -(* (kept for compatibility) *) -(********************************************************************) - - -(**************************************************************************) -(* Backend pragma: Zenon with different timeouts (default is 10 seconds) *) -(* *) -(**************************************************************************) - -SlowZenon == TRUE (*{ by (prover:"zenon"; timeout:20) }*) -SlowerZenon == TRUE (*{ by (prover:"zenon"; timeout:40) }*) -VerySlowZenon == TRUE (*{ by (prover:"zenon"; timeout:80) }*) -SlowestZenon == TRUE (*{ by (prover:"zenon"; timeout:160) }*) - - - -(********************************************************************) -(* Backend pragma: Isabelle's automatic search ("auto") *) -(* *) -(* This pragma bypasses Zenon. It is useful in situations involving *) -(* essentially simplification and equational reasoning. *) -(* Default imeout for all isabelle tactics is 30 seconds. *) -(********************************************************************) -Auto == TRUE (*{ by (prover:"isabelle"; tactic:"auto") }*) -SlowAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:120) }*) -SlowerAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:480) }*) -SlowestAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:960) }*) - -(********************************************************************) -(* Backend pragma: Isabelle's "force" tactic *) -(* *) -(* This pragma bypasses Zenon. It is useful in situations involving *) -(* quantifier reasoning. *) -(********************************************************************) -Force == TRUE (*{ by (prover:"isabelle"; tactic:"force") }*) -SlowForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:120) }*) -SlowerForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:480) }*) -SlowestForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:960) }*) - -(***********************************************************************) -(* Backend pragma: Isabelle's "simplification" tactics *) -(* *) -(* These tactics simplify the goal before running one of the automated *) -(* tactics. They are often necessary for obligations involving record *) -(* or tuple projections. Use the SimplfyAndSolve tactic unless you're *) -(* sure you can get away with just Simplification *) -(***********************************************************************) -SimplifyAndSolve == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp auto?") }*) -SlowSimplifyAndSolve == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:120) }*) -SlowerSimplifyAndSolve == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:480) }*) -SlowestSimplifyAndSolve == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:960) }*) - -Simplification == TRUE (*{ by (prover:"isabelle"; tactic:"clarsimp") }*) -SlowSimplification == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:120) }*) -SlowerSimplification == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:480) }*) -SlowestSimplification == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:960) }*) - -(**************************************************************************) -(* Backend pragma: Isabelle's tableau prover ("blast") *) -(* *) -(* This pragma bypasses Zenon and uses Isabelle's built-in theorem *) -(* prover, Blast. It is almost never better than Zenon by itself, but *) -(* becomes very useful in combination with the Auto pragma above. The *) -(* AutoBlast pragma first attempts Auto and then uses Blast to prove what *) -(* Auto could not prove. (There is currently no way to use Zenon on the *) -(* results left over from Auto.) *) -(**************************************************************************) -Blast == TRUE (*{ by (prover:"isabelle"; tactic:"blast") }*) -SlowBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:120) }*) -SlowerBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:480) }*) -SlowestBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:960) }*) - -AutoBlast == TRUE (*{ by (prover:"isabelle"; tactic:"auto, blast") }*) - - -(**************************************************************************) -(* Backend pragmas: multi-back-ends *) -(* *) -(* These pragmas just run a bunch of back-ends one after the other in the *) -(* hope that one will succeed. This saves time and effort for the user at *) -(* the expense of computation time. *) -(**************************************************************************) - -(* CVC3 goes first because it's bundled with TLAPS, then the other SMT - solvers are unlikely to succeed if CVC3 fails, so we run zenon and - Isabelle before them. *) -AllProvers == TRUE (*{ - by (prover:"cvc33") - by (prover:"zenon") - by (prover:"isabelle"; tactic:"auto") - by (prover:"spass") - by (prover:"smt3") - by (prover:"yices3") - by (prover:"verit") - by (prover:"z33") - by (prover:"isabelle"; tactic:"force") - by (prover:"isabelle"; tactic:"(auto intro: setEqualI)") - by (prover:"isabelle"; tactic:"clarsimp auto?") - by (prover:"isabelle"; tactic:"clarsimp") - by (prover:"isabelle"; tactic:"auto, blast") - }*) -AllProversT(X) == TRUE (*{ - by (prover:"cvc33"; timeout:@) - by (prover:"zenon"; timeout:@) - by (prover:"isabelle"; tactic:"auto"; timeout:@) - by (prover:"spass"; timeout:@) - by (prover:"smt3"; timeout:@) - by (prover:"yices3"; timeout:@) - by (prover:"verit"; timeout:@) - by (prover:"z33"; timeout:@) - by (prover:"isabelle"; tactic:"force"; timeout:@) - by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@) - by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@) - by (prover:"isabelle"; tactic:"clarsimp"; timeout:@) - by (prover:"isabelle"; tactic:"auto, blast"; timeout:@) - }*) - -AllSMT == TRUE (*{ - by (prover:"cvc33") - by (prover:"smt3") - by (prover:"yices3") - by (prover:"verit") - by (prover:"z33") - }*) -AllSMTT(X) == TRUE (*{ - by (prover:"cvc33"; timeout:@) - by (prover:"smt3"; timeout:@) - by (prover:"yices3"; timeout:@) - by (prover:"verit"; timeout:@) - by (prover:"z33"; timeout:@) - }*) - -AllIsa == TRUE (*{ - by (prover:"isabelle"; tactic:"auto") - by (prover:"isabelle"; tactic:"force") - by (prover:"isabelle"; tactic:"(auto intro: setEqualI)") - by (prover:"isabelle"; tactic:"clarsimp auto?") - by (prover:"isabelle"; tactic:"clarsimp") - by (prover:"isabelle"; tactic:"auto, blast") - }*) -AllIsaT(X) == TRUE (*{ - by (prover:"isabelle"; tactic:"auto"; timeout:@) - by (prover:"isabelle"; tactic:"force"; timeout:@) - by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@) - by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@) - by (prover:"isabelle"; tactic:"clarsimp"; timeout:@) - by (prover:"isabelle"; tactic:"auto, blast"; timeout:@) - }*) - -============================================================================= From b5e3705210665231b1ef26893d2195574531e82c Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 22 Apr 2026 11:17:23 -0700 Subject: [PATCH 2/3] Prove deadlock-freedom at the level of BlockingQueueSplit. Co-authored-by: Claude Code 4.7 Signed-off-by: Markus Alexander Kuppe --- BlockingQueueSplit.tla | 48 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/BlockingQueueSplit.tla b/BlockingQueueSplit.tla index afc10a0..798b1d4 100644 --- a/BlockingQueueSplit.tla +++ b/BlockingQueueSplit.tla @@ -101,4 +101,52 @@ THEOREM Implements == Spec => A!Spec A!vars, A!Put, A!Get, A!Wait, A!NotifyOther, A!RunningThreads <1>3. QED BY <1>1, <1>2, PTL, ITypeInv DEF Spec, A!Spec + +----------------------------------------------------------------------------- + +(* The IInv below mirrors the high-level BlockingQueue!IInv translated to *) +(* the split form: keep TypeInv!2 (Len) and the wait-set domain *) +(* constraints, the deadlock-freedom Invariant on the union, and the same *) +(* two existential clauses guarding the buffer = <<>> and full buffer *) +(* cases. *) +(* *) +(* Strictly speaking, proving DeadlockFreedom directly here is redundant: *) +(* the THEOREM Implements above already establishes Spec => A!Spec, hence *) +(* []A!Invariant transfers to BlockingQueueSplit by refinement. We prove *) +(* it locally as scaffolding/illustration of the inductive invariant. *) +IInv == + /\ Len(buffer) \in 0..BufCapacity + /\ waitSetP \in SUBSET Producers + /\ waitSetC \in SUBSET Consumers + /\ (waitSetC \cup waitSetP) # (Producers \cup Consumers) + /\ buffer = <<>> => \E p \in Producers : p \notin (waitSetC \cup waitSetP) + /\ Len(buffer) = BufCapacity => \E c \in Consumers : c \notin (waitSetC \cup waitSetP) + +(* This proof of deadlock freedom is self-contained: it only references *) +(* A!Invariant (the predicate) and never relies on BlockingQueue's *) +(* state machine (A!Init, A!Next, A!Spec) or its inductive invariant *) +(* A!IInv. *) +THEOREM DeadlockFreedom == Spec => []A!Invariant +<1> USE Assumption, ITypeInv DEF IInv, TypeInv, A!Invariant +<1>1. Init => IInv BY DEF Init +<1>2. TypeInv /\ IInv /\ [Next]_vars => IInv' + <2> SUFFICES ASSUME TypeInv, IInv, [Next]_vars + PROVE IInv' OBVIOUS + <2>1. ASSUME NEW p \in Producers, Put(p, p) + PROVE IInv' BY <2>1 DEF Put, Wait, NotifyOther, vars + <2>2. ASSUME NEW c \in Consumers, Get(c) + PROVE IInv' BY <2>2 DEF Get, Wait, NotifyOther, vars + <2>3. CASE UNCHANGED vars BY <2>3 DEF vars + <2>4. QED BY <2>1, <2>2, <2>3 DEF Next +<1>3. IInv => A!Invariant OBVIOUS +<1>4. QED BY <1>1, <1>2, <1>3, PTL DEF Spec + +(* IInv matches A!IInv up to splitting the wait-set constraint into its *) +(* Producers/Consumers components, hence implies it pointwise. Combined *) +(* with THEOREM Implements (Spec => A!Spec), this gives an alternative, *) +(* refinement-based route to deadlock freedom that does not require the *) +(* self-contained inductive proof of DeadlockFreedom above. *) +THEOREM IInvRefines == ASSUME IInv PROVE A!IInv + BY Assumption DEF IInv, A!IInv, A!TypeInv, A!Invariant + ============================================================================= From 777a7636b35a1dec9ce81fb078ed45c720bad369 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 22 Apr 2026 11:18:36 -0700 Subject: [PATCH 3/3] Prove all safety properties of (non-trivial/non-textbook) BlockingQueuePoisonApple. Co-authored-by: Claude Code 4.7 Signed-off-by: Markus Alexander Kuppe --- .github/workflows/main.yml | 2 +- BlockingQueuePoisonApple_proofs.tla | 319 ++++++++++++++++++++++++++++ 2 files changed, 320 insertions(+), 1 deletion(-) create mode 100644 BlockingQueuePoisonApple_proofs.tla diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index f290eb3..92f2d0c 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -18,7 +18,7 @@ jobs: - name: Install TLAPS run: tar -xzf tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz - name: Run TLAPS - run: tlapm/bin/tlapm --cleanfp -I CommunityModules/ BlockingQueue.tla BlockingQueueSplit.tla BlockingQueueFair.tla + run: tlapm/bin/tlapm --cleanfp -I CommunityModules/ BlockingQueue.tla BlockingQueueSplit.tla BlockingQueueFair.tla BlockingQueuePoisonApple_proofs.tla - name: Get (nightly) TLC run: wget https://nightly.tlapl.us/dist/tla2tools.jar - name: Run TLC diff --git a/BlockingQueuePoisonApple_proofs.tla b/BlockingQueuePoisonApple_proofs.tla new file mode 100644 index 0000000..db71e4e --- /dev/null +++ b/BlockingQueuePoisonApple_proofs.tla @@ -0,0 +1,319 @@ +------------------- MODULE BlockingQueuePoisonApple_proofs ------------------ +(***************************************************************************) +(* TLAPS proofs for the BlockingQueuePoisonApple module. Kept in a *) +(* separate file so that the main specification stays free of TLAPS- *) +(* related INSTANCE statements and assumptions. *) +(* *) +(* Run with *) +(* tlapm --nofp -I /path/to/CommunityModules/modules *) +(* BlockingQueuePoisonApple_proofs.tla *) +(* so that the CommunityModules theorem files *) +(* (FunctionTheorems with SumFunction theorems) are visible to TLAPS. *) +(***************************************************************************) +EXTENDS BlockingQueuePoisonApple + +INSTANCE TLAPS +INSTANCE FiniteSetTheorems +INSTANCE SequenceTheorems +INSTANCE FunctionTheorems + +ASSUME FinAssumption == + /\ IsFiniteSet(Producers) + /\ IsFiniteSet(Consumers) + /\ Poison \notin Producers + +(***************************************************************************) +(* Step 1: TypeInv is itself inductive and is therefore a stand-alone *) +(* invariant of Spec . *) +(***************************************************************************) +LEMMA TypeInvInit == Init => TypeInv + BY Assumption, FinAssumption, FS_CardinalityType, EmptySeq DEF TypeInv, Init + +LEMMA TypeInvInductive == TypeInv /\ [Next]_vars => TypeInv' +<1> USE Assumption, FinAssumption, FS_CardinalityType + DEF TypeInv, vars, NotifyOther, Wait +<1> SUFFICES ASSUME TypeInv, [Next]_vars PROVE TypeInv' OBVIOUS +<1>1. ASSUME NEW p \in Producers, Put(p, p) PROVE TypeInv' + BY <1>1, AppendProperties DEF Put +<1>2. ASSUME NEW c \in Consumers, Get(c) PROVE TypeInv' + BY <1>2, HeadTailProperties DEF Get +<1>. QED BY <1>1, <1>2 DEF Next + +LEMMA TypeCorrect == Spec => []TypeInv + BY TypeInvInit, TypeInvInductive, PTL DEF Spec + +(***************************************************************************) +(* Step 2: NoDeadlock follows from a strengthened invariant DInv that *) +(* contains the two existential clauses guarding the empty / full buffer. *) +(***************************************************************************) +DInv == + /\ NoDeadlock + /\ (buffer = <<>>) => \E p \in Producers : p \notin waitSet + /\ (Len(buffer) = BufCapacity) => \E c \in Consumers : c \notin waitSet + +THEOREM Safety == Spec => []NoDeadlock +<1> USE Assumption, FinAssumption + DEF TypeInv, NoDeadlock, DInv, vars, Wait, NotifyOther +<1>1. Init => DInv BY EmptySeq DEF Init +<1>2. TypeInv /\ DInv /\ [Next]_vars => DInv' + <2> SUFFICES ASSUME TypeInv, DInv, [Next]_vars PROVE DInv' OBVIOUS + <2>1. ASSUME NEW p \in Producers, Put(p, p) PROVE DInv' BY <2>1 DEF Put + <2>2. ASSUME NEW c \in Consumers, Get(c) PROVE DInv' BY <2>2 DEF Get + <2>. QED BY <2>1, <2>2 DEF Next +<1>. QED BY <1>1, <1>2, TypeCorrect, PTL DEF Spec + +(***************************************************************************) +(* Step 3: QueueEmpty. Strengthen QueueEmpty into the inductive QInv: *) +(* (A) Cardinality(PoisonsInBuf) + SumFunction(prod) = SumFunction(cons).*) +(* The total of the remaining producer credits prod[p] plus the *) +(* number of Poison items in the buffer equals the total of the *) +(* remaining consumer credits cons[c] . *) +(* (B) FIFO ordering. Every non-Poison item in the buffer is followed *) +(* by a Poison further back, or some producer is still active. *) +(* Together (A) and (B) force buffer to be empty whenever ap = ac = {}. *) +(***************************************************************************) + +\* Index set of Poison occurrences in the buffer. +PoisonSet(buf) == { i \in 1..Len(buf) : buf[i] = Poison } +PoisonsInBuf == PoisonSet(buffer) + +QInv == + /\ Cardinality(PoisonsInBuf) + SumFunction(prod) = SumFunction(cons) + /\ \A i \in 1..Len(buffer) : buffer[i] # Poison => + (\E p \in Producers : prod[p] > 0) + \/ (\E j \in (i+1)..Len(buffer) : buffer[j] = Poison) + +(***************************************************************************) +(* Auxiliary lemmas about PoisonSet under Append and Tail. *) +(***************************************************************************) + +LEMMA PoisonSetFinite == + ASSUME NEW buf \in Seq(Producers \cup {Poison}) + PROVE IsFiniteSet(PoisonSet(buf)) + BY FS_Interval, FS_Subset DEF PoisonSet + +LEMMA PoisonAppendOther == + ASSUME NEW buf \in Seq(Producers \cup {Poison}), + NEW x \in Producers \cup {Poison}, x # Poison + PROVE PoisonSet(Append(buf, x)) = PoisonSet(buf) + BY AppendProperties, LenProperties DEF PoisonSet + +LEMMA PoisonAppendPoison == + ASSUME NEW buf \in Seq(Producers \cup {Poison}) + PROVE /\ PoisonSet(Append(buf, Poison)) = PoisonSet(buf) \cup {Len(buf) + 1} + /\ Cardinality(PoisonSet(Append(buf, Poison))) + = Cardinality(PoisonSet(buf)) + 1 +<1>1. PoisonSet(Append(buf, Poison)) = PoisonSet(buf) \cup {Len(buf) + 1} + BY AppendProperties, LenProperties DEF PoisonSet +<1>2. (Len(buf) + 1) \notin PoisonSet(buf) + BY LenProperties DEF PoisonSet +<1>. QED BY <1>1, <1>2, PoisonSetFinite, FS_AddElement + +LEMMA PoisonTail == + ASSUME NEW buf \in Seq(Producers \cup {Poison}), buf # <<>> + PROVE Cardinality(PoisonSet(Tail(buf))) + = Cardinality(PoisonSet(buf)) - (IF Head(buf) = Poison THEN 1 ELSE 0) +<1> USE FinAssumption +<1> DEFINE n == Len(buf) +<1> DEFINE Shift == { j \in 2..n : buf[j] = Poison } +<1>1. /\ Len(Tail(buf)) = n - 1 /\ n \in Nat /\ n >= 1 + /\ \A i \in 1..(n-1) : Tail(buf)[i] = buf[i + 1] + /\ Head(buf) = buf[1] + BY HeadTailProperties, LenProperties, EmptySeq +<1>2. IsFiniteSet(Shift) + BY FS_Interval, FS_Subset +<1>3. PoisonSet(Tail(buf)) = { i \in 1..(n - 1) : buf[i + 1] = Poison } + BY <1>1 DEF PoisonSet +<1>4. Cardinality(PoisonSet(Tail(buf))) = Cardinality(Shift) + <2> DEFINE f == [i \in PoisonSet(Tail(buf)) |-> i + 1] + <2>1. f \in Bijection(PoisonSet(Tail(buf)), Shift) + <3>1. f \in [PoisonSet(Tail(buf)) -> Shift] BY <1>3, <1>1 + <3>2. \A i, j \in PoisonSet(Tail(buf)) : f[i] = f[j] => i = j BY <1>3 + <3>3. \A k \in Shift : \E i \in PoisonSet(Tail(buf)) : f[i] = k + <4> SUFFICES ASSUME NEW k \in Shift + PROVE \E i \in PoisonSet(Tail(buf)) : f[i] = k + OBVIOUS + <4>1. (k - 1) \in PoisonSet(Tail(buf)) /\ f[k - 1] = k + BY <1>3, <1>1 + <4>. QED BY <4>1 + <3>. QED BY <3>1, <3>2, <3>3, Fun_IsBij + <2>2. IsFiniteSet(PoisonSet(Tail(buf))) + BY <1>3, <1>1, FS_Interval, FS_Subset + <2>. QED BY <2>1, <2>2, FS_Bijection DEF ExistsBijection +<1>5. CASE Head(buf) = Poison + <2>1. PoisonSet(buf) = Shift \cup {1} + <3> SUFFICES ASSUME NEW i \in 1..n + PROVE (buf[i] = Poison) <=> (i \in Shift \/ i = 1) + BY DEF PoisonSet + <3>. QED BY <1>1, <1>5 + <2>. QED BY <2>1, <1>4, <1>5, <1>2, FS_AddElement, FS_CardinalityType +<1>6. CASE Head(buf) # Poison + <2>1. PoisonSet(buf) = Shift + <3> SUFFICES ASSUME NEW i \in 1..n + PROVE (buf[i] = Poison) <=> i \in Shift + BY DEF PoisonSet + <3>. QED BY <1>1, <1>6 + <2>. QED BY <2>1, <1>4, <1>6, <1>2, FS_CardinalityType +<1>. QED BY <1>5, <1>6 + +(***************************************************************************) +(* The QInv components are well-typed. *) +(***************************************************************************) +LEMMA QInvTypes == + ASSUME TypeInv + PROVE /\ SumFunction(prod) \in Nat + /\ SumFunction(cons) \in Nat + /\ Cardinality(PoisonsInBuf) \in Nat + BY FinAssumption, FS_CardinalityType, SumFunctionNat, PoisonSetFinite + DEF TypeInv, PoisonsInBuf + +(***************************************************************************) +(* Main inductive proof. *) +(***************************************************************************) +THEOREM QueueEmptyTheorem == Spec => QueueEmpty +<1> DEFINE Inv == TypeInv /\ QInv +<1> USE Assumption, FinAssumption, FS_CardinalityType + DEF TypeInv, vars, NotifyOther, Wait, ap, ac, QueueEmpty, QInv +<1>1. Init => Inv + <2> SUFFICES ASSUME Init PROVE Inv OBVIOUS + <2>1. TypeInv BY EmptySeq DEF Init + <2>2. PoisonsInBuf = {} /\ Cardinality(PoisonsInBuf) = 0 + BY EmptySeq, FS_EmptySet DEF PoisonsInBuf, PoisonSet, Init + <2>3. SumFunction(prod) = Cardinality(Consumers) * Cardinality(Producers) + BY SumFunctionConst DEF Init + <2>4. SumFunction(cons) = Cardinality(Producers) * Cardinality(Consumers) + BY SumFunctionConst DEF Init + <2>. QED BY <2>1, <2>2, <2>3, <2>4, EmptySeq DEF Init +<1>2. Inv /\ [Next]_vars => Inv' + <2> SUFFICES ASSUME Inv, [Next]_vars PROVE Inv' OBVIOUS + <2>0. TypeInv' BY TypeInvInductive + <2> USE QInvTypes DEF Inv + <2>1. ASSUME NEW p \in Producers, Put(p, p) PROVE QInv' + <3> USE <2>1 + <3>0. /\ prod \in [Producers -> 0..Cardinality(Consumers)] + /\ buffer \in Seq(Producers \cup {Poison}) + /\ p \in Producers \cup {Poison} + /\ DOMAIN prod = Producers + BY DEF TypeInv + <3>1. CASE /\ Len(buffer) < BufCapacity + /\ buffer' = Append(buffer, p) + /\ UNCHANGED prod + /\ NotifyOther(Consumers) + /\ UNCHANGED <> + <4> USE <3>1 + <4>1. p # Poison BY DEF TypeInv + <4>2. PoisonsInBuf' = PoisonsInBuf + BY <4>1, <3>0, PoisonAppendOther DEF PoisonsInBuf + <4>3. \A i \in 1..Len(buffer') : buffer'[i] # Poison => + (\E q \in Producers : prod'[q] > 0) + \/ (\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison) + BY DEF Put + <4>. QED BY <4>2, <4>3 + <3>2. CASE /\ Len(buffer) < BufCapacity + /\ buffer' = Append(buffer, Poison) + /\ prod' = [ prod EXCEPT ![p] = @ - 1] + /\ NotifyOther(Consumers) + /\ UNCHANGED <> + <4> USE <3>2 + <4>1. SumFunction(prod') = SumFunction(prod) - 1 + BY <3>0, SumFunctionExcept + <4>2. Cardinality(PoisonsInBuf') = Cardinality(PoisonsInBuf) + 1 + BY <3>0, PoisonAppendPoison DEF PoisonsInBuf + <4>3. \A i \in 1..Len(buffer') : buffer'[i] # Poison => + \E j \in (i+1)..Len(buffer') : buffer'[j] = Poison + <5> SUFFICES ASSUME NEW i \in 1..Len(buffer'), buffer'[i] # Poison + PROVE \E j \in (i+1)..Len(buffer') : buffer'[j] = Poison + OBVIOUS + <5>1. /\ Len(buffer') = Len(buffer) + 1 + /\ buffer'[Len(buffer) + 1] = Poison + BY AppendProperties, <3>0 + <5>2. (Len(buffer) + 1) \in (i+1)..Len(buffer') BY <5>1 + <5>. QED BY <5>1, <5>2 + <4>. QED BY <4>1, <4>2, <4>3 + <3>3. CASE /\ Len(buffer) = BufCapacity + /\ Wait(p) + /\ UNCHANGED prod + /\ UNCHANGED <> + BY <3>3 DEF Wait, PoisonsInBuf, PoisonSet + <3>. QED BY <3>1, <3>2, <3>3 DEF Put + <2>2. ASSUME NEW c \in Consumers, Get(c) PROVE QInv' + <3> USE <2>2 + <3>0. /\ cons \in [Consumers -> 0..Cardinality(Producers)] + /\ buffer \in Seq(Producers \cup {Poison}) + /\ DOMAIN cons = Consumers + BY DEF TypeInv + \* Helper for the FIFO part of QInv: when buffer' = Tail(buffer), any + \* non-Poison item in buffer' shifts down from a non-Poison item in + \* buffer that was witnessed by a Poison further back. + <3>F. ASSUME /\ buffer # <<>> + /\ buffer' = Tail(buffer) + /\ UNCHANGED prod + PROVE \A i \in 1..Len(buffer') : buffer'[i] # Poison => + (\E q \in Producers : prod'[q] > 0) + \/ (\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison) + <4> USE <3>F + <4>1. /\ Len(buffer') = Len(buffer) - 1 + /\ \A k \in 1..Len(buffer') : buffer'[k] = buffer[k+1] + BY HeadTailProperties, <3>0 + <4> SUFFICES ASSUME NEW i \in 1..Len(buffer'), buffer'[i] # Poison + PROVE (\E q \in Producers : prod'[q] > 0) + \/ (\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison) + OBVIOUS + <4>2. (i+1) \in 1..Len(buffer) /\ buffer[i+1] # Poison + BY <4>1 + <4>3. (\E q \in Producers : prod[q] > 0) + \/ (\E j \in (i+2)..Len(buffer) : buffer[j] = Poison) + BY <4>2 + <4>4. ASSUME NEW j \in (i+2)..Len(buffer), buffer[j] = Poison + PROVE \E j2 \in (i+1)..Len(buffer') : buffer'[j2] = Poison + <5>1. (j-1) \in (i+1)..Len(buffer') /\ buffer'[j-1] = buffer[j] + BY <4>1 + <5>. QED BY <5>1, <4>4 + <4>. QED BY <4>3, <4>4 + <3>1. CASE /\ buffer # <<>> + /\ buffer' = Tail(buffer) + /\ NotifyOther(Producers) + /\ Head(buffer) # Poison + /\ UNCHANGED <> + <4> USE <3>1 + <4>1. PoisonsInBuf' = PoisonSet(Tail(buffer)) BY DEF PoisonsInBuf + <4>2. Cardinality(PoisonsInBuf') = Cardinality(PoisonsInBuf) + BY <3>0, PoisonTail, <4>1 DEF PoisonsInBuf + <4>. QED BY <4>2, <3>F + <3>2. CASE /\ buffer # <<>> + /\ buffer' = Tail(buffer) + /\ NotifyOther(Producers) + /\ Head(buffer) = Poison + /\ cons' = [ cons EXCEPT ![c] = @ - 1] + /\ UNCHANGED <> + <4> USE <3>2 + <4>1. SumFunction(cons') = SumFunction(cons) - 1 + BY <3>0, SumFunctionExcept + <4>2. /\ PoisonsInBuf' = PoisonSet(Tail(buffer)) + /\ Cardinality(PoisonSet(Tail(buffer))) + = Cardinality(PoisonSet(buffer)) - 1 + BY <3>0, PoisonTail DEF PoisonsInBuf + <4>. QED BY <4>1, <4>2, <3>F DEF PoisonsInBuf + <3>3. CASE /\ buffer = <<>> + /\ Wait(c) + /\ UNCHANGED <> + BY <3>3 DEF Wait, PoisonsInBuf, PoisonSet + <3>. QED BY <3>1, <3>2, <3>3 DEF Get + <2>3. CASE UNCHANGED vars + BY <2>3 DEF PoisonsInBuf, PoisonSet + <2>. QED BY <2>0, <2>1, <2>2, <2>3 DEF Next +<1>3. Inv => (ap \cup ac = {} => buffer = <<>>) + <2> SUFFICES ASSUME Inv, ap \cup ac = {}, buffer # <<>> PROVE FALSE OBVIOUS + <2>1. /\ \A p \in Producers : prod[p] = 0 + /\ \A c \in Consumers : cons[c] = 0 + OBVIOUS + <2>2. SumFunction(prod) = 0 /\ SumFunction(cons) = 0 + BY <2>1, SumFunctionZero + <2>3. PoisonsInBuf = {} + BY <2>2, QInvTypes, FS_EmptySet, PoisonSetFinite DEF PoisonsInBuf + <2>4. 1 \in 1..Len(buffer) /\ buffer[1] # Poison + BY <2>3, EmptySeq DEF PoisonsInBuf, PoisonSet + <2>. QED BY <2>1, <2>3, <2>4 DEF PoisonsInBuf, PoisonSet +<1>. QED BY <1>1, <1>2, <1>3, PTL DEF Spec + +=============================================================================