Support :let in the Cryptol REPL?

dylanmc commented 10 years ago

It would be nice to be able to define new symbols at the REPL, like this:

:let timesTwo x = x * 2
:let double x = x + x
:prove \x = timesTwo x == double x

Yes, this could be done with lots of lambdas, but the above would be very helpful.

LeventErkok commented 10 years ago

Cryptol-1 used to support this; but scoping was always an issue. In particular, if the defined name is already in scope, then do you still accept it? Cryptol-1 used to warn but otherwise override the old definition. Same thing for "type" definitions as well.

kiniry commented 10 years ago

The proposal is to not extend the semantics at all; only permit the binding of new names and not perform any overriding.

acfoltzer commented 10 years ago

Added in ceb084c, but as just let rather than :let:

Cryptol> let f x = x + 2
Cryptol> let g x = f x + 1
Cryptol> g 5 : [32]
8
Cryptol> let f x = 0
Cryptol> g 5 : [32]
8

Let bindings disappear when changing module contexts, eg using :load, :reload, and :edit.

The biggest limitation is that we don't syntactically support multiple bindings at once, so you won't be able to write mutually-recursive definitions with let. However, this would probably be too big for one line anyway.

We could probably extend this to adding type synonyms at the REPL, but should open a new ticket for that if the need arises.

weaversa commented 10 years ago

This is wild. It actually works the other way in the old Cryptol. I had no idea… Actually, your example gives an error "BitModel.lit: Literal has unresolvable type: $6”, but one can easily fix it to see the behavior differ between versions.

I don’t know personally what I’d prefer the behavior to be. I’m sure this is one reason Levent was hesitant to reveal :let to us so many years ago...

On Aug 19, 2014, at 8:32 PM, Adam C. Foltzer notifications@github.com wrote:

Added in ceb084c, but as just let rather than :let:

Cryptol> let f x = x + 2 Cryptol> let g x = f x + 1 Cryptol> g 5 : [32] 8 Cryptol> let f x = 0 Cryptol> g 5 : [32] 8 Let bindings disappear when changing module contexts, eg using :load, :reload, and :edit.

The biggest limitation is that we don't syntactically support multiple bindings at once, so you won't be able to write mutually-recursive definitions with let. However, this would probably be too big for one line anyway.

We could probably extend this to adding type synonyms at the REPL, but should open a new ticket for that if the need arises.

— Reply to this email directly or view it on GitHub.

acfoltzer commented 10 years ago

This is wild. It actually works the other way in the old Cryptol. I had no idea… Actually, your example gives an error "BitModel.lit: Literal has unresolvable type: $6”, but one can easily fix it to see the behavior differ between versions.

I don’t know personally what I’d prefer the behavior to be. I’m sure this is one reason Levent was hesitant to reveal :let to us so many years ago...

Yep, :let in Cryptol 1 is broken, and this example is chosen to show how. Introducing a new binding for f shouldn’t change the behavior of g in a language with proper lexical scope. The old behavior is dynamic scope, which is widely agreed to be a Bad Idea and confusing semantically.

This all comes down to names and how to produce fresh names out of the ether. Essentially you want the first f to be distinct from the second f, but in Cryptol 1 there was no easy way to introduce unique names while keeping them hidden from the user. Now we’ve got the capability, so we can implement a proper let and the it variable.

On Aug 19, 2014, at 8:32 PM, Adam C. Foltzer notifications@github.com wrote:

Added in ceb084c, but as just let rather than :let:

Cryptol> let f x = x + 2 Cryptol> let g x = f x + 1 Cryptol> g 5 : [32] 8 Cryptol> let f x = 0 Cryptol> g 5 : [32] 8 Let bindings disappear when changing module contexts, eg using :load, :reload, and :edit.

The biggest limitation is that we don't syntactically support multiple bindings at once, so you won't be able to write mutually-recursive definitions with let. However, this would probably be too big for one line anyway.

We could probably extend this to adding type synonyms at the REPL, but should open a new ticket for that if the need arises.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.

weaversa commented 10 years ago

But, now it seems to be the case that let bindings can't make use of expressions that even mention 'undefined'. This doesn't seem proper :-)

Cryptol> 0 where y = undefined 0 Cryptol> let x = 0 where y = undefined

[error] unbound symbol: (at :1:21--1:30, undefined)

On Wed, Aug 20, 2014 at 12:56 PM, Adam C. Foltzer notifications@github.com wrote:

This is wild. It actually works the other way in the old Cryptol. I had no idea… Actually, your example gives an error "BitModel.lit: Literal has unresolvable type: $6”, but one can easily fix it to see the behavior differ between versions.

I don’t know personally what I’d prefer the behavior to be. I’m sure this is one reason Levent was hesitant to reveal :let to us so many years ago...

Yep, :let in Cryptol 1 is broken, and this example is chosen to show how. Introducing a new binding for f shouldn’t change the behavior of g in a language with proper lexical scope. The old behavior is dynamic scope, which is widely agreed to be a Bad Idea and confusing semantically.

This all comes down to names and how to produce fresh names out of the ether. Essentially you want the first f to be distinct from the second f, but in Cryptol 1 there was no easy way to introduce unique names while keeping them hidden from the user. Now we’ve got the capability, so we can implement a proper let and the it variable.

On Aug 19, 2014, at 8:32 PM, Adam C. Foltzer notifications@github.com wrote:

Added in ceb084c, but as just let rather than :let:

Cryptol> let f x = x + 2 Cryptol> let g x = f x + 1 Cryptol> g 5 : [32] 8 Cryptol> let f x = 0 Cryptol> g 5 : [32] 8 Let bindings disappear when changing module contexts, eg using :load, :reload, and :edit.

The biggest limitation is that we don't syntactically support multiple bindings at once, so you won't be able to write mutually-recursive definitions with let. However, this would probably be too big for one line anyway.

We could probably extend this to adding type synonyms at the REPL, but should open a new ticket for that if the need arises.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/6#issuecomment-52807760.

acfoltzer commented 10 years ago

On Aug 20, 2014, at 10:03 AM, weaversa notifications@github.com wrote:

But, now it seems to be the case that let bindings can't make use of expressions that even mention 'undefined'. This doesn't seem proper :-)

Cryptol> 0 where y = undefined 0 Cryptol> let x = 0 where y = undefined

[error] unbound symbol: (at :1:21--1:30, undefined)

Oh, indeed, this is a bug: names from the prelude aren’t in scope in the body of the let somehow:

Cryptol> let f x = tail x

[error] unbound symbol: (at <interactive>:1:11--1:15, tail)

I’ll get working on this.

weaversa commented 10 years ago

I'm also a little confused about why 'let' isn't ':let' and how that's different than the colon needed in sat, prove, set, etc.

On Wed, Aug 20, 2014 at 1:07 PM, Adam C. Foltzer notifications@github.com wrote:

On Aug 20, 2014, at 10:03 AM, weaversa notifications@github.com wrote:

But, now it seems to be the case that let bindings can't make use of expressions that even mention 'undefined'. This doesn't seem proper :-)

Cryptol> 0 where y = undefined 0 Cryptol> let x = 0 where y = undefined

[error] unbound symbol: (at :1:21--1:30, undefined)

Oh, indeed, this is a bug: names from the prelude aren’t in scope in the body of the let somehow:

Cryptol> let f x = tail x

[error] unbound symbol: (at :1:11--1:15, tail)

I’ll get working on this.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/6#issuecomment-52809116.

acfoltzer commented 10 years ago

There are two reasons:

When it's :let, it clashes with :load, meaning that you can no longer do :l Somefile.cry, which would require a bunch of fixes in the documentation.
The bare let is more like ghci, which makes it more intuitive to folks coming to Cryptol from Haskell.

The main reason is 1, but us nerds appreciate 2 as well.

weaversa commented 10 years ago

It always annoys me when :set clashes with :sat

On Wed, Aug 20, 2014 at 1:18 PM, Adam C. Foltzer notifications@github.com wrote:

There are two reasons:

When it's :let, it clashes with :load, meaning that you can no longer do :l Somefile.cry, which would require a bunch of fixes in the documentation.

The bare let is more like ghci, which makes it more intuitive to folks coming to Cryptol from Haskell.

The main reason is 1, but us nerds appreciate 2 as well.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/6#issuecomment-52810638.

acfoltzer commented 10 years ago

As of 46bcc18, let x = 0 where y = undefined now works. Thanks for the report!

neshat1 commented 9 years ago

I am new in cryptol!! everything write it gives me this error: unbound symbol: (at :1:1--1:5, load)

plz helpme

weaversa commented 9 years ago

What happens when you type this?

Cryptol> 1 + 1

neshat1 commented 9 years ago

Cryptol> 1 + 1 Assuming a = 1 0x0 Cryptol>

 On Wednesday, February 4, 2015 4:37 PM, weaversa <notifications@github.com> wrote:

What happens when you type this?Cryptol> 1 + 1 — Reply to this email directly or view it on GitHub.

weaversa commented 9 years ago

Great! Now, create a file called test.cry and place this text into it:

f x = x + 1

Then, in the same directory as test.cry, start Cryptol and type:

Cryptol> :load test.cry

Don't forget to type the colon! Then, type:

Cryptol> f 2

What happens for those commands?

neshat1 commented 9 years ago

HIi,I have done the works you told me. but here is my problem:I want to run your DES.cry and testDES.cry example and I want to see the results.what are the exact steps that I should take??bestsNeshat

 On Wednesday, February 4, 2015 4:49 PM, weaversa <notifications@github.com> wrote:

Great! Now, create a file called test.cry and place this text into it:f x = x + 1 Then, in the same directory as test.cry, start Cryptol and type:Cryptol> :load test.cry Don't forget to type the colon! Then, type:Cryptol> f 2 What happens for those commands?— Reply to this email directly or view it on GitHub.

weaversa commented 9 years ago

Here is a transcript of me running the DES example.

[cryptol]$ cd examples/
[examples]$ ls
ChaChaPolyCryptolIETF.md DEStest.cry              Salsa20.cry              ZUC.cry                  maliciousSHA
Cipher.cry               FNV-a1.cry               Test.cry                 contrib
DES.cry                  SHA1.cry                 TripleDES.cry            funstuff
[examples]$ cryptol
                        _        _
   ___ _ __ _   _ _ __ | |_ ___ | |
  / __| '__| | | | '_ \| __/ _ \| |
 | (__| |  | |_| | |_) | || (_) | |
  \___|_|   \__, | .__/ \__\___/|_|
            |___/|_| version 2.1.0 (a15fb75)

Loading module Cryptol
Cryptol> :load DES.cry
Loading module Cryptol
Loading module Cipher
Loading module DES
[warning] at DES.cry:1:1--171:10:
  Defaulting type parameter 'bits'
             of literal or demoted expression
             at DES.cry:25:35--25:36
  to max 1 (width ?v38)
  where
  ?v38 is sequence length of comprehension match
DES> DES.encrypt 30482039 0
0x7281f9dd58575f3a
DES> DES.decrypt 30482039 0x7281f9dd58575f3a
0x0000000000000000
DES> :q
[examples]$

neshat1 commented 9 years ago

thank you so muchhhhh is there any C code as cryptol output?? bestsNeshat

 On Saturday, February 7, 2015 4:42 PM, weaversa <notifications@github.com> wrote:

Here is a transcript of me running the DES example.[cryptol]$ cd examples/ [examples]$ ls ChaChaPolyCryptolIETF.md DEStest.cry Salsa20.cry ZUC.cry maliciousSHA Cipher.cry FNV-a1.cry Test.cry contrib DES.cry SHA1.cry TripleDES.cry funstuff [examples]$ cryptol _ | | | | / | '| | | | ' | **/ | | | (| | | || | |) | || (_) | | || , | ./ ****/|| |**/|| version 2.1.0 (a15fb75)

Loading module Cryptol Cryptol> :load DES.cry Loading module Cryptol Loading module Cipher Loading module DES [warning] at DES.cry:1:1--171:10: Defaulting type parameter 'bits' of literal or demoted expression at DES.cry:25:35--25:36 to max 1 (width ?v38) where ?v38 is sequence length of comprehension match DES> DES.encrypt 30482039 0 0x7281f9dd58575f3a DES> DES.decrypt 30482039 0x7281f9dd58575f3a 0x0000000000000000 DES> :q [examples]$ — Reply to this email directly or view it on GitHub.

weaversa commented 9 years ago

There used to be a way to translate Cryptol specifications to C, but I don't think that feature has been reimplemented. Though, the path is clear as SBV can translate it's internal representation to C, and Cryptol already uses SBV for theorem proving. This feature will likely be added someday.

neshat1 commented 9 years ago

Hi!I have another problem.I want to install Cryptol by source.i have installed Hasell and Cabal.but every time i want to make Cryptol, this error occurs : cabal: unrecognised command: sandbox (try --help)what is sandbox?? how can solve this?Regards

 On Saturday, February 7, 2015 9:01 PM, weaversa <notifications@github.com> wrote:

There used to be a way to translate Cryptol specifications to C, but I don't think that feature has been reimplemented. Though, the path is clear as SBV can translate it's internal representation to C, and Cryptol already uses SBV for theorem proving. This feature will likely be added someday.— Reply to this email directly or view it on GitHub.

neshat1 commented 9 years ago

I know my version is 1.14i use cabal update and then cabal install Cabal cabal-install but again my version is still 1.14 and i know that sandboxes are added in version 1.18 what should I do now? Regards

 On Monday, February 16, 2015 11:44 AM, Neshat Korivand <neshatkorivand@yahoo.com> wrote:

Hi!I have another problem.I want to install Cryptol by source.i have installed Hasell and Cabal.but every time i want to make Cryptol, this error occurs : cabal: unrecognised command: sandbox (try --help)what is sandbox?? how can solve this?Regards

 On Saturday, February 7, 2015 9:01 PM, weaversa <notifications@github.com> wrote:

There used to be a way to translate Cryptol specifications to C, but I don't think that feature has been reimplemented. Though, the path is clear as SBV can translate it's internal representation to C, and Cryptol already uses SBV for theorem proving. This feature will likely be added someday.— Reply to this email directly or view it on GitHub.

dylanmc commented 9 years ago

Probably the easiest thing to do is start with the current "Haskell Platform" installation of Haskell. We should update the web page, because the current Haskell Platform includes a sandbox version of cabal.

TomMD commented 9 years ago

@neshat1 If you did cabal update && cabal install Cabal cabal-install then you do have the most recent cabal installed, but it might not be in your PATH.

So you need to either call the new cabal-install directly (instead of the old one indirectly) or update your path to include your cabal/bin directory before the others. How you update your path and where cabal/bin is varies by operating system.

neshat1 commented 9 years ago

how can I call the new cabal-install directly??sry I am kind of new in linux. so if you help me with this i will appreciate that.

 On Monday, February 16, 2015 6:39 PM, Thomas M. DuBuisson <notifications@github.com> wrote:

@neshat1 If you did cabal update && cabal install Cabal cabal-install then you do have the most recent cabal installed, but it might not be in your PATH.So you need to either call the new cabal-install directly (instead of the old one indirectly) or update your path to include your cabal/bin directory. How you update your path and where cabal/bin is varies by operating system.— Reply to this email directly or view it on GitHub.

dylanmc commented 9 years ago

You'll be well-served by learning Linux basics. The part you need at this point is to understand how the PATH environment variable sets what commands are available to you. As Tom points out, this varies from OS to OS, and from Linux distribution to Linux distribution. Just guessing you're on Ubuntu, here is a tutorial. If not, google is your friend.

The high-level steps you'll need to complete:

editing files (vim, emacs, or whatever you choose)
figuring out which "shell" you're using (likely it's bash)
editing your shell's init/configuration to modify your PATH environment variable (if bash, either .profile or .bashrc)
adding your cabal/bin directory (where the new "cabal" executable is) to your PATH

At this point, you'll be well along your way.

neshat1 commented 9 years ago

i finally could update my cabal to 1.22.1.0 now when i want to make run my cryptol i get this : cabal install -j --only-dependencies Resolving dependencies... cabal: Could not resolve dependencies: trying: MonadRandom-0.3.0.1/installed-8c9... (user goal) next goal: cryptol (user goal) rejecting: cryptol-2.1.0 (conflict: MonadRandom => base==4.5.0.0/installed-40b..., cryptol => base>=4.6) Dependency tree exhaustively searched.

Note: when using a sandbox, all packages are required to have consistent dependencies. Try reinstalling/unregistering the offending packages or recreating the sandbox. make: *\ [dist/setup-config] Error 1

please help me!

 On Tuesday, February 17, 2015 10:23 AM, Dylan McNamee <notifications@github.com> wrote:

You'll be well-served by learning Linux basics. The part you need at this point is to understand how the PATH environment variable sets what commands are available to you. As Tom points out, this varies from OS to OS, and from Linux distribution to Linux distribution. Just guessing you're on Ubuntu, here is a good tutorial. If not, google is your friend.The high-level steps you'll need to complete:

editing files (vim, emacs, or whatever you choose)
figuring out which "shell" you're using (likely it's bash)
editing your shell's init/configuration to modify your PATH environment variable (if bash, either .profile or .bashrc)
adding your cabal/bin directory (where the new "cabal" executable is) to your PATH At this point, you'll be well along your way.— Reply to this email directly or view it on GitHub.

acfoltzer commented 9 years ago

@neshat1 it sounds like you have incorrect versions of other packages installed, probably left over from using a version of cabal without sandboxes. I recommend deleting your $HOME/.cabal and $HOME/.ghc directories, making sure you have a new version of cabal (1.18 or greater), and trying again.

Most of what you're running into now is not specific to Cryptol, but is part of the process of getting a proper set of Haskell build tools going. I recommend checking out Stephen Diehl's page introducing the basics of Cabal: http://dev.stephendiehl.com/hask/#cabal. If you're still getting stuck with GHC or cabal errors, try asking on the Haskell StackOverflow tag or one of the other venues listed on the Haskell Community page.

If you run into another issue once you get Cryptol going, feel free to open a new issue here or to mail the cryptol-users mailing list. I'm going to go ahead and close this issue now, as this isn't about the original topic.

GaloisInc / cryptol

Support :let in the Cryptol REPL? #6