[Verifpal] (feature request) Better unused outputs

[Loup Vaillant David]

Hi,

Looking a bit more closely at HMACVERIF, I see that its syntax is
currently not ideal (I can sense why: this simplifies your parser,
letting you (Nadim) concentrate on more important stuff).

Currently, we have to declare a new constant for each call of
HMACVERIF:

    unused1 = HMACVERIF(tag1, real tag1)
    unused2 = HMACVERIF(tag2, real tag2)
    unused3 = HMACVERIF(tag3, real tag3)

But we never use those constants! So I was thinking of two possible
alternatives. The first one is simply to allow some primitives to not
have otuputs at all (currently only HMACVERIF):

    HMACVERIF(tag1, real tag1)
    HMACVERIF(tag2, real tag2)
    HMACVERIF(tag3, real tag3)

The second one is to have a special keyword for ignored outputs:

    _ = HMACVERIF(tag1, real tag1)
    _ = HMACVERIF(tag2, real tag2)
    _ = HMACVERIF(tag3, real tag3)

We could use "null" or "nil" instead of "_". The Ocaml programming
language does this: "_" is a place holder for ignored variables (useful
for pattern matching), so the compiler doesn't complain with "unused
variable".

We could also interpret that keyword as a known public constant
(without requiring users to declare it). This would facilitate some
questionable uses of HKDF, such as:

    key1, key2 = HKDF(_, ikm, _)

But that's a separate feature, and a potentially confusing one. We
might want to force the user to be explicit there.

---

My personal preference would be to use "_" as a special keyword for
unused values (on the left of the "=" sign). It's a clear marker that
the user intend to ignore that output, and keeps the syntax simple and
regular.

Ideally, I think we would:

- Mandate that HMACVERIF use "_" as its output.
- Allow SIGNVERIF to use "_" as its output.
- Forbid the other primitives to use "_" as their output.

(Personally, I'm not sure the output of SIGNVERIF has any use. NaCl
wanted to make sure users didn't forget to verify the signature, but
Verifpal is not a C program: if we forget to verify a signature, the
model will likely be vulnerable, and Verifpal will catch the problem.)

Loup.