recent changes

src/PARADOXES_FOUNDATIONS_COMPUTABILITY.md

@@ -24,4 +24,7 @@ In other words, Hilbert sought for a foundation that was:
 3. Decidability: There should be an algorithm for deciding the truth or falsity
 of any math statement.
 
-(TODO: Godel Incompleteness, then Turing and Church takes defining computability and algorithms)
+(TODO: Godel Incompleteness, then Turing and Church takes defining computability and algorithms)
+
+****
+### Uncompiled

src/SUMMARY.md

@@ -11,9 +11,14 @@
   - [PAT]()
   - [Logic <-> Type Theories]()
 - [SMT Solvers]()
-  - [Interfacing solvers with SAT](./interfacing_solvers_with_sat.md) 
+  - [Theory and Implementation](./smt_theory_and_implementation.md)
+
 
 - [Verified Rust with Verus]()
   - [Verus Fundamentals](./verus_fundamentals.md)
   - [Borrow Checker, Linear Types]()
-  - [Case Study: Verified Parsers](./verified_parsers.md)
+  - [Case Study: Verified Parsers](./verified_parsers.md)
+
+- [Verifying Cryptography]()
+  - [Crypto Fundamentals]()
+  - [Cryptol and SAW](./cryptol_and_saw.md)

src/cryptol_and_saw.md

@@ -0,0 +1,46 @@
+# Cryptol and SAW
+
+Cryptol is very Haskell-like, from the syntax to the type system, and even to the REPL.
+Since Cryptol is a crypto DSL, it accustoms to the low-level, providing types such as bit-width. Let's play with the REPL:
+
+```bash
+# prints with base=16 by default
+Cryptol> 0b101
+0x5
+Cryptol> :t 0b101 # :t or :type
+0xabc : [3]
+Cryptol> :t 0xabc
+0xabc : [12]
+Cryptol> :t 100
+100 : {a} (Literal 100 a) => a
+Cryptol> 100 : [6]
+
+[error] at <interactive>:31:1--31:4:
+  • Unsolvable constraint:
+      6 >= 7
+        arising from
+        use of literal or demoted expression
+        at <interactive>:31:1--31:4
+Cryptol> 100 : [7]
+0x64
+```
+
+The `[n]` is a type that informs us the number of bits a word is represented with.
+Numbers such as `0b101`, `0xabc`, and `100` are all words.
+`0xabc : [12]` because each hexadecimal requires 4 bits to store. 
+Prompting the REPL with the value `100 : [6]` (explicitly annotated type)
+gives an unsolvable constraint because the decimal 100 can't be represented in 6 bits.
+
+The only unexpected output is `:t 100`. What the hell is `100 : {a} (Literal 100 a) => a`?
+Essentially, this is an uninferred type. The reason Cryptol cannot infer `100 : [7]` is
+that Cryptol does not perform real arithmetic during type inference. Thus, since decimal 
+digit require anywhere from 1 to 4 bits to represent, Cryptol does not give 100 a concrete type.
+Conversely, the number of bits used to represented binaries and hexadecimals are evident at
+the syntax level.
+
+
+
+
+0101
+
+1010

src/interfacing_solvers_with_sat.md → src/smt_theory_and_implementation.md

@@ -1,4 +1,9 @@
-# Interfacing Solvers with SAT
+# SMT Theory and Implementation
+
+## Blob
+asdf
+
+## Interfacing Solvers with SAT
 
 
 ### Keywords

src/verus_fundamentals.md

@@ -33,9 +33,14 @@ int vs usize
 Seq, Set, Map 
 
 
-## Three(?) ways to deal with Recursion
+## Dealing with Recursion
+Say `f_spec` is recursive but the executable `f` is imperative. How to verify that `f`
+adheres to `f_spec`?
 
+Hoare logic; loop invariants.
 ### Induction
+You probably want to write a `f_induct` that ensures the inductive case.
+After which, the main proof won't be too far away.
 
 
 ## Limitations: How to Fail Something True