verified parsers

Stream: general

[Frederick Pu]

I saw there was a library for writing parser combinators in lean https://github.com/fgdorais/lean4-parser/tree/main.
I was wondering if there is a library or an effort to create an api for writing verified parsers. That is a given a grammar denoted by a type T along with a map interp : T \r String, parse (s : String) returns a non none value iff there is a (t : T) such that interp t = s and forall (t : T), parse (interp t) = some t

[Frederick Pu]

maybe a similar approach to the SizeOf instance could be used to assure that parsers compose nicely

[Yakov Pechersky]

Feel free to look at https://leanprover-community.github.io/mathlib_docs/data/buffer/parser/basic.html#parser.nat_eq_done which proved that the mathlib3 parser of nat gave the expected number.

[Yakov Pechersky]

There is a lot of general proof API for any parser, that was built up to prove this specific result.

[Yakov Pechersky]

The nat related proofs are highly commented

[Frederick Pu]

is there a corresponding mathlib4 version of that file?

[Frederick Pu]

also where can i find the more general proof api about parsers

[Yakov Pechersky]

That file wasn't ported because the whole parser framework used in lean4 is different.

[Yakov Pechersky]

I claim that qualities about baseline parsers like bounded, step, prog will be applicable in any monadic parser library, and how those propagate into the parser combinators.