Support quantification over the Cryptol # kind

[Isweet]

Example

Suppose we have a Cryptol module Example in Example.cry below and the subsequent SAW script.

module Example where

p : {N} (fin N, N % 2 == 0, 2 <= N, N <= 6) => [N] -> Bit
p w = w == w

import "./Example.cry" as Example;

// Verify a new property, `p`, named `name`, using tactic `t`.
let verify name p t = time do { print (str_concat (str_concat "Verifying " name) "..."); prove_print t (rewrite basic_ss p); };

Example <- verify "example" {{ Example::p }} rme;

The example above will cause SAW to produce an error:

[14:57:36.508] Stack trace:
"verify" (/.../proof.saw:13:12-13:18)
"time" (/.../proof.saw:11:23-11:27)
"prove_print" (/.../proof.saw:11:90-11:101)
"t" (/.../proof.saw:11:102-11:103)
"rme" (/.../proof.saw:13:42-13:45)
sequentToSATQuery: expected first order type or assertion:
Cryptol.Num

As an aside, this error message probably also deserves a SAW issue for usability.

To confirm that this error is due to Example::p being parametric, we can instantiate the type parameter explicitly:

Example <- verify "example" {{ Example::p`{2} }} rme;

In this case, SAW successfully proves the theorem.

Discussion

An example like this is surprising to me because the kind of the type variable in the Cryptol expression is #, which is the numeric kind. I'd sort of expect, at a high level, that quantifying over the numeric should be possible by (say) translating to SMT by introducing a symbolic variable for the type variable, and introducing SMT constraints corresponding to the type constraints (e.g, 2 <= N above). As I write this, it occurs to me that if a Cryptol sequence is encoded as an SMT bitvector then this would mean the SMT solver would need to support variables whose kind is "bitvector of length x" where x is a symbolic Nat. Maybe that's not a thing?

I don't think I have any recommendations for this. It is chiefly a usability issue since the user can always manually instantiate the property with all satisfying numerics. However, it does show up quite a bit in conjunction with #2208, because the mitigation for that is to make every declaration in the module parametric.

[RyanGlScott]

As I write this, it occurs to me that if a Cryptol sequence is encoded as an SMT bitvector then this would mean the SMT solver would need to support variables whose kind is "bitvector of length x" where x is a symbolic Nat. Maybe that's not a thing?

That is not a thing in SMT-LIB as far as I am aware.

[sauclovian-g]

Indeed, that's not a thing. If the range is bounded (as it is in the example) we could always expand it, but I don't think that should happen without someone saying so as it could end up expensive.

[sauclovian-g]

It is also possibly feasible in some cases to prove it for e.g. bits == 3 and generalize the proof to larger bitvectors by rewriting and rechecking the proof itself; however, that's going to take real work 😐

[Isweet]

A quick literature search yielded this paper from the Stanford / CVC5 folks: https://arxiv.org/pdf/1905.10434. It is possibly helpful in encoding symbolic bit-width statements into fixed bit-width.

In any event, I agree 100% that it is not an easy fix.

[sauclovian-g]

Cryptol refuses to let you prove things of this form, right? It'll complain they're polymorphic, IIRC.

We should be able to fix the error message relatively soon; the rest is ... problematic, alas.

[RyanGlScott]

Cryptol refuses to let you prove things of this form, right?

Correct:

Cryptol> :prove \(x : [n]) -> x == x
[warning] at <interactive>:1:15--1:16
    Unused name: n
Not a monomorphic type:
{n} (fin n) => [n] -> Bit
(Total Elapsed Time: 0.000s)

[Isweet]

Another thought I had in passing...

In contrast to having the SMT layer support bit-vector kinds with symbolic width, could you enhance SAWCore reasoning so the user could manually discharge any propositions over Cryptol types with symbolic widths before going to the SMT layer?

I can't imagine what that reasoning would be. I was imagining a case analysis and induction principle. The case analysis would be for situations where the symbolic width is highly constrained (e.g., in AES n is 128, 192, or 256). SAWCore could give you a tactic case or something that discharges to the solver to determine possible values and then transforms the goal into k sub-goals (e.g., k = 3 for AES). The situation where the symbolic width is not highly constrained is trickier because you'd want to use a (likely conditional) induction principle. However, proving the inductive goal would involve a bit-vector with symbolic width. I have this vague feeling that you could use the inductive hypothesis and some uninterpreted function reasoning to sneak around the issue of a symbolic width, but that's just an intuition.

It'd be valuable to punt on the more complicated situation (unconstrained) and implement the easier situation (highly constrained). The highly constrained situations show up everywhere (key sizes, elliptic curve choices, hash function choice, block cipher choice). There's rarely more than 5-10 choices for a lot of the parametric code in Cryptol.

• Key Sizes in AES
• Elliptic Curves
• HMAC (should eventually be parametric over hash functions)

Thoughts?

[RyanGlScott]

I was imagining a case analysis and induction principle

SAW includes an extremely experimental induction-based command called prove_by_bv_induction for this purpose. That being said, it is pretty rough around the edges—I wouldn't recommend using it unless you know exactly what you are doing.

[sauclovian-g]

My experience mucking with bitvectors in Coq is that induction on the bitvector size is rarely workable. So splitting the goal into a smallish number of fixed sizes is reasonable (I think there's already a way to do that, but I can't find it now) but even if saw were good at induction, which it isn't, I don't think trying to prove things for all bitvector sizes is advisable.

[Isweet]

So, just to check my understanding...

I think there's already a way to do that, but I can't find it now

Does that mean I can define a theorem like

\(fin n, 0 < n, n <= 4, n % 2 == 0) => (x : [n]) -> x == x

and you believe there's some tactic which will allow me to prove it by doing case analysis on n and then reducing the proof obligation to two goals: (x : [2]) -> x == x and (x : [4]) -> x == x? (Sorry, I know I'm using Cryptol syntax here, and these would technically be SAWCore terms, but I don't know the syntax of SAWCore well enough to create them on the fly.)

Note: I'm not sure if the Cryptol syntax I have above that includes constraints on an anonymous function is A Thing... but just pretend :)

[Isweet]

As a follow-up, I ran into this limitation again today while trying to do some proofs over SHA3. The top-level function provided by each instantiation (e.g., SHA3_{224,256,384,512}), hash, doesn't fix an upper bound on the input size of the message.

hash : {n} (fin n) => [n] -> [digest]

So, without some way to work around this limitation, I'm unsure how to prove any property (over all possible n) of this function. AFAIK prove_by_bv_induction is my only option, and pushing through that seems like a big time sink (per Ryan).

This was just a usability issue with AES, since the top-level functions for each instantiation were all monomorphic. But, here that isn't the case.

[sauclovian-g]

Does that mean I can define a theorem like

\(fin n, 0 < n, n <= 4, n % 2 == 0) => (x : [n]) -> x == x

and you believe there's some tactic which will allow me to prove it by doing case analysis on n and then reducing the proof obligation to two goals: (x : [2]) -> x == x and (x : [4]) -> x == x?

Yes. If that tactic doesn't actually exist (or isn't general enough) it can be made to exist, not necessarily for free (especially as the constraints get more complex) but abstractly it's just a finite case analysis on n.

(Sorry, I know I'm using Cryptol syntax here, and these would technically be SAWCore terms, but I don't know the syntax of SAWCore well enough to create them on the fly.)

You don't really want to. Cryptol syntax is fine.

doesn't fix an upper bound

That's harder, yeah. But that one's not a bitvector size and it's definitely plausible to do it by induction on n; getting saw to actually go along will be the exciting part.

(also, you don't want to do it by proving each possible size separately, even if you could try)

[sauclovian-g]

Update: I found it again, llvm_refine_spec.

[Isweet]

@sauclovian-g Should I not pay too much attention to the llvm_ prefix? I'm only doing Cryptol - Cryptol verification, but maybe that doesn't matter?

[sauclovian-g]

Hmm, no, it won't work, it operates on LLVMSpecs. You need the equivalent for Theorems, right? That does not seem to exist. I wouldn't think it would be that hard to add though.

[Isweet]

Yes, that's right. I'm imagining something of type ProofScript () that, when placed in a proof, takes the current goal and creates sub-goals in the way described above. The proof would be proof of a SAW Theorem (e.g., using prove_print or something similar).

[sauclovian-g]

I was thinking of something of the form [Theorem] -> ProofScript -> Theorem. As a tactic, you might be able to just construct a theorem and apply it rather than needing any specific support. Something like P 2 -> P 4 -> (\n -> 0 < n /\ n <= 4 /\ n % 2 == 0 -> P n); I would hope that would prove with P marked uninterpreted, and then goal_apply ought to do the trick.