structure for everything

src/SUMMARY.md

@@ -1,30 +1,40 @@
 # Summary
-[Introduction]()
-- [Foundations](./foundation.md)
-  - [Glossary]()
-  - [Paradoxes]()
-  - [Incompleteness, Undecidability, Inconsistency]()
-  - [Computability and Lambda Calculus]()
-  - [Propositions as Types: The First Correspondence]()
-  - [Church Encodings]()
-  - [Lambda Cube]()
-  - [Propositions as Types: More Incarnations]()
-    - [System F and the Polymorphic Lambda Calculus]()
-    - [Modal Logic and Monads]()
-  - [HoTT]()
-- [Modern Dependently Typed Languages]()
-  - [Idris](./idris.md)
-- [SMT Solvers]()
-  - [Theory and Implementation](./smt_theory_and_implementation.md)
-  - [Symbolic Execution]()
 
+[Introduction](./introduction.md)
+[Glossary, Resources](./glossary_resources.md)
 
-- [Verified Rust with Verus]()
-  - [Verus Fundamentals](./verus_fundamentals.md)
-  - [Borrow Checker, Linear Types]()
-  - [Case Study: Verified Parsers](./verified_parsers.md)
+- [Foundations](./foundations/front.md)
+  - [Paradoxes](./foundations/paradoxes/front.md)
+  - [Incompleteness, Undecidability, Inconsistency](./foundations/incompleteness_undecidability_inconsistency/front.md)
+  - [Computability and Lambda Calculus](./foundations/computability_and_lambda_calculus/front.md)
+  - [Propositions as Types: The First Correspondence](./foundations/propositions_as_types/front.md)
+  - [Church Encodings](./foundations/church_encodings/front.md)
+  - [Lambda Cube](./foundations/lambda_cube/front.md)
+  - [Propositions as Types: More Incarnations](./foundations/propositions_as_types_more/front.md)
+    - [System F and the Polymorphic Lambda Calculus](./foundations/propositions_as_types_more/system_f/front.md)
+    - [Modal Logic and Monads](./foundations/propositions_as_types_more/modal_logic_and_monads/front.md)
+  - [HoTT](./foundations/hott/front.md)
 
-- [Verifying Cryptography]()
-  - [Cryptol for Haskell Knowers](./cryptol_for_haskell_devs.md)
-  - [Cryptol for Anyone](./cryptol_for_anyone.md)
-  - [Cryptol + Saw]()
+- [Dependently Typed Languages](./dependently_typed_languages/front.md)
+  - [Idris](./dependently_typed_languages/idris/front.md)
+  - [Coq](./dependently_typed_languages/coq/front.md)
+  - [Lean](./dependently_typed_languages/lean/front.md)
+  - [Agda](./dependently_typed_languages/agda/front.md)
+  - [Isabelle/HOL](./dependently_typed_languages/isabelle_hol/front.md)
+  - [F*](./dependently_typed_languages/fstar/front.md)
+
+- [SMT Solvers](./smt_solvers/front.md)
+  - [Theory and Implementation](./smt_solvers/theory_and_implementation/front.md)
+
+- [Model Checking](./model_checking/front.md)
+
+- [Full Applications](./full_applications/front.md)
+  - [Verifying Rust with Verus](./full_applications/verifying_rust_with_verus/front.md)
+    - [Verus Fundamentals](./full_applications/verifying_rust_with_verus/verus_fundamentals/front.md)
+    - [Borrow Checker, Linear Types](./full_applications/verifying_rust_with_verus/borrow_checker_linear_types/front.md)
+    - [Case Study: Verified Parsers](./full_applications/verifying_rust_with_verus/case_study_verified_parsers/front.md)
+  - [Verified Cryptography](./full_applications/verified_cryptography/front.md)
+    - [Cryptol for Haskell Knowers](./full_applications/verified_cryptography/cryptol_for_haskell_knowers/front.md)
+    - [Cryptol for Anyone](./full_applications/verified_cryptography/cryptol_for_anyone/front.md)
+    - [Cryptol + Saw](./full_applications/verified_cryptography/cryptol_and_saw/front.md)
+  - [Verified Hardware with SystemVerilog](./full_applications/verified_hardware_with_systemverilog/front.md)

src/dependently_typed_languages/agda/front.md

@@ -0,0 +1 @@
+# Agda

src/dependently_typed_languages/coq/front.md

@@ -0,0 +1 @@
+# Coq

src/dependently_typed_languages/front.md

@@ -0,0 +1 @@
+# Dependently_Typed_Languages

src/dependently_typed_languages/fstar/front.md

@@ -0,0 +1 @@
+# FStar

src/dependently_typed_languages/isabelle_hol/front.md

@@ -0,0 +1 @@
+# Isabelle_HOL

src/dependently_typed_languages/lean/front.md

@@ -0,0 +1 @@
+# Lean

src/foundations/church_encodings/front.md

@@ -0,0 +1 @@
+# Church_Encodings

src/foundations/computability_and_lambda_calculus/front.md

@@ -0,0 +1 @@
+# Computability_And_Lambda_Calculus

src/foundations/hott/front.md

@@ -0,0 +1 @@
+# HoTT

src/foundations/incompleteness_undecidability_inconsistency/front.md

@@ -0,0 +1 @@
+# Incompleteness_Undecidability_Inconsistency

src/foundations/lambda_cube/front.md

@@ -0,0 +1 @@
+# Lambda_Cube

src/foundations/paradoxes/front.md

@@ -0,0 +1 @@
+# Paradoxes

src/foundations/propositions_as_types/front.md

@@ -0,0 +1 @@
+# Propositions_As_Types

src/foundations/propositions_as_types_more/front.md

@@ -0,0 +1 @@
+# Propositions_As_Types_More

src/foundations/propositions_as_types_more/modal_logic_and_monads/front.md

@@ -0,0 +1 @@
+# Modal_Logic_And_Monads

src/foundations/propositions_as_types_more/system_f/front.md

@@ -0,0 +1 @@
+# System_F

src/full_applications/front.md

@@ -0,0 +1 @@
+# Full_Applications

src/full_applications/verified_cryptography/cryptol_and_saw/front.md

@@ -0,0 +1 @@
+# Cryptol_And_Saw

src/full_applications/verified_cryptography/front.md

@@ -0,0 +1 @@
+# Verified_Cryptography

src/full_applications/verified_hardware_with_systemverilog/front.md

@@ -0,0 +1 @@
+# Verified_Hardware_With_SystemVerilog

src/full_applications/verifying_rust_with_verus/borrow_checker_linear_types/front.md

@@ -0,0 +1 @@
+# Borrow_Checker_Linear_Types

src/full_applications/verifying_rust_with_verus/front.md

@@ -0,0 +1 @@
+# Verifying_Rust_With_Verus

src/introduction.md

@@ -0,0 +1 @@
+# Journey Through Formal Verifications

src/model_checking/front.md

@@ -0,0 +1 @@
+# Model_Checking

src/resources/front.md

@@ -0,0 +1 @@
+# resources

src/smt_solvers/front.md

@@ -0,0 +1 @@
+# SMT_Solvers

src/smt_theory_and_implementation.md → src/smt_solvers/theory_and_implementation/front.md

@@ -1,5 +1,30 @@
 # SMT Theory and Implementation
 
+## SAT
+
+SAT is a NP-complete problem.
+
+Input to SAT solver is a propositional formula in CNF (conjunctive normal form).
+The CNF is a conjunction of one or more clauses, where a clause is a disjunction
+of literals. In other words: One outer, multi-arged AND of many ORs.
+
+For example, here's the CNF for the constraints on a single sudoku cell:
+
+```clojure
+(and (or x1 x2 x3 ...)
+     (or (not x1) (not x2))
+     (or (not x1) (not x3))
+     (or (not x1) (not x4))
+	 ...
+     (or (not x8) (not x9))
+
+)
+```
+
+The cell needs to be one of the values between `[1..9]`, and it can not be 
+simultaenously more than one value.
+
+Looking at the sudoku 
 ## Blob
 asdf