Hi, On Tue, Sep 13, 2016 at 08:12:58PM +0200, Jens-Wolfhard Schicke-Uffmann wrote: > today I finished proving correctness of the first C function of a larger > project against an axiomatisation of a subset of binary ARM assembly, > run as a bare-metal image on a Rasberry Pi. This project is the reason > why I made igor. > > You can find the abridged, relevant files at > http://drahflow.name/2016-09-13-large-proof.tbz2 > > The proof of lem-function-exchange_mail is potentially > the largest currently existing metamath proof and might be > an interesting test case for verifiers in its own right. It _was_ the largest (showing correctness of a 102 instruction function). After resuming said project a few months back, I found that the proof assistant infrastructure would not scale up very well, and instead rewrote most of it to tackle a function of 287 instructions.
http://drahflow.name/2019-09-09-lem-function-init_local_framebuffer.tbz2 % metamath system-invariant.mm MM> verify proof lem-function-init_local_framebuffer ... 17 seconds and 1.3 GB RAM later ... lem-function-init_local_framebuffer MM> Files: * arm.mm - Axiomatization of a (very small) subset of ARM instructions * kernel7.img.mm - Metamath-yfied firmware image * kernel7.invariant.mm - Assembler-generated (very simple) invariant definition * kernel7.mm - Lemmata for the C functions * lem-function-init_local_framebuffer.igor - Proof script input to igor * system-invariant.ey - Project specific automations for igor * system-invariant.mm - Root metamath file, includes the others * set.mm - Pretty old, but compatible set.mm This is all work in progress, so don't expect particularly good presentation. Also, I am sure the proof could be optimized in many ways. According to igor's statistics, the proof has 1775932 steps (after proof compression), of which ~1100000 should be non-syntax steps of some sort. It took around 60 minutes (and ~10 GB RAM) to build this proof from lem-function-init_local_framebuffer.igor Most relevant (to me) is the fact that this proof includes a function call to exchange_mail, i.e. the other function already shown. The invariant from the calling function is successfully carried through all steps of the called function, without having to explicitly show this for each instruction. I invite you to also check lem-function-init_local_framebuffer.igor, to get an idea of what automations are already available, some nice things (if you're used to step-by-step style): * Everything is deduction style, shuffling of the antecedents is fully automated. * Rewrite support > rewrite ( ; ; ; ; ; ; ; 1 6 7 7 7 2 1 7 mod ; ; ; ; 6 5 5 3 6 ) = 1 The left side is replaced in all antecedents and in the goal conclusion with the right side. (And the arithmetics for this case are fully automated, too.) * Instantiating universal quantifiers for concrete instances > instantiate A. a e. cpu-mem ( ( a >_ ( x reg ; 1 3 ) /\ -. a e. ( { n e. NN0 > | ( n >_ ; ; ; ; 3 7 4 3 6 /\ n < ; ; ; ; 3 7 4 4 0 ) } u. ( { n e. NN0 | ( n > >_ ; ; ; ; 3 7 4 4 0 /\ n < ; ; ; ; 3 7 4 4 4 ) } u. { n e. NN0 | ( n >_ ; ; > ; ; 3 7 4 4 4 /\ n < ; ; ; ; 3 7 4 4 8 ) } ) ) ) -> ( u mem a ) = ( x mem a ) > ) for a (Including the required renaming, where needed.) Regards, Drahflow -- 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/20190909074140.GA7085%40serpentis.drahflow.name.
signature.asc
Description: PGP signature
