Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] signed and unsigned words

view this post on Zulip Email Gateway (Aug 22 2022 at 19:09):

From: Viorel Preoteasa <viorel.preoteasa@gmail.com>
Hello,

I need new types of signed and unsigned words with operations (+, -, ...) identical with the operations on words, but with a new operation:

overflow_add a b which is defined differently for signed and unsigned words.

Basically I need the two types to be instantiations of the following class:

class overflow = plus +
fixes overflow_add:: "'a ⇒ 'a ⇒ bool"

I tried something inspired from the AFP entry "Finite Machine Word Library":

type_synonym 'a sword = "'a signed word"
type_synonym 'a uword = "'a usigned word"

consts to_int :: "'a word ⇒ int"

overloading
to_int_sword ≡ "to_int:: 'a sword ⇒ int"
to_int_uword ≡ "to_int::'a uword ⇒ int"
begin
definition "to_int_sword (a:: 'a::len sword) = sint a"
definition "to_int_uword (a:: 'a::len uword) = uint a"
end

instantiation word :: (len0) overflow
begin
definition "overflow_add a b = (to_int (a::'a word) + to_int b = to_int (a + b))"
instance ..
end

this seems to work, but I don't know how to get code generation for overflow_add:

value "overflow_add (-2::4 sword) (-3)"

gives the error:

No code equations for to_int

Any help would be appreciated.

Best regards,

Viorel Preoteasa

view this post on Zulip Email Gateway (Aug 22 2022 at 19:11):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Viorel,

it is difficult to test your problem, since the “signed” and “usigned” types are something that I do neither find in the distribution nor in the AFP.

Hence, I can only blindly guess:

There might be a problem in your definition of “overflow_add” which uses the generic “to_int”, not a specific implementation.
This will work if “to_int” is defined as a class-constant (class some_name = fixes to_int :: …), but I’m not sure whether your approach via “consts to_int” is supported with code-generation.

So, you might try to reformulate the definition of to_int via class and instantiation.

Best regards,
René
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 19:12):

From: Viorel Preoteasa <viorel.preoteasa@gmail.com>
Dear René,

Thank you for your message.

On 18/02/2019 15.18, Thiemann, René wrote:

Dear Viorel,

it is difficult to test your problem, since the “signed” and “usigned” types are something that I do neither find in the distribution nor in the AFP.

The definition of the signed type is here:

https://www.isa-afp.org/browser_info/current/AFP/Word_Lib/Signed_Words.html

and the definition of unsigned is identical.

Hence, I can only blindly guess:

There might be a problem in your definition of “overflow_add” which uses the generic “to_int”, not a specific implementation.
This will work if “to_int” is defined as a class-constant (class some_name = fixes to_int :: …), but I’m not sure whether your approach via “consts to_int” is supported with code-generation.

So, you might try to reformulate the definition of to_int via class and instantiation.

This was my first attempt, but I did not manage the instantiation  of
class overflow as 'a signed word .

Now I have implemented a different solution. I created a new copy of the
type 'a word:

typedef (overloaded) 'a::len sword = "UNIV::'a word set"
  morphisms sword_to_word word_to_sword by auto

and I lifted all operations from word to sword. This seems to work, but
I am interested to find the best possible solution.

Best regards,

Viorel

Best regards,
René

I need new types of signed and unsigned words with operations (+, -, ...) identical with the operations on words, but with a new operation:

overflow_add a b which is defined differently for signed and unsigned words.

Basically I need the two types to be instantiations of the following class:

class overflow = plus +
fixes overflow_add:: "'a ⇒ 'a ⇒ bool"

I tried something inspired from the AFP entry "Finite Machine Word Library":

type_synonym 'a sword = "'a signed word"
type_synonym 'a uword = "'a usigned word"

consts to_int :: "'a word ⇒ int"

overloading
to_int_sword ≡ "to_int:: 'a sword ⇒ int"
to_int_uword ≡ "to_int::'a uword ⇒ int"
begin
definition "to_int_sword (a:: 'a::len sword) = sint a"
definition "to_int_uword (a:: 'a::len uword) = uint a"
end

instantiation word :: (len0) overflow
begin
definition "overflow_add a b = (to_int (a::'a word) + to_int b = to_int (a + b))"
instance ..
end

this seems to work, but I don't know how to get code generation for overflow_add:

value "overflow_add (-2::4 sword) (-3)"

gives the error:

No code equations for to_int

view this post on Zulip Email Gateway (Aug 22 2022 at 19:12):

From: Thomas Sewell <sewell@chalmers.se>
I recall the addition of the signed words, and maybe I can add some information.

I think that "'a signed word" and "'a word" are equivalent for all key operations. The signed variant was added as part of an adjustment of the C-to-Isabelle parser, so that in the resulting code it was possible to tell whether the variables were designated signed or unsigned in C. Note that most arithmetic is exactly the same.

Also note that the outer type constructor is word, that is, "32 signed word" is an instance of "'a word" where the length parameter is "32 signed". To make use of this, I think you want to define some kind of is_signed class with a class constant of type bool, and ensure that "32 signed" is signed, and that each numeral type counts as unsigned. Finally, you can lift that to a query on the outer word type.

I think that all might work, but I haven't tried any of it.

Cheers,

Thomas.

From: cl-isabelle-users-bounces@lists.cam.ac.uk <cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of Viorel Preoteasa <viorel.preoteasa@gmail.com>
Sent: Tuesday, February 19, 2019 10:40:26 AM
To: Thiemann, René
Cc: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] signed and unsigned words

Dear René,

Thank you for your message.

On 18/02/2019 15.18, Thiemann, René wrote:

Dear Viorel,

it is difficult to test your problem, since the “signed” and “usigned” types are something that I do neither find in the distribution nor in the AFP.

The definition of the signed type is here:

https://www.isa-afp.org/browser_info/current/AFP/Word_Lib/Signed_Words.html

and the definition of unsigned is identical.

Hence, I can only blindly guess:

There might be a problem in your definition of “overflow_add” which uses the generic “to_int”, not a specific implementation.
This will work if “to_int” is defined as a class-constant (class some_name = fixes to_int :: …), but I’m not sure whether your approach via “consts to_int” is supported with code-generation.

So, you might try to reformulate the definition of to_int via class and instantiation.

This was my first attempt, but I did not manage the instantiation of
class overflow as 'a signed word .

Now I have implemented a different solution. I created a new copy of the
type 'a word:

typedef (overloaded) 'a::len sword = "UNIV::'a word set"
morphisms sword_to_word word_to_sword by auto

and I lifted all operations from word to sword. This seems to work, but
I am interested to find the best possible solution.

Best regards,

Viorel

Best regards,
René

I need new types of signed and unsigned words with operations (+, -, ...) identical with the operations on words, but with a new operation:

overflow_add a b which is defined differently for signed and unsigned words.

Basically I need the two types to be instantiations of the following class:

class overflow = plus +
fixes overflow_add:: "'a ⇒ 'a ⇒ bool"

I tried something inspired from the AFP entry "Finite Machine Word Library":

type_synonym 'a sword = "'a signed word"
type_synonym 'a uword = "'a usigned word"

consts to_int :: "'a word ⇒ int"

overloading
to_int_sword ≡ "to_int:: 'a sword ⇒ int"
to_int_uword ≡ "to_int::'a uword ⇒ int"
begin
definition "to_int_sword (a:: 'a::len sword) = sint a"
definition "to_int_uword (a:: 'a::len uword) = uint a"
end

instantiation word :: (len0) overflow
begin
definition "overflow_add a b = (to_int (a::'a word) + to_int b = to_int (a + b))"
instance ..
end

this seems to work, but I don't know how to get code generation for overflow_add:

value "overflow_add (-2::4 sword) (-3)"

gives the error:

No code equations for to_int

view this post on Zulip Email Gateway (Aug 22 2022 at 19:12):

From: viorel.preoteasa@gmail.com
Hi Thomas,

Than you for your message. I know that most operations are the same,

but the overflow conditions are different. I need the signed and unsigned words

to be different (data)types such that I can instantiate differently a class overflow.

In the end I created a new copy of ‘a word as I mentioned in my previous message with lifting of definitions.

This gives me exactly what I need, but I don’t know if it adds overhead, especially when reasoning with the elements of the new type.

Best regards,

Viorel

From: Thomas Sewell <sewell@chalmers.se>
Sent: Tuesday, February 19, 2019 3:15 PM
To: Viorel Preoteasa <viorel.preoteasa@gmail.com>; Thiemann, René <Rene.Thiemann@uibk.ac.at>
Cc: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] signed and unsigned words

I recall the addition of the signed words, and maybe I can add some information.

I think that "'a signed word" and "'a word" are equivalent for all key operations. The signed variant was added as part of an adjustment of the C-to-Isabelle parser, so that in the resulting code it was possible to tell whether the variables were designated signed or unsigned in C. Note that most arithmetic is exactly the same.

Also note that the outer type constructor is word, that is, "32 signed word" is an instance of "'a word" where the length parameter is "32 signed". To make use of this, I think you want to define some kind of is_signed class with a class constant of type bool, and ensure that "32 signed" is signed, and that each numeral type counts as unsigned. Finally, you can lift that to a query on the outer word type.

I think that all might work, but I haven't tried any of it.

Cheers,

Thomas.

From: cl-isabelle-users-bounces@lists.cam.ac.uk <mailto:cl-isabelle-users-bounces@lists.cam.ac.uk> <cl-isabelle-users-bounces@lists.cam.ac.uk <mailto:cl-isabelle-users-bounces@lists.cam.ac.uk> > on behalf of Viorel Preoteasa <viorel.preoteasa@gmail.com <mailto:viorel.preoteasa@gmail.com> >
Sent: Tuesday, February 19, 2019 10:40:26 AM
To: Thiemann, René
Cc: cl-isabelle-users@lists.cam.ac.uk <mailto:cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] signed and unsigned words

Dear René,

Thank you for your message.

On 18/02/2019 15.18, Thiemann, René wrote:

Dear Viorel,

it is difficult to test your problem, since the “signed” and “usigned” types are something that I do neither find in the distribution nor in the AFP.

The definition of the signed type is here:

https://www.isa-afp.org/browser_info/current/AFP/Word_Lib/Signed_Words.html

and the definition of unsigned is identical.

Hence, I can only blindly guess:

There might be a problem in your definition of “overflow_add” which uses the generic “to_int”, not a specific implementation.
This will work if “to_int” is defined as a class-constant (class some_name = fixes to_int :: …), but I’m not sure whether your approach via “consts to_int” is supported with code-generation.

So, you might try to reformulate the definition of to_int via class and instantiation.

This was my first attempt, but I did not manage the instantiation of
class overflow as 'a signed word .

Now I have implemented a different solution. I created a new copy of the
type 'a word:

typedef (overloaded) 'a::len sword = "UNIV::'a word set"
morphisms sword_to_word word_to_sword by auto

and I lifted all operations from word to sword. This seems to work, but
I am interested to find the best possible solution.

Best regards,

Viorel

Best regards,
René

I need new types of signed and unsigned words with operations (+, -, ...) identical with the operations on words, but with a new operation:

overflow_add a b which is defined differently for signed and unsigned words.

Basically I need the two types to be instantiations of the following class:

class overflow = plus +
fixes overflow_add:: "'a ⇒ 'a ⇒ bool"

I tried something inspired from the AFP entry "Finite Machine Word Library":

type_synonym 'a sword = "'a signed word"
type_synonym 'a uword = "'a usigned word"

consts to_int :: "'a word ⇒ int"

overloading
to_int_sword ≡ "to_int:: 'a sword ⇒ int"
to_int_uword ≡ "to_int::'a uword ⇒ int"
begin
definition "to_int_sword (a:: 'a::len sword) = sint a"
definition "to_int_uword (a:: 'a::len uword) = uint a"
end

instantiation word :: (len0) overflow
begin
definition "overflow_add a b = (to_int (a::'a word) + to_int b = to_int (a + b))"
instance ..
end

this seems to work, but I don't know how to get code generation for overflow_add:

value "overflow_add (-2::4 sword) (-3)"

gives the error:

No code equations for to_int

Last updated: Apr 26 2024 at 01:06 UTC