mm0 for kotlin

[Lakedaemon]

Hello,

In the peano examples. Is it normal that term al
has type wff () in mmu :
(term al ((x nat) (ph wff (x))) (wff ()))
and type wff (x) in mm0 :
term al {x: nat} (p: wff x): wff;

Is a proofchecker supposed to let that go or not ?
and the variable names are also different p != ph, is it supposed to let that go ?

In which case, how does the proofchecker decide that a mmu directive corresponds to a mm0 statement ?

I get that the mmu file is the source of truth and that binders are actually used with respects to the order they have in the mmu file and that the mm0 file is just supposed to reflect how variables are used in the formula but present it to the human reader in a eye-pleasing manner (for example (x y z : nat) (ph:wff) instead of (x:nat) (ph : wff) (z:nat) (y:nat)
and that order is not that important in the mm0 file.

All that because, the computer will do the proof building dirty work behind the scene and it knows what it needs to do it.

But shouldn't the names be the same ?
(for terms, that might not be that important, maybe that is a tolerance for them)

[bjorn3]

The proofchecker doesn't know anything about mmu files. Mmu files are compiled to mm0 files containing all theorems and mmb fioes containing all proofs. The proofchecker then checks that all theorems in the mm0 file are satisfied by using the proofs in the corresponding mmb file. Mmu files only exist to make it easier to write everything as far as I know. This allows for a simpler and thus more likely correct proofchecker.

[Lakedaemon]

thanks for the answer.
I'm not planning to use mmb files because, as I understand it those are supposed to be platform/software dependant,
contrary to mmu files (which are somewhat documented)

The way I see it, mmu files would be a really good interchange format between software/platforms.
As it is quite easy to understand how they work and to implement software on top of them.

Once mmu (and mm0) is fully understood, it is easier to implement a performance-oriented custom binary format to work with proofs.

Though I am planning to use a custom binary format (that avoids allocation, if possible by proofChecking in place),
I plan to support conversion from/to classic mmu files to allow interchange between my software and those of others

Also, just before merging mm0/mmu files, I check that the mm0 statement and the mmu directive points to the same stuff (or the public guman api publicized in the mm0 file would be lying about what goes on, whch is unproductive) and then I check theorems (assynchronically) before yielding a merged statement/directive...(with a Future check answer)

It allows me to build more complete error reports than just the first one and stopping
And I hope, to give humans a better user experience

[Lakedaemon]

My Bad. I was using old versions of peano.mm0 and peano.mmu

With the latest versions of peano;mmu and peano.mm0, I'm still encountering issues with names though like
(term im ((ph wff ()) (ps wff ())) (wff ()))
term im (p q: wff): wff;

[digama0]

MMU files are the "text mode" representation of MMB files, like with WASM text/binary formats. They are intended primarily for debugging, and you can use mm0-rs to convert between MMB and MMU format. Support for MMU is limited, however, and in particular the reference proof checker mm0-c knows nothing about MMU files.

MMB files are not platform dependent, and while I think the possibility of alternate proof formats still exists I'm trying to get all the supporting tools to converge on MMB. Currently you can use the mmb_parser rust crate to parse out data in the MMB format, but beyond that the documentation is in the form of comments around C data structures in mm0-c.

If you are planning a custom binary format, then I would like to know what you intend to support so that MMB can be made inter-convertible with it. I recently added an extensible table structure for the "index" (the non-verified data), which should now be able to handle arbitrary metadata coming from different provers like theorem names, attributes on theorems, lisp metaprograms (in the case of MM1) and so on.

Regarding the error in peano.mmu, you might consider checking up to alpha equivalence (i.e. including renamings of local variables), but the real reason for the error is that peano.mmu is ancient and almost certainly does not reflect recent changes to peano.mm1. But it's not so hard to regenerate the file using mm0-rs compile peano.mm1 peano.mmu.

[digama0]

I updated the MMB and MMU files in commit 13e7bfd.

[digama0]

There is now an MMB spec at https://github.com/digama0/mm0/blob/master/mm0-c/mmb.md . Hopefully that addresses your documentation needs, and if not feel free to make additional suggestions on what should go in there if something needs clarification.

[Lakedaemon]

This helps really a lot (now I can look at the mmu documentation and the mmb documentation, without having to learn a new language). This makes things a lot better on my side.

I have juste looked quickly at the mmb spec. I am sure that it is full of really smart stuff.
I cannot promise that I will work on the mmb format though because :

• I worked on FlatBuffer a few years ago (I pr-ed Kotlin-support in 2017, but it never went in. It looks like they finally have kotlin support in now, since mid 2019) and Kotlin is really different from C/C++/Assembly language.
  For example, kotlin projects to Java/Javascript/native code...

And Java uses (or used to use) modified UTF-16 strings (not utf8). So, in my experience, something that works really great for C++ isn't sometimes appropriate for Kotlin/Jvm
(I had to encode modified U-16 strings in unsigned U16 vectors)

• I could call a C/C++/Rust library from kotlin but then, I would lose the awesome benefits form writing kotlin code (it works on many platforms at the same time)

So, that probably means using ByteBuffer (to be able to mmap things) and working on bytes like you do, ..

So well, maybee there is a way, but it is too soon for me to know; So, I cannot promise anything. :)
thanks for the documentation, tough, I love it ! :)

I'll look really really hard at it and try to implement the smart stuff I get.
(proof as streams sound to me like the way to go, ...)

Time will tell.
Concerning aligning mm0 and mmu. I am looking at the alpha-renaming problem (trying to find a good/performant way to do it).

[Lakedaemon]

The proofchecker doesn't know anything about mmu files. Mmu files are compiled to mm0 files containing all theorems and mmb fioes containing all proofs. The proofchecker then checks that all theorems in the mm0 file are satisfied by using the proofs in the corresponding mmb file. Mmu files only exist to make it easier to write everything as far as I know. This allows for a simpler and thus more likely correct proofchecker.

I ponder your answer.

So you say that
mmu file --[exports]--> a mm0 file and a mmb file
And then
mm0 + mmb --[proofChecker]--> pass or fail

This is not what I have been believing for the past year and a half (but maybe I was wrong)

I thought that mmu and mmb files were intercheangeable and could both be used with a mm0 file to checkproof stuff
(mmu being string based and mmb behing binary based).

Also, till now, only mmu was documented which led me to think that it was expected for software developer to implement their own binary format and to use the documented mmu format for interoperability with others.

My bad, if I was wrong.

Anyway, it is already hard enough to implement a (correct) proofchecker for mm0 + mmu (it is even harder with alpha renaming to do), I cannot fathom how hard it would be for someone new to mm0 to implement a correct proof checker for mm0 + mmb
(maybee one day I'll be able to, ONCE I have implemented a mmu+mm0 proofChecker though and truely understood all the stuff going on :) )

On a side point, the documentation of mmb is a real treasure. Thank you Mario for this effort.
Thank you, thank you, thank you (I love you) !

I USED to have some minor gripes with mm0/mmu.
But usually, those disappear once I understand Mario's intention (for example, it is completely unnecessary and foolish to change the mmu format, as I wanted to, once).

At the moment, I do not understand why the names of variables aren't the same on the mm0 and the mmu side.
This sounds like a huge performance regression and headache to me. But maybe I am missing something.

Is there something that is supposed to help computing the alpha-renaming stuff ?
I started thinking about it (drew dags, trees, networks) and it is not that simple to alpha-rename say
A : wff x y
B : wff x y z
C : wff x y
D : wff z
There is a way, of course for this particular setting (there are 4 alpha-renaming possibilities, here with A<->C and x<->y)
but for the general case... O.O

Am I missing something ?

[digama0]

And Java uses (or used to use) modified UTF-16 strings (not utf8). So, in my experience, something that works really great for C++ isn't sometimes appropriate for Kotlin/Jvm
(I had to encode modified U-16 strings in unsigned U16 vectors)

Kotlin should presumably have a way of decoding UTF-8 into whatever the native format is. I am using UTF-8 for specification purposes, in case other proof translators want to use unicode characters (like lean, for example), but all strings that appear in all MM0 and MM1 files in this repo (including the translated ones) are pure ASCII (and more than that, restricted to the very small character set [a-z][A-Z][0-9]_). So if you can handle ASCII you should be fine.

So, that probably means using ByteBuffer (to be able to mmap things) and working on bytes like you do, ..

Using mmap is not a requirement for parsing MMB files. It was designed so that this was reasonably possible and useful, but you can always just parse it like a regular binary format, and for languages that aren't too "systems-y" that's probably the better choice. You still have to use a ByteBuffer or something like it in order to read binary data, but maybe there is a binary deserializer package on kotlin that you can use instead.

So you say that
mmu file --[exports]--> a mm0 file and a mmb file
And then
mm0 + mmb --[proofChecker]--> pass or fail

This is not what I have been believing for the past year and a half (but maybe I was wrong)

I thought that mmu and mmb files were intercheangeable and could both be used with a mm0 file to checkproof stuff
(mmu being string based and mmb behing binary based).

I think @bjorn3 is confusing mmu with mm1 files. The picture is something like this:

mm1 -\               mm0 -\
mmb ---> mm0-rs ---> mmb ---> mm0-c -> verified
mmu -/           \-> mmu

You can use mm0-rs to import mm1, mmb or mmu files (also mm0 but those don't produce output) and export mmb or mmu files. The main pipeline is to take in mm1 and produce mmb files, but by using the other import pathways you can also use this to transform a mmb file into mmu or vice versa. The mm0-c verifier can only handle mm0 + mmb, but if you have an mm0 + mmu verifier then you would use the other export mechanism in mm0-rs to get mmu files for your use.

At the moment, I do not understand why the names of variables aren't the same on the mm0 and the mmu side.
This sounds like a huge performance regression and headache to me. But maybe I am missing something.

I haven't really decided how strict to be about allowing names in the mmu file to be different from the corresponding mm0 file. It's certainly easier to require that they are the same, but I also want to minimize the number of instances where the mm0 file has to change because of convenience for the proof author. For example, the scenario might be that the mm0 is written by someone (the "client") who wants a particular theorem verified, and the proof author should still be able to have some flexibility in writing the proof as they would like to without having to bother the client to make trivial changes to the mm0 file (which will require review, i.e. "have we accidentally trivialized the theorem?").

This is weighed against the bother of having to alpha rename things. In mmb this isn't really an issue because everything is named by indices, so the textual names of things matter very little, except when parsing the mm0 file. In fact the mm0-c verifier doesn't even care if you give different names to all the term constructors and theorems, as long as they have the same types and come in the same order. But in mmu, since it's a textual format, it's logical to index things by string names, and then you have to keep track also of the name used in the mm0 file (if applicable) for each of these entities so that you can perform the necessary translation.

In any case, for the present if it makes easier for you you can just assume that alpha renaming isn't necessary. peano.mm1 and peano.mm0 have axioms that agree exactly, not just up to alpha renaming, so the generated mmu file should also agree. That's why I updated the mmu files a little while ago - if it still has alpha renaming issues let me know.

Is there something that is supposed to help computing the alpha-renaming stuff ?
I started thinking about it (drew dags, trees, networks) and it is not that simple to alpha-rename say
A : wff x y
B : wff x y z
C : wff x y
D : wff z
There is a way, of course for this particular setting (there are 4 alpha-renaming possibilities, here with A<->C and x<->y)
but for the general case... O.O

Am I missing something ?

Ah, okay. Alpha renaming is really simple here, no fancy stuff is needed. Suppose you are trying to match expressions like:

(term al ((y nat) (ph wff (y))) (wff ()))
term al {x: nat} (p: wff x): wff;

You initialize a name map, let's say MM0 -> MMU although I think either direction will work. It starts out empty. You read the binders on both sides: (y nat) vs {x: nat}. These binders have the same type and the same sort, so they match. We add x -> y to the name map. The next binder pair is (ph wff (y)) vs (p: wff x). We apply the renaming from the name map to the dependencies, which rewrites the type to wff y. This matches the binder on the mmu side, so they match. We add p -> ph to the name map. We run out of binders on both sides at the same time, so the hypotheses match. The two return values are (wff ()) vs wff. We apply the name map to the dependencies but there aren't any, and the sorts match, so the return types match. Thus the declarations match. We clear the name map and move on.

The reason your complicated alpha renaming possibilities don't come up is because the order of arguments is not allowed to change. term foo (x: set) (y: nat): nat; and term foo (y: nat) (x: set): nat; are not the same, even up to alpha renaming. So we just compare the binders pairwise and add things to the name map as we go.

It's also possible to do alpha renaming at the level of statements; that is we would also keep a mapping of sorts, terms and such. In this case we would have nat -> nat, wff -> wff in the sort map and al -> al in the term map (there isn't any renaming happening), but the basic idea is the same: all names in the MM0 file are translated via the name map before using them to look up anything. The declared names of entities are skipped for equality testing until you know the rest of it matches, and then you use the declared name on each side to add an entry to the relevant name map, so that later uses of the declaration will have its name translated appropriately.

[bjorn3]

I think @bjorn3 is confusing mmu with mm1 files

My bad.

[Lakedaemon]

The reason your complicated alpha renaming possibilities don't come up is because the order of arguments is not allowed to change. term foo (x: set) (y: nat): nat; and term foo (y: nat) (x: set): nat; are not the same, even up to alpha renaming.

This is the important bit that I was missing.
binders for terms have THE SAME ORDER. It isn't allowed to change

I guess that this is also true for definitions, theorems and axioms.

Without that bit, the mm0/mmu model I had in my head was :
The truth (binder order) is in the mmu file
mm0 only holds an human-friendly api

Instead of seeing Strees (termId arg1 arg2) that require binder order,
I was seeing functions calls Term(arg2=,arg1=), whose binder order is irrelevant

I think that there are still alpha-renaming issues in peano.mm0 and peano.mmu (you did not refresh peano.mm0)
But now, I had the information bit I was missing to do a decent job.

IMO, it is weird that the proof author would not provide a proof with the variables names used by the client (he can change the variables names in his proof assistant software and change them back one he is finished).
It is also weird that names can be different in mm0 and mmu/mmb (but only very slightly annoying now that the same order requirements provide a quick/efficient way of doing alpha renaming)
The "same order requirement" somewhat defeats the human mm0 binders that can share names, those are now a lot less useful

But oh well, it will be ok. :)
I can work with that.

Thanks for taking the time to explain things to me.

[digama0]

I think that there are still alpha-renaming issues in peano.mm0 and peano.mmu (you did not refresh peano.mm0)

Fixed in 16fa2d8

IMO, it is weird that the proof author would not provide a proof with the variables names used by the client (he can change the variables names in his proof assistant software and change them back one he is finished).

Sure. But I'm not really "finished" with peano.mm1, and proof assistants should be useful even before the proof is "finished". For a bare bones verifier it makes sense not to include things like alpha renaming if they are too much work to implement, since you would generally only use such a verifier with a "finished" proof, but during development a more full-featured verifier (ideally with good error messages) can help move things along.

It is also weird that names can be different in mm0 and mmu/mmb (but only very slightly annoying now that the same order requirements provide a quick/efficient way of doing alpha renaming)

It is a bit weird. But in mmb names are second class citizens, shuffled off in the debugging data, so it wouldn't be able to check even if it wanted to. Plus, the primary purpose of the mmb format is to provide evidence that the mm0 file is provable, not that the mmb file is correct, so it's not necessary to make sure the mmb file is well formed beyond the requirements of delivering a proper proof. Even if the names are wrong, as long as it still proves the theorem who cares what it's called. In practice if the theorem name is different it's probably proving a different statement, so it will be caught at that point.

I think the same argument applies to mmu to a lesser extent. Even though mmu files use text to express the proof, they are still only a means to justify the provability of the mm0 file, so things like alpha renaming are only a performance concern.

The "same order requirement" somewhat defeats the human mm0 binders that can share names, those are now a lot less useful

What do you mean by this? If you shadow names in mm0 binders, you will only be able to refer to the later binding. Internally the other binding is still there, and in MMB everything is numbered so you can refer to whatever you want. Not having to worry about name clashes just makes a lot of things simpler.

[Lakedaemon]

Yeah, I get that in mmb strings are second class citizen as indices instead are unsed, which makes string equality trivial.
In the mmu parser, I have to canonize strings to avoid using memory like crazy and I could compare strings (== in java) by comparing their adress in memory (===).
The next step, of course is to use int or indices for strings like you do and to have canonized strings once for all, as a list of strings in your file

in mm0, say that ou have
Term bob (p q:wff) {x:setVar} (r:wff)

you cannot share the wff this way
Tem bob (p q r:wff) {s : setvar}
as it is another different term actually because of binder order.

so, users of mm0 files might wrongly think that they can share vairaibles declarations (like you do sometimes at the start of a human proof) but they can't and the name sharing capacities of the mm0 binders are then of very limited usefulnes (they just save some typing...)

When they use math stuff, I wouldn't be surprised if humans somewhat used (in their heads) NAMED arguments
like I am summing u(n) for n that goes from start to end
But then, humans have to write maths somewhere so they Memorize a graphic representation
like $\sum_{n=start}^end u(n)$
And in these graphic representations or sentences, arguments do have a place (an order in 1 dimension sentences),
which might be different depending on the language used/the country...

mm0 files encode BOTH things (the concept AND a Stree representation),
in a smart way (less typing) with binders AND their fixed order.

And it enforces 1 single way to write trees (which is a good thing)

you could have used the same syntax to encode binders that the way programmers do it

instead of
Term and (ph : wff) (ps :wff) : wff
or
Term and (ph ps:wff):wff

You could have used
Term and(ph:wff, ps:wff):wff
with a slightly different syntax for bound variables like
Term al(x . setvar, y : wff):wff

It is quite surprising that you did not (no complain here though)

Of course, it is important to be able to use a partially written mm0/mmu file.
But, still, I fail to see why it should be a concern of the mm0/mmu/mmb spec or of the proofchecker to be usefull when files are partially written.
It is the concern of the proof assistant software, it should allow partially written files to be used by itself, it's the whole point, isn't it :)

But a proof checker should just always reject unfinished files (ideally with a great reports that says what theorems where proved and why other were rejected)

[digama0]

in mm0, say that ou have
Term bob (p q:wff) {x:setVar} (r:wff)

you cannot share the wff this way
Tem bob (p q r:wff) {s : setvar}
as it is another different term actually because of binder order.

Well you can reorder the binders, but it is a different term and all subsequent uses of the term will have to use that order of arguments. It's still basically equivalent, so you might just be able to use it that way, unless the mm0 file has it the other way for some reason.

When they use math stuff, I wouldn't be surprised if humans somewhat used (in their heads) NAMED arguments
like I am summing u(n) for n that goes from start to end
But then, humans have to write maths somewhere so they Memorize a graphic representation
like $\sum_{n=start}^end u(n)$
And in these graphic representations or sentences, arguments do have a place (an order in 1 dimension sentences),
which might be different depending on the language used/the country...

Note that notations can reorder arguments. You can define

term sum (start end: nat) {n: nat} (u: nat n): nat;
notation sum (start end: nat) {n: nat} (u: nat n): nat =
 ($sum_$:0) n ($=$:0) start ($to$:0) end ($,$:0) u;

even though the arguments come in a different order in the notation than in the term itself.

You could have used
Term and(ph:wff, ps:wff):wff
with a slightly different syntax for bound variables like
Term al(x . setvar, y : wff):wff

MM0's syntax is based on functional programming languages, which is why it uses space for application and a binder list syntax similar to that used in Lean, Coq, or Agda. If you are coming from a C-derivative language like Kotlin this will be slightly unfamiliar.

[Lakedaemon]

This is very interesting and will help me in the future.

Thanks to your explanations, the proofChecker I intend to contribute passes string, hello and set.mm
but fails with peano :

This is my fault, I suspect my dynamic Parser to be slightly incorrect.

I'll delve into the mmu documentation once more to make things right and update stuff with the latest changes (my old code only used both-delimiters) and once everything looks fine, I'll pr stuff.

[digama0]

Is any of your code public? You should just create a new repo, like https://github.com/ammkrn/second_opinion , and I can make suggestions if I see anything I can help with. If you wait until you are done and PR your whole project that will be way too much to properly review.

[Lakedaemon]

Ok, I'll do that. :)

[Lakedaemon]

I did it there. This is the stuff I'm going to contribute (the patcher isn't there yet as I want to at least bug fix the proofChecker before that)
https://github.com/Lakedaemon/mm0kt

Also, I usually code in intellij idea and I am the lone consummer of my code (except for my android apps).
I execute stuff as tests, with a button click
So, I'm not sure that I have set things up right for executing this code for others (but I'll do it in the near future)

[Lakedaemon]

I fixed my dynamic parser for notations (it wasn't doing what the spec said it should... it is quite hard sometimes to understand what should be going on and, sometimes I grow impatient and I try to guess...with my limited understanding :/)

in peano.mm0
def if (p: wff) (a b: nat): nat;
doesn't match
(def if ((p wff ()) (a nat ()) (b nat ())) (nat ()) ((n nat)) (the (ab n (ifp p (eq n a) (eq n b)))))

Or, is it ok if the additional n : nat dummy is not declared in the mm0 definition ?
I'm guessing it is ok :D (you'll be the death of me ^^)

[digama0]

The dummy is not declared in the mm0 definition because the definition itself is not provided. For "abstract definitions" like this one, you only need to check that the type signatures match. In other words, ignore the dummies and value in the mmu definition and pretend you are matching two terms.

I forget whether dummies are permitted in an abstract def, but there isn't any reason to have them unless you are trying to stress test the verifier.

[Lakedaemon]

ok, then check dummies for non abstract def and do not check them for abstract def (which makes sense).

[Lakedaemon]

the additional dummies do not always have the same order in mm0 and mmu

def all2 (R: set) {.l1 .l2 .x .y .n: nat}: set =
$ S\ l1, {l2 | len l1 = len l2 /\ A. n A. x A. y
(nth n l1 = suc x -> nth n l2 = suc y -> x <> y e. R)} $;

(def all2 ((R set ())) (set ())
((l1 nat) (l2 nat) (n nat) (x nat) (y nat))
(sab l1 (ab l2 (an (eq (len l1) (len l2)) (al n (al x (al y (im (eq (nth n l1) (suc x)) (im (eq (nth n l2) (suc y)) (el (pr x y) R))))))))))

[digama0]

heh. You won't want to hear this, but dummies are unordered; the dummy declarations in mmu serve only to tell you what the types of the dummy variables are. MM1 will automatically put them in alphabetical order, so it's a bit tricky to change this behavior. Probably you should just collect them and then sort them before comparing.

Actually the ordering of dummies in MMU files does matter a bit, because the ordering of the dummy list argument to :unfold is in the same order as the MMU declaration of the definition. But it's not an error if the MMU declaration order doesn't match the binder order in MM0. (Note that MM0 also allows interspersing dummies with other arguments as well; the order they appear with respect to other binders doesn't matter.)

[digama0]

I just double checked the haskell verifier, which does mm0 + mmu verification, and it sorts the binders at the MM0 parsing stage: when it parses an MM0 declaration, it adds dummy binders into an ascii-ordered dummy_name -> sort_name map, and then when storing the declaration in the AST it turns the map into a list of pairs, in increasing order. Then, during verification, it just checks the lists for equality. I think this is incorrect, because it means that if the MMU binders are not in alphabetical order then they will not match. The correct solution is to sort the MMU binders for the purpose of doing the binder matching, but store them in the environment with the original binder sort order from the MMU text.

Fixed in 3218744

[Lakedaemon]

Checking that the unordered aditionnal dummies match, let peano.mm0/mmu pass for me.

So, I have a proofchecker (with missing pieces) that is able to pass 4 (mm0/mmu) pairs.
I'll implement the missing pieces next (Input, Output support, checking sort uses) and in parallel start designing
mm0/mmu paris that SHOULD Fail to catch incorrect proofCheckers

As I have A LOT of experience with my badly designed proofcheckers, I might even do a good job at setting traps for faulty or sloppy proof checkers :)

(Btw, I hope to get your proof checkers too ! Game is on ! :) )

Please tell me, how/when you want prs done, what the requirements are, how to proceed.

I'm a patient man, and I have a lot of work to do so I can afford to patiently polish things further

For example, error messages need to be polished and returned (instead of a boolean sometimes...)

Also, please tell me your needs so that a kotlin proof-checker can be added to your pipeline making everything just a sligh bit safer for us all. :)
Best regards,
Olivier

[digama0]

Writing test cases has never been my strong suit. If you write a bunch of positive and negative test cases, I would very much like it as a PR.

[Lakedaemon]

Then, let's complement each other !
I'll do just that

I could pr a
"stressTest" directory
with pairs (mm0,mmu) of very short files
with the mm0 file that has a 1 line comment at the top, that says why it should fail.

Any suggestion ?

for positive tests, we could just use the many valid mm0/mmu/mmb pairs that will be produced in the future :)

Those files will be exported from the kotlin library, from a single .kt file, that will also rely on classes I'll pr later

This reminds me that my mm0 perser doesn't save line comments, which is not nice. I'll have to do something about it

[digama0]

I would just call it tests/pass/ and tests/fail/. They should also be categorized by how they are executed, i.e. mm1 vs mmu vs mmb files. The term "stress test" is usually reserved for tests that stress some particular resource requirement in the verifier or compiler, like https://github.com/digama0/mm0/blob/master/examples/big_unifier.mm1 (which creates an exponentially large proof term with very high redundancy).

Of course real world mm0/mm1 files are also a good test, and that's what I've been using in the examples/ directory, but there is a lack of small focused examples that test a single feature or code path. For example, you should try making mm1 or mmu proofs that use each proof rule. Some configurations are not tested by automatically generated MMU files, like the one that just came up in the haskell verifier, because it only manifests if the MMU dummy list is not in alphabetical order.

[Lakedaemon]

ok. This sounds sensible.
I'll create both negative and positive tests (mm0 vs mmu).

The source for the test creating process will be released so you'll be able to port that to mm1, if you need to
I'm pretty sure that the kotlin api I'll use to create proof will look a lot like mm1 (if you extrapolate the mindbogingly nested parentheses and comma structures)

I'll do my best

[Lakedaemon]

It will also complement your mm0/mmu documentation.
It's a bit like pair coding/unit testing for proof-checker developpers

I think that I can come up with 50/100+ "interesting" tests in a few days
And then, it'll be possible to slowly cover more corner cases

[Lakedaemon]

Hello. Could you please have a look at the tests there : tests ?

the fail tests are implemented in fails.kt
and the pass tests are implemented in pass.kt

The test authoring api is kind of simple and user-friendly and I think that anybody could easily contribute tests

[digama0]

Is the bizarre formatting in things like https://github.com/Lakedaemon/mm0kt/blob/main/tests/pass/matching/same%20order%20for%20binders.mm0 deliberate? I need to double check but I don't think tabs are allowed, and the terma in this one looks like it should be a parse error.

EDIT: From mm0.md, the only valid whitespace characters are " " and "\n".

Except for the tests that are testing weird formatting or special characters, I think all of the tests should use proper formatting, similar to that used in peano.mm0 or the mm0 pretty printer in mm0-hs.

[digama0]

• fail/matching/different binders order: Not a fail test, since verifiers are permitted to alpha rename. Maybe "optional success"?
• fail/matching/blank file: This should be valid, assuming no weird whitespace characters are in the file.
• fail/matching/empty delimiters: This is valid.
• fail/matching/empty delimiters2: This is valid.
• fail/parsingBoth/term typed with a dummy: I don't see anything wrong with this one.
• fail/parsingMM0/abstract def with declared dummies: doesn't seem to describe what it tests, which is an empty expression in a def.
• fail/registering/dummy variable with a pure sort: this would fail with pure, but the test actually uses strict and so should pass. (It also doesn't have any dummies.)
• fail/registering/formula without provable sort: This is valid, because there are no theorems or axioms. (Defs don't have to live in provable sorts.) (EDIT: I see now this was a typo in the spec, fixed in b350919.)
• fail/registering/idempotent coercion: technically this is a reflexive coercion.
• pass/parsingBoth/big int support: The mm0 spec says verifiers are only required to support up to prec 2046.
• pass/parsingBoth/carriage return is whitespace: This is a fail test, carriage return is not valid. Same with the other whitespace.

[digama0]

Here's a fail test for the free sort modifier:

free sort s;
term f {x: s}: s;
def y (.x: s): s = $ f x $;

It means that dummies can never have sort s even if all the other requirements for using dummies is satisfied.

[Lakedaemon]

thanks, I'll update the test asap and also add your comments for the future readers, so that they aren't lost

[Lakedaemon]

• fail/parsingBoth/term typed with a dummy: I don't see anything wrong with this one.

The mmu spec says that term have
ret-type ::= '(' sort-name '(' (var-name)* ')' ')'

This prevent them from having a return type that is a dummy type like (sort-name), right ?
It should be (sort-name ())

[digama0]

Oh I see now. Yes, that's a parse error then.

[Lakedaemon]

I'll format things like peano.mm0 ans sanitize spaces.

I want to make an api change for test declaration on my side (I made a bad decision at some point), so this will take some time to happen though.

I'll use the time to slowly mature the test declaration api, grow the tests and make them better

[digama0]

test declaration api

Could you explain what this means, beyond just having a list of mm0/mmu files? I see some kotlin code that specifies e.g. the parsed forms of some of the tests, but is there more to it? Are you producing the test files automatically?

[Lakedaemon]

I am producing tests semi-automatically because it would be a burden to maintain tests in hundred of files.

I'm writting both mm0 and mmu files and categorizing them in fail/pass/parsingMMU/oarsingBoth with stuff like
fun registeringFails() = failBoth("registering") { "duplicated ids for sorts".test { sort("s", isPure = false) sort("s", isPure = true) } }
But I am not producing tests automatically

[digama0]

The { sort("s", isPure = false) sort("s", isPure = true) } is going to be difficult to maintain on my end because it requires kotlin parsing. Assuming the test suite is committed to the mm0 repo, that means that you will have to either keep up with new tests that are added, or allow for some tests to not have any parsing assertions in them (which seems preferable). That is, the .test assertion can mean "in addition to checking pass/fail, also make sure that this test parses to the equivalent of this AST". Then those assertions will remain in the kotlin code and the tests themselves can move to the mm0 repo.

[Lakedaemon]

I'm not sure that I understand all you say (with the AST thingie) but yes.
The kotlin code is just a convenient way for me to maintain the tests in a sane manner.
the official mm0 repository should probably just commit the mm0/mmu test files (once you are satisfied with them)

And the test producing kotlin code should probably remain outside of your repository.
I'll release it publicly though, so people may use it, as a convenient way to produce test files, if they have a need

[digama0]

Okay, how about opening a PR with just the test files? Check "allow edits from maintainers" and I will be able to make tweaks on the PR.

[Lakedaemon]

Not yet, but soon.
I have to improve the test formatting
I also would like to include a line comment in the mm0 test file refering to the spec that explains why this should fail
Because for naive readers like me, some tests may appear cryptic otherwise

[Lakedaemon]

I managed to change my test creation api (thanks to the already written proofChecker code). This will speed up things quite a bit
(my brain bugs with mmu stuff and is happy with the mm0 notations).

Those 50 "tests" are way not enough : there is not even things about axioms, theorems and proofs in there.
Once I'm quite satisfied with the formating, I'll pr some tests (just a few to start). Hopefully, this will go well (I do not have much experience pr-ing things).

And as time go by, I'll pester you with an ever growing collection of tests as I write the set.mm patcher
Please hold fast !

As long as I have not pr-ed tests that caught my code, I cannot fix the buggy code (or I take the risk of writing faulty tests and not catching it), so at some point, I'll grow restless and pr some tests just to be able to fix my code ! :)
Have a nice day !

[Lakedaemon]

1. say you have
   term a:wff;
   def b:wff = $ a garbage $;

should it fail because of the unnecessary garbage in the formula ?

2. why did you allow simple notation to be used in formula before they are defined ?
   This will make all 1st pass proofChecker crash/fail (and technically forces everyone to write 2-pass proofCheckers)
   Or you cannot check that definitions/axioms/theorems match, nor proof check theorems BEFORE the end of the file (so you delay it, which is the same that having a 2 pass proofCheckers)

If you wanted to allow people to write 1 and 2 pass proofCheckers, shouldn't you have forbidden usage before definitions ?
Both 1 and 2 pass proofcheckers would then be happy

[digama0]

1. yes
2. I may have written that in the initial version of the spec, but I've been working on the assumption of a 1 pass proof checker for a while. I think the spec says something about how verifiers are allowed to be either 1 pass or 2 pass and the answer should not change (which results in some restrictions on redefining notations, for example). Usage before definition is not okay

[digama0]

Here's the relevant text:

Verifiers may choose to interpret math strings on the spot (in a single pass), or collect all notations and build a parser to run on all strings (two pass). A consequence of the two pass approach is that notations may be used before they are defined in the file, for example:

term wi (ph ps: wff): wff;
axiom ax-1 (ph ps: wff): $ ph -> ps -> ph $;
infix wi: $->$ prec 25;

Verifiers are allowed but not required to support out of order notation declarations.

So it says that verifiers are allowed to do two pass notation parsing, in which case this example is legal, but they are also allowed to do one pass notation parsing in which case it is not. It is implementation defined, so it should not be used as a pass or fail test.

[Lakedaemon]

Yes, this is precisely my point. If the example you cite is allowed to exist, I'll cry !

A consequence of the two pass approach is that notations may be used before they are defined in the file`

This means that when mm0/mmu/mmb becomes popular (because if you and/or I succeed, it will),
there are going to be mm0 files flying around written by people who use 2 pass proof-checkers and those mm0 files will break your proof-checker and mine, because we both implement 1 pass proof checkers :)

And they will say that we suck because our proof checkers do not even work though theirs do :D

Maybee I do not understand what you say (my brain doesn't behave sometimes).
To be clear, I also want developpers to have the choice of implementing 1 or 2 pass proof-checkers (freedom !!!).
But I want neither of them to break with the files that the spec says is ok.

[Lakedaemon]

maybee I do not understand what you wrote.
Because you say : Usage before definition is not okay (yayyyyy, I want this too)
But I understand this sentence
A consequence of the two pass approach is that notations may be used before they are defined in the file
as "usage before definition is allowed (and I'm crying really hard now :( )

[Lakedaemon]

Also, I do not remember reading in the spec that "garbage in a formula makes the proofChecking process fail even if the dynamic parser returned a tree".

If I do not presume, I would love that to be written in the spec.

[digama0]

A consequence of the two pass approach is that notations may be used before they are defined in the file`

This means that when mm0/mmu/mmb becomes popular (because if you and/or I succeed, it will),
there are going to be mm0 files flying around written by people who use 2 pass proof-checkers and those mm0 files will break your proof-checker and mine, because we both implement 1 pass proof checkers :)

That's true. Conversely, if they want to write mm0 files that are broadly checkable, they need to follow the strictest guidelines, which means they can't use conditionally supported features. Anything that is accepted by some checkers and not others should be viewed with suspicion. But it's not always practical to require verifiers to precisely reject everything, and in this case it doesn't matter much. You should just reject such files and move on.

By the way, the reason you might want the 2 pass style is if you have used a parser generator to construct the math parser. There are a lot of parser generators that expect the grammar up front and don't allow the parser to be dynamically extended. So if you first get all the notations and turn them into a BNF description and hand them to yacc or something, you will get a parser that parses all math in the file equally. Given a parsed expression it is then difficult to tell whether you have used a notation from "the future", although if you use a term from the future this is more obvious.

Also, I do not remember reading in the spec that "garbage in a formula makes the proofChecking process fail even if the dynamic parser returned a tree".

If I do not presume, I would love that to be written in the spec.

The expression does not parse. The dynamic parser is required to parse the entire string. There is nothing in the spec that says you can add additional text after the end, the expr(p) nonterminal is being matched against the content of $ stuff... $ (excluding the $ delimiters), not against a prefix of the stuff....

[Lakedaemon]

A consequence of the two pass approach is that notations may be used before they are defined in the file`
This means that when mm0/mmu/mmb becomes popular (because if you and/or I succeed, it will),
there are going to be mm0 files flying around written by people who use 2 pass proof-checkers and those mm0 files will break your proof-checker and mine, because we both implement 1 pass proof checkers :)

That's true. Conversely, if they want to write mm0 files that are broadly checkable, they need to follow the strictest guidelines, which means they can't use conditionally supported features. Anything that is accepted by some checkers and not others should be viewed with suspicion. But it's not always practical to require verifiers to precisely reject everything, and in this case it doesn't matter much. You should just reject such files and move on.

I see. It buggs me less now, thanks to your explanation

By the way, the reason you might want the 2 pass style is if you have used a parser generator to construct the math parser. There are a lot of parser generators that expect the grammar up front and don't allow the parser to be dynamically extended. So if you first get all the notations and turn them into a BNF description and hand them to yacc or something, you will get a parser that parses all math in the file equally. Given a parsed expression it is then difficult to tell whether you have used a notation from "the future", although if you use a term from the future this is more obvious.

Having generated a parser for Metamath, I see what you mean.
But throwing away parser generator and embracing the dynamic Parser is one of the 2 main sellign points of mm0. Who would want to do that ?

They might as well use the slow, cumbersome and unmaintainable parser I generated for Metamath like 2 years ago.
It is doable, but it means throwing away all the benefits (and the simplicity) of mm0.

Because, when I had the metamath parser, I had like 100 grammar rules :/
Throwing away mm and embracing mm0, on of the best decisions I took. (though I have still not regained the level of math I achieved with metamath....but soon)

Also, having people write strict mm0 because they hope to have universally useful files does not achieve the same results that
making people write strict mm0, because it is not valid otherwise (yet, I respect your decision, I understand now thanks to your explanations).

I just do not see benefits in having this tolerance and lots of pain later
(with strict mm0, you can do everything that not-strict mm0 can and more)

But, I will abide by any decision you take
(also, I already have a solution : take their weird files, rewrite them in strict mode, done....it gives me more work, but if I can patch set.mm, I can shuffle around notations and simple notations, on one leg, with a blindfold, arm tied, while singing)

But please consider history and why there is a Strict mode for html. :)

Also, I do not remember reading in the spec that "garbage in a formula makes the proofChecking process fail even if the dynamic parser returned a tree".
If I do not presume, I would love that to be written in the spec.

The expression does not parse. The dynamic parser is required to parse the entire string.

YES ! I remember reading that. Good !

There is nothing in the spec that says you can add additional text after the end, the expr(p) nonterminal is being matched against the content of $ stuff... $ (excluding the $ delimiters), not against a prefix of the stuff....

[digama0]

But throwing away parser generator and embracing the dynamic Parser is one of the 2 main sellign points of mm0. Who would want to do that ?

Well you pretty much have to write the dynamic parser by hand, because it doesn't exactly fit most parser architectures. It's not huge but it's sometimes nice to pull a parser off the shelf instead of writing your own.

Actually, metamath is broadly the same as regards dynamic parsing. You can preprocess the file to construct a CFG if you like, or you can build the parser dynamically. In metamath you definitely can't use a syntax before the syntax axiom is introduced, so you have the same issues (although the term constructor and the syntax are the same so there isn't any danger of accidentally using notations from the future without also using term constructors from the future).

I just do not see benefits in having this tolerance and lots of pain later
(with strict mm0, you can do everything that not-strict mm0 can and more)

Yes, but if the definition of "strict mm0" is itself difficult to check then that can mean a meaningless performance penalty. For example, there are a few things in the MMB files that are not checked for validity, because you can still verify the proof even if the data in the file is slightly off. The verifier is not supposed to be a validator, odd as that may sound. It's supposed to verify the well formedness and the truth of the theorems in the file. If the theorems are stated in some unusual way that the verifier is nevertheless able to make sense of, that should still be okay.

The most important thing that should be in fail tests are false proofs. If the proof doesn't follow the rules, then it needs to be rejected. That would be the negation of "loose mm0". But there is a gap between loose mm0 and strict mm0 in order to give some flexibility for verifiers to implement things as conveniently and efficiently as possible. There will be "strict mode mm0" validators, but I do not want to mandate that all conforming mm0 verifiers are such.

By the way, another example of a gap I'm considering is alternative whitespace and unicode identifiers. Sometimes, for implementation simplicity, you want to use an is_whitespace function from the standard library that thinks that \r and \t should be whitespace, and similarly perhaps you want to have french theorem names or something. In these cases "strict mm0" says no, but a few foreign names doesn't make the file unintelligible as a collection of theorems, so if the verifier is willing to deal with it then there isn't any need to require that the verifier reject.

[Lakedaemon]

Wow. It is possible to build a dynamic parser with metamath ? (you say it, so it must be true, wow)
You musr mean metamath the formalism with the few rules

yet a metamath dynamic parser with set.mm (yuckkkk, it gives me goose bumps.... )

Also, thanks for the insights (you are quite the theorist...I'm amazed at the depth of thoughts you put in your creation)

I was considering the unicode identifiers also (for operators, sum, arrows....). It would make reading textual mm0 slightly cuter but it would open a whole new can of worms. And degrade performance. Also, graphical rendering is going to be donne by TeX/MathJax on my side, so unicode wouldn't bring anything to the table (ans unicode is hard to input).

Unicode makes sense for human languages though. Yet, there is still the possibility to map unicode ids to ascii ones, so it may be done by alother layer on top of an ascii- mm0 powered engine. So, for now, I'm sticking with good old ascii :/
(though I'm all for utf-8/unicode/multi-language stuff (even wrote a multi-lingual Japanese dictionary supporting 50 languages), that says something... Who would have thought that I would write an ascii only software...that is so 80-ties...)

false proofs... I'm not sure if I'll be good at building that.
28+ years of maths makes me pretty much only able to write proofs (force of the habit).
Maybe I should ask my students for help :)

[Lakedaemon]

The "tests I'm writing" right now look more like Unit tests, making sure the developpers make their job implementing things on top of your specs.

But if those tests ensure that verifyers are implemented correctly, maybe the strength of your formalism will ensure that it is not possible to write false proof (I'm naive and an optimist, maybe).

[digama0]

false proofs... I'm not sure if I'll be good at building that.
28+ years of maths makes me pretty much only able to write proofs (force of the habit).
Maybe I should ask my students for help :)

In theory, "code coverage tests" should help here. That is, every time the program has to check something and fail otherwise, it should be possible to construct an input that hits that check. There are 88 uses of ENSURE(...) in mm0-c/verifier.c, so that might give you a place to start (or the analogous checks in your verifier).

[Lakedaemon]

I think that I got the "false proof" stuff.

false proof test = design a test code, so that if a proof checker doesn't respect an aspect of the mm0/mmu spec, then it is possible to prove something false

Basically, such a test would prove that your requirements are necessary (on the theorical side).
But such exploits are much more difficult to create than basic unit tests that make sure that the single requirement is met
I'm not sure that it would add a layer of security/accuracy over a proof checker.

Writing tests makes me look again/harder at the different specs, which is a very good thing for my software (making it go from the "somehow working" to the "mostly working" state)

I discovered that mmu can have line comments !
This is nice for tests because I'll be able to explain to test consummers why they should fail or pass (with quotation from the spec)

I'll be implementing line comment support in my mmu parser and next pr-ing my first tests

I also sanitized the names of the test to allow easy navigation like
ids cannot ....
ids cannot ....
formulas cannot ...

The folders can be used to test different parts of the mm0/mmu toolchain (mm0 parser, mmu parser or proofchecker at different stage : matching, registering, dynamic parsing, proof checking)

[digama0]

Basically, such a test would prove that your requirements are necessary (on the theorical side).
But such exploits are much more difficult to create than basic unit tests that make sure that the single requirement is met
I'm not sure that it would add a layer of security/accuracy over a proof checker.

Yes that's right. You don't have to create an actual "exploit"; exploit tests are generally best written against a specific verifier with a bug in it, to demonstrate that the bug is in fact a soundness hole. For general testing it's simpler to just check all the primitives that can potentially be used in an exploit for general robustness. It's not perfect, but that's just a limitation of testing.

By the way it's also okay to have multiple tests in a single file. Basic parsing tests should be short and focused but for more high level tests like secondary parsing or binder order stuff I think it's fine if you have 4 to 10 individual tests in one file. The whole file fails as one so you probably don't want to put too much in the file, but I think it's organizationally easier not to have thousands of (pairs of) two line files.