kevinmkane
commented
5 years ago For context, what happened to me was I had a lemma that provided a fact involving the Euclidean division operator. Originally it was above the function I needed it in, and everything was fine. Then I moved it into a file of general lemmas where I happened to have open FStar.Int, because I make heavy use of that module in my lemmas and that was more convenient. Unbeknownst to me this caused the division operator to be overloaded to the flooring division type, and so now my lemma was stating something slightly different. Worse, this lemma is assumed for the moment pending some other work coming in, so there was no proof yet that should have failed. Nik helped dig into the guts until we discovered the slash operator had been overloaded in one of the two places. This lemma deals in signed integers, so the difference matters for negative dividends.
As a user I voice my desire for #3 (jumping to the definition site of an operator) and #5 (print the fully qualified names of operators with --print_full_names). Being able to jump has helped me track down terms that are resolving to the same name in different modules in different places in the past.
As for op_Slash, I like the idea of renaming it to something else, and then going through and using that operator everywhere division operators are defined in the machine integer classes, so that it's clear to users who need to prove facts (like the size (v a / v b) n precondition on div) which to use. When someone using div or /^ gets an assertion failed and jumps to a precondition like size (v a /_ v b) n they need to prove, since /_ isn't one of the "pure" operators, I would not assume anything about its behavior and instead would go to its definition to see what's going on. Right now, if someone is opening one of the FStar.IntNN modules but not FStar.Int itself, they won't get that overloaded op_Slash used to define div and may run into the same trap I did.
Intuitively I didn't expect the operators over mathematical integers to be redefined, and that's why I didn't think of looking into the slash operator being redefined. I was also unaware Z3's native division operator was a Euclidean division until this adventure. As a developer I think assuming a division operator on mathematical integers behaves like the machine integer equivalent is a natural assumption to make. A note on the definition of /_ to point out Z3's native division operator is Euclidean may be another good way to get the word out.
FStar.Int defines
op_Slashto be "round towards zero" division. Meanwhile,Prims.op_Divisionis Euclidean division. This means that depending on whether or not you haveopen FStar.Intthe semantics of the/operator can vary, leading to very hard to diagnose proof failures.Here are some things we could do to reduce confusion:
Redefining commonly used operators with different semantics is a bad idea. We should avoid doing this. Redefining them while preserving semantics is better, but even that should be done rarely. For an example of this, see FStar.Integers, which redefines all the arithmetic operators, extending their domains from just mathematical integers to machine integers also. That's quite special, but at least it does this while preserving their semantics on math integers. I've added this to recommendation the the style guide.
We should rename FStar.Int.op_Slash to something else. Suggestions welcome.
The interactive mode does not allow jumping to the definition site of an operator. That's probably due to a limitation in the lookup-identifier feature of the F* side of the IDE protocol. Fixing this would at least allow diagnosing more easily name resolution confusions on operators.
Despite the style guideline in 1, we will inevitably have cases where we have redefined operators in scope. Maybe F* could whenever resolving an operator symbol if the chosen operator shadows any others in scope? Perhaps that's too specific.
The pretty printer, even with --print_full_names, does not print the fully qualified names of operators. E.g., it just prints
a / b. But, it could printa `FStar.Int.(/)` b, in case print_full_names is on.Our libraries use a mixture of notations for operators:
let op_Slash = ...andlet (/) = .... Can we do a cleanup pass settling uniformly on the latter and deprecating support theop_notation? While we're at it, there's more messiness to fix in prims, where we have special treatment ofop_Division, op_Addition, op_Multiply, op_AmpAmp, ...etc.What else could we do to make this better?
Thanks and apologies to @kevinmkane who was bitten badly by this recently. Thanks also to @Chris-Hawblitzel who helped diagnose and suggested some of these improvements.