[isabelle-dev] Word Libraries

[Gerwin Klein]

> On 11 Oct 2021, at 03:19, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> Signed PGP part
> 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.

Excellent.


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

Also sounds good.


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

This sounds all good.


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

The last update fixed all the occurrences that Isabelle2021 introduces, so it might be nontrivial to find examples. I can try to start a partial update to Isabelle2021-1-RC0 and report on how that goes. I can probably also still relatively easily find the positions where looping with commutativity was the specific problem.


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

I'd be happy with that.

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/20211012/8ff9832c/attachment.sig>