From 97775065c93a841a61c1e7b663552dc893f2dd83 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 10:24:18 +0000 Subject: [PATCH 01/36] feat: a section about validating lean proofs --- Manual/Elaboration.lean | 4 + Manual/ValidatingProofs.lean | 201 ++++++++++++++++++++++++ static/screenshots/doublecheckmarks.png | Bin 0 -> 33104 bytes static/theme.css | 11 ++ 4 files changed, 216 insertions(+) create mode 100644 Manual/ValidatingProofs.lean create mode 100644 static/screenshots/doublecheckmarks.png diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index 31d36edcb..e38e5b183 100644 --- a/Manual/Elaboration.lean +++ b/Manual/Elaboration.lean @@ -8,6 +8,8 @@ import VersoManual import Manual.Meta import Manual.Papers +import Manual.ValidatingProofs + open Verso.Genre Manual open Verso.Genre.Manual.InlineLean @@ -464,3 +466,5 @@ builtin_initialize $x:ident : $t:term ← $cmd* ``` ::: + +{include 0 Manual.ValidatingProofs} diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean new file mode 100644 index 000000000..1808d63a0 --- /dev/null +++ b/Manual/ValidatingProofs.lean @@ -0,0 +1,201 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Joachim Breitner +-/ +import VersoManual + +import Manual.Meta + +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean + +set_option pp.rawOnError true +set_option guard_msgs.diff true + +open Lean (Syntax SourceInfo) + +#doc (Manual) "Validating a Lean Proof" => +%%% +file := "ValidatingProofs" +tag := "validating-proofs" +%%% + +This section discusses how to validate a proof expressed in Lean. + +Depending on the circumstances, additional steps may be recommended to rule out misleading proofs. +In particular, it matters a lot whether one is dealing with an honest proof attempt, and needs protection against only benign mistakes, or a possibly-malicious proof attempt that actively tries to mislead. + +In particular, we use “honest” when the goal is to create a valid proof. +This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system. + +In contrast, we use “malicious” to describe code to go out of its way to trick or mislead the user, exploit bugs or compromise the system. +This includes unreviewed AI-generated proofs and programs. + +Furthermore it is important to distinguish the question “does the theorem have a valid proof” from “what does the theorem statement mean”. + +Below, an escalating sequence of checks are presented, with instructions on how to perform them, an explanation of what they entail and the mistakes or attacks they guard against. + +# The blue double check marks + +In regular everyday use of Lean, it suffices to check the blue double check marks next to the theorem statement for assurance that the theorem is proved. + +## Instructions + +While working interactively with Lean, once the theorem is proved, blue double check marks appear in the gutter to the left of the code. + +:::figure "A double blue check mark" +![Double blue check marks appearing in the editor gutter](/static/screenshots/doublecheckmarks.png) +::: + +## Significance + +The blue ticks indicate that the theorem statement has been successfully elaborated, according to the syntax and type class instances defined in the current file and its imports, and that the Lean kernel has accepted a proof of that theorem statement that follows from the definitions, theorems and axioms declared in the current file and its imports. + +## Trust + +This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and trusts the authors of the imported libraries to be honest, that they performed this check, and that no unsound axioms have been declared and used. + +## Protection + +This check protects against + +* Incomplete proof (missing goals, tactic error) *of the current theorem* +* Explicit use of `sorry` *in the current theorem* +* Honest bugs in meta-programs and tactics +* Proofs still being checked in the background + +## Comments + +In the Visual Studio Code extension settings, the symbol can be changed. +Editors other than VS Code may have a different indication. + +Running `lake build Module`, where `Module` refers to the file containing the theorem, and observing success without error messages or warnings provides the same guarantees. + +# Printing axioms + +The blue double check marks appear even when there are explicit uses of `sorry` or incomplete proofs in the dependencies of the theorem. +Because both `sorry` and incomplete proofs are elaborated to axioms, their presence can be detected by listing the axioms that a proof relies on. + +## Instructions + +Write `#print axioms thmName` after the theorem declaration, with `thmName` replaced by the name of the theorem and check that it reports only the built-in axioms `propext, Classical.choice, and Quot.sound.`. + +## Significance + +This command prints the set of axioms used by the theorem and the theorems it depends on. +The three axioms above are standard axioms of Lean's logic, and benign. + +* If `sorryAx` is reported, then this theorem or one of its dependencies uses `sorry` or is otherwise incomplete. +* If `Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion. +* Any other axiom means that a custom axiom was declared and used, and the theorem is only valid relative to the soundness of these axioms. + +## Trust + +This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and one trusts the authors of the imported libraries to be honest. + +## Protection + +(In addition to the list above) + +* Incomplete proofs +* Explicit use of `sorry` +* Custom axioms + +## Comments + +At the time of writing, the `#print axioms` command does not work in a `module`. +To work around this, create a non-module file, `import` your module, and use `#print axioms` there. + +# Re-checking proofs with lean4checker + +There is a small class of bugs and some dishonest ways of presenting proofs that can be caught by re-checking the proofs that are stored on file when building the project. + +## Instructions + +Build your project using `lake build`, run `lean4checker --fresh` on the module that contains the theorem of interest and check that no error is reported. + +## Significance + +The lean4checker tool reads the declarations and proofs as they are stored by `lean` during building (the `.olean` files), and replays them through the kernel. +It trusts that the olean files are structurally correct. + +## Trust + +This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and believes the authors of the imported libraries to not be very cunningly malicious, and to neither compromise the user’s system nor use Lean’s extensibility to change the interpretation of the theorem statement. + +## Protection + +(In addition to the list above) + +* Bugs in Lean’s core handling of the kernel’s state (e.g. due to parallel proof processing, or import handling) +* Meta-programs or tactics intentionally bypassing that state (e.g. using low-level functionality to add unchecked theorems) + +## Comments + +Since `lean4checker` reads the `.olean` files without validating their format, this check is prone to an attacker crafting invalid `.olean` files (e.g. invalid pointers, invalid data in strings). + +Lean tactics and other meta-code can perform arbitrary actions when run. +Importing libraries created by a determined malicious attacker and building them without further protection can compromise the user's system, after which no further meaningful checks are possible. + +We recommend running `lean4checker` as part of CI for the additional protection against bugs in Lean's handling of declaration and as a deterrent against simple attacks. +The [lean-action](https://github.com/leanprover/lean-action) Github Action provides this functionality by setting `lean4checker: true`. + +Without the `--fresh` flag the tool can be instructed to only check some modules, and assume others to be correct (e.g. trusted libraries), for faster processing. + +# Gold standard: `comparator` + +To protect against a seriously malicious proof compromising how Lean interprets a theorem statement or the user's system, additional steps are necessary. +This should only be necessary for high risk scenarios (proof marketplaces, high-reward proof competitions). + +## Instructions + +In a trusted environment, write the theorem *statement* (the ”challenge”), and then feed the challenge as well as the proposed proof to the [`comparator`](https://github.com/leanprover/comparator) tool, as documented there. + +## Significance + +Comparator will build the proof in a sandboxed environment, to protect against malicious code in the build step. +The proof term is exported to a serialized format. +Outside the sandbox and out of the reach of possibly malicious code, it validates the exported format, loads the proofs, replays them using Lean's kernel, and checks that the proved theorem statement matches the one in the challenge file. + +## Trust + +This check is meaningful if the theorem statement in the trusted challenge file is correct and the sandbox used to build the possibly malicious code is safe. + +## Protection + +(In addition to the list above) + +* Actively malicious proofs + +## Comments + +At the time of writing, `comparator` uses only the official Lean kernel. +In the future it will be possible to use multiple, independent kernel implementations easily; then this will also protect against implementation bugs in the official Lean kernel. + +# Remaining issues + +When following the gold standard of checking proofs using comparator, some assumptions remain: + +* The soundness of Lean’s logic. +* The implementation of that logic in Lean’s kernel (for now; see comment above). +* The plumbing provided by the `comparator` tool. +* The safety of the sandbox used by `comparator` +* No human error or misleading presentation of the theorem statement in the trusted challenge file. + +# On Lean.trustCompiler + +Lean supports proofs by native evaluation. +This is used by the `decide +native` tactic or internally by specific tactics (`bv_decide` in particular) and produces proof terms that call compiled Lean code to do a calculation that is then trusted by the kernel. + +Specific uses wrapped in honest tactics (e.g. `bv_decide`) are generally trustworthy. +The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted. + +General use (`decide +native` or direct use of `ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the Kernel's evaluation. +In particular, all `implemented_by`/`extern` attributes in libraries become part of the trusted code base. + +All these uses show up as an axiom `Lean.trustCompiler` in `#print axioms`. +External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler. +When that level of checking is needed, proofs have to avoid using native evaluation. + +All these uses show up as an axiom `Lean.trustCompiler` in `#print axioms`. External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler. When that level of checking is needed, proofs have to avoid using native evaluation. diff --git a/static/screenshots/doublecheckmarks.png b/static/screenshots/doublecheckmarks.png new file mode 100644 index 0000000000000000000000000000000000000000..4f23cf00fc67a3be15eea11c0a80454b1e8c6ccb GIT binary patch literal 33104 zcmaf*1ymeO+olJCdvJGmcM0z9?lLgATX1*xgy8NB?yd>$?jAfq2ut4Y`(^jvJ$vSy znV#yd?&^A;>Y2LkyE{rnNg5de9{~UWAj`@~r~v?w!|%(DaFFls&_0T7?;oV*GHQwd zfDbhQ5Eu#oJiiwO9s>aGtN_5N2>`&K2>{?Y<+iH|zOR5Wlb4nNy#0OUca^5Rm!O%O zDtQ0^uz>&oRNeb`J^%oM(uil|<$W&zSqV`Muhok@UjudNhhAm2VFKt*(IWVm^!x(Z z`fQyJ>T0{LDy@*!ud>x?P0jdv_I)1uvzIj%FLhB`(E1F(GYa<^C*C_izR+O}b+lCL2~=Dpy3gI@qDr%6?;zw#i z2JL;iwbC(O7N0Cc_!S>Bt1dVf0|j_t_{Kx>K6V+_NxrvoKa1C>20J zg(-VI4@r~biqirBs;UDvXo*5y1K*eTXpJYw%cJmL=o>9h1ji7!b>lMc&PAU1p9E-!TN&KOGtS#{im){Rm7mW2)<=rj4jkiF=e$^tjP&rB)0fc`Npj|S5QO!W0(cIqwD@QrjS`xWrUTYcU@BjxD zzcF(|kXA*rmB#fb>kq~eqZj4=sipK>-ygCa)NrVhQ0^%@3SR?i0;YdwsXmkg(~!IL zPEc@R>9nTCpTlpV+XGUudHm+=*6#yz9>?MLCw;fMN(@vbZ_BpCk8o_fsh!nQCzb6M zgysLV25n;p;*LrUz)Kd7*KzYv_o81rptPLgkghBF8T9Ez*Akh7L&_H0S{nJZ9KR?hG{ksaRip)PX zp!!ks6aP6J+NSBoZ+3SaPftrbnr72JJQjhnx-9wHA>RE%9CS&3-?BSfB5VfAEZn_@g zC+y;%H&9Kw~zf7OJBrh_Bh>J*9UKC|*b|aS{YIGRCA9upe|SNBZmH zah8d=n0?bW;I|tOx2Ww~LdX0KjM=|o2XY>ut3AGMJH4lWV(Fi}u1dk|Okq!EilR+t zsTNP;l9UENHlDj_Yu}F^xJv2Ept#;sRwMJ4Hi&*5{~Gx_iZ~^l6?uv}W*k|_Mc6Y1 z`~dF6frXOAvoG%Ci>h6wmGV~v=r0N|~ zz`p&2qbA5ufI8JHAkUmsFST%;^X}57K6Umq0T$6%4V{aP+QfTx6$|OI za^v7-+g8$1zR^k{y5OS7LE*V&Cy$LKpH;4YbF>qI8o4y{#I|e zD&;@BimOWpWJr$DRCtcyERoAq-924aki90zyjvjbQ!1V*<-OqUfA3ivWmG{ zKu)i|d?{U4r$0A*$FZbMT}UVccCAH}tW7@sJ7K=%49%Z*A%DsRRm-7U53fDitf!0cGgCsvM;<&-zk znDU!rqCUQ?ev(=PTX=cVj0kom14Qq)=>iTnctV67J zePLaplQHYLp%&W122sNzmz=9XUC>RybQNV}u5msdKgQNm(E5Gf(HK26Ym1-Zs?`{l z;LNn<%r)TYMyiXJlp{<01)u5hnHUC6XJ{;&lxUiD1}_ZfBy~%HA4g`ORx2p|?fOou zS6&7?k@zpfeI~=bt{sXOcPt%!eY@N(?T&-}7<9idt*wUHHS8m1zBhNuMZQq8{PNtd z%KM@OcadG-WamQC|E0+YZqAZFnS689lpc7O0G<3BTlupz@UEik4h16jSH9WB5u2bp z<&U2~{%q!5aAlejB2C8A11eUI0kKWEhP|lZ6&Vv`QwV?;<2WOEmrgy?OL!o8%amA+nt=~opV6-LFx2HU%FgJOx1 zMkcf!0H6pcB1%XjnS!;7TXI{VXO#HKV2VwcX%NqVcwc86!iiL#ostiKx~V`A0?`25 zPDtOYR2l@b@Yzh}ByEUte84wLIdY&8fwbgs)yoOqPiRXuEy0RXg3 z8(Mp*_T{h=N;!nA+`lNahgeWrqiY13M9Im`bFa>KpwI8viVOD8N#hT9rWEObVCF9C zRs&6f6dR4nU1e`KCn;%7{xrkI$XG((SCN&84UxOzCq4@a;uYmsBeDSi_>Dj`P-}lH zV>6v!GZ6+2=H`05l6law%J)>k8l_>-s$UzZCHF;&S`-2>TbCfitAy}X<)F?mNalj~J#UrE(HM17CkVFa8ypl`mh)f+j zZ8DjaYRLZHKA%j8MV!ItFZV_G2at2jg3kR@+4}77>sD zaY0quH?2bV7~tZLm7_^VC2&2KdPgy zjg&BLPMpV1FjjQpkjeFx_)`mrvfP4(X?OaD+{PTR{2PQ*1`2q9GGTh1TtoPD%3r^Z z6)z)GXMsAP()VSYYvr|z=TaLeVvw+|` zK_34aRl@KU1}2yoIrnHZ_FqO#*BAHL0GTy!U9pd22lSjN0v*(sB+bLl&D*0gqik?T zC&?82yd)2M&*%;*X&p^l2>U!4FN+1;{;LA;bCy3o!iQyY3eTZUQ4;Ar{edC_vQBpv ze)3r`x(rEtpDNWXr8K8KxLPNi#d}dtlJR1aOh3Tr@WvqXapM3oV@08Y2;wX)Y>PHF zNB6^a044&=^0jER={Cs&0Dz8iS$$=0Cel$ zWt{LCn~XKVc{L*of<9Ozr>EgMkAG#DMi}@O9`(Vb52U5N)M1M|8%zM zH-2HaaKQxtDEOw;($B3^?9dTmXI1j&VPxGAIl^!OKc6W0_I>)di|ew7*CtK?loYW; zr)JEDi!~=G%So+@ZLS#XeinEerYpCygDv7AM826gbLw2&oa>JRyQ% z8#Z5@MtT2^;Nfeg!gGe{~TwWB*?JcLr!V8SKukas3~KUyw1^& zlOM&e{g8yjam%VsdPqdTQSfqL#R$^6F<2&NVyD%nDGXlnW9C6{lG_TX*DL}eaNuW3 zQY<<=Y%&wzh)h_^w8^J27?om>!rA|eN~dx$Q+<28Oh5TBdiA{ps-V1+=i1KPHVK zeSdN)?|GykezsN>KZ6R@K2IJ)W^7!X0tHx?&!5TVsd_C7ElEW~^`^y6VG0PJ)0~`EUbKR5}Gi(-2~UX=sUcL zdi1}l%i+XP{Jx!Bz*L@JRuHkOM4_Jx@DMB9*fjl;WN|wmon*+DE)__sXUArP2?#vw zJMa-#DvuG68oX&LGZKm+7-}-)_N~2pkR!kwH-mm+R)|H51I9_HRTbyTVnG<1J5bb(NvM<+?)bPBBLLz>h()$zu} zI&h?r(TMTVSu0?dY)D$x2SecJq43CRQ4Uopoo3R{2*{gKPPeeemsBcQ$|RJw2I~xF z?l=9?fb2>0tJ4y(s`Y?OTQWrt5wk{yl5a)~9I~t%Bd@F`Zb@zQN@z5sxwqnxWocoj z@an4f=^5Ay9x0iUPx=ZrLkfb{O{}b2?8<~co9R6}IsGnUgQCF?e<>f-geg`^*M;e{ z34S4sA?h2H=f8);eL*#ZwKf1J`fF6P#>^))j7`u>CZ%MGaps@{J-uY+L{VN%Mmob^ z>N>MJl^~%@-IX&h99Jvg!*lUc2_$Fo_F4yC5ilUQNux}+0E7FUhq&4_pu=5;DQoE&-$JFW(@E{Na!5^g z5O4SZd7nQ4ulhg|titR_`bi~$pujU9HUEA5i*q~~W^V4*b;#n57QO6q5(I(n?CWMV zX%&~R5}E5txIEFBn>9~uu}2@${wlktJOaRC&! zeNzU4_%Mm%CaKBz<&i~7)rlVq#7x4o0c<*z168r9nV#KNz8q?o9xEUjFy|y}#t+4r ztkSy;yYTZwhe;zWV-4rZYr!4WhxlxwbwP*pSq6)0uj^^gUN*gGX126ccqqqXWuLR7 z#cumnLjIwYE1d4 ziHC&cW+rBKrjS@Ue)$?0chSnop=0W|U~mKO+K=mG3idE7Lhq-Ybdoba>r)|Q$PMeL z;!&P;H_j9#bl_c{KGQdz4Z_cvTDs_gVLvu`Tu?D3#enUoZlKaFoch_={0axN!taL> z+Gt)BU77+NXC=?KezY!@xvmOTDObtdmXb=xS?0;-J75GUpDz||XYEn-2D+FQr}<3( zvamzT#A*Lx?QosXmXf_W*ZI0)6wVb2eIRxFNtmVSM0dri6Xa;vH*#oQ1ap?sB9|IQ zZC5~W>SH;B#ipS5WR;c7P?Zt(x;aNb)p!Z@l|H3;~#$yP^ zjW3COI5}}f(4ABJX+rFouV@Uiltggq^%~#>n{`n|P9Z_vV6fX?}n!s5S*{H2-)5|IeUbgIBW~&D=!+1x>(3|S{L*yZ{#vtLKtPK zT{K`K7H$gV8pIt2Q|5+W>L}B>*n{-H7A}9ar*Byyq<)nR;env$NQFmn_eokf0OKoJ zQ`%!!`p4eZ9b24y@_#07W;4je-Dw=HmkA;r%^&~H&Bqwt4-!vVHB*2YDtY@lu5sX! zdb03>4&~i_Zm|qk zL?FVm9?Q$V!KaXYA?;_toZYZhZ(DHV7f(*Bdc6M_n?#BP2HxzivgcH46Qa9-4epoy&*Lyy5xN{uC_ic<|9HoI=JW$)R=C6&r2sYW2sa z7moz-OJ`cl>yO)WN66YKe7u_Tya9Kb8dQlD^4iuJa092FAFl0CFQ|H<=!C}W0^Z+1Z}ArXyP#5k;8>!bh^c=D_opN1!7H9+sLXi1m_ z8CFagDEfGl48e|YafuzH1H#h9Da`&bw-XOyhLEwfZ*}1ecZh0TIk~-2P$8xjy`SZ% z$H|l9b@>v`kdzT~90>;xB@-9rXs%Eh0VWdHS(@1TxCs{noFAFxeiTWsYVtu&O9gp- zl{3Da+T#+x(P)Qrq0G@ezbHR7UIE73?C<1>Qw|r}PML#TgEAla5=N8kK7)PsK0Cv- zlw%vve?n94t1J9tE2^-Tx1lN@ltOXr&~P5E9C8D7%MqWbTvl-NA52%;)@9c7LXBx}%rVGxn>e@dk)^NKB^^^Ipf>;jGG*8}@Om=Ib-tsYt7g?% zY)l~Z+qs%tt5L8*!bI-^Lnn*Oq_HihUS+GUg^UMF1A$StqoKz<9YXy$mO z=e5*U%!=3FCN+Thd*-+hk5jgwcvJ-{ZFLaE$)OKDRx;{14cN?8qWO>Bglz= z2}zw-A7nxU$P6_pv7@)7a}*wQ$hnwtmxY4vbTW%3B!{khr|Xh6QP?wQUUSk%%{=tx zlHJwb9yp0JLI!b#9cxd1Tw>DJDZGNnD9ZRqCY;Mzm*@>OiXv~+R}5Bmr(DkI3J*Vq zi-fJnw9E9ulIwTYo>2LoK>x5FK-&Nes0z-=l7Hx6N+d?aKy(v?0O;7D?!r3(6M(kn zMP@xO(g@SX!yX&=!@1}Ny!BM?!Vbc8oW%@8>5J;bwS*?5=?aZndi!s>Nm8UCj7Nbk zE0(T*Fup{-(^^%A;>yd=7!~0PrsMk`GdK-y*cPiJ>tiC6*$)*YC6+GL*}hlvVF!r+*)aSI*{t@}Z2mi=9VY-4>k0 zoX@JW6B@~oA~ZgvnnRY@^$YU9^n-tDzl#a~Q!9Aa6+{BX{-vs*eFlVK{+IZ0Ngv0o zEtCxTt|;8u%be9~C&#}oPYqhyrF5^kw}{AKqP^=2JoQ8$Z^7e8o)>4?MRdx&226<= z$^NqR8wCo}Pl+@=evVkHY1Q9mJS&GHl- z+igF_UN{Nb+eh!j8?$vOiW_K6+}!oVT$UxQ$%pOqcBZ;wZOF(5k68Ijx^0hkT>-Bo z0OHYlBk->^2_kwF^7>CL3Bu|Z!di>>EfE`~9yPvuwP)Q=Pk(qmrhiHyuE{tbt@FB6 zg2>fGfd#tGufIjdALA!%sO~jrujGCH-Zo=d>(b`;=EZLtsnp7Br#XaubfrS=j}R-w zrq7dCy+mC>@23S6JiX!{bIG<0npgAqIuV6lMv(OXqV_Fw-~;W1^QU1cc;x52Uu5CO zz&LM?B!f@5du>52=sR$V*U>Mt>*-MgB;(XiH}2dBE?yml(Q zGd#V^7>&0-{cE-_-Ews1*V@C(ky3xYC^6=p3!7B4Dg9pcosgLGE-awHtM3G|C`DBW zY3s~8=kGorh_7{fDtTp-VAZ)SSjT9?r-spA`|t}ML?0i7=``P<} zMDS;C1n1!hq~(j~!Y<_@jPAoV<)$saYvZ~KFtO77xRP(Ta1ku0ah%q%>-~=gFp*r& z;wvy}DnO|GT}{B2v0~#ocY$-2Ug`H2kiP5Pv6|x*Z^epDvgHpbSo=*b3;RZ!BL=G3vu;GCj$(T6#vC90ma z=c<9-kk?femz0(aCU4UjDhiM>uNcImGU72SoN!UgDgZ8eE2T58%^2Y?#>Tl_%c9#V zoH}B7*`08{hv@q!u$`H9IlW~EsTJ0HN05%$xOgw1Eh2HH)D#Wv=Zw1Wm1Y9>7&M>4D1yBx>smVCN7+|5t7$B*5sEJtDGj`bjuWKE1vc}YIWGlcAz+oX;8vQ zjW2|6(vIV{Ot008qFeOr-*uIyMtGP*N+Wy~KLCXuiSs|oKk zyky4Wy`8%|+#fg=xY_KrDlsk53-_UZ-SsjRvM5}mVEInhCjh|063i)Yi%Y8(>3%w* z15TMO+T#}C!~g_x`FlpQX%wNIxvRrlo2vB_`^&c(zz~UIW@cfqBg;>Q1L2ungPnTH zLwd?RapQJ>`NKR9Al&~ZytjzT_Xfmqo+~H*ftziUT4Q%r5^Knx$>+DcUo!aUEv)-n zBzfEVl*;zxQ;JzBZ6P555R)#~&x9XSoCj64N{;9WB46u>t(Fcmlee439;!Lag$R6Y z?bd}z&zg(aI^Q=47YhAU>MlubJf!$%z4B_RwRS>U^!9TJ6EacJukklv$Lz{bHf&D0>{#yw(yQ)Aj7 z<8Xu1kzLYMjMgh6haQ9HYj4AAn8^jVFWD4zG%wq<9YW{XA}MAtBxe&DaYDVz0NKV& ze)k_sAbwsBglI!IwoEt-bE4-42_z2Ev zkfsx#*w`7Kb+*KxEtahMt8Vo@t*;t&x+=C{Yb#GJ`<&~FIqv*iJP>>-hY~3HeMxk2 z<;MRsTP)85DdTT=!R0%4{pR=D2Yc4YIPGCwk?_W_S4)t=#;4+3m2T6<1_8u;rChAymp)Z{38B0rDfH2$*arWF!D=!fLUy(Bb~%Qzv42R3|yCzbgqz^hWe^vja?*aiR;fOczg!>{uU+%p2YQ&6%+tAKfH2$2N@7!|O zSU(x_M$WstSbR{+NGa=;sCMYflBLxt=dK;{?gINWol`@qM`qubi_*Np;To6Z=!4oG z4A||U1uk${8f&V%Hihk=J)tR{O1TZ?-yjDtk@`()F4W){!m_m2&>dI8&5et2yywvV z#>07_%-Z}bU35Erx-$!+mPwVpesqne=5hN&7N2W_Gf3U4lA}Fu+V`T>VJF*x=@ha2 z9BaMF!$1BtKnzr@;km(Zi#O)QX&Mx|=QsLt~J15?tl824?{R?*~jsQ)D6F`T>EUs2DbSKw|s^%!P9rJImTB z*@c5|$2_AMX1@0aZpU?)KRPG(LBohY5&*7GWVw!t>@?bkZlRE@$$TX~UoK3mCs{`VT3O<)>xl@_JbT?Y`*#gYT$m*f_gFp5(Vpc~ za-eA{c5#VGH!?bpp|Lr~Yi2cnnZnx&e4K~xS|Rr^9@CDR{^!tooozR7fwf3eOhCef zUd4BA`h$^JW~Y@6B28g2uq8sv8Kk<-IatdajgeR*v-%HyR51dUviyqS)TOxw5 zH&qemW?}0Oon_;!ryBW4W67D#DY64h=T#(%chP-WCAK zy`c&6$CC)f7U-o^3QQRaesP(0tE&3Kxc0OX<*}6JVC)$zd_Co9CAGEC#bFRO8~TcJ z0%@n`inFVxZ;5|3w`T^7HSp-q$DN+Z<7ybDZ8g*!(LI7fDt#=75>2g=3A`J7WKHU;RJQ>Q~QTWkeMVfo{E+gs= z$8D@Aw}nD-n%gRV@Kx0x=9*RX``pCB3fRX)irSXaCHT~ER;p5sVllKb){&Z9WGH<# zRXX+$Ef#R~D=8C}ZTfMjVpo#1-EysqJCDE%mw*Z%Qmr8iHq;L|i^2qkEd$#zC1`G4 zM+{C8Z5_J>VbJ<+-rngK!EZChy3KQ^n{JA5SMWNX7v(M<^@Vfp39ta(+b!Lm=MAvP z)1-~u&wcGp!?%_WLS;bUQ*Ph1Oe$D7*$0HO1-|SH!x(Zhs;>P3WN94QYxh%6ZAxFu zGzA$C1g#E(t(By|NnM%Vn(K5ipwN@W_9K;Yf~9(_<92XiG$pI~I+#ymyP=;i46({v zY%V^)2SWgQi6rYPnryGMe|e6#-1E`ES&ztIDbpb0Po*pQ3Tfia!*VpRynIGf?ik5J zQ1rlqllpnRNP$$&Ia|eN$)=Pg+1JB3%8GMLUEX45lgA{#S{l**529SwS~+fXmLMitsHtsc9+!lm z|J7l`V=KEY2}CgaQ-?DQ8`PS3$iONRtP`u7Tg%6bQH{@t9spmp{$RFhN_M~GE9GGL6XEsWh0;u zE@3syC|GAnC6$)Ca?&MrF`yQ9904=NuCvBI)y@fUA;W znm8zmv*Km8vi{OMC*GH#eN&AmfMJqtfUauCSFFHPMP*fju82U)B%d%B;~Khe;e8{+ zy?I=hYQwn{dYUEnJHD-bem4#eEhASjeLIXTsOc017^@++Dmq{ExreuW6nX>{%fk+D zTowJ71m~V4V7O(F32DERVD~*;A}C?eveAq&g0avnv9DEO@0)n6UZKwj70?9YJsfn2%c3bit%-FH~<-0fatbVF0`ohat`aNj|_&>N!h-MAJeR`=$Q(ACr zIrTazrn5NE5Z@zg%Zv4$B|9}f)!U+uv9CjhEyL>8OHn)B&SAa4Ka)JgN<}QFP7o`v z*OS$&P&cwk8=7q2@agwt!~ZYD+w}JClzs8cq7S%L5&LOMLCuoImc>z4ix@ejJvKoZZAiHA2}~-N$-9>6 zmrh#Y=OPO_f%;tf~~SHrrq@3w0j?$)sqRUakGe}PF30EbAH zoE9-k2GPIjH!mpeeiJl{)i_T$ksbc!)+{9JkWQVMwVr7)gm@C~sGGG}T1s7_Yz}mV zw?rOBpeb^VyJ^+(<_L9-3#YibQ)hP$nnF?VC{pQvWd1T#oQ-2s@dm`?Lx@>}z{D1i zOMMC^uNO~aTNH=Xs^8QyZ`Oj?83=_N4p5+SE{)+SO~lnlOL54|n!M6s%%#9O8m=Ve zb1ZVi4^B{}?T?Gjb*qe+KBGTcfJ^?42e@i=KR+ zjk#iTi;c3$;Yg`)aO>r5);HtP42Ly-bXX*{Ret;z>FRchNY)umBjBK!C%dzBSP-!H zp|Vmc7ZbSbCr{zSOk+vN&tezrd0yXbwp=@f(XTRY^~pkF^QdLE(Hfr4{V|T!xCi;l ziPAgIhM6*Qix=RE*Ij0c#tPo5R?g#+xP}hJ?IX6~-$G&eeib3o_JrG=7|H?*A*?Vn z#bYFo;TyI}{|fXks#)LERXY!Ban#wj+;Kg+b(iW&^(D@zlURwEjTWST zW)1xoSK{oa9QFsls~;}cS8BHDL-jwOS(Q6hn>;WXn^iGyzI7tE_)*j=yUO+{xZ2)U8i{+O1Yx#Ur-9zSdalGv6)_m2D*LZ6>><@%oMk9^(YI>BN z9RtH2Ec8t?9x_X~r4}SR4a}3TWSV0&2u3{Z{2-?AJr=Zn^>(2_JN=*)zokF^+5zDo)x_ic-=J+Ov(XzE%Q736e&hU$vKYlBGxLOM)IKex za>}!#KjR5)i(a&5vf)WQTlCg|A8X9mu-u%bRZ4X@6zWMCtL53?&4l2}9@Mjv%%`@L zJuy-TX#C=1$*K`b$ig&Y=G3Y0G8Yx{CPEcszL;Yto2A3~!t(M)CNl94##`F88IEcD zQ1#G+X%4GbrL$=NFNgD~Fd0G?Vq2H+GZrI~8>lIO#GH%!7roQ@j+S^J*Og(N1%9P{5`M2$kMdP<_`Zm^FTd_$qg0#H8?{lZ6~D9C zT@96;4_!?WL_F-CD*naAx@To%5Rff7iT^f(Bfj=T#jhp1t_CVA-uvI${)NKuRHBWa z`0oZs*)gVyjPt45dB;&H21@ChWr`#SiADfJRD5^eYwllyrLI$R%WLgTzM*s|-q9y`wVrNN72KghGKyzf z41?Z-=&~zZahjp}RY>lwpibF$Nq{{gB;NaPyZPFe(yrrH9~f@UdMBQ%3|hfnU6NbiBpjO-UCoRmFpWsjB_NlU@ULh2aDJR=j+Zl}6clcn(Db*IUxrxm_Xs61{{ zZ5Tt?xu`Y_GWDWSKAy45VtXDavP%&3C0EB2(-%_pJN~KoWTq2k%J@i-E62NI0(Wqk#_thl!yeAD>Di-1=bQEkCH#L-aF-w37aD4X!a#S0 z@dPdV8cL&~B8IHa3wC?U4#f3SC`&&ns>FCuR`}l=IP|Av=|Q&A5k3snk|`wl)~p!u zO&#{m=&m7*FJ9=5TzPG}4rQF93vBPs_G?wU7c&OWp?8Y@PMtHT)Qun7>EtbP7u>Sh zjSi@hz1etl2lFJ5nPYURRd3(T-tQ_waGsn!^hvekynf?j6!g16UXx9*Swh$1Oy!sy z-all0R%SIiH93y$AAql8c!J|;w?M3r1j6D>;}e!%=xYn)GN&-~OAf_PdB1FI>hUX% z?O)jCT=jI_w)u-^x)B~a2yyZwMWpO5ah$x{;Q0q!j^Kq^2yslBNF#RgB@#v7UH7?+ zZQbJn)yyfbTCz>|HTuQ(i>`|3anYygd#CL7sBqhQ2=r2Ro;=D#@J*uMUULGBYN>>p zwi7#USP#_XUD&HWgw2+6hKFU(!`Vs2>#R7K#a2zGTgf7SkVL3gdc~daP|J4f9I6va zk7W$HlSWgTnh~ic6}0vKHnsM`t(Ph=m}MdM+)ut%33G2jrj=gaz5H#=-kNe(9HnpX zG}rrNmox;_vi{?IMRx9U@F>SNDC_~+|B$!jNd>ZA`U(;NlL0H4?g9WbP>Ls0BynMl zS=KK$dLtpxifOw1rPaxnR8+hBH847|@21{ zdpQpU-atQk=2)I|Mvl>|&Psv*9iC2*${vF0!$)Yhm=`?hPS?0GJfk-|i$(?2Lt#Hg zOEU4%*cJVGiY%A|OI7La;XbrKuhh;-2lds-e6CTi75xVBgZ6PMMAws`pP;%sPSWB$ z*>;_gOhmnBG@tl8Cst&!bSF1$-T$QV1B~^5P1GQ5oq?hgGs9{1@&cK6j*Xk_Ey={+ zNR_l27L)k3-?H(ba~w%FefHYP#|P;ckv%)EUW{pzUTX>C=4qI`oSJW*bd6cnSKAzy zd8rG;?4y|yY5JQcHjil+rDn`>SsczyPus%f(67+6MzF6i>CJ?)s~#?a%e>>0o&>eR z;xSd$7?QM=Qs6Q_kqUN4#THhWT69`4lQh5giQRDAvShaz1lQeM+eTb#hwS zkDn_qXqjf+HB$<(%Vk7e#Nr(s!aOsfFbY$Tj{kDakTJRX)9Q$@gmpaq_)x(=Fz zToJ=x<>xfqN+m;UO-fg7^Eh%} zC}P5@|J3i{`!k-JrF6pFXuF2IrP{65%Z|mj8_$QAJuHv6Ecpcd-3L8?Yxyes+GxHN zUNBwbU`{GB|A{p2qp!KXk3PLGw73uW;L|yk)IPq>`J$g3|y& zjFX;(muqo0>T$QJ={t?CZsyI2tnIB+F5(kj@pwtrmsmznRoa;1H(u+GyZDQvIqf5& zXM1{Cp+i_R?HuKN^p9MR!dWjZ`w(KA?d4TlVh^<9&xZekcHXy_PA%0eRHyocqIMXT zre`If?}qbJPA>}LKSt$~UMv8Du+p#d&TFqVj!n2rx6e#=yUVI>a@Bj%11--)`UbCC z2CQV1Xb1gefKU9)1aTSFiOfW8E$4 ze>F3VVq!|3i0Pg8K!kU@wGk?&m}R1a3iY=|``|Se+_D!+)hSg=#rIrPX5P-N-xCq{9she&Urg<@)Iz5#IvG z^0h_*3J`l={5mAbyKdONf#$h*x~5MK11Op>>$CwI)Mpz4?zyEY>N+_XeBdgpp~DfO zHPTibJ}8~dLM2bBGe~)egWarH0VZfrO(xVR08yPrrg;JvIm2~X^7IJG9BB!ib=s2M zh85`bFD<+F688Ua<}t!8XNY+1VDh*lBua5+dxFd1Fbs)F@~%DziL*YbcTaTtn~1$q zA1k1&K8rbf@_>7dMaibBxkG?iEGE%DtN)@u(_zoA69iYGa^2K~vxr?ESub&BxGb)# za^>a?DBHBTznFb!-@Ea>g_&3Wf01Fpj{qBk;JT-ZKdR1ekA4@$Trcst9?D*Vt&cI1 zdQ%Ol!G!vCfswn;5l$-~*lw$7mRF&Xi@L%?O{g1l9xeZ`w&h(dZo<&!)r789cn#vh zt|`^ysvwhc4~V)}ByL@c=7qg<7wju%@LAF3IrYhbmK9X3uU*>OcOB;yu?N-WenvHs zacY)IOi3j(gc*7He1T!>ZZ364eB{Nn6_Y+yg~^u0U`4`8Dgc16ab(qsiKl@ zcX;_}Tf)HyIH6&_NkQKE$n4OkQlERu;ONX1u$J$$+aMaA)r756sB6o0_ZeA~P%bHrKY;U}WpCgTOv{pszCvx@mJ*^40w zpWBC^o)xAEu|D%hN0yijJHpy7UY7UCBi|)* zVqz23xsWUstDXTgr6ug388)PfTp~j4xD99pKNA)^<@cNFKHBwb4)b8>D#rKBmk65O zh1{M@g&#-l-85=FdP9N*=iXhwW-E{G38fQ_OGL#(3%DUcu=y5;t}p@=s`wi&ED2Mp zd)4vIcp%!PGkqK}9)6I+)dz*yg?3b=;a!pBk}r&*a*YcyQ>M6VP%Sh0!Ykn65!JHA zg~ljcY=8+8Gc3reas|KdKy?KYCX?kjxspaosP|3Wj+)4W^Jzo~n zo8y`<7{v-7>z>%E-U)mfnv`j{I=(&&Qs#!y{C}`qQu2l`cm3q7eYB9SWsPh6+_NS# zt1#&OGH+>Lf*}&8l`f1dSv7t{!M{H}An-50#W|YGL7u@FS#YiH&e5fdEbEa;;VA#D<0Uqi;XVSYNeLO$@)Ia5k@%S$QC941p&%O-i_ zk@i0VvE`o6CFcQMB3X`3mgutG3v z)oChLm5~&pqv+(#RVA|$DnFaMrKVEG(O8_Jw(=i=Yn$SY?Fe`v4F=@%unS{cZM-8K zxA%U9I(Z+4iM~EJFbZ?Jv$p5m+E4W$T6@Gkci?>=I`9UeDt1ETe;lQd7>k>db;Q05vCucJIEc zG$4RN-cT;pSI|}41gDz5C+ahPR{Jn8bp(SNo_kJY)b*Y3&L%|vo5J%*KP&C{#;j(! zYlQA;O+ci7;n)uck?!P7sV^75^UJ>5ix=tL6@woN`Q12^FB~QNGi@-T=XY_bi0Ug}1jv85e+ifk z)LuH7sJ;}^k~+~+u67V?oWT{a(-D~3s}I=>5OEqs{|tUmiVyerNvlZR2{~HJdBhDZ}4Ck6~_=?j?Z)N98Ku( zfZ7}hUh_L?!)H$_Oh$6lxS9gp@MK*zF;9F+exF@=vf_{dsh~rO_-ok=W{4qXYum%9 zEJ2f@UY&*hS4RtEsaDNZF?P!ID8CPCBn|UWg~KIPfv-Y)=h?lrn++x0^;+JV&6Gdk zfEe+*W^aZAwZbMZ(F@5!qm6_}t(>l#c$#}w)VVs??vkt4?1Q# zXj7`DKixXkSQ!73?^7noA8S_AUZkb$qv?|D%xGjb2R{CHh1}UC4aC5tD?i`wd5YU1 zV-}`Gs7sqhwl3`}Be2RhtEypzZEhPESvdN0xUZn&u{z|4UaFf0DTQ zKor;R#(ICzdX@AR_REUE@Hd)nInb#Xfiyh zv0d05T2!VP%1&E9iA#4qEb^DkvV*tbd4x2w9e^v?Dz6=d@NB&~L?_#YNB1X`52obK zr@UG)T5sZy!TUe;o9r7TG zqA<^_=0Q(=Q#y*DmdeH!I&}mexgSG4ZF?1`&nStC7U?Axb+TQ9Qs5<{_w7{#wT9u& z`h73W-?3l(k5Go{TMUzk-=gzeUJf5T&n6Pk+C}((R;hFkC%*-82>enwJT~k9@Yy(W za3iyo;-AVZFJ37&85x~7Q>@=;BJa9nSJa;VCr^D1)&3MQ1R!6aR>9@_?Lay48yq+Q zx~i0X>ZPEyIh$yoDmJj^@mlmR0c4FCzopyCT;|!B45aennfi;|b3eXPNcjWjF_um3 zrKJ(8@?k1pjP2XRKV+NWAw+krRd)eRZ8IU4tD2)=lQwd{aYtBJXt_NJSAzF$PwFF# z&!q6=0>|iE68pKCo+}K9DJUznd4;k_VC^QGC{oX=Hvrc1{|g=IkVE9kHgzPwaUAz$ z1PDBnPiEcLPh;^b-)C>f`5jnJbp+H#6Jx%yg7rUsQNOy3nkEY0yTl{?7jMR&M`Amf z&eA8~-KePmT7r>nHs?Q9;|1B3X0g3my~8HQR(ICpk=j-j6}{ve2rf9ws=M!Sdj?~P zDAL>wspDtKoukiV&x7U=~)aB)tJ^Ox?sg|}R3 zB*USkvIWJZ6a)P%l$>AK>TkNWP6ud-=5DfVTM)RL&9czrloBu@2jC7#3gubhY!l?#)wPmKh`@sZ!_-ldQET^zUEP|)vb zPSPZ1IZ;H4%Srbq;qN;UO-JsGe>S0kvC}#AjYPq1Oftrtz)=j<_nTY1O)vk&w^>-f zR`k2DxWWEB@30pGiB7>b4Ob2gEx+X#GpS&&Kq*W_+)I+c1rauBreMcMyt1~f`4)@o zP`B4mUQ$ul>9tq@0M>lEKdr4IG9n|PBs!nSQh;rS%qXT=FVh%YQRH9wDG1Tay6))9 z%60nGb(nuM!}{4`zeA zuc@tAbD7wq**ca_&_%%#zkO*IM`s-+8v##(+jj99m=_u|vbF!Nt5pxMLk ztoPUxXeu`b9zOK+a-k8{hrfo2;(vcsNW=5u#+b4>kO9FgK6%Yw6nnX7&3%V1+?gMR zHpj2&d0ZC9_z7`ffNn5^u#b6CgsKupm zcvUc*vvgi+H@O~BgF2vxFl>7!ZrHToG1Zu_ zLJ9Kqkk0;UEoB7ZQ=H>?y(G$y{h`MgVdk~brhxEFRK9Z-LTb6sF)!$ByA!P)p-kTu z87|alq&!Fv3WExi`pNY3u;j|DCTs)`Uk)n_IM23=UPrXv1;YwL_U zEG) z$rYUN@#$%&UGAk| z!sSt>6hJ5;=>EWGp{>`R1~b_Gb261C|L6cp^V&Kz9-8$j<}qflZyQ;Sd=$S}I|%j$ zfVj%G0h{@VLxq{rwaZ;5zlRS#oesCeh5XZS={wPZX`G-hO^KNgGR8vm%Y4_-#~(1J z86~Ps*Zp$vxy?)+(9Nqqg(blz8xC8Q8RI;vCRGtkKMc+z$%1iIad zrXiB~JP2hq6qR11?K=!~s@wB-xChmm}C&Lk`hq<8WCS@Mm@Tan5vJn z;gj{jV@X+)0*~vifNl$RIl5{^BQ+VQzt=qZV9a=a5s4nQ)^YM$B~KRp^eLmEN~7L= z(bwI(?<~-6sm^OJpun&6SPtnki$wJWb0E?ikBJKgHofetWEuAxKK}g(<2d1}E<^e& zNZGqtX{9~dqHaMb>6N0RM$j@sgS^a_=BV#al9{|?zh>NqOr6IKHOG7gq>}bh6hAgT z>+ zX)V=Pq@)*UUNy{hb_QZ=z}}O~yUa!3Ua>v>5pbcNX$#8U5BC7`_IOm@X0I|y&R~zdhs0xUyo_o_5}_lR29N>Do_GX% zvL1C2WQ@=zXIC_w{&)ySqq?nFcY+C_7BJzl3FzcO=v`HRJu z>BSpZr^-W)w@o6~kNS%OdLTHt?C`KV2~Ry`ftR~lwEV?G%;I{8-{RsbjY`txt8T5G8@*UkYEbEu|)3k%85GIL`!iV$Kj8qH{ zdswCHqxL81S8?zw{LU+e%?#%uFN*iTY41YruNmoJ>YP?QC{*STjP(-Hif*6FIDVOIr`syn{JI3c-D-;Qt~)5Z+yaTR(g(P!2hP)4C$b z;wQ~hgnJuE7gc9qn(3r{e%AeE#Ck>F{$a!_-$2k=CvUq4($!Bi)MnQtx^kP?B`A-k zN`%r~h5a{Kq$oDk)=H%?rmZ)R7fW9qB8^{g!(z`&^uIDn*5Bp4+oq~g?ftAPkf&qt zqoMzg)yuGJYp;C;&#OBWp>QvmCnOe(oox)M&i* zpT?l0&23VPza5P&kwx=aSApyMV;*kO0CALE?BxC|L>Mba zMu`N(_^w{~0`D_$IiXy%p-&JAFH&-G(89)xugZ1i!jb3b0(MEJB0Kd=QU8~U*Twn6SiY3cJZ(4y0JP7lh%6|W z>J-0y+N5l+94+x=G~ZJKJ%nYSZok)V=I8ThufeT(=pV*q3!D{nJc8L8(~>veaG;T6 z0%YWYSjeapfN;h|a6VrE&wC;L-_R(bDw~74u)9fCKE}=6p($Gw1Fnw|G7tM%Md*>M z=Q7k`X{lTk7%V)tMF-OF!?6o_EBB)@E;?oOecqP~0panqawXo^wW4m~(OV7x;LY&1 zSt0C=h`x#K+$|#50)UU|Wv^B+`W|jJQJWPdGD-`<^mSJ!xluqLU~^ zYK$1Fx|=@1`eX0l`sX)V%PO9pHUmKAf_)lwH@2Z`po+}K@Up!HdFRY0T_S9NHPpNH zO%JchML6Nr(aF)IL+8(lpuFKVaTU1u7Xungf3~e1YVSqLDBAKWLHrDp-pCc7ti3D@ zx68=QNup;t-;T1lH|qS z-K@0-mZ<{4M2+W1YWrg)O^m6P9ehab8ZYnh@M!?xMn}r(^e)CHwM_a=MWaj=k8xY8;Q zk&QUBBZKNukpS<)piKMtnW28&-+sI}rETe}$h6)_ky!pN>q!a}e|%+87;{_GG@6!+ z{|j1o{S>cmMvv6zyoyxY1l<6AeF0K*S1i%>Y#=wK-q|U zB!urwwY65mS{AUsicrl_#1z#sqyo_ObQXkBOMshGpa35G;rsJ)cmz**uOh42xR0&{cHTZ@b*>i* zj=c=3o6~2ay9A{ja_iFWj4Z{hmV|z>^PIlP$nb}QO7EgPqTqA_=^$W2m|Fe9eU|-NhvYAn>zg8Xeg(H!MF0;>0PbC6~Ny{bk(N8Qb zRu;Q8p%{<6|76szf8r07>nG-TkdV#e<#xb&xh(|A5D_SfZ0i{%Bv#yUDD-#}rDxcieS z$dK@=kUWT?Jx|de?S1IsAqk1YR8ajFr`bOfl!N}Pnuo}#AS5{Kt!SVE4hSd#ytp=E ze4nLha6MVgaMi%{@@sk^T@d*#{zfCFl7CWUQ!VlD@1@tT(-B+8gxVH@sCS+Vfotfl z;utI^kkPEgI&EAU;VMt}%KI^-{niF6#$h=*H#@`bQPk;>al#CvT=DBwrkYac#o$Hk zY=jO`K8&AU6hO-nJVYc&i5r;}AXn$r893g18TQ9NB>)qiotJWZs1`%*XxU;=cozf} zH=CS1dfO7TWS&}AS5E#bjI-o;*OiAqlM+CNAfUAT{PpcPRdxD@6T!Qft;NIMta62K z@PML7<}1VPK?M&do$kyL$~Cc@>p{On#>wf`a_1v-tM2tOCY)u2yx=96dCgP*x*OxS zgQCpm_ng#+y+5!d%F+A&i~{_$4Hfl-fy;{AI=Sx9pa+K6Rr5}HiogSbXi&%$aj=%p zPiwa)H?QlTq##*e^zx}V&db*x9O_>vp}RiI@$AL(GI$8@;Rpm^&@k_-AD)Y0_77X~T=T@DI8={qQyOu8KsqC~bH3bSi0^gq`*#dwVIO@z7_=@n& z_W(2d8={!RebG6mBUjH8Fk)NSx`(R;gIlRn#u~|4F>Cc-ZT%pl{^;bY{*m&1kX_V>0v#3|565;hKZQi%0f6}2tAW&%Z_*uv3%2|%q!{ziESHKM?u%OVcxuF zpO32hCyt7$iRJb#>Bvc8y&+L{8)A=Q*J%4u3{rO2DSkh$^aXG!4-OY}L^nfHUV^L` zzj@0iJhlatdS8oC6by8y-OsNN3;Wk!O!!<|FaKel#GaoD(@ITi+bV+nesuQ(aPjaK zBKv%{>nqWo+@w0ZYe|tgPK5=A^1Ce{YlV6WJZvfOMNpc zJoM>t{ z?)_Sy?pi55sb{tI$3e1%E_Oe!LLDJL{dk-AEBwr$2~_vS^Do-DO4-0XOJPNH@V@?E zg3>74j)+B0GHiOZzX64Et|U`1vPiiDQ?RTLkiamRd^my4AM zPZBHPv3;gvagWBW5kt;mT4`NnE)A3n4LDigxoINNTf~Ct!e@|Vdtx-}_#-Hj%rs_<{)J5q7aN|3oEGJ`#>}D5 zw>CVi2^$er@X3DEcd0F;ay?0}r$U|LTwzA(v`=qF#>CMW20VO;2hS0+n}Ibks^!29 zGpI+)51d4Oa3iuU(8V8Rh1AIp{Yho)tA;>iHwmWjCT0K}t2L zJh&yB5xpa)DWV94)TbtdMK!HxChEMKJj<{lU{nV&NuQnd5l{l&>EQM)-*rHTLs=K2 zx_3dCrzai-KqkPzZhDzfoHib)b932q+CY=qYW3Z$V|^HNxp@t|6&e-zBcquxWf2zA zi_F^4iEOBkFaLJLv+3jx*4XD0fN%fU_jx~cUH#3Vk2fzefFm8yCZOHq#kOC~P1hMX zmAV|=d@V^|W_EVc^e*p2VjH%(@oQ4QsGi+w>*9qdiYm;Uf!~q#V)ueB6G%VWPH}j@ zUHh;*%umk8Zb_w@y6kl0Na4jk9fZ|UciAO@KM|rJFS*=sSojMrvLyW6flf>RL~~98 zX4n3EtkmX-tF_F`=hj5!+ot(4F*6G}?L^)PJf2*V56nnl~8hTe!6rr@?gY>qDp+ zhS<2PQNpUCiupoQHIM5-k&>-CTGG=TqetB5rl;w`5?c8XBjrLC0-_!HfOqc4wIs*v z^g=X`LZNFEl#yE#h1kYAU+B5Y?T(Lq3b_T{!*_L~T)|vq&u=eH|eQ0%RS>ekt&l zf|9Y7MRV;`hkTF*j6E0XMtBV);Y2L^677^q)OSi$FcRf2{)0#ZJh)6prJ#@1w{F`D zRf`;0{p?sP=SK-HVfmdQV~le)>Xr=o{?8>ljp2a}`Ai%{h;*v%&H41)@cWktB3~8K z>RiWn*3<#7q554#7Kb?|o2YG+aJ(^fJqlOODrj?q4(5-XyW=U<2P7g(H$>jHF10zXZG)$GCF}^L;-A`6%EMaL zzV$88#gu!UR#m&NXLZw-Aj}~9Z9*duSGCi<>d%RWI}9Obtz5(baC5G!&iwyU;7l>zCgw7?$!XY&@uQkKs2tu1Q z`7CUy9N*ptPAZ4?)H+$FMX)ovG@pilyWWfq9F^p@_C2hKASYCDF~=T_TY7(xZbAsG zR=ai%VBrz9ycxMDP(lY#L5SvTj~){mBe#NSMVXntG`4IutM3f>q(fU>zn;R>tRX4KXvMbar#*Oip&?h zkX94sQX+kiOjPuO?K>-w{#@s550%?gXu397PMZ+BK}DN7hX^5`ZGwwVtwZ#V$JHg= zo|U~e_1_79ZYPi|1PKMkf&|-~hznR2>Z{%RJkppqve=UDBiE@?(S}TMOAtFVo0Rjh z|5MMWs*?aM<@}@kp>{O39}8sn3=F(uVUci${#6#maD=n|B|!dPWL&IrtBRyYB6$Ty z_Uc5P62&iE=ll~TbISMX-?#EOZ?jO|Utf2JdKcvH5tG07OJX&7yG=Ql+KF(b-?DkX zJ=zNQAqmb0<)-yo{_{U6Dm5X{K!SfOLRmfSw5g2~C*dg34a;e=hJSpr7pdOvXIW*j zk&UQR|Effv&V$TA%W4b4uWJdM!2K(FUJJtQmzDjSP=vXyakcFseNs-Y)!{5k%vO=0 zZ;8Bdu%J)}aW9|tV9(%P92|b&?`H(sizIrlFiegzq&V^eqJiP31jc|HA|Hu+pT^mU z;K)1j#(xq^YM@G1m5CUPL_0#AMbIM>6+-oee&nmjGhO#UE=?336z>?EfGP#@Z=Ww& zikfAiM*^uwZNDpb+fPsejdWYd_Sr{y>COC=!*}`-ZE>NYqjQUcDiZKkil(rwG)`W5 z8b^>x6^A#kKSi<6y}pJD5Cv84f2U6H5&q8bSKSgi3&z9kA)yHXnOcV}YeP4uwBGA-`%9OXY+UF#hgP&hS?t;Vr z4sWM`cSHR4zd9-=p7J?ry5!QxFA&Q%fgXi?5z+d^5l(rMDz} zY`O5n;Kr=OU?c9G1+c96+laqczFsu_jo|;}dqggyv%@}|Y4qqh=#9>7zn@m0`L<2k zcOn5BsDo)!VFxIsyAdNY`jTOCF^=4{m@F_%N-8#>qxDnwB8>GadSGt!`#!<uTfJvGc z*Q;0X1%JVNRJa0gUR;=eH~v?=&-3QLL-zewKgRz}UeLb=3{ABo=i!V>6Z6|)oQNav zteiK7E%vuwv5kE7Z5?-!$;X5Ddbh(^m*#K5HzER-xr;JhCLP`g9P}B7joFs3zIm*T zO1hoi-j<~a4%m+C6C8WeI8K{;%GbSCQ2ERfQqIq9Mai}e@@Q1QUyB$P8tt=~TY4LR zocu7x(U{}=hQ)eD{k*<N3xZ*52m15ezXIxiV=TY%pg+4S? z&t|dSY(GlL;RddrW+Dz&vT^VoL!$XDuN%`Ry_geL<#fJvxOSU;%0Zkc-7{G8C}acZCpC{5YQCa+F?pQ8=BK2(tEV)dvVvHg!}KhJdjzOyPXd(=0B ziT4Ade=MqumiL+;GM!J8R91PM(X?9Uy7Tpl4&mlncL-c0a`Iqx>$A?nNv%>s=f;z$FFN8?6H^+Nxrr+{`jEJ#03gEDo}l^Sb$KczGHa!OTnJy{thDM z<2lLUvv_*I$l|1}MSSIbaW_^ibbj5!gZ!H&>Xl!71{j1SMWz)qh=lis*7C^p)F3#+ ze{NNGC?{Pu;CXLWD*_HD3~j0^c@g2F3~~y!!jXJ~z=61v1=fA8z}(`FH@`;1ieLDq z!qM%^LGWjTsTd8AO%vrO-jT(n^&8#fRw9Hs?1r0l;7e)dTway@NTfsDD*7<$S(j1n z3fqc&s=II-#q^6meMs83m*JHUo`@x~yj_V9KmQ_2^Cg(5xzWI;tX@-Dvt*Dem~PAK zla7zI!@O~OSW=kwL{U=_xEReT_mV#! zPs6*4bWx64jON>&!)!N>+`;(joruVC1ywG`D7B-n)x=?6a1q%g$}bMpG?88(d9;qw zG`xc1gH(&WhS#3ieqV#GPypy&XrWVUQP9a$MaFt}*U|0oon(_SSLtQkiQ-e}D$_`y zzavHITW~Eo?J<;z%oaEScfpU837_%OfAqBi^(-NovF_+00k|x{En|8KwBuwenY_Lg z>hEpdKm1=sWrTU{?=v{2P3$R1`HPHq=lx}HNvP1iwu5k-s+17#t;PfK2Uh(fnb_o5 zK?j1Q0Ts(fe76o-{VWC2!9MNq`zUdt^ygb`RWDQHdQ#7UA^C2vdH6*9MRAZ!1(87W zt57B0OmPO5@*wDA$C8z% zW*PjZiUBaXc3mxBQo^|O^lU7RwoqpYws!tXJ&5mc)o3Oo$a_BGz|gOfc|R*ROD5=g zxG*_9B}6>_sp@VI!(&;$x|fp9d-WJ2s738Ms^{5IGdk>5XYp}dN5ZK!u``KRtssME zA5JR_ z!A=#(XL+#P-Cv$KjaH6X|5{V*!ENJdBsDu%e0<^$2kiZO&G?8ZNqiv`>@xFzYN@&R zMl)br^-n)o$t{|GV?&_bN=NXh$NR4?z=v7s`m+a@J6yPy$XO`Qk9PFGVreX|T{l89 zTrYEJBlT549`d5JDR0!%YmJ)pzMug!z1Z+x znl}MI9|&&gyd9rK-ah=KP0&US5(8PeNd)@UhuhcOG7N*sFE9aCw`aXtFV@C^X=`n1 z8%zN{l*qZ$T1Ez-cXw6KwQcyA-oxh71^U);Q&aYn#egze68?H z%bcfUd=F$s$l;Y#w_mYkYCj#@D+VE&EHD)n5X7V*T0Dqk{qk^&u_5k^x?T6e?6wH1QNQ|A1a zLY8x!44dP_Vxtqk`!E4q_5kPTPZwdjHK$2&+86?RjdyD%f;~*7!(KxmHYBkj-CJ=7 za@;)3g7|7no1yROYfoZ<&($^VIHNeznDYd=F%p^j#F~$lM$E8HCBXJl$L{sz>TZSW zs4DOUkt3G-u(s)F?S zOp#NSF#+g1q;_tPAY&kY6!_ty}y0UZ6qFC{`+;- ze@KKb{aGacQV3V9B;m@=r+v7EO2_EAi62n$pUxI8tUK@lR^#}c;bJtqDO*fwNjlf* z$@gqfUMO!%bx7m`=Nib$zbh={9RO@O=zIReBaX`VyX)!K-_bkTL#&jDv~FcGdUlY3 zWszKoi)c&Ppgd9X$eUbIktmqZfgo}`)r!XcDTGP@TIoQY%KQ<7*1|fJ&i#wrZ%r7-Cnc+MJ`;Z*u}%$54|MF`iEh1O6AaR0r%b3#gbRP>PfTG@&;RBlUpE6wCo zyW6I~uHs9Fcg_d9Tm#bP_t7h8CD}^^3a;9w`PIZ}Jld`q7iS8efl5MkvKAJ`IR79_ zGse+&{5Oa`Y8sv|p9l`Ql0psIv^nP1VoS{`Zpg;u$t#-qL(y82#X26(E7W9`S%_Xd zpf&J(VWm2vgTKc!`zxOD>ptBjVZ2fPW}|&OY}CwEMKZ_{0=rgpdipl}$=GtMG!nH%2GbI$t?@~JmTE>v#m-Ol7JdwH<%~MHzUy zcCu2J)~cdeZY^CZp{XOkQ>vFZAL^+ttwubtIxMUl=1H)5kjpuuc+V&c9Z76f=d4t& ztTn!0`I+4%`N-TlID$>2B$#wytB(drIhs-e+A^arJYE9W;j!5_vQd!qC4{!w^hK04 zs}-vUO3ciJbRk4EOI!GpEkEx-mUhX-KuXLNs!5Bsr@tR7W8n+s>jd00j$eQtQ2I{uK@uqwS|*_)$j%3Pj%m`k*L&W>d(`; zjnQ&)(y*h1Ex(_2l}SDa6lm{t8t3rH0ta8=PHcxexMRWJ?tZ9fOwt)RM zHn~i!ns*m5dcz=-ew(yA{b2U$#gGv2^D}2O3(0iRb3JQ&B-5nvd~?c2w&rA3xmV~a z7WriJOuEAPTu6I*ewoJcu}k8jtvJZ0E6BACAv^ETM~(}k;yZ1wOd_d|*zR1q<&TZh zt6C!CfoJRi2}29DgjD-lQ`jP~I}fhFMcTV11z za{3tlxeu;d7gV{tq*!hu@x$>gj5|!x>)j#l-~Re@>sVmay&;2#yP7ASj%0rQMfu%$ zF2|*j$)FjQ=sK}5tQ_aw z1vz#vMh>L))pirZ8DTLYEza*Gu{+H+33{mu4c8|*&p*3!+2?)9N#I6saL=-qCXS5=e5N8gl@Rg??%Q=G}_ z*gj5Tyml&6kb}VgY~CS!`VlD@r4-l5`AA&@nX9EP%i**a=xRLN&8ya0IEU5auv==SN>Y+nAki$RM1s;Yf${WKu< zSfRYYS$IEE6t{ik<*_~w;-n38qn-?WUgEt&O~}w0`7;@$n-u#8A(shPZaw1jS5dhF zyZfcJm9mPDi}SxJN2QNw8D3#}hxBk?ISUEuEk3i+EzV`{HlY0sfB9uYV}JE-5IE znqe(?NN17MpSfmqTEY=V4I#H9hJWw96(OHA?TNYr6Lo#J1pQL;amr|1e{cs}MZEe;MP>ZId47wy+iv znd&!)IB6U;96*b1dmH73nr%l>6708OMzw?#>eRGxPoFLCpG_=0si&SN@`Vf4!^wgd zJ^K)t$4HMy*roA}$4V@r)+7Lm(UU6QZFUH;3u(n9y(Hw0z24~mr7+ysd?S`Lcd~qU zFg{bvcjaASUecJ_M=o%sP+*~daP!G{z|SR4|IyW=YkzrC^dxGhMzc3k0fLMmHmK}P z^rP~##MJ#Xeub#jV(%d9PP7C)DkzG~?9E!+AVghz)x zkDNkP?PWdBh(2--fzPjm<_gnec@32MX38l**+l9=9r95{3O)uR{axv;__1DhW*xbM z%O%lP1-a}J3Qp#j$fbW+ zoD$;TIG;61iwNG4i*WWuxSL`24PM5fwEYfUekEA_8-B?J!UZ?K|6rLW>d9q#1%PaZ zmhBK}E8sqXm&(Da!9@USkah7wQ`zPF;ii|>OHudE6ZQT31ut5!XL<_i%kkRU9_}5d zAb0euRvu$6`)O$Voj>YHw+GC1N+Zju5NA&sI~p4`R+j*jKP5bC%!xO}&zU0r?qsNX z*VL&1@MsNrUG=LXi9g6thBS7H5BbB_+4Rk?%kbx?MU{H`h}KS0Wh#ai zQnUcna2xo0J&k+L>*JW({M%zOTUE;g-MY){IEEm-k4&~W{!_{qPg?&99q~qa5c+Th W4^uwNse3+nKuTO*?6(NS@Bag4TRyM= literal 0 HcmV?d00001 diff --git a/static/theme.css b/static/theme.css index 6bc5d6dd6..3ee587c07 100644 --- a/static/theme.css +++ b/static/theme.css @@ -137,3 +137,14 @@ figcaption { display: none; } } + + +/* +TODO: +This covers all lists in this section, but I only want to style the lists in the “Protection” sections. +How can I add a HTML class to that section (or list) from verso? +*/ +#validating-proofs ~ * ul li::marker { + content: "🛡️ "; + font-size: 1.2em; +} From b0f4917d9ea826909acd32af8fe3c6c9d889a7b7 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 10:26:00 +0000 Subject: [PATCH 02/36] Guessing what prettier might complain about --- static/theme.css | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/static/theme.css b/static/theme.css index 3ee587c07..5a47b9743 100644 --- a/static/theme.css +++ b/static/theme.css @@ -145,6 +145,6 @@ This covers all lists in this section, but I only want to style the lists in the How can I add a HTML class to that section (or list) from verso? */ #validating-proofs ~ * ul li::marker { - content: "🛡️ "; - font-size: 1.2em; + content: "🛡️ "; + font-size: 1.2em; } From 62ae72b173dc0d3177bf705e34de471a71015b4d Mon Sep 17 00:00:00 2001 From: nomeata Date: Fri, 9 Jan 2026 10:35:19 +0000 Subject: [PATCH 03/36] Run the Prettier code formatter --- static/theme.css | 1 - 1 file changed, 1 deletion(-) diff --git a/static/theme.css b/static/theme.css index 5a47b9743..eb20608ab 100644 --- a/static/theme.css +++ b/static/theme.css @@ -138,7 +138,6 @@ figcaption { } } - /* TODO: This covers all lists in this section, but I only want to style the lists in the “Protection” sections. From 79e82f13d3562773cb56625ac8e37063afcc6964 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 15:10:40 +0000 Subject: [PATCH 04/36] Hack together a :::shieldList directive --- Manual/Meta.lean | 1 + Manual/Meta/ShieldList.lean | 50 ++++++++++++++++++++++++++++++++++++ Manual/ValidatingProofs.lean | 8 ++++++ static/theme.css | 12 +-------- 4 files changed, 60 insertions(+), 11 deletions(-) create mode 100644 Manual/Meta/ShieldList.lean diff --git a/Manual/Meta.lean b/Manual/Meta.lean index c6b10d7d2..ccd170861 100644 --- a/Manual/Meta.lean +++ b/Manual/Meta.lean @@ -32,6 +32,7 @@ import Manual.Meta.ModuleExample import Manual.Meta.ParserAlias import Manual.Meta.Syntax import Manual.Meta.Tactics +import Manual.Meta.ShieldList import Manual.Meta.SpliceContents import Manual.Meta.Markdown import Manual.Meta.Imports diff --git a/Manual/Meta/ShieldList.lean b/Manual/Meta/ShieldList.lean new file mode 100644 index 000000000..e8cc4571c --- /dev/null +++ b/Manual/Meta/ShieldList.lean @@ -0,0 +1,50 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Joachim Breitner +-/ + +import VersoManual +import Lean.Elab.InfoTree.Types + +import Manual.Meta.Basic + +open Verso Doc Elab +open Verso.Genre Manual +open Verso.ArgParse + +open Lean Elab + + + +namespace Manual + +def Block.shieldList : Block where + name := `Manual.shieldList + data := .null + +@[directive_expander shieldList] +def shieldList : DirectiveExpander + | _args, contents => do + let blocks ← contents.mapM elabBlock + -- Figures are represented using the first block to hold the caption. Storing it in the JSON + -- entails repeated (de)serialization. + pure #[← ``(Block.other Block.shieldList #[$blocks,*])] + +@[block_extension shieldList] +def shieldList.descr : BlockDescr where + traverse _id _data _contents := pure none + toTeX := + some <| fun _ goB _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← goB b, .raw "\n"] + toHtml := + open Verso.Doc.Html in + open Verso.Output.Html in + some <| fun _goI goB _id _data blocks => do + pure {{ +
+ {{← blocks.mapM goB}} +
+ }} + extraCss := [r##".shieldList li::marker { content: "🛡️ "; font-size: 1.2em; }"##] diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 1808d63a0..aefc67d97 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -58,12 +58,14 @@ This check is meaningful if one believes the formal theorem statement correspond ## Protection +:::shieldList This check protects against * Incomplete proof (missing goals, tactic error) *of the current theorem* * Explicit use of `sorry` *in the current theorem* * Honest bugs in meta-programs and tactics * Proofs still being checked in the background +::: ## Comments @@ -96,11 +98,13 @@ This check is meaningful if one believes the formal theorem statement correspond ## Protection +:::shieldList (In addition to the list above) * Incomplete proofs * Explicit use of `sorry` * Custom axioms +::: ## Comments @@ -126,10 +130,12 @@ This check is meaningful if one believes the formal theorem statement correspond ## Protection +:::shieldList (In addition to the list above) * Bugs in Lean’s core handling of the kernel’s state (e.g. due to parallel proof processing, or import handling) * Meta-programs or tactics intentionally bypassing that state (e.g. using low-level functionality to add unchecked theorems) +::: ## Comments @@ -164,9 +170,11 @@ This check is meaningful if the theorem statement in the trusted challenge file ## Protection +:::shieldList (In addition to the list above) * Actively malicious proofs +::: ## Comments diff --git a/static/theme.css b/static/theme.css index eb20608ab..f65b42c25 100644 --- a/static/theme.css +++ b/static/theme.css @@ -136,14 +136,4 @@ figcaption { .header-title { display: none; } -} - -/* -TODO: -This covers all lists in this section, but I only want to style the lists in the “Protection” sections. -How can I add a HTML class to that section (or list) from verso? -*/ -#validating-proofs ~ * ul li::marker { - content: "🛡️ "; - font-size: 1.2em; -} +} \ No newline at end of file From a9a965fe3b7e85b5e02c7809cf2f98702d060ece Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 15:30:24 +0000 Subject: [PATCH 05/36] Generalize to :::listBullet --- Manual/Meta.lean | 2 +- Manual/Meta/ListBullet.lean | 55 ++++++++++++++++++++++++++++++++++++ Manual/Meta/ShieldList.lean | 50 -------------------------------- Manual/ValidatingProofs.lean | 8 +++--- 4 files changed, 60 insertions(+), 55 deletions(-) create mode 100644 Manual/Meta/ListBullet.lean delete mode 100644 Manual/Meta/ShieldList.lean diff --git a/Manual/Meta.lean b/Manual/Meta.lean index ccd170861..48067ce20 100644 --- a/Manual/Meta.lean +++ b/Manual/Meta.lean @@ -28,11 +28,11 @@ import Manual.Meta.LakeCmd import Manual.Meta.LakeOpt import Manual.Meta.LakeToml import Manual.Meta.Lean +import Manual.Meta.ListBullet import Manual.Meta.ModuleExample import Manual.Meta.ParserAlias import Manual.Meta.Syntax import Manual.Meta.Tactics -import Manual.Meta.ShieldList import Manual.Meta.SpliceContents import Manual.Meta.Markdown import Manual.Meta.Imports diff --git a/Manual/Meta/ListBullet.lean b/Manual/Meta/ListBullet.lean new file mode 100644 index 000000000..0a76185e6 --- /dev/null +++ b/Manual/Meta/ListBullet.lean @@ -0,0 +1,55 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Joachim Breitner +-/ + +import VersoManual +import Lean.Elab.InfoTree.Types + +import Manual.Meta.Basic + +open Verso Doc Elab +open Verso.Genre Manual +open Verso.ArgParse + +open Lean Elab + + + +namespace Manual + +def Block.listBullet (bullet : String) : Block where + name := `Manual.listBullet + data := .str bullet + +@[directive_expander listBullet] +def listBullet : DirectiveExpander + | args, contents => do + let bullet ← ArgParse.run (.positional `bullet .string) args + let blocks ← contents.mapM elabBlock + pure #[← ``(Block.other (Block.listBullet $(quote bullet)) #[$blocks,*])] + +@[block_extension listBullet] +def listBullet.descr : BlockDescr where + traverse _id _data _contents := pure none + toTeX := + some <| fun _ goB _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← goB b, .raw "\n"] + toHtml := + open Verso.Doc.Html in + open Verso.Output.Html in + some <| fun _goI goB _id data blocks => do + let bullet ← + match data with + | .str bullet => pure bullet + | _ => + HtmlT.logError "Invalid data for listBullet block" + pure "" + pure {{ +
+ {{← blocks.mapM goB}} +
+ }} + extraCss := [r##".listBullet li::marker { content: var(--bullet); font-size: 1.2em; }"##] diff --git a/Manual/Meta/ShieldList.lean b/Manual/Meta/ShieldList.lean deleted file mode 100644 index e8cc4571c..000000000 --- a/Manual/Meta/ShieldList.lean +++ /dev/null @@ -1,50 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Joachim Breitner --/ - -import VersoManual -import Lean.Elab.InfoTree.Types - -import Manual.Meta.Basic - -open Verso Doc Elab -open Verso.Genre Manual -open Verso.ArgParse - -open Lean Elab - - - -namespace Manual - -def Block.shieldList : Block where - name := `Manual.shieldList - data := .null - -@[directive_expander shieldList] -def shieldList : DirectiveExpander - | _args, contents => do - let blocks ← contents.mapM elabBlock - -- Figures are represented using the first block to hold the caption. Storing it in the JSON - -- entails repeated (de)serialization. - pure #[← ``(Block.other Block.shieldList #[$blocks,*])] - -@[block_extension shieldList] -def shieldList.descr : BlockDescr where - traverse _id _data _contents := pure none - toTeX := - some <| fun _ goB _ _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← goB b, .raw "\n"] - toHtml := - open Verso.Doc.Html in - open Verso.Output.Html in - some <| fun _goI goB _id _data blocks => do - pure {{ -
- {{← blocks.mapM goB}} -
- }} - extraCss := [r##".shieldList li::marker { content: "🛡️ "; font-size: 1.2em; }"##] diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index aefc67d97..5148256b2 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -58,7 +58,7 @@ This check is meaningful if one believes the formal theorem statement correspond ## Protection -:::shieldList +:::listBullet "🛡️" This check protects against * Incomplete proof (missing goals, tactic error) *of the current theorem* @@ -98,7 +98,7 @@ This check is meaningful if one believes the formal theorem statement correspond ## Protection -:::shieldList +:::listBullet "🛡️" (In addition to the list above) * Incomplete proofs @@ -130,7 +130,7 @@ This check is meaningful if one believes the formal theorem statement correspond ## Protection -:::shieldList +:::listBullet "🛡️" (In addition to the list above) * Bugs in Lean’s core handling of the kernel’s state (e.g. due to parallel proof processing, or import handling) @@ -170,7 +170,7 @@ This check is meaningful if the theorem statement in the trusted challenge file ## Protection -:::shieldList +:::listBullet "🛡️" (In addition to the list above) * Actively malicious proofs From 627b3964ce80f10d2dff79d7a47bd2046bc08361 Mon Sep 17 00:00:00 2001 From: nomeata Date: Fri, 9 Jan 2026 15:32:05 +0000 Subject: [PATCH 06/36] Run the Prettier code formatter --- static/theme.css | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/static/theme.css b/static/theme.css index f65b42c25..6bc5d6dd6 100644 --- a/static/theme.css +++ b/static/theme.css @@ -136,4 +136,4 @@ figcaption { .header-title { display: none; } -} \ No newline at end of file +} From c9289ad42b73c3c9cd8f6502441bfeb6e4d6603a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:43:30 +0100 Subject: [PATCH 07/36] Update Manual/Meta/ListBullet.lean Co-authored-by: David Thrane Christiansen --- Manual/Meta/ListBullet.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Manual/Meta/ListBullet.lean b/Manual/Meta/ListBullet.lean index 0a76185e6..3cf957fb3 100644 --- a/Manual/Meta/ListBullet.lean +++ b/Manual/Meta/ListBullet.lean @@ -33,10 +33,7 @@ def listBullet : DirectiveExpander @[block_extension listBullet] def listBullet.descr : BlockDescr where traverse _id _data _contents := pure none - toTeX := - some <| fun _ goB _ _ content => do - pure <| .seq <| ← content.mapM fun b => do - pure <| .seq #[← goB b, .raw "\n"] + toTeX := none toHtml := open Verso.Doc.Html in open Verso.Output.Html in From 687548a7d44173c1e7d0d0d26939dba48f9b7c5c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:44:00 +0100 Subject: [PATCH 08/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 5148256b2..29406ac9a 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -72,7 +72,7 @@ This check protects against In the Visual Studio Code extension settings, the symbol can be changed. Editors other than VS Code may have a different indication. -Running `lake build Module`, where `Module` refers to the file containing the theorem, and observing success without error messages or warnings provides the same guarantees. +Running `lake build +Module`, where `Module` refers to the file containing the theorem, and observing success without error messages or warnings provides the same guarantees. # Printing axioms From 645d4748ce80505dd063b7bc1c624708a25f0ece Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:44:12 +0100 Subject: [PATCH 09/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 29406ac9a..26016b576 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -81,7 +81,7 @@ Because both `sorry` and incomplete proofs are elaborated to axioms, their prese ## Instructions -Write `#print axioms thmName` after the theorem declaration, with `thmName` replaced by the name of the theorem and check that it reports only the built-in axioms `propext, Classical.choice, and Quot.sound.`. +Write `#print axioms thmName` after the theorem declaration, with `thmName` replaced by the name of the theorem and check that it reports only the built-in axioms {name}`propext`, {name}`Classical.choice`, and {name}`Quot.sound.`. ## Significance From 8e4ec57b2a541afec2351b969427636c0732677b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:44:21 +0100 Subject: [PATCH 10/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 26016b576..ec9eaca28 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -89,7 +89,7 @@ This command prints the set of axioms used by the theorem and the theorems it de The three axioms above are standard axioms of Lean's logic, and benign. * If `sorryAx` is reported, then this theorem or one of its dependencies uses `sorry` or is otherwise incomplete. -* If `Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion. +* If {name}`Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion. * Any other axiom means that a custom axiom was declared and used, and the theorem is only valid relative to the soundness of these axioms. ## Trust From e00739dff89753b4cfd73e1605c6930be213fc32 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:45:27 +0100 Subject: [PATCH 11/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index ec9eaca28..d1d4cd6b5 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -88,7 +88,7 @@ Write `#print axioms thmName` after the theorem declaration, with `thmName` repl This command prints the set of axioms used by the theorem and the theorems it depends on. The three axioms above are standard axioms of Lean's logic, and benign. -* If `sorryAx` is reported, then this theorem or one of its dependencies uses `sorry` or is otherwise incomplete. +* If {name}`sorryAx` is reported, then this theorem or one of its dependencies uses `sorry` or is otherwise incomplete. * If {name}`Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion. * Any other axiom means that a custom axiom was declared and used, and the theorem is only valid relative to the soundness of these axioms. From b9dde8801d9da025b384029168162674164647b6 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 15:45:07 +0000 Subject: [PATCH 12/36] tags --- Manual/ValidatingProofs.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index d1d4cd6b5..a38c95a1e 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -37,6 +37,9 @@ Furthermore it is important to distinguish the question “does the theorem have Below, an escalating sequence of checks are presented, with instructions on how to perform them, an explanation of what they entail and the mistakes or attacks they guard against. # The blue double check marks +%%% +tag := "validating-blue-check-marks" +%%% In regular everyday use of Lean, it suffices to check the blue double check marks next to the theorem statement for assurance that the theorem is proved. @@ -75,6 +78,9 @@ Editors other than VS Code may have a different indication. Running `lake build +Module`, where `Module` refers to the file containing the theorem, and observing success without error messages or warnings provides the same guarantees. # Printing axioms +%%% +tag := "validating-printing-axioms" +%%% The blue double check marks appear even when there are explicit uses of `sorry` or incomplete proofs in the dependencies of the theorem. Because both `sorry` and incomplete proofs are elaborated to axioms, their presence can be detected by listing the axioms that a proof relies on. @@ -112,6 +118,9 @@ At the time of writing, the `#print axioms` command does not work in a `module`. To work around this, create a non-module file, `import` your module, and use `#print axioms` there. # Re-checking proofs with lean4checker +%%% +tag := "validating-lean4checker" +%%% There is a small class of bugs and some dishonest ways of presenting proofs that can be caught by re-checking the proofs that are stored on file when building the project. @@ -150,6 +159,9 @@ The [lean-action](https://github.com/leanprover/lean-action) Github Action provi Without the `--fresh` flag the tool can be instructed to only check some modules, and assume others to be correct (e.g. trusted libraries), for faster processing. # Gold standard: `comparator` +%%% +tag := "validating-comparator" +%%% To protect against a seriously malicious proof compromising how Lean interprets a theorem statement or the user's system, additional steps are necessary. This should only be necessary for high risk scenarios (proof marketplaces, high-reward proof competitions). From e9326f9ac7b53f51020bcb3ff0ba9bb57f26294a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 15:45:57 +0000 Subject: [PATCH 13/36] chicago --- Manual/ValidatingProofs.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index a38c95a1e..60958caff 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -36,7 +36,7 @@ Furthermore it is important to distinguish the question “does the theorem have Below, an escalating sequence of checks are presented, with instructions on how to perform them, an explanation of what they entail and the mistakes or attacks they guard against. -# The blue double check marks +# The Blue Double Check Marks %%% tag := "validating-blue-check-marks" %%% @@ -77,7 +77,7 @@ Editors other than VS Code may have a different indication. Running `lake build +Module`, where `Module` refers to the file containing the theorem, and observing success without error messages or warnings provides the same guarantees. -# Printing axioms +# Printing Axioms %%% tag := "validating-printing-axioms" %%% @@ -117,7 +117,7 @@ This check is meaningful if one believes the formal theorem statement correspond At the time of writing, the `#print axioms` command does not work in a `module`. To work around this, create a non-module file, `import` your module, and use `#print axioms` there. -# Re-checking proofs with lean4checker +# Re-Checking Proofs with lean4checker %%% tag := "validating-lean4checker" %%% @@ -158,7 +158,7 @@ The [lean-action](https://github.com/leanprover/lean-action) Github Action provi Without the `--fresh` flag the tool can be instructed to only check some modules, and assume others to be correct (e.g. trusted libraries), for faster processing. -# Gold standard: `comparator` +# Gold Standard: `comparator` %%% tag := "validating-comparator" %%% @@ -193,7 +193,7 @@ This check is meaningful if the theorem statement in the trusted challenge file At the time of writing, `comparator` uses only the official Lean kernel. In the future it will be possible to use multiple, independent kernel implementations easily; then this will also protect against implementation bugs in the official Lean kernel. -# Remaining issues +# Remaining Issues When following the gold standard of checking proofs using comparator, some assumptions remain: From 182f5f514f49dd56aac682ccd3c438aa4a6c08cb Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 15:46:28 +0000 Subject: [PATCH 14/36] Backticks --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 60958caff..d09610dec 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -117,7 +117,7 @@ This check is meaningful if one believes the formal theorem statement correspond At the time of writing, the `#print axioms` command does not work in a `module`. To work around this, create a non-module file, `import` your module, and use `#print axioms` there. -# Re-Checking Proofs with lean4checker +# Re-Checking Proofs with `lean4checker` %%% tag := "validating-lean4checker" %%% From e25e5900e99c111e2377c4ffd1638f53db60ca95 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:46:55 +0100 Subject: [PATCH 15/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index d09610dec..62a044312 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -122,7 +122,7 @@ To work around this, create a non-module file, `import` your module, and use `#p tag := "validating-lean4checker" %%% -There is a small class of bugs and some dishonest ways of presenting proofs that can be caught by re-checking the proofs that are stored on file when building the project. +There is a small class of bugs and some dishonest ways of presenting proofs that can be caught by re-checking the proofs that are stored in {tech}[`.olean` files] when building the project. ## Instructions From 654a07b947ef97f453adc496b3f6aab071f55a0b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:47:08 +0100 Subject: [PATCH 16/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 62a044312..2146f66ae 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -126,7 +126,7 @@ There is a small class of bugs and some dishonest ways of presenting proofs that ## Instructions -Build your project using `lake build`, run `lean4checker --fresh` on the module that contains the theorem of interest and check that no error is reported. +Build your project using {lake}`build`, run `lean4checker --fresh` on the module that contains the theorem of interest, and check that no error is reported. ## Significance From a76edbc56f186978893071f8e0a86ec4a40a08b3 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:47:16 +0100 Subject: [PATCH 17/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 2146f66ae..aa1a1fa4b 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -130,7 +130,7 @@ Build your project using {lake}`build`, run `lean4checker --fresh` on the module ## Significance -The lean4checker tool reads the declarations and proofs as they are stored by `lean` during building (the `.olean` files), and replays them through the kernel. +The `lean4checker` tool reads the declarations and proofs as they are stored by `lean` during building (the {tech}[`.olean` files]), and replays them through the kernel. It trusts that the olean files are structurally correct. ## Trust From c7c64efbf70b69d697446b1bdb1a66bee5b8c8c6 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:47:24 +0100 Subject: [PATCH 18/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index aa1a1fa4b..4f35b9b4e 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -131,7 +131,7 @@ Build your project using {lake}`build`, run `lean4checker --fresh` on the module ## Significance The `lean4checker` tool reads the declarations and proofs as they are stored by `lean` during building (the {tech}[`.olean` files]), and replays them through the kernel. -It trusts that the olean files are structurally correct. +It trusts that the `.olean` files are structurally correct. ## Trust From 9ed947b6f46a61b3feffe31167889c5fdcce6bdf Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 15:50:42 +0000 Subject: [PATCH 19/36] Add test (but now to hide from output?) --- Manual/ValidatingProofs.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 4f35b9b4e..00049626a 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -117,6 +117,15 @@ This check is meaningful if one believes the formal theorem statement correspond At the time of writing, the `#print axioms` command does not work in a `module`. To work around this, create a non-module file, `import` your module, and use `#print axioms` there. +```leanModule +module +/-- +error: cannot use `#print axioms` in a `module`; consider temporarily removing the `module` header or placing the command in a separate file +-/ +#guard_msgs in +#print axioms sorryAx +``` + # Re-Checking Proofs with `lean4checker` %%% tag := "validating-lean4checker" From ade2f738e13c0c9e3b0fe4b6dcb70e6b7e3df100 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 15:53:38 +0000 Subject: [PATCH 20/36] Stray period --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 00049626a..2270285f7 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -87,7 +87,7 @@ Because both `sorry` and incomplete proofs are elaborated to axioms, their prese ## Instructions -Write `#print axioms thmName` after the theorem declaration, with `thmName` replaced by the name of the theorem and check that it reports only the built-in axioms {name}`propext`, {name}`Classical.choice`, and {name}`Quot.sound.`. +Write `#print axioms thmName` after the theorem declaration, with `thmName` replaced by the name of the theorem and check that it reports only the built-in axioms {name}`propext`, {name}`Classical.choice`, and {name}`Quot.sound`. ## Significance From 70868428622de1b28018cf648afefbb05c3f996a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:56:27 +0100 Subject: [PATCH 21/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 2270285f7..650443ff3 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -223,7 +223,7 @@ The trusted code base is larger (it includes Lean's compilation toolchain and li General use (`decide +native` or direct use of `ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the Kernel's evaluation. In particular, all `implemented_by`/`extern` attributes in libraries become part of the trusted code base. -All these uses show up as an axiom `Lean.trustCompiler` in `#print axioms`. +All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`. External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler. When that level of checking is needed, proofs have to avoid using native evaluation. From da16d22dda4a62e2f33a34562be7470d1c0f9169 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:56:41 +0100 Subject: [PATCH 22/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 650443ff3..4d42b8bcc 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -227,4 +227,3 @@ All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler. When that level of checking is needed, proofs have to avoid using native evaluation. -All these uses show up as an axiom `Lean.trustCompiler` in `#print axioms`. External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler. When that level of checking is needed, proofs have to avoid using native evaluation. From 087e419020db15ec53fdf9fd4cec5ed6dc09cfd0 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:56:59 +0100 Subject: [PATCH 23/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 4d42b8bcc..40f97b0d0 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -82,7 +82,7 @@ Running `lake build +Module`, where `Module` refers to the file containing the t tag := "validating-printing-axioms" %%% -The blue double check marks appear even when there are explicit uses of `sorry` or incomplete proofs in the dependencies of the theorem. +The blue double check marks appear even when there are explicit uses of {lean}`sorry` or incomplete proofs in the dependencies of the theorem. Because both `sorry` and incomplete proofs are elaborated to axioms, their presence can be detected by listing the axioms that a proof relies on. ## Instructions From e010eb80ba25b59ee2cd59d7640bb0aa5dd59bee Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:57:55 +0100 Subject: [PATCH 24/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 40f97b0d0..cbbe3738b 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -83,7 +83,7 @@ tag := "validating-printing-axioms" %%% The blue double check marks appear even when there are explicit uses of {lean}`sorry` or incomplete proofs in the dependencies of the theorem. -Because both `sorry` and incomplete proofs are elaborated to axioms, their presence can be detected by listing the axioms that a proof relies on. +Because both {lean}`sorry` and incomplete proofs are elaborated to axioms, their presence can be detected by listing the axioms that a proof relies on. ## Instructions From cad4b9baf0be88e6a84e035d5341c26fcdde0a25 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:59:02 +0100 Subject: [PATCH 25/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index cbbe3738b..b3075fcfb 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -220,7 +220,7 @@ This is used by the `decide +native` tactic or internally by specific tactics (` Specific uses wrapped in honest tactics (e.g. `bv_decide`) are generally trustworthy. The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted. -General use (`decide +native` or direct use of `ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the Kernel's evaluation. +General use (`decide +native` or direct use of {name}`ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation. In particular, all `implemented_by`/`extern` attributes in libraries become part of the trusted code base. All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`. From 259853b3deb0c5a7fff4410e52047a4fa6bf529c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:59:17 +0100 Subject: [PATCH 26/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index b3075fcfb..dae39901a 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -200,7 +200,7 @@ This check is meaningful if the theorem statement in the trusted challenge file ## Comments At the time of writing, `comparator` uses only the official Lean kernel. -In the future it will be possible to use multiple, independent kernel implementations easily; then this will also protect against implementation bugs in the official Lean kernel. +In the future it will be easy to use multiple, independent kernel implementations; then this will also protect against implementation bugs in the official Lean kernel. # Remaining Issues From f19516f7b9f08315a32e369cab1a6855062b8b52 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:59:31 +0100 Subject: [PATCH 27/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index dae39901a..8ce823a32 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -212,7 +212,7 @@ When following the gold standard of checking proofs using comparator, some assum * The safety of the sandbox used by `comparator` * No human error or misleading presentation of the theorem statement in the trusted challenge file. -# On Lean.trustCompiler +# On `Lean.trustCompiler` Lean supports proofs by native evaluation. This is used by the `decide +native` tactic or internally by specific tactics (`bv_decide` in particular) and produces proof terms that call compiled Lean code to do a calculation that is then trusted by the kernel. From 885dd2ac87cfd8ea7bc1cd7a1c03d55ea705772f Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:59:47 +0100 Subject: [PATCH 28/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 8ce823a32..786e68c24 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -215,7 +215,7 @@ When following the gold standard of checking proofs using comparator, some assum # On `Lean.trustCompiler` Lean supports proofs by native evaluation. -This is used by the `decide +native` tactic or internally by specific tactics (`bv_decide` in particular) and produces proof terms that call compiled Lean code to do a calculation that is then trusted by the kernel. +This is used by the `decide +native` tactic or internally by specific tactics ({tactic}`bv_decide` in particular) and produces proof terms that call compiled Lean code to do a calculation that is then trusted by the kernel. Specific uses wrapped in honest tactics (e.g. `bv_decide`) are generally trustworthy. The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted. From 6c1ac0ddf66f3d20dc8346222bf09aa2307faefa Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:59:58 +0100 Subject: [PATCH 29/36] Update Manual/ValidatingProofs.lean Co-authored-by: David Thrane Christiansen --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 786e68c24..5405f1e61 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -217,7 +217,7 @@ When following the gold standard of checking proofs using comparator, some assum Lean supports proofs by native evaluation. This is used by the `decide +native` tactic or internally by specific tactics ({tactic}`bv_decide` in particular) and produces proof terms that call compiled Lean code to do a calculation that is then trusted by the kernel. -Specific uses wrapped in honest tactics (e.g. `bv_decide`) are generally trustworthy. +Specific uses wrapped in honest tactics (e.g. {tactic}`bv_decide`) are generally trustworthy. The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted. General use (`decide +native` or direct use of {name}`ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation. From c8ce32db78ad453f940a57e19742fa3e8262c070 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 9 Jan 2026 16:01:31 +0000 Subject: [PATCH 30/36] fix --- Manual/ValidatingProofs.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 5405f1e61..9a4dfe497 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -220,10 +220,9 @@ This is used by the `decide +native` tactic or internally by specific tactics ({ Specific uses wrapped in honest tactics (e.g. {tactic}`bv_decide`) are generally trustworthy. The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted. -General use (`decide +native` or direct use of {name}`ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation. +General use (`decide +native` or direct use of {name}`Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation. In particular, all `implemented_by`/`extern` attributes in libraries become part of the trusted code base. All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`. External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler. When that level of checking is needed, proofs have to avoid using native evaluation. - From d47c44207a2a8d5090835725ae98e941d0db1107 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 12 Jan 2026 11:14:05 +0100 Subject: [PATCH 31/36] Update Manual/ValidatingProofs.lean Co-authored-by: Joachim Breitner --- Manual/ValidatingProofs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 9a4dfe497..60725a4f1 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -221,7 +221,7 @@ Specific uses wrapped in honest tactics (e.g. {tactic}`bv_decide`) are generally The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted. General use (`decide +native` or direct use of {name}`Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation. -In particular, all `implemented_by`/`extern` attributes in libraries become part of the trusted code base. +In particular, for every {attr}`implemented_by`/{attr}`extern` attribute in libraries it becomes part of the trusted code base that the replacement is semantically equivalent. All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`. External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler. From 941080980b416ac31b83c95054cad4bfdd163a1d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 12 Jan 2026 14:37:53 +0100 Subject: [PATCH 32/36] Full markup + bump Verso for new feature --- Manual/Meta/LakeCmd.lean | 2 +- Manual/Meta/ModuleExample.lean | 10 +++-- Manual/ValidatingProofs.lean | 69 ++++++++++++++++++++-------------- lake-manifest.json | 2 +- 4 files changed, 50 insertions(+), 33 deletions(-) diff --git a/Manual/Meta/LakeCmd.lean b/Manual/Meta/LakeCmd.lean index 1e25cc54a..9ea9d29b7 100644 --- a/Manual/Meta/LakeCmd.lean +++ b/Manual/Meta/LakeCmd.lean @@ -390,7 +390,7 @@ a.lake-command:hover { if let some dest := (← read).traverseState.externalTags[id]? then return {{s!"lake {n}"}} - HtmlT.logError "No name for lake command" + HtmlT.logError s!"No name for lake command in {data.compress}" is.mapM goI @[role_expander lakeArgs] diff --git a/Manual/Meta/ModuleExample.lean b/Manual/Meta/ModuleExample.lean index bc857057d..f1302fb85 100644 --- a/Manual/Meta/ModuleExample.lean +++ b/Manual/Meta/ModuleExample.lean @@ -29,13 +29,14 @@ structure ModuleConfig where name : Option Ident := none moduleName : Option Ident := none error : Bool := false + «show» : Bool := true section variable [Monad m] [MonadError m] instance : FromArgs ModuleConfig m where - fromArgs := ModuleConfig.mk <$> .named' `name true <*> .named' `moduleName true <*> .flag `error false + fromArgs := ModuleConfig.mk <$> .named' `name true <*> .named' `moduleName true <*> .flag `error false <*> .flag `show true end @@ -90,7 +91,7 @@ def lineStx [Monad m] [MonadFileMap m] (l : Nat) : m Syntax := do @[code_block] def leanModule : CodeBlockExpanderOf ModuleConfig - | { name, moduleName, error }, str => do + | { name, moduleName, error, «show» }, str => do let line := (← getFileMap).utf8PosToLspPos str.raw.getPos! |>.line let leanCode := line.fold (fun _ _ s => s.push '\n') "" ++ str.getString ++ "\n" let hl ← IO.FS.withTempDir fun dirname => do @@ -153,7 +154,10 @@ def leanModule : CodeBlockExpanderOf ModuleConfig if !error && hasError then logError "No error expected in code block, but one occurred." - ``(Verso.Doc.Block.other (Verso.Genre.Manual.InlineLean.Block.lean $(quote hl)) #[]) + if «show» then + ``(Verso.Doc.Block.other (Verso.Genre.Manual.InlineLean.Block.lean $(quote hl)) #[]) + else + ``(Verso.Doc.Block.empty) structure IdentRefConfig where name : Ident diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 9a4dfe497..818da75da 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -7,12 +7,16 @@ import VersoManual import Manual.Meta +import Verso.Code.External + open Verso.Genre Manual open Verso.Genre.Manual.InlineLean set_option pp.rawOnError true set_option guard_msgs.diff true +open Verso.Code.External (lit) + open Lean (Syntax SourceInfo) #doc (Manual) "Validating a Lean Proof" => @@ -24,12 +28,12 @@ tag := "validating-proofs" This section discusses how to validate a proof expressed in Lean. Depending on the circumstances, additional steps may be recommended to rule out misleading proofs. -In particular, it matters a lot whether one is dealing with an honest proof attempt, and needs protection against only benign mistakes, or a possibly-malicious proof attempt that actively tries to mislead. +In particular, it matters a lot whether one is dealing with an {tech}[honest] proof attempt, and needs protection against only benign mistakes, or a possibly-{tech}[malicious] proof attempt that actively tries to mislead. -In particular, we use “honest” when the goal is to create a valid proof. +In particular, we use {deftech}_honest_ when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system. -In contrast, we use “malicious” to describe code to go out of its way to trick or mislead the user, exploit bugs or compromise the system. +In contrast, we use {deftech}_malicious_ to describe code to go out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes unreviewed AI-generated proofs and programs. Furthermore it is important to distinguish the question “does the theorem have a valid proof” from “what does the theorem statement mean”. @@ -48,7 +52,7 @@ In regular everyday use of Lean, it suffices to check the blue double check mark While working interactively with Lean, once the theorem is proved, blue double check marks appear in the gutter to the left of the code. :::figure "A double blue check mark" -![Double blue check marks appearing in the editor gutter](/static/screenshots/doublecheckmarks.png) +![A theorem with double blue check marks appearing in the editor gutter](/static/screenshots/doublecheckmarks.png) ::: ## Significance @@ -57,7 +61,7 @@ The blue ticks indicate that the theorem statement has been successfully elabora ## Trust -This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and trusts the authors of the imported libraries to be honest, that they performed this check, and that no unsound axioms have been declared and used. +This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and trusts the authors of the imported libraries to be {tech}[honest], that they performed this check, and that no unsound axioms have been declared and used. ## Protection @@ -65,8 +69,8 @@ This check is meaningful if one believes the formal theorem statement correspond This check protects against * Incomplete proof (missing goals, tactic error) *of the current theorem* -* Explicit use of `sorry` *in the current theorem* -* Honest bugs in meta-programs and tactics +* Explicit use of {lean}`sorry` *in the current theorem* +* {tech}[Honest] bugs in meta-programs and tactics * Proofs still being checked in the background ::: @@ -75,7 +79,7 @@ This check protects against In the Visual Studio Code extension settings, the symbol can be changed. Editors other than VS Code may have a different indication. -Running `lake build +Module`, where `Module` refers to the file containing the theorem, and observing success without error messages or warnings provides the same guarantees. +Running {lake}`build`{lit}` +Module`, where {lit}`Module` refers to the file containing the theorem, and observing success without error messages or warnings provides the same guarantees. # Printing Axioms %%% @@ -87,20 +91,28 @@ Because both {lean}`sorry` and incomplete proofs are elaborated to axioms, their ## Instructions -Write `#print axioms thmName` after the theorem declaration, with `thmName` replaced by the name of the theorem and check that it reports only the built-in axioms {name}`propext`, {name}`Classical.choice`, and {name}`Quot.sound`. +:::keepEnv +```lean -show +inductive TheoremStatement : Prop where | intro +theorem thmName : TheoremStatement := .intro +``` + +Write {leanCommand}`#print axioms thmName` after the theorem declaration, with {lean}`thmName` replaced by the name of the theorem and check that it reports only the built-in axioms {name}`propext`, {name}`Classical.choice`, and {name}`Quot.sound`. + +::: ## Significance This command prints the set of axioms used by the theorem and the theorems it depends on. The three axioms above are standard axioms of Lean's logic, and benign. -* If {name}`sorryAx` is reported, then this theorem or one of its dependencies uses `sorry` or is otherwise incomplete. -* If {name}`Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion. +* If {name}`sorryAx` is reported, then this theorem or one of its dependencies uses {lean}`sorry` or is otherwise incomplete. +* If {name}`Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion. * Any other axiom means that a custom axiom was declared and used, and the theorem is only valid relative to the soundness of these axioms. ## Trust -This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and one trusts the authors of the imported libraries to be honest. +This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and one trusts the authors of the imported libraries to be {tech}[honest]. ## Protection @@ -108,16 +120,17 @@ This check is meaningful if one believes the formal theorem statement correspond (In addition to the list above) * Incomplete proofs -* Explicit use of `sorry` +* Explicit use of {lean}`sorry` * Custom axioms ::: ## Comments -At the time of writing, the `#print axioms` command does not work in a `module`. -To work around this, create a non-module file, `import` your module, and use `#print axioms` there. +At the time of writing, the {keywordOf Lean.Parser.Command.printAxioms}`#print axioms` command does not work in a {tech}[module]. +To work around this, create a non-module file, import your module, and use {keywordOf Lean.Parser.Command.printAxioms}`#print axioms` there. -```leanModule +```leanModule -show +-- This module validates the claim in the preceding paragraph that #print axioms doesn't work here module /-- error: cannot use `#print axioms` in a `module`; consider temporarily removing the `module` header or placing the command in a separate file @@ -140,11 +153,11 @@ Build your project using {lake}`build`, run `lean4checker --fresh` on the module ## Significance The `lean4checker` tool reads the declarations and proofs as they are stored by `lean` during building (the {tech}[`.olean` files]), and replays them through the kernel. -It trusts that the `.olean` files are structurally correct. +It trusts that the {tech}[`.olean` files] are structurally correct. ## Trust -This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and believes the authors of the imported libraries to not be very cunningly malicious, and to neither compromise the user’s system nor use Lean’s extensibility to change the interpretation of the theorem statement. +This check is meaningful if one believes the formal theorem statement corresponds to its intended informal meanings and believes the authors of the imported libraries to not be very cunningly {tech}[malicious], and to neither compromise the user’s system nor use Lean’s extensibility to change the interpretation of the theorem statement. ## Protection @@ -157,10 +170,10 @@ This check is meaningful if one believes the formal theorem statement correspond ## Comments -Since `lean4checker` reads the `.olean` files without validating their format, this check is prone to an attacker crafting invalid `.olean` files (e.g. invalid pointers, invalid data in strings). +Since `lean4checker` reads the {tech}[`.olean` files] without validating their format, this check is prone to an attacker crafting invalid `.olean` files (e.g. invalid pointers, invalid data in strings). Lean tactics and other meta-code can perform arbitrary actions when run. -Importing libraries created by a determined malicious attacker and building them without further protection can compromise the user's system, after which no further meaningful checks are possible. +Importing libraries created by a determined {tech}[malicious] attacker and building them without further protection can compromise the user's system, after which no further meaningful checks are possible. We recommend running `lean4checker` as part of CI for the additional protection against bugs in Lean's handling of declaration and as a deterrent against simple attacks. The [lean-action](https://github.com/leanprover/lean-action) Github Action provides this functionality by setting `lean4checker: true`. @@ -172,7 +185,7 @@ Without the `--fresh` flag the tool can be instructed to only check some modules tag := "validating-comparator" %%% -To protect against a seriously malicious proof compromising how Lean interprets a theorem statement or the user's system, additional steps are necessary. +To protect against a seriously {tech}[malicious] proof compromising how Lean interprets a theorem statement or the user's system, additional steps are necessary. This should only be necessary for high risk scenarios (proof marketplaces, high-reward proof competitions). ## Instructions @@ -181,20 +194,20 @@ In a trusted environment, write the theorem *statement* (the ”challenge”), a ## Significance -Comparator will build the proof in a sandboxed environment, to protect against malicious code in the build step. +Comparator will build the proof in a sandboxed environment, to protect against {tech}[malicious] code in the build step. The proof term is exported to a serialized format. Outside the sandbox and out of the reach of possibly malicious code, it validates the exported format, loads the proofs, replays them using Lean's kernel, and checks that the proved theorem statement matches the one in the challenge file. ## Trust -This check is meaningful if the theorem statement in the trusted challenge file is correct and the sandbox used to build the possibly malicious code is safe. +This check is meaningful if the theorem statement in the trusted challenge file is correct and the sandbox used to build the possibly-{tech}[malicious] code is safe. ## Protection :::listBullet "🛡️" (In addition to the list above) -* Actively malicious proofs +* Actively {tech}[malicious] proofs ::: ## Comments @@ -215,13 +228,13 @@ When following the gold standard of checking proofs using comparator, some assum # On `Lean.trustCompiler` Lean supports proofs by native evaluation. -This is used by the `decide +native` tactic or internally by specific tactics ({tactic}`bv_decide` in particular) and produces proof terms that call compiled Lean code to do a calculation that is then trusted by the kernel. +This is used by the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` tactic or internally by specific tactics ({tactic}`bv_decide` in particular) and produces proof terms that call compiled Lean code to do a calculation that is then trusted by the kernel. -Specific uses wrapped in honest tactics (e.g. {tactic}`bv_decide`) are generally trustworthy. +Specific uses wrapped in {tech}[honest] tactics (e.g. {tactic}`bv_decide`) are generally trustworthy. The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted. -General use (`decide +native` or direct use of {name}`Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation. -In particular, all `implemented_by`/`extern` attributes in libraries become part of the trusted code base. +General use ({tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` or direct use of {name}`Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation. +In particular, all {attr}`implemented_by`/{attr}`extern` attributes in libraries become part of the trusted code base. All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`. External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler. diff --git a/lake-manifest.json b/lake-manifest.json index af350f700..afea7924d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "3efce68b1f739bc9f10d9d9ced5156764f0adbfc", + "rev": "4abb9845e9019e09769c8f0656c0948c5336d2be", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "main", From 76abf711d2817020718695793a22a8eaed88bb90 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 12 Jan 2026 14:59:52 +0100 Subject: [PATCH 33/36] move to top-level appendix --- Manual.lean | 2 ++ Manual/Elaboration.lean | 2 -- Manual/ValidatingProofs.lean | 1 + 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Manual.lean b/Manual.lean index 62db87c79..c11321c2f 100644 --- a/Manual.lean +++ b/Manual.lean @@ -140,6 +140,8 @@ Overview of the standard library, including types from the prelude and those tha {include 0 Manual.BuildTools} +{include 0 Manual.ValidatingProofs} + {include 0 Manual.ErrorExplanations} {include 0 Manual.Releases} diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean index e38e5b183..24d41dc3a 100644 --- a/Manual/Elaboration.lean +++ b/Manual/Elaboration.lean @@ -466,5 +466,3 @@ builtin_initialize $x:ident : $t:term ← $cmd* ``` ::: - -{include 0 Manual.ValidatingProofs} diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index cb6eee5ec..ed8b97745 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -23,6 +23,7 @@ open Lean (Syntax SourceInfo) %%% file := "ValidatingProofs" tag := "validating-proofs" +number := false %%% This section discusses how to validate a proof expressed in Lean. From abb752f362336e81dcfc6db7e0f5284bb0cee326 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 12 Jan 2026 15:28:37 +0100 Subject: [PATCH 34/36] prose linter --- .vale/styles/config/ignore/terms.txt | 1 + .vale/styles/proselint/Cliches.yml | 2 +- Manual/ValidatingProofs.lean | 4 ++-- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt index bb5c84359..d976246cf 100644 --- a/.vale/styles/config/ignore/terms.txt +++ b/.vale/styles/config/ignore/terms.txt @@ -164,6 +164,7 @@ recursor recursor's recursors Repr +sandboxed satisfiability scrutinee scrutinees diff --git a/.vale/styles/proselint/Cliches.yml b/.vale/styles/proselint/Cliches.yml index eae0b1f3c..5fe497caa 100644 --- a/.vale/styles/proselint/Cliches.yml +++ b/.vale/styles/proselint/Cliches.yml @@ -341,7 +341,7 @@ tokens: - in hot water - in light of - in the final analysis - - in the gutter + # - in the gutter # we use this for the editor gutter - in the last analysis - in the nick of time - in the thick of it diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index ed8b97745..89e714475 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -35,7 +35,7 @@ In particular, we use {deftech}_honest_ when the goal is to create a valid proof This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system. In contrast, we use {deftech}_malicious_ to describe code to go out of its way to trick or mislead the user, exploit bugs or compromise the system. -This includes unreviewed AI-generated proofs and programs. +This includes un-reviewed AI-generated proofs and programs. Furthermore it is important to distinguish the question “does the theorem have a valid proof” from “what does the theorem statement mean”. @@ -177,7 +177,7 @@ Lean tactics and other meta-code can perform arbitrary actions when run. Importing libraries created by a determined {tech}[malicious] attacker and building them without further protection can compromise the user's system, after which no further meaningful checks are possible. We recommend running `lean4checker` as part of CI for the additional protection against bugs in Lean's handling of declaration and as a deterrent against simple attacks. -The [lean-action](https://github.com/leanprover/lean-action) Github Action provides this functionality by setting `lean4checker: true`. +The [lean-action](https://github.com/leanprover/lean-action) GitHub Action provides this functionality by setting `lean4checker: true`. Without the `--fresh` flag the tool can be instructed to only check some modules, and assume others to be correct (e.g. trusted libraries), for faster processing. From 1bd374ad2ce5a968c04b0ecb561863b7e6fb56d3 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Mon, 12 Jan 2026 16:48:13 +0100 Subject: [PATCH 35/36] no split --- Manual/ValidatingProofs.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index 89e714475..b8d548a1f 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -24,6 +24,7 @@ open Lean (Syntax SourceInfo) file := "ValidatingProofs" tag := "validating-proofs" number := false +htmlSplit := .never %%% This section discusses how to validate a proof expressed in Lean. From 752f528d1bed458b858ef210276829b5aaae7e08 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 13 Jan 2026 15:23:00 +0100 Subject: [PATCH 36/36] Apply suggestion from @nomeata --- Manual/ValidatingProofs.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Manual/ValidatingProofs.lean b/Manual/ValidatingProofs.lean index b8d548a1f..224b3ac7f 100644 --- a/Manual/ValidatingProofs.lean +++ b/Manual/ValidatingProofs.lean @@ -228,6 +228,9 @@ When following the gold standard of checking proofs using comparator, some assum * No human error or misleading presentation of the theorem statement in the trusted challenge file. # On `Lean.trustCompiler` +%%% +tag := "validating-trustCompiler" +%%% Lean supports proofs by native evaluation. This is used by the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` tactic or internally by specific tactics ({tactic}`bv_decide` in particular) and produces proof terms that call compiled Lean code to do a calculation that is then trusted by the kernel.