Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2022-RC0: Simp-rules for bit


view this post on Zulip Email Gateway (Aug 23 2022 at 12:28):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

I already sent this to the mailing list last year when 2021-1 came out
but there was no answer, it probably got lost in the excitement of the
RC-process.

Personally, I think this is a confusing problem and should be changed.
However, if this is intended behavior, I would be happy if someone who
feels responsible for the "bit" type (in Z2) can confirm this.

In Isabelle2021-1, the simplification rules for the type bit (from
HOL-Library.Z2) have changed.

Besides other rules, we have the following simp rules:

* xor ?b ?c = of_bool (odd ?b ≠ odd ?c)
* of_bool (¬ ?P) = 1 - of_bool ?P
* (-) = (+)
* (+) = xor

These rules can give us a rewrite-cycle: xor is rewritten in terms of
"of_bool (... ~= ...)" which goes to "1 - of_bool ..." which goes to "1

Whether this actually happens depends on the concrete case (sometimes
the a case distinction splitter rule on the arguments of the xor happens
instead, I think).

But I have found that it can be quite easily triggered nonetheless.

For example, ‹xor b c = of_bool (b ≠ c)› makes the simplifier loop.

And if we add the (quite useful, imho) simp rule "((a=x) = (b=x)) =
(a=b)" for bits, then even something as natural as ‹a + b + b = a› loops.

An example theory is attached.

Of course, I don't know if there are any important reasons for those
xor-related simp-rules, but personally I feel that removing them (at
least the "xor ?b ?c = of_bool (odd ?b ≠ odd ?c)" rule) would make the
simplifier much less fragile in the presence of bit-related arithmetic.

(Also, as an aside: why is there "odd" in the definition of xor?
Wouldn't "xor ?b ?c = of_bool (?b ≠ ?c)" be simpler and equivalent?)

Best wishes,
Dominique.
Scratch.thy

view this post on Zulip Email Gateway (Aug 23 2022 at 15:42):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dominique,

thanks for reporting this.

a) The evil simp rule clearly is ‹of_bool (¬ ?P) = 1 - of_bool ?P›, I am
working on getting rid of it. (As often, the problem does not reside in
the theory which exposed it).

b) Concerning the deeper rationale, the history of theory Z2 is relevant.

Before 2013/14, the type bit = 0 | 1 was heavily used to represent
single bit values e. g. in what is nowadays HOL/Bit_Operations.thy and
HOL-Library/Word.thy – but not in all consequence, in some places bool
was used for the same purpose.

Andreas Lochbihler then suggested to reconcile this, and from that time
bool has been used consistently, the of_bool embedding stemming from
that time. The »bit« type has been kept for backward compatibility.

When starting re-working bit operations and word operations from 2019
on, I did not dare to cut of that backward compatibility strain but
asked myself for which applications »bit« could be preferable to »bool«
and came to the conclusion that it is a complete model of the field with
two elements, hence re-shaping it into theory Z2.

At that time I did not know of any applications but appreciated it as a
nice example how to introduce a data type with overloaded constructor
symbols. Also I tried to provide automation to reduce problems on type
»bit« to »bool«, hence using existing automation on »bool« to prove
problems on »bit«, which explains the rather aggressive default simp rules.

(Also, as an aside: why is there "odd" in the definition of xor?
Wouldn't "xor ?b ?c = of_bool (?b ≠ ?c)" be simpler and equivalent?)

You are clearly right that those RHSs could be formulated in a logically
simpler way, but then the expression of the primary idea would get lost:
reduce expressions on »bit« to expressions on »bool« with simple
straightforward correspondences.

Your proposal would essentially loose the rewriting the »bool«.

Cheers,
Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Aug 23 2022 at 18:12):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,

I wonder whether "xor ?b ?c = of_bool (odd ?b ≠ odd ?c)" shouldn't
removed from the simp-set instead (or in addition to) "of_bool (¬ ?P) =
1 - of_bool ?P". And then of course add enough simp-rules for xor to
compensate for this (such as "xor a a = 0" etc). (I would assume not too
many are needed.) One advantage would be that it leads to more readable
simplifications. Or alternatively rewrite xor to plus, that fits best
with the Z2-view and also leads to readable simplification results.

But that would of course not fit with the idea of rewriting everything
to bool.

Another possibility would be to make bit a type synonym for bool and
define 1 := true, 0 := false. (While still possibly instantiating the
field typeclass.)

At that time I did not know of any applications
I can explain where I use it. In cryptography, we often have an
adversary with a one-bit output (and we look at how the probability
distribution of that output changes). Now we could, of course, say the
output is of type bool, but there are two stylistic arguments against
it: (a) We get farther away from the established notation in crypto
(where we'd write Pr[x=1 : x<-A] and not Pr[x : x<-A]). (b) Using type
bool implies a certain meaning of the bit values (truth) but the outputs
0/1 of the adversary do not represent a yes/no answer per se, but just
two choices.

These arguments are of course a bit subjective, and technically there is
nothing that stops us from using bool here.

You are clearly right that those RHSs could be formulated in a logically
simpler way, but then the expression of the primary idea would get lost:
reduce expressions on »bit« to expressions on »bool« with simple
straightforward correspondences.
Ah, I understand now. "odd" is kind of "to_bool", and then it makes
sense intuitively!

Best wishes,
Dominique.

On 8/23/22 18:41, Florian Haftmann wrote:

Hi Dominique,

thanks for reporting this.

a) The evil simp rule clearly is ‹of_bool (¬ ?P) = 1 - of_bool ?P›, I am
working on getting rid of it. (As often, the problem does not reside in
the theory which exposed it).

b) Concerning the deeper rationale, the history of theory Z2 is relevant.

Before 2013/14, the type bit = 0 | 1 was heavily used to represent
single bit values e. g. in what is nowadays HOL/Bit_Operations.thy and
HOL-Library/Word.thy – but not in all consequence, in some places bool
was used for the same purpose.

Andreas Lochbihler then suggested to reconcile this, and from that time
bool has been used consistently, the of_bool embedding stemming from
that time. The »bit« type has been kept for backward compatibility.

When starting re-working bit operations and word operations from 2019
on, I did not dare to cut of that backward compatibility strain but
asked myself for which applications »bit« could be preferable to »bool«
and came to the conclusion that it is a complete model of the field with
two elements, hence re-shaping it into theory Z2.

At that time I did not know of any applications but appreciated it as a
nice example how to introduce a data type with overloaded constructor
symbols. Also I tried to provide automation to reduce problems on type
»bit« to »bool«, hence using existing automation on »bool« to prove
problems on »bit«, which explains the rather aggressive default simp rules.

(Also, as an aside: why is there "odd" in the definition of xor?
Wouldn't "xor ?b ?c = of_bool (?b ≠ ?c)" be simpler and equivalent?)
You are clearly right that those RHSs could be formulated in a logically
simpler way, but then the expression of the primary idea would get lost:
reduce expressions on »bit« to expressions on »bool« with simple
straightforward correspondences.

Your proposal would essentially loose the rewriting the »bool«.

Cheers,
Florian

view this post on Zulip Email Gateway (Aug 25 2022 at 06:22):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dominique,

see now https://isabelle.sketis.net/repos/isabelle/rev/c530cb79ccbc and
https://isabelle.sketis.net/repos/afp-devel/rev/cf809a286330 where the
rule »of_bool (Not P) = …« is removed.

I wonder whether "xor ?b ?c = of_bool (odd ?b ≠ odd ?c)" shouldn't
removed from the simp-set instead (or in addition to) "of_bool (¬ ?P) =
1 - of_bool ?P". And then of course add enough simp-rules for xor to
compensate for this (such as "xor a a = 0" etc). (I would assume not too
many are needed.) One advantage would be that it leads to more readable
simplifications. Or alternatively rewrite xor to plus, that fits best
with the Z2-view and also leads to readable simplification results.

But that would of course not fit with the idea of rewriting everything
to bool.

There might be reasons that the global rewriting to bool should be
removed entirely,
but then it should be done consequently for all operations, not just xor.

Another possibility would be to make bit a type synonym for bool and
define 1 := true, 0 := false. (While still possibly instantiating the
field typeclass.)

That could be worth a try.

At that time I did not know of any applications
I can explain where I use it. In cryptography, we often have an
adversary with a one-bit output (and we look at how the probability
distribution of that output changes). Now we could, of course, say the
output is of type bool, but there are two stylistic arguments against
it: (a) We get farther away from the established notation in crypto
(where we'd write Pr[x=1 : x<-A] and not Pr[x : x<-A]). (b) Using type
bool implies a certain meaning of the bit values (truth) but the outputs
0/1 of the adversary do not represent a yes/no answer per se, but just
two choices.

These arguments are of course a bit subjective, and technically there is
nothing that stops us from using bool here.

If your applications demands a very particular binary type, it could be best
to construct your own copy of bool.

Cheers,
Florian
OpenPGP_signature

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

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,

I can confirm that it works well for me now in Isabelle2022-RC2.

Best wishes,
Dominique.


Last updated: Mar 29 2024 at 12:28 UTC