> On 11 Oct 2021, at 03:19, Florian Haftmann > <[email protected]> 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
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
