Lab listing

[weaversa]

I suggest creating a listing of the desired labs, then we can divvy up the work.

[weaversa]

Ideas so far are:

• Overview of Cryptol
• Installing the Tools (done)
• Interpreter (done)
• Working with files
  • Load, reload, editing
  • Syntax highlighting
  • Mention Cryptol Emacs mode
• Language Basics - in progress
• Wrap/Tag Example
• Properties (SAT/Prove)
  • We have a bunch of Project Euler examples
• Simple Crypto (XOR, Ceasar)
• Salsa20
• CRC
• Capstone - in progress
• Speck
• xxHash
• Parameterized SHA
• Parameterized Z-type ECDSA
• Remote Cryptol API

This doesn't touch on SAW. Perhaps we focus on Cryptol first, and when that looks good we try saw.

[weaversa]

I updated the list above to reflect work done and added an overview

[weaversa]

How do you feel about a lab on common errors? A kind of guide to help people understand the incomprehensible gibberish spewed at them by the interpreter. For example, how to know that all the errors below stem me forgetting an -> in a function definition. Though, I guess we could start simpler...

[error] at Salsa20.md:1:1--332:18:
  Type '[8][16][8]' does not support literals.
[error] at Salsa20.md:296:1--304:32:
  Type mismatch:
    Expected type: [64][8]
    Inferred type: [?front`1778][8] -> [64][8]
  where
  ?front`1778 is type argument 'front' of '(Cryptol::#)' at Salsa20.md:301:14--301:45
[error] at Salsa20.md:301:14--301:45:
  Type mismatch:
    Expected type: Bit
    Inferred type: [16][8]
[error] at Salsa20.md:302:14--302:45:
  Type mismatch:
    Expected type: Bit
    Inferred type: [16][8]
[error] at Salsa20.md:310:6--310:23:
  Type mismatch:
    Expected type: [16][7] -> [64][8]
    Inferred type: [64][8]
[error] at Salsa20.md:315:6--315:23:
  Type mismatch:
    Expected type: [16][7] -> [64][8]
    Inferred type: [64][8]
[error] at Salsa20.md:329:1--332:18:
  Failed to infer the following types:
    • ?each`1865, type argument 'each' of 'Cryptol::join' at Salsa20.md:331:19--331:23
  while validating user-specified signature
    in the definition of 'labs::Salsa20::Salsa20::Salsa20_encrypt', at Salsa20.md:329:1--329:16,
    we need to show that
      for any type a, l
      assuming
        • a >= 1
        • 2 >= a
        • l <= 2 ^^ 70
      the following constraints hold:
        • fin ?each`1865
            arising from
            use of expression Cryptol::join
            at Salsa20.md:331:19--331:23
        • inf * ?each`1865 >= l
            arising from
            matching types
            at Salsa20.md:331:19--331:23
[error] at Salsa20.md:331:26--331:43:
  Type mismatch:
    Expected type: [8 + ?parts`1886][8] -> [?each`1865][8]
    Inferred type: [64][8]
  where
  ?each`1865 is type argument 'each' of 'Cryptol::join' at Salsa20.md:331:19--331:23
  ?parts`1886 is type argument 'parts' of 'Cryptol::split' at Salsa20.md:331:61--331:66
[error] at Salsa20.md:331:44--331:45:
  Type mismatch:
    Expected type: [16][8]
    Inferred type: Bit

[jdwoolc]

I really like working through common errors as a lab. I think making sense of the output and building a sensible development loop is very important. I plan on taking a closer look at the interpreter lab you built and may take a stab at starting the files lab tomorrow.

[weaversa]

That would be wonderful!

Here's an idea --- make a literate markdown specification that's full of common errors and have the exercises be to correct them. See the Salsa20 branch for how to do literate markdown.

[weaversa]

@jpziegler Any ideas for the listing above?

Also, if you want to pick a lab to start/tackle, go ahead.

[weaversa]

@WeeknightMVP What if we had a lab on functional programming -- introduce map, fold, compose, and just the notion of programming from the standpoint of Cryptol? We could reintroduce some of the functions cut from the salsa20props lab.