[Verifpal] (feature request) Consistent case sensitivity

Loup Vaillant David loup at loup-vaillant.fr
Fri Aug 30 19:52:08 CEST 2019


Yet another nice to have, quality of life suggestion. This one is quite
bikeshed-y, and I'm not even sure what's the best solution myself (I
just have my personal preferences). You may want to just make a call
and stick to it.


I noticed that Verifpal is *partially* case insensitive:

- Constant identifiers are case insensitive.
- Primitive names are case insensitive.
- Keywords (principal, attacker…) seem to be case *sensitive*.

I didn't like the inconsistency. If you want case insensitivity,
*everything* should be case insensitive. I think. Maybe. In any case,
this got me thinking. There are basically 3 possible policies:

- Case sensitive.
- Case insensitive.
- Case "consistent" (a paranoid version of case insensitivity).

My personal preference is case sensitivity, for two reasons: first, if
you accept unicode characters, case insensitivity is locale sensitive.
Take "i" and "I" for instance. In English, the lower case one is
dotted, the upper case one is not. In Turkish however, there's a real
difference between the dotted "i" and the non-dotted one.  Changing the
case of an "i" in Turkish preserves the (lack of) dot! I see only 3
ways out of this nightmare: forbid unicode characters, assume an
English locale, or give up and become case insensitive.

The second reason is more serious: there's this convension where we
give the same name to both halves of a key pair: (ak, AK). By
convention, the lower case half "ak" represent the private key, and the
uppercase half "AK" represents the public key. I personally like this
convention, and use it when generating Monokex specifications. I can't
do the same with Verifpal however, because its identifiers are case

Now there are valid reason to still prefer case insensitivity my
beloved convention be dammed. But then there's a tweak that might help
readability: once we have chosen a case, we have to *stick to it*. For
instance, the following would fail:

    principal Alice [
        knows public FOO
    principal Bob [
knows public foo

  Syntax error: same identifier with different casings: "FOO", "foo"

That way the casual reader would not be left wondering whether "FOO",
"foo", or "Foo" refer to different things: once you've passed Verifpal,
it would not even matter to the reader whether that thing is case
sensitive or not.

Now there's nothing urgent about the colour of that bike shed. When we
polish for 1.0 however, this might be worth thinking about.


More information about the Verifpal mailing list