Teach the typechecker more about exponents

[robdockins]

Regarding some kind of binary view - one thing I have encountered is having to add the explicit hint of 2 * 2 ^^ k == 2 ^^ (1 + k) into algorithms that work on types of size [2^^k] by splitting; it would be good if the typechecker could deal with powers of 2, at least, in this manner automatically: I don't know if this needs its own issue or might naturally be solved as part of this?

Originally posted by @linesthatinterlace in #701 (comment)

[robdockins]

I don't know how difficult this would be, but it would really be nice if the typechecker knew that
x ^^ (a+b) == (x ^^ a) * (x ^^ b)

[brianhuffman]

Another thing we might teach Cryptol about exponents is injectivity: x ^^ a == x ^^ b iff a == b, as long as x > 1. A rule like this would probably be useful even if it only applied when x was a numeric literal.

[yav]

We may want to use the kind of normalization that Clash does, something like what this package does: http://hackage.haskell.org/package/ghc-typelits-natnormalise

[robdockins]

I was recently annoyed that cryptol could not deduce that 2^^(width n) >= n. That would be another nice fact to have.

[robdockins]

FWIW, I tried adding the following axiom and a couple of variations to the typechecking database, and it seemed to cause an instantiation loop. We might still be able to do something here inside Cryptol itself, but just adding axioms to Z3 doesn't seem to work very well.

 (assert (forall ((x Int) (y Int) (z Int))
   (! (=> (and (> x 0) (> y 0) (> z 0))
       (= (cryExpUnknown x (+ y z))
          (* (cryExpUnknown x y) (cryExpUnknown x z))))
   :pattern ( (cryExpUnknown x (+ y z)) ) )
   ))

[linesthatinterlace]

Do you need >y 0 and >z 0? Surely this rule applies when they are 0 (or indeed when they are negative, but obviously negative exponents might not be defined).

I assume this isn't causing your issue though.

[robdockins]

Yeah, I don't think it's relevant to the issue of Z3 getting lost in the woods with this axiom. I don't have much experience with Z3's pattern triggering mechanism, so it's possible I messed something up, but I could not figure out how to get this to behave well.

[linesthatinterlace]

I have actually managed to sort some of my previous issues with recursion - or rather, I've reduced it to the above problem. But I now need to implement the following...

reduceThis : {m, a} (fin m, m>=1) => [2^^m]a -> [2*2^^(m - 1)]a
reduceThis xs = undefined

reduceThat : {m, a} (fin m, m>=1) => [2*2^^(m - 1)]a -> [2^^m]a
reduceThat xs = undefined

boost : {m} (fin m) => [2^^m] -> [2 ^^ max 1 m]
boost = undefined // ("Double if m = 0, otherwise leave the same".)

unboost : {m} (fin m) => [2^^max 1 m] -> [2^^m]
unboost = undefined // ("Half if m = 0, otherwise leave the same.")

But I can't work out a way to do even the reduce pair with the tools available: Cryptol doesn't know anything about inequalities and powers, even, so one can't even use drop or zero#... rather stuck!

[robdockins]

Humm... I also don't see any obvious way to witness these equivalences with the tricks currently at our disposal.

I wonder about allowing the following escape hatch for these kinds of size equivalences that we can't prove.

coerceSize : {m, n, a} [m]a -> [n]a

With the semantics that the function is a no-op at runtime if m = n and raises an error otherwise.

[yav]

@robdockins I like the coerceSize idea, it seems simple and probably more honest than some of the hackery we currently do to get the types to "fit in" (e.g., the min/take tricks)

[linesthatinterlace]

powAdd : {x, y, z, a} (fin x, fin y, fin z) => [x^^y*x^^z]a -> [x^^(y + z)]a
powAdd xs = take <~ (xs # undefined`{[max (x^^y*x^^z) (x^^(y + z)) - x^^y*x^^z]a})

powAddRev : {x, y, z, a} (fin x, fin y, fin z) => [x^^(y + z)]a-> [x^^y*x^^z]a
powAddRev xs = take <~ (xs # undefined`{[max (x^^y*x^^z) (x^^(y + z)) - x^^(y + z)]a})

These do it (or in the special case...):

reduceThis : {m, a} (fin m, m>=1) => [2^^m]a -> [2*2^^(m - 1)]a
reduceThis xs = take <~ (xs # undefined`{[max (2*2^^(m - 1)) (2^^m) - 2^^m]a})

reduceThat : {m, a} (fin m, m>=1) => [2*2^^(m - 1)]a -> [2^^m]a
reduceThat xs = take <~ (xs # undefined`{[max (2*2^^(m - 1)) (2^^m) - 2*2^^(m - 1)]a})

Your solution is nicer, though. As yav says, it's "more honest".

[linesthatinterlace]

I have managed to get my code to work using my powAdd and powAddRev functions (powAddRev{2, 1, m - 1} and powAdd{2, 1, m - 1} in this case). God knows what'll happen when I throw it at SAW though...

[linesthatinterlace]

coerceSize : {m, n, a} (fin m, fin n) => [m]a -> [n]a
coerceSize xs = take <~ (xs # undefined`{[max m n - m]a})

This does you the job of coerceSize, I think.

Edit: actually, this might be even better:

coerceSize' : {m, n, a} (fin m, fin n) => [m]a -> [n]a
coerceSize' xs = take <~ (xs # undefined`{[inf]a})

(not sure).

Edit2: or this!

coerceSize : {m, n, a} [m]a -> [n]a
coerceSize xs = [ xs @ i | i <- [0 .. <n]]

[robdockins]

That works, but I think it's desirable for efficiency reasons to make it a primitive.

[linesthatinterlace]

Yeah, that makes sense.

Using coerceSize, then, here's a rewrite of that sorting algorithm you added recently:

sortBy' : {n, a} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
sortBy' le vs = if `n == (0 : Integer)
                then coerceSize (sortBy_zero le vs_zero)
                else coerceSize (sortBy_rec`{max 1 n} le vs_rec)
  where vs_zero = coerceSize vs : [0]a
        vs_rec  = coerceSize vs : [max 1 n]a

sortBy_zero : {n, a} (fin n, n==0) => (a -> a -> Bit) -> [n]a -> [n]a
sortBy_zero le vs = vs

sortBy_rec : {n, a} (fin n, n>=1) => (a -> a -> Bit) -> [n]a -> [n]a
sortBy_rec le vs = insertBy' le (head vs) (sortBy' le (tail vs))

insertBy' : {k, a} (fin k) => (a -> a -> Bit) -> a -> [k]a -> [k+1]a
insertBy' le x0 ys = xys.0 # [last xs]
  where
    xs : [k+1]a
    xs = [x0] # xys.1
    xys : [k](a, a)
    xys = [ if le x y then (x, y) else (y, x) | x <- xs | y <- ys ]

So it's a nice way of doing this sort of pattern, I think?

[weaversa]

I have found (and been told by new students of Cryptol) that they find it hard to grasp why Cryptol won't allow them to write something like this (nonsensical example):

f : {a} (fin a) => Bit
f = head x
  where
    x = if `a == 0
        then 0xab
        else 0xa

This kind of pattern shows up in many different crypto algorithms such as Salsa20 (Salsa20Expansion), HMAC (kinit), and NIST-800-38F (KW and KWP). The solution being presented here is something along the lines of:

coerceSize : {m, n, a} [m]a -> [n]a
coerceSize xs = [ xs @ i | i <- [0 .. <n]]

f : {a} (fin a) => Bit
f = head x
  where
    x = if `a == 0
        then coerceSize 0xab
        else coerceSize 0xa

Consider going a step farther -- what would it look like for coerceSize to be totally under the hood / transparent to the user? What if arguments to conditionals (and maybe arguments to function calls) where all implicitly wrapped in coerceSize?

The concatenation with undefined protects from expanding more than you meant to. I don't see how to avoid unintended truncation with the tools we have. Perhaps if coerseSize x returned x when the size didn't change and undefined otherwise?

[weaversa]

Rereading my comment, I think what I'm suggesting (and to a lesser extent what coerseSize does now) is to move some type checking into the runtime system. Perhaps that's not a good thing?

[linesthatinterlace]

Certainly the concatenation with undefined was designed to achieve exactly that (in my head it is somewhat analogous to accessing a C-style array outside of its initialised bounds).

I think this issue is trying to solve this kind of problem/pattern in general: #701 - it avoids the hack of, effectively as you say, doing typechecks at runtime. That being said: it wouldn't solve the issue of the typechecker not understanding exponential arithmetic (in a sense they are different but enmeshed issues both of which coerceSize solves).

Note that coerceSize actually can be used for when m is not equal to n, as it is currently written, and as long as you then don't try to actually ultimately output any junk data, it'll be fine (or it just truncates).

It doesn't act on double arrays, of course, but one can just use map for this

[robdockins]

The version I had in mind is morally equivalent to:

coerceSize : {m,n,a} [m]a -> [n]a
coerceSize xs = assert (`m == `n) "coerceSize: size mismatch" [ xs@i | i <- [0..<n] ] 

Modulo the fact that Cryptol won't accept this definition without fin constraints.

I certainly don't think we should be inserting these coercions automatically; the whole point is to only allow things that the user is very confident are correct but that the typechecker cannot prove for one reason or another.

[weaversa]

I appreciate the assert! That's a nice way to stop accidental truncation.

[weaversa]

@robdockins If the type system could demote type constraints to Bit, we wouldn't need the fin constraint (I think).

Cryptol> `(1 == 2) : Bit

[error] at <interactive>:4:3--4:9:
  Incorrect type form.
    Expected: a numeric type
    Inferred: a constraint

I've stumbled into the forced fin constraints a few times now. For example, how to write an isPrefix function that supports an infinite sequence as a first argument?

isPrefix : {m, n, a} (fin n, Eq a) => [m]a -> [n]a -> Bit
isPrefix xs x =
    if `m < `n then False
    else and [ xi == xsi | xi <- x | xsi <- xs ]

[error] at a.cry:2:1--4:49:
  Failed to validate user-specified signature.
    in the definition of 'Main::isPrefix', at a.cry:2:1--2:9,
    we need to show that
      for any type m, n, a
      assuming
	• fin n
	• Eq a
      the following constraints hold:
	• fin m
            arising from
            use of literal or demoted expression
            at a.cry:3:8--3:15

Would it be feasible to support this type of thing? If so, I can create an issue for it. Then we could do:

isPrefix : {m, n, a} (fin n, Eq a) => [m]a -> [n]a -> Bit
isPrefix xs x =
    if `(m < n) then False
    else and [ xi == xsi | xi <- x | xsi <- xs ]

And coerceSize could be (no fin needed):

coerceSize : {m,n,a} [m]a -> [n]a
coerceSize xs = assert `(m == n) "coerceSize: size mismatch" [ xs@i | i <- [0..<n] ] 

[robdockins]

That's an interesting idea. I think demoting all constraints would probably be a little tricky (class constraint resolution is sort of three-valued), but we can certainly add one or more primitives specifically for computing values corresponding to type-level comparisons.

I'm imagining something like:

primitive compareEq : {n:#, m:#} Bit
primitive compareLt : {n:#, m:#} Bit
primitive compareLeq : {n:#, m:#} Bit

Those should be pretty simple to implement, and would let us do things like you've sketched above. We could maybe even add magic backtick support for desugaring exactly those constraints, as we currently do for number.

I think that would work, and I like it better than just making a special case for coerceSize.

[robdockins]

On second thought, we wanted coerceSize to be a primitive anyway for efficiency. Nonetheless, being able to demote these constraints seems like good idea.

[msaaltink]

@weaversa asked:

I've stumbled into the forced fin constraints a few times now. For example, how to write an isPrefix function that supports an infinite sequence as a first argument?

isPrefix : {m, n, a} (fin n, Eq a) => [m]a -> [n]a -> Bit
isPrefix xs x =
    if `m < `n then False
    else and [ xi == xsi | xi <- x | xsi <- xs ]

[error] at a.cry:2:1--4:49:
  Failed to validate user-specified signature [...]

Well, that specific problem is not so hard to solve; using min can force values to be finite:

isPrefix : {m, n, a} (fin n, Eq a) => [m]a -> [n]a -> Bit
isPrefix xs x =
    if `(min m n) < `n then False
    else and [ xi == xsi | xi <- x | xsi <- xs ]

Now Cryptol is perfectly happy:

 Main> isPrefix 0b1010101 0b10
True
Main> isPrefix 0b1010101 0b11
False
Main> isPrefix 0b00 0b111
False
Main> isPrefix (zero:[inf]) 0b11
False
Main> isPrefix (zero:[inf]) 0b00
True

I admit, though, that this smells like a hack rather than some generic easy-to-use method. Demotion to Bit sure seems more general.