diff --git a/src/SUMMARY.md b/src/SUMMARY.md index db689cd..9c4af5b 100644 --- a/src/SUMMARY.md +++ b/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) diff --git a/src/curry_howard_correspondence.md b/src/curry_howard_correspondence.md deleted file mode 100644 index 4a53a82..0000000 --- a/src/curry_howard_correspondence.md +++ /dev/null @@ -1,3 +0,0 @@ -# Curry Howard Correspondence - -## Wadler's Account diff --git a/src/dependently_typed_languages/agda/front.md b/src/dependently_typed_languages/agda/front.md new file mode 100644 index 0000000..1945fe2 --- /dev/null +++ b/src/dependently_typed_languages/agda/front.md @@ -0,0 +1 @@ +# Agda diff --git a/src/dependently_typed_languages/coq/front.md b/src/dependently_typed_languages/coq/front.md new file mode 100644 index 0000000..49fa06c --- /dev/null +++ b/src/dependently_typed_languages/coq/front.md @@ -0,0 +1 @@ +# Coq diff --git a/src/dependently_typed_languages/front.md b/src/dependently_typed_languages/front.md new file mode 100644 index 0000000..f4e0007 --- /dev/null +++ b/src/dependently_typed_languages/front.md @@ -0,0 +1 @@ +# Dependently_Typed_Languages diff --git a/src/dependently_typed_languages/fstar/front.md b/src/dependently_typed_languages/fstar/front.md new file mode 100644 index 0000000..c74f856 --- /dev/null +++ b/src/dependently_typed_languages/fstar/front.md @@ -0,0 +1 @@ +# FStar diff --git a/src/idris.md b/src/dependently_typed_languages/idris/front.md similarity index 100% rename from src/idris.md rename to src/dependently_typed_languages/idris/front.md diff --git a/src/dependently_typed_languages/isabelle_hol/front.md b/src/dependently_typed_languages/isabelle_hol/front.md new file mode 100644 index 0000000..74fa1e0 --- /dev/null +++ b/src/dependently_typed_languages/isabelle_hol/front.md @@ -0,0 +1 @@ +# Isabelle_HOL diff --git a/src/dependently_typed_languages/lean/front.md b/src/dependently_typed_languages/lean/front.md new file mode 100644 index 0000000..b585df4 --- /dev/null +++ b/src/dependently_typed_languages/lean/front.md @@ -0,0 +1 @@ +# Lean diff --git a/src/foundations/church_encodings/front.md b/src/foundations/church_encodings/front.md new file mode 100644 index 0000000..2f5b02e --- /dev/null +++ b/src/foundations/church_encodings/front.md @@ -0,0 +1 @@ +# Church_Encodings diff --git a/src/foundations/computability_and_lambda_calculus/front.md b/src/foundations/computability_and_lambda_calculus/front.md new file mode 100644 index 0000000..4af3331 --- /dev/null +++ b/src/foundations/computability_and_lambda_calculus/front.md @@ -0,0 +1 @@ +# Computability_And_Lambda_Calculus diff --git a/src/foundation.md b/src/foundations/front.md similarity index 100% rename from src/foundation.md rename to src/foundations/front.md diff --git a/src/foundations/hott/front.md b/src/foundations/hott/front.md new file mode 100644 index 0000000..8d6e62e --- /dev/null +++ b/src/foundations/hott/front.md @@ -0,0 +1 @@ +# HoTT diff --git a/src/foundations/incompleteness_undecidability_inconsistency/front.md b/src/foundations/incompleteness_undecidability_inconsistency/front.md new file mode 100644 index 0000000..dbc37f3 --- /dev/null +++ b/src/foundations/incompleteness_undecidability_inconsistency/front.md @@ -0,0 +1 @@ +# Incompleteness_Undecidability_Inconsistency diff --git a/src/foundations/lambda_cube/front.md b/src/foundations/lambda_cube/front.md new file mode 100644 index 0000000..4260966 --- /dev/null +++ b/src/foundations/lambda_cube/front.md @@ -0,0 +1 @@ +# Lambda_Cube diff --git a/src/foundations/paradoxes/front.md b/src/foundations/paradoxes/front.md new file mode 100644 index 0000000..abd1222 --- /dev/null +++ b/src/foundations/paradoxes/front.md @@ -0,0 +1 @@ +# Paradoxes diff --git a/src/foundations/propositions_as_types/front.md b/src/foundations/propositions_as_types/front.md new file mode 100644 index 0000000..695053f --- /dev/null +++ b/src/foundations/propositions_as_types/front.md @@ -0,0 +1 @@ +# Propositions_As_Types diff --git a/src/foundations/propositions_as_types_more/front.md b/src/foundations/propositions_as_types_more/front.md new file mode 100644 index 0000000..6c50545 --- /dev/null +++ b/src/foundations/propositions_as_types_more/front.md @@ -0,0 +1 @@ +# Propositions_As_Types_More diff --git a/src/foundations/propositions_as_types_more/modal_logic_and_monads/front.md b/src/foundations/propositions_as_types_more/modal_logic_and_monads/front.md new file mode 100644 index 0000000..c1375f5 --- /dev/null +++ b/src/foundations/propositions_as_types_more/modal_logic_and_monads/front.md @@ -0,0 +1 @@ +# Modal_Logic_And_Monads diff --git a/src/foundations/propositions_as_types_more/system_f/front.md b/src/foundations/propositions_as_types_more/system_f/front.md new file mode 100644 index 0000000..d260f46 --- /dev/null +++ b/src/foundations/propositions_as_types_more/system_f/front.md @@ -0,0 +1 @@ +# System_F diff --git a/src/full_applications/front.md b/src/full_applications/front.md new file mode 100644 index 0000000..aaaa9f7 --- /dev/null +++ b/src/full_applications/front.md @@ -0,0 +1 @@ +# Full_Applications diff --git a/src/full_applications/verified_cryptography/cryptol_and_saw/front.md b/src/full_applications/verified_cryptography/cryptol_and_saw/front.md new file mode 100644 index 0000000..4c378c5 --- /dev/null +++ b/src/full_applications/verified_cryptography/cryptol_and_saw/front.md @@ -0,0 +1 @@ +# Cryptol_And_Saw diff --git a/src/cryptol_for_anyone.md b/src/full_applications/verified_cryptography/cryptol_for_anyone/front.md similarity index 100% rename from src/cryptol_for_anyone.md rename to src/full_applications/verified_cryptography/cryptol_for_anyone/front.md diff --git a/src/cryptol_for_haskell_devs.md b/src/full_applications/verified_cryptography/cryptol_for_haskell_knowers/front.md similarity index 100% rename from src/cryptol_for_haskell_devs.md rename to src/full_applications/verified_cryptography/cryptol_for_haskell_knowers/front.md diff --git a/src/full_applications/verified_cryptography/front.md b/src/full_applications/verified_cryptography/front.md new file mode 100644 index 0000000..c5ace84 --- /dev/null +++ b/src/full_applications/verified_cryptography/front.md @@ -0,0 +1 @@ +# Verified_Cryptography diff --git a/src/full_applications/verified_hardware_with_systemverilog/front.md b/src/full_applications/verified_hardware_with_systemverilog/front.md new file mode 100644 index 0000000..1c48673 --- /dev/null +++ b/src/full_applications/verified_hardware_with_systemverilog/front.md @@ -0,0 +1 @@ +# Verified_Hardware_With_SystemVerilog diff --git a/src/full_applications/verifying_rust_with_verus/borrow_checker_linear_types/front.md b/src/full_applications/verifying_rust_with_verus/borrow_checker_linear_types/front.md new file mode 100644 index 0000000..f214699 --- /dev/null +++ b/src/full_applications/verifying_rust_with_verus/borrow_checker_linear_types/front.md @@ -0,0 +1 @@ +# Borrow_Checker_Linear_Types diff --git a/src/verified_parsers.md b/src/full_applications/verifying_rust_with_verus/case_study_verified_parsers/front.md similarity index 100% rename from src/verified_parsers.md rename to src/full_applications/verifying_rust_with_verus/case_study_verified_parsers/front.md diff --git a/src/full_applications/verifying_rust_with_verus/front.md b/src/full_applications/verifying_rust_with_verus/front.md new file mode 100644 index 0000000..feae1c7 --- /dev/null +++ b/src/full_applications/verifying_rust_with_verus/front.md @@ -0,0 +1 @@ +# Verifying_Rust_With_Verus diff --git a/src/verus_fundamentals.md b/src/full_applications/verifying_rust_with_verus/verus_fundamentals/front.md similarity index 100% rename from src/verus_fundamentals.md rename to src/full_applications/verifying_rust_with_verus/verus_fundamentals/front.md diff --git a/src/glossary_resources.md b/src/glossary_resources.md new file mode 100644 index 0000000..e69de29 diff --git a/src/introduction.md b/src/introduction.md new file mode 100644 index 0000000..6fdbe4d --- /dev/null +++ b/src/introduction.md @@ -0,0 +1 @@ +# Journey Through Formal Verifications \ No newline at end of file diff --git a/src/model_checking/front.md b/src/model_checking/front.md new file mode 100644 index 0000000..de9284a --- /dev/null +++ b/src/model_checking/front.md @@ -0,0 +1 @@ +# Model_Checking diff --git a/src/resources/front.md b/src/resources/front.md new file mode 100644 index 0000000..abbe70d --- /dev/null +++ b/src/resources/front.md @@ -0,0 +1 @@ +# resources diff --git a/src/sat.md b/src/sat.md deleted file mode 100644 index 6fbc870..0000000 --- a/src/sat.md +++ /dev/null @@ -1,25 +0,0 @@ -# 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 \ No newline at end of file diff --git a/src/smt_solvers/front.md b/src/smt_solvers/front.md new file mode 100644 index 0000000..06e9e1d --- /dev/null +++ b/src/smt_solvers/front.md @@ -0,0 +1 @@ +# SMT_Solvers diff --git a/src/smt_theory_and_implementation.md b/src/smt_solvers/theory_and_implementation/front.md similarity index 66% rename from src/smt_theory_and_implementation.md rename to src/smt_solvers/theory_and_implementation/front.md index 9e64887..64a14e5 100644 --- a/src/smt_theory_and_implementation.md +++ b/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