On Mon, Dec 14, 2020 at 3:11 PM David A. Wheeler <[email protected]> wrote:
> > > On Dec 14, 2020, at 3:01 PM, Mario Carneiro <[email protected]> wrote: > I also think that 200 is an okay "soft maximum". I've definitely got some > theorems larger than that, some a lot larger, and the MM0 project is going > to generate some really large proofs (the largest so far is 673 steps but > that's still mostly handwritten; the autogenerated proofs are going to be > huge), but given that several verifiers tend to choke on large proofs it's > best to keep them out of set.mm. > > > No one’s going to be shot for exceeding 200. But if it’s really unusual > for handwritten proofs to exceed 500, and the vast majority are under 200, > then writing this down as a convention has succeeded. I would encourage > even smaller proofs than that, especially if they create reusable proofs; I > think there are hidden reusable gems in some of our larger proofs. > > If autogenerated proofs are huge, I presume it’s because they’re expanding > something in place. That’s okay short-term. Longer-term, maybe we can > modify the generators to also break up the proofs (e.g., if a template > generates something long, create the template as a separate proof), or > create a more-general proof that other proofs can directly use. So I think > the guideline can help us create long-term improvements to generated proofs > as well. > No, here I mean irreducibly huge. Breaking them up would make them a lot *less* efficient because there are a lot of interconnections and reused terms. > *Verifiers* shouldn’t struggle with large proofs. Can you give an example? > Here's the largest definition in MM0 right now (below). It's larger than the largest set.mm definition by a pretty significant margin, I think. Proving the equality theorem for this is already 250 steps, and the 673 step proof I mentioned is the typing statement (i.e. closure) for it. (It is the execution semantics of x86.) This is peanuts compared to the definition of an actual program, as a sequence of instructions. Currently the plan is to segment the definitions at the function level, which is still going to result in definitions which are about 50 times the size of this one, and the typing/correctness proof of said function will be on the same order of magnitude with a hefty constant factor. The MM0 verifier makes very short work of this theorem and all others. Currently the entire library (7400 theorems) verifies in 25ms, and I don't expect that to change once I start bringing out the big guns. But MM0 was designed with this use in mind, and it makes much greater use of long theorem statements that can be represented more efficiently in MM0 than in MM due to the use of expression tree deduplication. Eventually I will try to port things over but I expect that some of the proofs being generated will bring one verifier or another to its knees. Mario abstract def execXAST (k ast k2: nat): wff = $ ast e. Sum (Sum (Sum (Sum (S\ op, S\ sz, {rm | E. q (readEA k sz (RM_EA k rm) q /\ writeUnop k op sz (RM_EA k rm) q k2)}) (S\ op, S\ sz, {ds | E. d E. s (readEA k sz (destEA k ds) d /\ readEA k sz (srcEA k ds) s /\ writeBinop k op sz (destEA k ds) d s k2)})) (Sum (S\ _0, {_1 | _0 e. ocasep (_1 e. S\ sz, {rm | E. n E. src E. res (n = wsizeBits sz /\ readEA k sz (RM_EA k rm) src /\ res = readRegSz k sz RAX * src /\ ifp (n = 8) (k2 = writeReg k wSz16 RAX res) (E. lo E. hi (splitBits ((n <> lo) : (n <> hi) : 0) res /\ k2 = writeReg (writeReg k sz RAX lo) sz RDX hi)))}) {_2 | _1 e. S\ sz, {rm | E. n E. a E. b E. d E. m (n = wsizeBits sz /\ readEA k sz (RM_EA k rm) b /\ divModSz sz a b d m /\ ifp (n = 8) (a = readRegSz k wSz16 RAX /\ eraseFlags (writeReg k sz RAX (shl m 8 + d)) k2) (splitBits ((n <> readRegSz k sz RAX) : (n <> readRegSz k sz RDX) : 0) a /\ eraseFlags (writeReg (writeReg k sz RAX d) sz RDX m) k2))}}}) (S\ sz, {ds | writeEA k sz (destEA k ds) (EA_addr (srcEA k ds)) k2}))) (Sum (S\ _0, {_1 | _0 e. {sz | _1 e. Sum (S\ _2, {_3 | _2 e. ocasep (_3 e. S\ ds, {sz2 | E. src (readEA k sz (srcEA k ds) src /\ writeEA k sz2 (destEA k ds) src k2)}) {_4 | _3 e. S\ ds, {sz2 | E. src (readEA k sz (srcEA k ds) src /\ writeEA k sz2 (destEA k ds) (sExt (wsizeBits sz) (wsizeBits sz2) src) k2)}}} ) (S\ _2, {_3 | _2 e. ocasep (_3 e. S\ rm, {r | E. v (readEA k sz (RM_EA k rm) v /\ writeEA (writeReg k sz r v) sz (RM_EA k rm) (readRegSz k sz r) k2)}) (ocasep (_3 e. S\ rm, {r | E. src E. acc E. dst E. ki (acc = readRegSz k sz RAX /\ readEA k sz (RM_EA k rm) dst /\ writeBinop k binopCmp sz (EA_r r) acc dst ki /\ ifp (acc = dst) (writeEA ki sz (RM_EA k rm) (readRegSz k sz r) k2) (writeEA ki sz (EA_r RAX) dst k2))}) {_4 | _3 e. S\ rm, {r | E. v (readEA k sz (RM_EA k rm) v /\ writeBinop k binopAdd sz (RM_EA k rm) (readRegSz k sz r) v k2)}})})}}) (S\ _0, {_1 | _0 e. {c | _1 e. Sum (S\ sz, {ds | ifp (readCond k c) (E. v (readEA k sz (srcEA k ds) v /\ writeEA k sz (destEA k ds) v k2)) (k2 = k)}) (S\ b, {rm | writeEA k (wSz8 (true b)) (RM_EA k rm) (nat (readCond k c)) k2})}}))) (Sum (Sum (Sum (Sum {rm | E. v (readEA k wSz64 (RM_EA k rm) v /\ k2 = writeRIP k v)} (S\ c, {q | k2 = if (readCond k c) (writeRIP k (readRIP k +_64 q)) k})) (Sum {irm | E. ki (pushRIP k ki /\ EA_jump ki (immRM_EA k irm) k2)} {q | E. ki (popRIP k ki /\ k2 = setReg ki RSP (readReg ki RSP +_64 q))})) (ocasep (popWrite (setReg k RSP (readReg k RBP)) (RM_reg RBP) k2) (Sum {irm | pushImmRM k irm k2} {rm | popWrite k rm k2}))) (ocasep (k2 = writeFlags k (setCF (readFlags k) (~CF (readFlags k)))) (ocasep (k2 = writeFlags k (setCF (readFlags k) F.)) (ocasep (k2 = writeFlags k (setCF (readFlags k) T.)) {_0 | E. r11 (r11 e. u64 /\ k2 = setException (setReg (setReg k RCX (readRIP k)) 11 r11) (suc exSysCall))})))) $; -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStFxUuGiY8TzSgQAe5dQQ%3DyuPdzZhkmCGr89FPnBg_frg%40mail.gmail.com.
