[isabelle-dev] Word Libraries

[Gerwin Klein]

> On 6 Oct 2021, at 23:30, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> * Theory Word contains the word type and its operations proper, located
> in session HOL-Library.
> 
> * Additional material of somehow unclear status in relevance is
> modularized into separate theories and moved to session Word_Lib in the AFP.
> 
> * The historically grown Word_Lib is minimally structured and augmented
> with a guide.
> 
> * The ultimate goal is that future development can happen mostly in the AFP.

So far that is as we discussed back then and I continue to agree with it. The problems are in the details.


> * Some disentanglement of theory dependencies to enable users to use the
> library more selectively (»Word_Lib is minimally structured«) – this
> affects genuine Word_Lib material .
> 
> * Movement of material from the distribution / HOL-Library.Word to
> Word_Lib (»moved to session Word_Lib in the AFP«)
> 
> * Restructuring of that (originally non-Word_Lib (!)) material
> (»modularized into separate theories«).
> 
> (I emphasize here that most of the changes seen in the AFP actually
> originate from the Bit/Word material in the distribution, where the
> cumulative reworking over two releases gives me kind of responsibility
> and »legitimacy« for proactive developments. Coming back to the original
> aims: »The ultimate goal is that future development can happen mostly in
> the AFP.« Ie. without subtle and hard to maintain dependencies between
> AFP and distribution. Note also that the changes towards Isabelle2021
> are far more massive than those afterwards.)

This is the thing: I don't object to the massive changes for Isabelle2021, at least not the ones we discussed and looked at together. I saw (and still see) the value in the reorganisation and generalisation you did there. The problem are the subsequent "cleanup" etc commits, which to me did not actually clean much up but have managed to leave Word_Lib unusable (it'll be fine with the changes I wanted). If we had gone through the same cycle of discussion beforehand I could have pointed these out very easily.

I can see where our misunderstand originated and I'll get over my annoyance. I'm glad I had the time now to look at it before we have to freeze this for the release.


> Generally: If there are any repositories I should have a look at for
> some kind of assessment, please let me know. Also if there is particular
> experience of the migration to Isabelle2021 I should take into
> consideration.

There is some relevant experience from Isabelle2021. As a rough order of magnitude, it took about 2 full person months to do the complete proof update for l4v, which finished a bit more than a week ago now. 2 person months is about 1 person month higher than a usual Isabelle update. Not quite all, but most of the changes were due to Word_Lib.

You did an initial foray into this proof update for one architecture (ARM, 32 bit) after the first half of the Isabelle2021 changes. The result of that foray was that those changes were relatively benign, which is why I was surprised by the much higher effort later. I think the main fallout was from a few small changes in the second half of the Isabelle2021 update. What is relevant for the next update are these:

- things started breaking immediately for 64-bit architectures, because the Sumo concept alone does not quite work. It is not enough to make all lemmas for all word lengths available. The point of the Word_SetupXX theories is to additionally establish a set of common names that refer to the default word type of the program (basically, whatever "unsigned int" is in C for that architecture, and what the register width is for the machine). Having these names common means that the same proof text can work on different concrete types. This is different to actually generic lemmas that work for any word length or that need to resolve preconditions on the word length before they can be applied (the latter can be solved in theories like Word8 etc). It is not the prettiest form of genericity, but it is crucial for not having to duplicate thousands of lemmas that for other reasons do need to refer to a concrete word length (which is known in the proof state, but unknown to the proof text). Ultimately this is comes from C, which as painful as it is, works on exactly that principle that the same type name can refer to different representations, depending on architecture.

- the default simpset setup changed, it no longer reliably normalises ground terms with numerals. This caused a bunch of proof changes, hunting for which rules are needed etc. My reading of NEWS it that this is getting worse with NOT terms not being normalised any more. This potentially makes sense for int/nat, but I would suggest to keep them for Word (and to make sure the rest of the numeral simplification actually covers all cases -- usually 0, 1, Suc 0 are the corner cases to look out for).

- the same issue caused C/assembly refinement to fail, as well as generated bitfield proofs (for 64 bit architectures) because arithmetic leaves different terms. This might be unavoidable for arbitrary terms in a larger update, but Isabelle should be able to compute with at least numeral ground terms reliably.

- punning max_word with -1 conflicts with normalising numerals to the interval [0; 2^len). There were a few test lemmas in the repository that made sure this was not accidentally removed, I'm not sure where these went. Removing normalisation for -1 in turn leads to terms like unat(-1) which proofs then get stuck on. This can be fixed locally by finding the right rule to re-establish the old normalisation, but that will of course mean that abstract lemmas that refer to -1 won't apply any more. This means there is no principled way to deal with ground terms any more. I can see the appeal of using -1 for generic lemmas, because it has nice algebraic meaning (as opposed to max_word). Maybe the solution is to build a rule set for arithmetic that can be added on demand or as a bundle. It's a bit of a crutch, but at least it would provide a choice.

- the new simpset often loops in the l4v proofs, because it either reversed polarity or added additional rules about ucast/unat. Some of this was fall-out from the more general treatment (e.g. unsigned)

- not all new looping is due to that specific problem. I haven't been able to track down what rules exactly are the problem, but adding field_simps now almost always loops in word proofs. This might be a symptom of a different problem (i.e. not related to Word_Lib), because the usual fix was to instantiate specific commutativity rules. This indicates that something doesn't quite work any more with ordered rewriting. Possibly there is now an additional rewriting step or something like that so that the simple test in `simp` no longer suffices.

- related to simp rules for "unsigned", there are many (hundreds) of instances where casts or unat now leave terms of the form "take_bit 32 .." in the goal which have little chance of making progress. This was such frequent cause of breakage that we introduced a bundle which removes the rules producing take_bit terms. Trying to remove them globally is hopeless, because any theory merge with a theory that still has them, will re-introduce them.

- similarly, there is a rule that automatically rewrites "x = 0" to something in the direction of "x dvd 2^len". This is rarely useful with concrete len, and preventing these terms from being produced is similarly manual as take_bit.

- the unat_arith tactic solves fewer goals. I might be mistaken, but I think this is mostly due to simpset changes, but I have not had the time to track down which exactly.

Overall, it looks like a number of aspects of the new simpset are convenient for reasoning abstractly about machine words when you are working within the library (esp take_bit and 0/dvd), but counterproductive once you are working with specific word lengths as you do in program verification.

I think it would make sense to attempt to tune the simpset such that both scenarios (concrete and abstract) are available separately as bundles, making the global default conservative.

The problem is that the old setup was fairly well tuned and recreating it will not be easy, but at least removing some of the global rules that only work well for the abstract setup would help, because adding simp rules later is easy, but removing them is annoying.

There is a separate question of what a good setup is for the interplay between casts to different types and what good normal forms for these are. We had settled on never unfolding ucast/unat/uint etc automatically, instead producing abstract rules that describe the interaction with the usual operators and relationships between each other. I still think that is a reasonable setting.


>> For instance, who on earth wants to read something like "is_aligned (push_bit m k) m" instead of "is_aligned (k << m) m"? . The syntax was introduced for good reasons. It is fine to make it a bundle to not pollute a global syntax space, it is not fine to change original material that was written with a purpose.
> 
> If your point is to to apply the ‹_ << _› syntax etc. thoroughly and
> consistently among Word_Lib theories, I am happy to look after these slips.

That would be appreciated. My complaint was not that a new lemma did not use the word syntax (although it would be nice to remain consistent), but that old lemmas were rewritten to not use it. Possibly as part of another change.


>> It is *absolutely* not fine to produce commits like "dropped junk" which removes a theory that was critical to how this library is used after in previous commits having made it unusable, entirely missing the point of its existence. Please revert that entire series of commits and reproduce the old setup.
> 
> After a second study of history I notice that I messed this up already
> in the AFP release for Isabelle2021; the change after that point of
> reference was indeed just a cleanup of dead theories. Looks I should
> just revert to pre-Isabelle2021 there?

Yes, I think that would be best.


>> Further, a whole lot of constants have been moved around. Why? What does this improve? This can cause major amounts of renaming work for no gain to anyone. Please either produce a convincing argument for the benefit of these moves or revert them
> 
> These moves AFAICS originate from the distribution (see above), where
> the elimination of the ancient HOL-Word session for Isabelle2021 already
> had massive impact on internal names for operations. Is your concern
> about renaming work just abstract or based on concrete observations? I
> am asking since if any tool survived the Isabelle2021 movements, there
> is little reason to assume that it won’t survive the current state of
> affairs – Isabelle is far more robust against such things as, say, 15
> years ago.

I'm fine with the move of eg shiftl1 etc from HOL to Word_Lib. My impression was that there were more moves and renaming internally in Word_Lib. For those I don't see any good reasons. I might not have looked carefully enough there.

In terms of Isabelle's robustness: I'd agree with it being more robust for moving constants where antiquotations can be used to refer to unqualified names, but renaming is still one of the major pain points in almost every Isabelle release -- compounded by the fact that by far not all of these are documented in a way that would be usable for a simple search/replace. Those names that are listed in NEWS with their replacements are highly appreciated, but the lists are not complete, and there is no such NEWS for Word_Lib.

Maybe the impression of robustness comes from the incremental way we update the AFP. Each specific renaming is obvious to the author of that change and likely not hard to automate. On the other hand, being confronted with all of these at the same time, and having to find all instances by proof failure is time consuming and can be extremely frustrating when you have to hunt in hg history for what something has been renamed to.


>> Changing definitions such as shiftl1 to input abbreviations is likely to cause major breakage because term structure changes significantly.
> 
> The shift*1 Operations have been auxiliary definitions in the
> distribution to bootstrap the bit shifts operations, similarly to
> iszero, equipped only with a minimal set of lemmas. If one tool out
> there relies on it as explicit constant i. e. due to pattern matching, I
> won’t shed a tear to keep it as constant.

Great, let's keep them constants.


> (Aside, the primitive definitions then would be maybe: shiftl1 a = (a << 1), shiftr1 a = (a >> 1), sshiftr1 a = (a >>> 1)).

I'd be fine with these as definitions as long as the old forms still available as lemmas, preferably under the previous names. Maybe we can make sure over time that these constants are not produced any more by any tools and then they can finally be removed, but that is a number of release cycles away.

Cheers,
Gerwin

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211008/03898d59/attachment.sig>