[Verifpal] (feature request) Consistent case sensitivity

[Loup Vaillant David]

Okay, here's what I have in mind: it's mostly about setting in stone
the conventions currently used in the manual.

First, everything is case sensitive: keywords, constant names,
primitive names, everything. Most notably "attacker", "ATTACKER",
"AtTaCkEr" all mean the same thing, and are all keywords.

Second, we should or error out when the following canonical form is not
respected:

- Keywords ("attacker", "principal"…) should be in lower case.
- Primitive names ("ENC", "DEC", "HASH"…) should be in all caps.
- Principal names ("Alice", "Bob"…) should start with an uppercase
  letter.
- Constant names ("a", "a_pub", "key"…) should start with a lowercase
  letter.

Third, we should error out when an inconsistent casing is detected in a
constant or principal name (the only words that are allowed to have
both lowercase and uppercase letters). We can't use both "ALICE" and
"Alice". We can't both use "key" and "kEY".

Fourth, we should punt on Unicode support, and do whatever Golang does
by default. If we enforce consistent casing, we shouldn't have any
locale problem.

---

That's about it. The first point is about the consistency I alluded to.
The second point is about setting the conventions you established in
stone. The third point is about avoiding the confusion that may arise
from reading "key", "Key", and "KEY" in the same model. The fourth
point is just about cutting corners.

Note for the second and third points that we don't have to error out.
We could issue warnings instead, or even provide a separate linter. My
personal preference goes to the full blown error, but I'm fine with
either solution.

Anything you disagree with?

Loup.



On Sun, 2019-09-01 at 19:48 +0200, Nadim Kobeissi wrote:
> Yes, but please describe your patch in more accurate technical detail
> here first (just a few bullet points, preferably with exactly which
> parts of the language you would be checking for casing, etc. etc.)
> and wait for my approval before expending your valuable time and
> effort on it.
> 
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> 
> > On Sep 1, 2019, at 2:59 PM, Loup Vaillant David <
> > loup at loup-vaillant.fr> wrote:
> > 
> > That's settled, then. Good.
> > 
> > Would you be willing to consider adding (or accept a patch that
> > adds)
> > warnings about inconsistent casing, such as using both "FOO" and
> > "foo"?
> > 
> > Loup.
> > 
> > 
> > On Sun, 2019-09-01 at 10:18 +0200, Nadim Kobeissi wrote:
> > > Dear Loup,
> > > 
> > > Thanks for raising this valid point. Despite your valid
> > > arguments,
> > > I’m personally very much in favor of moving towards full case
> > > insensitivity, because I think that this will make it harder for
> > > undergraduate students to make errors when using Verifpal. This
> > > is
> > > because goal 2 of Verifpal’s four main goals is "Modeling that
> > > avoids
> > > user error.”
> > > 
> > > I am pretty opinionated on this, and barring any hugely important
> > > arguments I don’t think I will change my mind. I hope the reason
> > > is
> > > clear. Happy to continue the discussion, however.
> > > 
> > > I’ll move the code more clearly in this direction in the coming
> > > weeks.
> > > 
> > > Have a great start of the academic year,
> > > 
> > > Nadim Kobeissi
> > > Symbolic Software • https://symbolic.software
> > > 
> > > > On Aug 30, 2019, at 7:52 PM, Loup Vaillant David <
> > > > loup at loup-vaillant.fr> wrote:
> > > > 
> > > > Hi,
> > > > 
> > > > 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
> > > > insensitive.
> > > > 
> > > > 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.
> > > > 
> > > > Loup.
> > > > 
> > > > 
> > > > 
> > > > _______________________________________________
> > > > Verifpal mailing list
> > > > Verifpal at lists.symbolic.software
> > > > https://lists.symbolic.software/mailman/listinfo/verifpal
> > > 
> > > 
> 
>