[isabelle-dev] Word Libraries

[Florian Haftmann]

A quick report after reaching isabelle 807b094a9b78 / AFP c42c2c2447c2.

* NOT <numeric expression> is normalized without interfering with other
normalization rules;  rules have been augmented accordingly.

* Conversions are not normalized over-aggressively, ie. only if no
auxiliary »glue« operations have to be inserted.

In the pipeline is a change which makes the normalizing set on int, nat,
word more complete, esp. wrt. negative numerals; while there is no
evidence that is the reason for the observed breakdown in normalization
of words, it has been a good opportunity to tackle that systematically.

An observation: Normalization rules for words typically work by
rewriting to int. This approach is historic – normalization could be
achieved by more elementary rewriting in most cases. At least this seems
to be the cause for the illusion of implicit normalization of word numerals:

unbundle bit_operations_syntax

lemma
  ‹w = 1705› for w :: ‹8 word›
  apply simp \<comment> ‹no normalization›
  oops

lemma
  ‹w = 1705 AND 255› for w :: ‹8 word›
  apply simp \<comment> ‹normalizes due to rewriting to int›
  oops

My next steps are to conclude the obvious normalization issues in the
distribution and then tackle the open more technical issues in the AFP.

Then I have to find a way to find out whether these resolve the observed
issues in l4v, particularly:

>> - the default simpset setup changed, it no longer reliably normalises ground terms with numerals.

>> - 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.

>> 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.

>> - 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.

Just a further observation:

>> 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.

Simp rules for concrete values are often oriented the other way round
than those for abstract reasoning; typical instances I’m familiar with
are abstract code equations and simp rules for numerals – which makes it
painful to prove *new* simp rules for numerals since the concrete
rewrites always get into the way.

But from what I have seen so far I don’t think that this applies here –
the bias towards take_bit stems from a few new simp rules on
conversions, which are now not default any longer.  Whether more rules
on take_bit would have resolved the problems is unclear to me, but the
idea behind the current setup to leave conversions in case of doubt
sounds like a reasonable and understandable approach to settle on.

Cheers,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211010/f55d22c1/attachment.sig>