Better handling of unexpected operations in bounds-checking

[jadephilipoom]

If ZRange.ident.interp returns None for the bounds of some operation in my code, it would be nice to get some message saying which operation it was--currently I just get "not unifiable" from solve_rop and I'm struggling to make it show me where exactly the None comes from.

[JasonGross]

This would be a nontrivial amount of work, and I'm not convinced it'll be worth it. The way to do it is to replace the option with an error type, and push that through the rest of the code ... but nth_default is the only operation that sometimes produces Some and sometimes produces None, and, beyond that, there's a list of the operations that produce None here:

fiat-crypto/src/Experiments/SimplyTypedArithmetic.v

Lines 4552 to 4573 in a90c2b5

	| ident.primitive _ _
	| ident.Nat_succ
	| ident.Nat_add
	| ident.Nat_sub
	| ident.Nat_mul
	| ident.Nat_max
	| ident.bool_rect _
	| ident.nat_rect _
	| ident.pred
	| ident.list_rect _ _
	| ident.List_nth_default _
	| ident.Z_pow
	| ident.Z_div
	| ident.Z_eqb
	| ident.Z_leb
	| ident.Z_of_nat
	| ident.Z_mul_split
	| ident.Z_add_get_carry
	| ident.Z_add_with_get_carry
	| ident.Z_sub_get_borrow
	| ident.Z_modulo
	=> fun _ => type.option.None

It should only take 5 minutes to write a procedure that lets you know if a given expression uses any of those (either in Ltac or in Gallina).

(I'm not opposed to having better error messages, I am just hesitant to spend the 3-6 hours I expect it take to write the code that pushes the relevant error messages through partial reduction :-/ )

[jadephilipoom]

Hmm, okay. No worries if it's that much work. I thought it might be easier.

I'm curious about what this 5-minute procedure is, though. I figured out where my problem was coming from[0] by printing the nested ltacs in solve_rop, painstakingly applying them until I had the reified term in view, making a simpler example with the same problem so the term wasn't huge, and then computing it step by step until I could actually see all the operations. It took me about 3 hours. I'm describing the whole process because I'm wondering if you have some more general advice about where to start with debugging when I have opaque problems with the pipeline (e.g. "there's a None in my bounds", "cache_reify takes ages", or "the bounds aren't tight enough").

[0] I think Z.cast2 should have a case in partial.bounds.ident.extract' here. Is there a reason it currently doesn't?

[JasonGross]

The 5-minute procedure only works if you have the reduced reified term in hand, and it wouldn't've caught [0]

But, uh, I could make the error messages for bad bounds include the reduced syntax tree, post-bounds-analysis, if that'd be useful?

Re [0]: It's because I was operating under the (now clearly mistaken) assumption that the relevant output types were Z and list Z, and not Z * Z. Feel free to add

| ident.Z_cast2 range => fun _ => ZRange.type.option.Some range

or

| ident.Z_cast2 (r1, r2) => fun _ => (Some r1, Some r2)

(they are the same)

[JasonGross]

Oh, urg, getting "not unifiable" is also not supposed to happen. You're supposed to get a unification failure that contains a description of the error in the term that's not unifying. Let me fix that.

[jadephilipoom]

Closed by #351