Defaulting #774

robdockins · 2020-06-21T00:37:15Z

Rework defaulting rules.

This is an experiment in progress. This branch implements new defaulting rules that are now possible with recent Cryptol changes.

In short: we no longer perform defaulting by guessing bit-widths. Instead literals are defaulted to unlimited precision types (Integer or Rational) when appropriate. Defaulting warnings are now suppressed by default, as they are essentially harmless.

There are only a tiny collection of tests in the test suite that changed semantics as a result of these changes. By far, the most common result was the elimination of defaulting warnings.

robdockins · 2020-06-21T00:39:03Z

tests/mono-binds/test05.icry.stdout

 module test05
 import Cryptol
 /* Not recursive */
 test05::foo : [10]
 test05::foo = Cryptol::number 10 [10] <>

 /* Not recursive */
-test05::test : {n, a, b} (Zero b, Literal 10 a) => [n]b -> a
-test05::test = \{n, a, b} (Zero b, Literal 10 a) (a : [n]b) ->
+test05::test : {n, m, a, b} (Literal 10 a, fin n, Zero b) =>


This is one of the more substantial changes to inference

robdockins · 2020-06-21T00:40:17Z

tests/parser/unary-2.icry.stdout

-[warning] at unary-2.cry:2:11--2:14:
-  Defaulting type argument 'a' of 'min' to [2]
-True
+Showing a specific instance of polymorphic result:


This is an actual change in semantics due to defaulting.

weaversa · 2020-06-21T00:47:03Z

we no longer perform defaulting by guessing bit-widths.

I hope that's an oversimplification. Does this type of defaulting no longer work?

Cryptol> 10 : [_]
Showing a specific instance of polymorphic result:
  * Using '4' for type wildcard (_)
0xa

robdockins · 2020-06-21T17:46:58Z

That example does still work; we apply additional defaulting at the REPL, and those haven't changed.

All the defaulting rules described above are the ones that apply during typechecking. The REPL defaulting rules are applied later, when a term is evaluated at the command line, or in a :check, etc.

weaversa · 2020-06-21T20:00:09Z

How about this ever so slightly modified (but still correct) DES.cry?
cryptol-specs.tar.gz

cryptol-specs]$ cryptol Primitive/Symmetric/Cipher/Block/DES.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.8.1 (e914cef)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Primitive::Symmetric::Cipher::Block::Cipher
Loading module Primitive::Symmetric::Cipher::Block::DES
[warning] at Primitive/Symmetric/Cipher/Block/DES.cry:25:40--25:41:
  Defaulting type wildcard (_) to max 1 (width ?n`1121)
  where
  ?n`1121 is length of comprehension generator at Primitive/Symmetric/Cipher/Block/DES.cry:22:15--24:35

weaversa · 2020-06-21T20:30:46Z

Does this still work:

g : {a} (fin a) => [a] -> [a] -> [a]
g a b = (a >>> 7) + (reverse b)

f : [32] -> Bit
f x = (x @ (g 10 11) ^ x @ (g 12 19)) && (x <<< (g 9 3)) @ (g 2 8)

[cryptol-course]$ cryptol test.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.8.1 (e914cef)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Main
[warning] at test.cry:5:13--5:14:
  Defaulting type argument 'a' of 'g' to 4
[warning] at test.cry:5:29--5:30:
  Defaulting type argument 'a' of 'g' to 5
[warning] at test.cry:5:50--5:51:
  Defaulting type argument 'a' of 'g' to 4
[warning] at test.cry:5:61--5:62:
  Defaulting type argument 'a' of 'g' to 4
Main> :prove \x -> f x >= False
Q.E.D.
(Total Elapsed Time: 0.008s, using "Z3")

robdockins · 2020-06-22T02:47:18Z

The DES example fails in this current branch with:

Loading module Cryptol
Loading module Primitive::Symmetric::Cipher::Block::Cipher
Loading module Primitive::Symmetric::Cipher::Block::DES
[error] at Primitive/Symmetric/Cipher/Block/DES.cry:13:24--13:27:
  Failed to infer the following types:
    • ?Primitive::Symmetric::Cipher::Block::DES::des_1`1268, 1st type argument of 'Primitive::Symmetric::Cipher::Block::DES::des' at Primitive/Symmetric/Cipher/Block/DES.cry:13:24--13:27
  subject to the following constraints:
    • fin ?Primitive::Symmetric::Cipher::Block::DES::des_1`1268
        arising from
        use of expression Primitive::Symmetric::Cipher::Block::DES::des
        at Primitive/Symmetric/Cipher/Block/DES.cry:13:24--13:27
[error] at Primitive/Symmetric/Cipher/Block/DES.cry:14:24--14:27:
  Failed to infer the following types:
    • ?Primitive::Symmetric::Cipher::Block::DES::des_1`1276, 1st type argument of 'Primitive::Symmetric::Cipher::Block::DES::des' at Primitive/Symmetric/Cipher/Block/DES.cry:14:24--14:27
  subject to the following constraints:
    • fin ?Primitive::Symmetric::Cipher::Block::DES::des_1`1276
        arising from
        use of expression Primitive::Symmetric::Cipher::Block::DES::des
        at Primitive/Symmetric/Cipher/Block/DES.cry:14:24--14:27

robdockins · 2020-06-22T02:49:02Z

Likewise, the example with f and g fail.

Loading module Cryptol
Loading module Main
[error] at asdf2.cry:5:7--5:67:
  Failed to infer the following types:
    • ?a`983, type argument 'a' of 'Main::g' at asdf2.cry:5:61--5:62
  subject to the following constraints:
    • fin ?a`983
        arising from
        use of expression (Cryptol::@)
        at asdf2.cry:5:7--5:67
[error] at asdf2.cry:5:8--5:37:
  Failed to infer the following types:
    • ?a`959, type argument 'a' of 'Main::g' at asdf2.cry:5:13--5:14
  subject to the following constraints:
    • fin ?a`959
        arising from
        use of expression (Cryptol::@)
        at asdf2.cry:5:8--5:37
[error] at asdf2.cry:5:15--5:17:
  Failed to infer the following types:
    • ?a`959, type argument 'a' of 'Main::g' at asdf2.cry:5:13--5:14
  subject to the following constraints:
    • ?a`959 >= 4
        arising from
        use of literal or demoted expression
        at asdf2.cry:5:15--5:17
[error] at asdf2.cry:5:31--5:33:
  Failed to infer the following types:
    • ?a`967, type argument 'a' of 'Main::g' at asdf2.cry:5:29--5:30
  subject to the following constraints:
    • ?a`967 >= 4
        arising from
        use of literal or demoted expression
        at asdf2.cry:5:31--5:33
[error] at asdf2.cry:5:34--5:36:
  Failed to infer the following types:
    • ?a`967, type argument 'a' of 'Main::g' at asdf2.cry:5:29--5:30
  subject to the following constraints:
    • ?a`967 >= 5
        arising from
        use of literal or demoted expression
        at asdf2.cry:5:34--5:36
[error] at asdf2.cry:5:43--5:56:
  Failed to infer the following types:
    • ?a`980, type argument 'a' of 'Main::g' at asdf2.cry:5:50--5:51
  subject to the following constraints:
    • fin ?a`980
        arising from
        use of expression (Cryptol::<<<)
        at asdf2.cry:5:43--5:56
[error] at asdf2.cry:5:52--5:53:
  Failed to infer the following types:
    • ?a`980, type argument 'a' of 'Main::g' at asdf2.cry:5:50--5:51
  subject to the following constraints:
    • ?a`980 >= 4
        arising from
        use of literal or demoted expression
        at asdf2.cry:5:52--5:53
[error] at asdf2.cry:5:54--5:55:
  Failed to infer the following types:
    • ?a`980, type argument 'a' of 'Main::g' at asdf2.cry:5:50--5:51
  subject to the following constraints:
    • ?a`980 >= 2
        arising from
        use of literal or demoted expression
        at asdf2.cry:5:54--5:55
[error] at asdf2.cry:5:63--5:64:
  Failed to infer the following types:
    • ?a`983, type argument 'a' of 'Main::g' at asdf2.cry:5:61--5:62
  subject to the following constraints:
    • ?a`983 >= 2
        arising from
        use of literal or demoted expression
        at asdf2.cry:5:63--5:64
[error] at asdf2.cry:5:65--5:66:
  Failed to infer the following types:
    • ?a`983, type argument 'a' of 'Main::g' at asdf2.cry:5:61--5:62
  subject to the following constraints:
    • ?a`983 >= 4
        arising from
        use of literal or demoted expression
        at asdf2.cry:5:65--5:66

robdockins · 2020-06-22T02:50:11Z

Both failures are proper, in my opinion. The DES one works fine if you leave off the : [_] annotation. The example with f and g is the sort of thing that really should never have worked.

weaversa · 2020-06-22T10:22:08Z

Does this proof still work? I'm pretty sure abc doesn't support Integers, but I'm hoping that since length is a constant, the Integer somehow gets resolved before making its way to smtlib...?

Primitive::Symmetric::Cipher::Block::DES> :s prover=abc
Primitive::Symmetric::Cipher::Block::DES> :prove \k pt -> DES.decrypt k (DES.encrypt k pt) == pt
Q.E.D.
(Total Elapsed Time: 0.730s, using "ABC")

weaversa · 2020-06-22T10:29:00Z

Those error messages are pretty rough...The warnings before were pretty concise ---

[warning] at test.cry:5:13--5:14:
  Defaulting type argument 'a' of 'g' to 4

Could we replicate that conciseness somehow?

[error] at test.cry:5:13--5:14:
  Cryptol cannot default type argument 'a' of 'g'.

It also look like, from the error messages, that the defaulting information is still there, so maybe Cryptol could say:

[error] at test.cry:5:13--5:14:
  Cryptol refuses to default type argument 'a' of 'g'. Cryptol was able to infer that a >= 4, but this may be unsafe to automatically apply.

robdockins · 2020-06-22T15:19:50Z

Does this proof still work? I'm pretty sure abc doesn't support Integers, but I'm hoping that since length is a constant, the Integer somehow gets resolved before making its way to smtlib...?
Primitive::Symmetric::Cipher::Block::DES> :s prover=abc
Primitive::Symmetric::Cipher::Block::DES> :prove \k pt -> DES.decrypt k (DES.encrypt k pt) == pt
Q.E.D.
(Total Elapsed Time: 0.730s, using "ABC")

This proof still works. Any concrete integers will get evaluated away during symbolic evaluation, so the solver should never see them.

robdockins · 2020-06-22T15:22:08Z

I agree, the error messages are quite unpleasant.

We might be able to get the best of both worlds here. The logic for doing width defaulting still exists: we could simply compute the same defaulting decisions we used to and report them as errors instead (maybe also have a configuration option to degrade them to warnings, preserving some of the previous behavior).

weaversa · 2020-06-22T15:26:55Z

I agree, the error messages are quite unpleasant.

We might be able to get the best of both worlds here. The logic for doing width defaulting still exists: we could simply compute the same defaulting decisions we used to and report them as errors instead (maybe also have a configuration option to degrade them to warnings, preserving some of the previous behavior).

I'm not too keen on Cryptol specs that rely on configuration options. It's nice to hear the messages can be improved, allowing the user to, in the worst case, just plop in what Cryptol suggests.

robdockins · 2020-06-22T18:02:42Z

Following the plan outlined above, the latest patch computes basically the same defaulting information as before, but issues an error instead of a warning. This gives good improvements to errors, but also converts some examples that would eventually typecheck with ambiguous types into outright failures instead. The specific examples I've seen seem like a strict improvement.

Regarding the two examples above, we now get the following interactions:

Loading module Cryptol
Loading module Primitive::Symmetric::Cipher::Block::Cipher
Loading module Primitive::Symmetric::Cipher::Block::DES
[error] at Primitive/Symmetric/Cipher/Block/DES.cry:13:24--13:27:
  Ambiguous size type: 1st type argument of 'Primitive::Symmetric::Cipher::Block::DES::des'
  Must be at least: 0
[error] at Primitive/Symmetric/Cipher/Block/DES.cry:14:24--14:27:
  Ambiguous size type: 1st type argument of 'Primitive::Symmetric::Cipher::Block::DES::des'
  Must be at least: 0
[error] at Primitive/Symmetric/Cipher/Block/DES.cry:25:40--25:41:
  Ambiguous size type: type wildcard (_)
  Must be at least: max 1 (width ?n`1144)
  where
  ?n`1144 is length of comprehension generator at Primitive/Symmetric/Cipher/Block/DES.cry:22:15--24:35

Here, the first two messages are basically symptoms of the root cause, identified in the third message. We can suppress them by actually doing the defaulting so that later definitions don't encounter unconstrained type variables. This has other side effects, I'm not certain what is the better way to go.

[error] at asdf2.cry:5:13--5:14:
  Ambiguous size type: type argument 'a' of 'Main::g'
  Must be at least: 4
[error] at asdf2.cry:5:29--5:30:
  Ambiguous size type: type argument 'a' of 'Main::g'
  Must be at least: 5
[error] at asdf2.cry:5:50--5:51:
  Ambiguous size type: type argument 'a' of 'Main::g'
  Must be at least: 4
[error] at asdf2.cry:5:61--5:62:
  Ambiguous size type: type argument 'a' of 'Main::g'
  Must be at least: 4

These messages are way more readable than the previous ones.

robdockins · 2020-06-22T18:23:21Z

If we actually apply the computed defaulting when typechecking dependent definitions, the error messages for the modified DES become:

Loading module Cryptol
Loading module Primitive::Symmetric::Cipher::Block::Cipher
Loading module Primitive::Symmetric::Cipher::Block::DES
[error] at Primitive/Symmetric/Cipher/Block/DES.cry:25:40--25:41:
  Ambiguous size type: type wildcard (_)
  Must be at least: max 1 (width ?n`1144)
  where
  ?n`1144 is length of comprehension generator at Primitive/Symmetric/Cipher/Block/DES.cry:22:15--24:35

I think doing this is probably a net positive.

src/Cryptol/REPL/Command.hs

tests/issues/issue268.cry

brianhuffman · 2020-06-22T18:40:05Z

Concerning the Ambiguous size type error message: Are we using the name "size type" anywhere in the Cryptol book, or is "numeric type" the preferred term? We should try to be consistent.

robdockins · 2020-06-22T18:45:14Z

A quick grep shows that both terms occur, but "numeric type" is much more prevalent. We should probably just stick to that.

src/Cryptol/TypeCheck/Default.hs

Instead of defaulting to `[n]` for some `n`, prefer instead to default to `Integer` or `Rational` depending on the other required constraints.

Fix up the test suite. This mostly delays defaulting warnings into "showing specific instance of polymorpic type warnings", but requires actual fixes in a small number of places. Those places were higly questionable, in my opinion.

Now that we only default to unlimited-precision types, this warning is considerably less useful.

use that information to emit error messages rather than warnings. This provides more specific messages than simply allowing the affected type variables to remain uninstantiated and failing later. It also causes some examples that otherwise would have ambiguous types to fail earlier. This converts some test instances where REPL defaulting would eventually succeed into examples that fail outright instead. I largely think these instances are improvements.

rest of a module. This helps prevent a single ambiguous size variable from causing additional errors in other definition.

This used to look for decimal literals applied to specific primitive operations and cause them to silently default to bitvector types large enough to hold their values. With the new literal defaulting system, this special case is no longer necessary.

robdockins · 2020-07-02T22:30:52Z

It is my understanding that we're now in agreement about this strategy, and I believe this code is ready to merge. Let me know if there are additional issues to discuss before I merge.

yav · 2020-07-02T22:35:38Z

I think its fine to merge it

…w4`. PR GaloisInc/cryptol#774 changed cryptol's defaulting rules in such a way that some indexing operators in `test_w4` are assigned different types. PR GaloisInc/saw-core#61 was then necessary to avoid a panic; also the out-of-bounds indexing tests have changed from expected proof success to expected proof failure.

robdockins requested review from yav, atomb and brianhuffman June 21, 2020 00:37

robdockins commented Jun 21, 2020

View reviewed changes

atomb reviewed Jun 22, 2020

View reviewed changes

src/Cryptol/REPL/Command.hs Outdated Show resolved Hide resolved

tests/issues/issue268.cry Show resolved Hide resolved

robdockins mentioned this pull request Jun 23, 2020

Rework defaulting #730

Closed

robdockins marked this pull request as ready for review June 24, 2020 00:13

robdockins force-pushed the defaulting branch from 6899d7a to 2e59a1e Compare June 30, 2020 22:56

yav reviewed Jun 30, 2020

View reviewed changes

src/Cryptol/TypeCheck/Default.hs Outdated Show resolved Hide resolved

robdockins added 4 commits July 2, 2020 14:56

Change the defaulting rules for Literal constraints.

709dc93

Instead of defaulting to `[n]` for some `n`, prefer instead to default to `Integer` or `Rational` depending on the other required constraints.

Remove all defaulting, except for literals.

620e62c

Fix up the test suite. This mostly delays defaulting warnings into "showing specific instance of polymorpic type warnings", but requires actual fixes in a small number of places. Those places were higly questionable, in my opinion.

Change the default so that defaulting warnings are suppressed.

7cd5e7b

Now that we only default to unlimited-precision types, this warning is considerably less useful.

robdockins added 5 commits July 2, 2020 15:04

Tenatively apply defaulting to definitions when typechecking the

84e1a06

rest of a module. This helps prevent a single ambiguous size variable from causing additional errors in other definition.

style fixes

c2d053e

Fixup test suite

ac3676d

Correct the commend describing how literal defaulting works.

a0b4e26

robdockins force-pushed the defaulting branch from 66093b8 to a0b4e26 Compare July 2, 2020 22:06

robdockins merged commit 1dbafa5 into master Jul 2, 2020

brianhuffman mentioned this pull request Jul 29, 2020

Update for Cryptol that takes file reading procedure as a parameter GaloisInc/saw-script#761

Merged

RyanGlScott deleted the defaulting branch March 22, 2024 14:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Defaulting #774

Defaulting #774

robdockins commented Jun 21, 2020

robdockins Jun 21, 2020

robdockins Jun 21, 2020

weaversa commented Jun 21, 2020

robdockins commented Jun 21, 2020

weaversa commented Jun 21, 2020 •

edited

Loading

weaversa commented Jun 21, 2020

robdockins commented Jun 22, 2020

robdockins commented Jun 22, 2020

robdockins commented Jun 22, 2020

weaversa commented Jun 22, 2020

weaversa commented Jun 22, 2020

robdockins commented Jun 22, 2020

robdockins commented Jun 22, 2020

weaversa commented Jun 22, 2020

robdockins commented Jun 22, 2020

robdockins commented Jun 22, 2020

brianhuffman commented Jun 22, 2020

robdockins commented Jun 22, 2020

robdockins commented Jul 2, 2020

yav commented Jul 2, 2020

Defaulting #774

Defaulting #774

Conversation

robdockins commented Jun 21, 2020

robdockins Jun 21, 2020

Choose a reason for hiding this comment

robdockins Jun 21, 2020

Choose a reason for hiding this comment

weaversa commented Jun 21, 2020

robdockins commented Jun 21, 2020

weaversa commented Jun 21, 2020 • edited Loading

weaversa commented Jun 21, 2020

robdockins commented Jun 22, 2020

robdockins commented Jun 22, 2020

robdockins commented Jun 22, 2020

weaversa commented Jun 22, 2020

weaversa commented Jun 22, 2020

robdockins commented Jun 22, 2020

robdockins commented Jun 22, 2020

weaversa commented Jun 22, 2020

robdockins commented Jun 22, 2020

robdockins commented Jun 22, 2020

brianhuffman commented Jun 22, 2020

robdockins commented Jun 22, 2020

robdockins commented Jul 2, 2020

yav commented Jul 2, 2020

weaversa commented Jun 21, 2020 •

edited

Loading