Email Gateway (Mar 22 2025 at 09:34): Email Gateway (Mar 22 2025 at 09:34):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi all,
in
https://isabelle.sketis.net/repos/afp-devel/file/tip/thys/AutoCorres2/lib/NatBitwise.thy#l19
there is an instance msb :: nat
That is trivial, since ‹not (msb n)› for all natural numbers n.
Given the context and history of that theory that appears to me as some
kind of accidental artifact. Is that instance actually deliberately used
somewhere?
The reason why I ask is that I am conducting an experiment how to equip
msb with an abstract specification, and while it would surely be
possible to allow degenerated instances like msb :: nat, it would be
cleaner to base everything on ring_bit_operations, which does not
include nat.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Mar 23 2025 at 00:03):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
It’s not accidental,— msb is an operation introduced for Word, and AutoCorres has an option to lift Word arithmetic into nat.
Cheers,
Gerwin
On 22 Mar 2025, at 20:32, Florian Haftmann <florian.haftmann@cit.tum.de> wrote:
Hi all,
in
https://isabelle.sketis.net/repos/afp-devel/file/tip/thys/AutoCorres2/lib/NatBitwise.thy#l19
there is an instance msb :: nat
That is trivial, since ‹not (msb n)› for all natural numbers n.
Given the context and history of that theory that appears to me as some kind of accidental artifact. Is that instance actually deliberately used somewhere?
The reason why I ask is that I am conducting an experiment how to equip msb with an abstract specification, and while it would surely be possible to allow degenerated instances like msb :: nat, it would be cleaner to base everything on ring_bit_operations, which does not include nat.
Cheers,
Florian
<OpenPGP_0xA707172232CFA4E9.asc>
Email Gateway (Mar 28 2025 at 13:43):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi Gerwin,
It’s not accidental,— msb is an operation introduced for Word, and AutoCorres has an option to lift Word arithmetic into nat.
this statement does not wholly fit the picture as found in the sources.
a) msb is not restricted to word types, it is generic (currently, purely
syntactic); there is an instance on int with ‹msb k <--> k < 0›.
b) In
https://isabelle.sketis.net/repos/afp-devel/file/tip/thys/AutoCorres2/lib/NatBitwise.thy#l19
there is the mentioned degenerate instance for nat with ‹not (msb n)›.
c) When lifting from word to nat, the corresponding operation is not msb:
‹msb w <--> msb (unat w)› does not hold
but ‹msb w <--> msb (unat w) (size w - 1)› does
d) At least concerning AutoCorres2, the degenerate instance nat :: msb
can be dropped safely:
<https://build.proof.cit.tum.de/build?id=e2dd2a76-3b4f-43f9-a83c-564c26bfa910>
– there is no theorem in AutoCorres2 referring to that instance. (I do
not know enough about the relationship between AutoCorres and
AutoCorres2 to judge how this observation transfers to AutoCorres).
Going back to the original question: is the instance msb :: nat actually
used somewhere? The evidence as found in the AFP suggests no, but this
might be illusive.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Mar 31 2025 at 09:25):From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Hi Florian,
On 28. Mar 2025, at 14:42, Florian Haftmann <florian.haftmann@cit.tum.de> wrote:
Going back to the original question: is the instance msb :: nat actually used somewhere? The evidence as found in the AFP suggests no, but this might be illusive.
Thanks for sorting this out. From our perspective and use cases feel free to remove the instance.
Regards,
Norbert
--
Norbert Schirmer (nschirmer@apple.com)
SEG Formal Verification
Email Gateway (Mar 31 2025 at 22:49):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
a) msb is not restricted to word types, it is generic (currently, purely syntactic); there is an instance on int with ‹msb k <--> k < 0›.
Yes, which was introduced later. The operation was originally written for the word type, like almost all bit operations that Isabelle currently supports.
b) In https://isabelle.sketis.net/repos/afp-devel/file/tip/thys/AutoCorres2/lib/NatBitwise.thy#l19 there is the mentioned degenerate instance for nat with ‹not (msb n)›.
Correct. And yes, I agree that it does not appear to be used in AutoCorres the way I thought it was.
d) At least concerning AutoCorres2, the degenerate instance nat :: msb can be dropped safely: <https://build.proof.cit.tum.de/build?id=e2dd2a76-3b4f-43f9-a83c-564c26bfa910> – there is no theorem in AutoCorres2 referring to that instance. (I do not know enough about the relationship between AutoCorres and AutoCorres2 to judge how this observation transfers to AutoCorres).
I don’t think the versions have deviated in that point, so that would not be a problem.
Going back to the original question: is the instance msb :: nat actually used somewhere? The evidence as found in the AFP suggests no, but this might be illusive.
Whether it is used or not was not your original question, and it should not decide the whether the instance should be dropped or not. Your question was whether it was intentional, and it was.
The real question is whether it is useful or not. I can see some scenarios where being able to write the term msb n for nat is useful, but since the instance is trivial, those can likely be avoided.
On the other side of the equation: what is the added benefit we get from dropping the nat instance?
Which instances are you intending for the new type class and which properties are you thinking to use for the axiomatisation? How much annoyance are we accepting if we want nat as an instance?
I’m not saying we can’t remove it under any circumstances, but we should remove it for the right reasons. You might have those, but that’s what we should be discussing.
Cheers,
Gerwin
Email Gateway (Apr 01 2025 at 11:37):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Am 01.04.25 um 00:48 schrieb Gerwin Klein (via cl-isabelle-users Mailing
List):
The real question is whether it is useful or not. I can see some scenarios where being able to write the term
msb nfor nat is useful, but since the instance is trivial, those can likely be avoided.On the other side of the equation: what is the added benefit we get from dropping the nat instance?
Which instances are you intending for the new type class and which properties are you thinking to use for the axiomatisation? How much annoyance are we accepting if we want nat as an instance?
OK, that is actually the next step in this mail thread.
For my currently favored proposal, see the attached theory.
There is some history behind.
The original motivation is to provide a type-agnostic abstract
specification for msb.
a) One idea would have been to restrict msb to word types, where there
is always a highest bit index. AFAIR, we have discarded this idea – I
don’t recall the details but I think there was a mail thread on this.
b) Another idea is purely hypothetical: There are a couple of operations
which conceptually exist in a »signed« and an »unsigned« variant on word
types. The signed variants correspond to counterparts on int (where
signed and unsigned coincide); but the syntax / type classes used on int
are used for the »unsigned« variants on word, breaking the
correspondence. Examples are (≤s, >>>, signed_take_bit) on word which
correspond to (≤, >>, take_bit) on int.
Would ≤ be signed and hence correspond to ≤ on int, then ‹msb a ↔ a < 0›
would hold. But this is just a theoretic observation: even if that
correspondence would justify to prefer the »signed« variants on word
types, it is now too late to change that.
c) What is demonstrated in the attached theory: a rather abstract
specification which nevertheless allows to deduce generic results like
‹msb (a AND b) ↔ msb a ∧ msb b›
The question is of course: how many instances of msb are around there
not part of the AFP?
For nat, it is surely possible to widen the superclass from
ring_bit_operations to semiring_bit_operations. This does however not
answer whether there are further instances outside there that would
require appropriate treatment.
Cheers,
Florian
Most_significant_bit.thy
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Apr 17 2025 at 20:22 UTC