diff --git a/1 Daily Notes/2025/2025-02-21.md b/1 Daily Notes/2025/2025-02-21.md index 3426019cc..946bfe1b9 100644 --- a/1 Daily Notes/2025/2025-02-21.md +++ b/1 Daily Notes/2025/2025-02-21.md @@ -9,7 +9,7 @@ tags: [[ Weekly Note 2025-02-17]] # Summary ## What's the plan? -- [<] Chess Graduate Student Tournament Plan #GSA ⏳ 2025-02-26 📅 2025-02-28 +- [<] Chess Graduate Student Tournament Plan #GSA ⏳ 2025-02-26 📅 2025-03-11 ## What's the results! ```tasks diff --git a/200 Library Papers/fromherzVerifiedEfficientEmbedding2019.md b/200 Library Papers/fromherzVerifiedEfficientEmbedding2019.md index c565975c7..16a0eef32 100644 --- a/200 Library Papers/fromherzVerifiedEfficientEmbedding2019.md +++ b/200 Library Papers/fromherzVerifiedEfficientEmbedding2019.md @@ -28,7 +28,7 @@ pages: 63:1–63:30 ## Tags: -- ["] A verified, efficient embedding of a verifiable assembly language #Reading ⏳ 2025-02-28 📅 2025-02-28 +- [-] A verified, efficient embedding of a verifiable assembly language #Reading ⏳ 2025-02-28 📅 2025-02-28 ❌ 2025-03-10 >[!Abstract] >High-performance cryptographic libraries often mix code written in a high-level language with code written in assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding of a subset of x64 assembly language in F* that allows efficient verification of both assembly and its interoperation with C code generated from F*. The key idea is to use the computational power of a dependent type system's type checker to run a verified verification-condition generator during type checking. This allows the embedding to customize the verification condition sent by the type checker to an SMT solver. By combining our proof-by-reflection style with SMT solving, we demonstrate improved automation for proving the correctness of assembly-language code. This approach has allowed us to complete the first-ever proof of correctness of an optimized implementation of AES-GCM, a cryptographic routine used by 90% of secure Internet traffic.>[!seealso] Related Papers diff --git a/3-99 Research/Haskell/Chapter 1 - Introduction.md b/3-99 Research/Haskell/Chapter 1 - Introduction.md index bb4aaf1b8..955ea32c1 100644 --- a/3-99 Research/Haskell/Chapter 1 - Introduction.md +++ b/3-99 Research/Haskell/Chapter 1 - Introduction.md @@ -5,11 +5,11 @@ What does that mean? What isn't a functional programming language? Well, just ab If I want to compute a factorial, I'd probably say take this value, and multiply it a whole bunch of times until you get to an end condition. The computer may change state at this point, where your input variable gets overwritten with the result, or some thing inside the task list, such as an iterator, changes to a value that can create a different result if run again. -- [?] What is a 'state' for a computer really? #Follow-Up #Haskell ⏳ 2025-02-28 📅 2025-02-28 +- [?] What is a 'state' for a computer really? #Follow-Up #Haskell ⏳ 2025-02-28 📅 2025-03-11 Functional programming languages do not do this. Instead of using iteratives like that or having the possiblity of functions changing variable states, everything is instead immutable. If I define a function for a factorial, I define *what a factorial is*, rather than explicit steps to compute one. Then, when I apply the 'function' to an input, the output is something new: the function applied to that variable that is fundamentally not an execution of the function or a wrought product of the original input. This is *maybe* what a monad is. -- [?] What is a 'monad' really? #Follow-Up #Haskell ⏳ 2025-02-28 📅 2025-02-28 +- [?] What is a 'monad' really? #Follow-Up #Haskell ⏳ 2025-02-28 📅 2025-03-11 There's a special property about functions that can be called multiple times with the same parameters being guaranteed to return the same result: **Referential Transparency**. This property allows us to deduce and then even proved that a function does exactly what it is supposed to, every time. diff --git a/3-99 Research/Haskell/Learning Plan.md b/3-99 Research/Haskell/Learning Plan.md index bc366f414..30238094c 100644 --- a/3-99 Research/Haskell/Learning Plan.md +++ b/3-99 Research/Haskell/Learning Plan.md @@ -1,7 +1,7 @@ https://learnyouahaskell.github.io/chapters.html - [x] Chapter 1: Introduction #Haskell ⏳ 2025-02-18 📅 2025-02-12 ✅ 2025-02-19 - [x] Chapter 2: Starting Out #Haskell ⏳ 2025-02-19 📅 2025-02-25 ✅ 2025-02-24 -- [<] Chapter 3: Types and Typeclasses #Haskell ⏳ 2025-02-26 📅 2025-03-04 +- [<] Chapter 3: Types and Typeclasses #Haskell ⏳ 2025-02-26 📅 2025-03-11 - [ ] Chapter 4: Syntax in Functions #Haskell 📅 2025-03-05 ⏳ 2025-03-11 - [ ] Chapter 5: Recursion #Haskell 📅 2025-03-12 ⏳ 2025-03-18 - [ ] Chapter 6: Higher Order Functions #Haskell 📅 2025-03-19 ⏳ 2025-03-25 diff --git a/3-99 Research/LEAN/Learning Plan.md b/3-99 Research/LEAN/Learning Plan.md index 23aec0324..30691ab45 100644 --- a/3-99 Research/LEAN/Learning Plan.md +++ b/3-99 Research/LEAN/Learning Plan.md @@ -1,5 +1,5 @@ - [x] Tutorial World #LEAN ⏳ 2025-02-17 📅 2025-02-21 ✅ 2025-02-24 - [<] Addition World #LEAN ⏳ 2025-02-23 📅 2025-02-28 - - [ ] Implication World #LEAN 📅 2025-03-07 ⏳ 2025-03-02 - - [ ] Multiplication World #LEAN 📅 2025-03-07 ⏳ 2025-03-07 - - [ ] Schedule further worlds #LEAN 📅 2025-03-07 ⏳ 2025-03-07 + - [ ] Implication World #LEAN 🔽 ⏳ 2025-03-02 📅 2025-03-07 + - [ ] Multiplication World #LEAN 🔽 ⏳ 2025-03-07 📅 2025-03-07 + - [ ] Schedule further worlds #LEAN 🔽 ⏳ 2025-03-07 📅 2025-03-07 diff --git a/3-99 Research/Rust/Learning Plan.md b/3-99 Research/Rust/Learning Plan.md index 861a47e08..a7c23d487 100644 --- a/3-99 Research/Rust/Learning Plan.md +++ b/3-99 Research/Rust/Learning Plan.md @@ -1,6 +1,6 @@ - [x] Chapter 1: Getting Started #Rust ⏳ 2025-02-17 📅 2025-02-11 ✅ 2025-02-17 - [<] Chapter 2: Programming a Guessing Game #Rust ⏳ 2025-02-18 📅 2025-02-24 -- [<] Chapter 3: Common Programming Concepts #Rust ⏳ 2025-02-25 📅 2025-03-03 +- [<] Chapter 3: Common Programming Concepts #Rust ⏳ 2025-02-25 📅 2025-03-11 - [ ] Chapter 4: Understanding Ownership #Rust ⏳ 2025-03-10 📅 2025-03-14 - [ ] Chapter 5: Using Structs to Structure Related Data #Rust 📅 2025-03-11 ⏳ 2025-03-17 - [ ] Chapter 6: Enums and Pattern Matching #Rust 📅 2025-03-18 ⏳ 2025-03-24 diff --git a/3-99 Research/TLA/Writing a MARVEL Specification in TLA+.md b/3-99 Research/TLA/Writing a MARVEL Specification in TLA+.md index d68a37e34..a55231a7b 100644 --- a/3-99 Research/TLA/Writing a MARVEL Specification in TLA+.md +++ b/3-99 Research/TLA/Writing a MARVEL Specification in TLA+.md @@ -1,9 +1,9 @@ # What is the MARVEL reactor? -- [?] What the fuck is MARVEL? #Reading 🆔 furwbi 📅 2025-02-28 +- [?] What the fuck is MARVEL? #Reading 🆔 furwbi ⏫ 📅 2025-02-28 # What are some specs that perhaps can be formalized in TLA+? ## What are the specs of interest? -- [ ] Write down some specs from MARVEL in natural language #Formal-methods 🆔 lofl94 ⛔ furwbi 📅 2025-02-28 +- [ ] Write down some specs from MARVEL in natural language #Formal-methods 🆔 lofl94 ⛔ furwbi ⏫ 📅 2025-02-28 ## How do they translate to TLA+? -- [ ] Translate a MARVEL specification into a TLA+ module #Formal-methods #TLA ⛔ lofl94 📅 2025-03-04 \ No newline at end of file +- [ ] Translate a MARVEL specification into a TLA+ module #Formal-methods #TLA ⛔ lofl94 ⏫ 📅 2025-03-04 \ No newline at end of file diff --git a/300s School/ME 2046 - Digital Control Theory/!Things That Need Done.md b/300s School/ME 2046 - Digital Control Theory/!Things That Need Done.md index 6f88a0d53..4f3d073a3 100644 --- a/300s School/ME 2046 - Digital Control Theory/!Things That Need Done.md +++ b/300s School/ME 2046 - Digital Control Theory/!Things That Need Done.md @@ -2,9 +2,12 @@ - [x] Homework Assignment 2 #ME2046 ⏳ 2025-02-03 📅 2025-02-06 ✅ 2025-02-13 - [x] Homework Assignment 2 - Code Files #ME2046 ⏳ 2025-02-03 📅 2025-02-06 ✅ 2025-02-13 - [x] Homework Assignment 3 #ME2046 ⏫ ⏳ 2025-02-17 📅 2025-02-27 ✅ 2025-03-06 -- [ ] Homework Assignment 4 #ME2046 ⏫ ⏳ 2025-03-11 📅 2025-03-18 +- [ ] Homework Assignment 4 #ME2046 ⏫ ⏳ 2025-03-14 📅 2025-03-18 # Projects -- [ ] Project Proposal #ME2046 ⏫ 📅 2025-03-20 ⏳ 2025-03-01 +- [ ] Project Proposal #ME2046 ⏫ 📅 2025-03-20 ⏳ 2025-03-14 - [ ] Project Update #ME2046 ⏫ 📅 2025-04-10 ⏳ 2025-03-20 -- [ ] Final Project Report #ME2046 ⏫ 📅 2025-04-24 ⏳ 2025-04-10 \ No newline at end of file +- [ ] Final Project Report #ME2046 ⏫ 📅 2025-04-24 ⏳ 2025-04-10 + +# Midterm +- [ ] Midterm #ME2046 🔺 📅 2025-03-17 ⏳ 2025-03-14 diff --git a/300s School/ME 2150 - High Assurance Cyber-Physical Systems/2025-02-18 Boyd Talk.md b/300s School/ME 2150 - High Assurance Cyber-Physical Systems/2025-02-18 Boyd Talk.md index 5752089ed..8eee3d455 100644 --- a/300s School/ME 2150 - High Assurance Cyber-Physical Systems/2025-02-18 Boyd Talk.md +++ b/300s School/ME 2150 - High Assurance Cyber-Physical Systems/2025-02-18 Boyd Talk.md @@ -9,4 +9,4 @@ Engineering is a step on top of science. Engineering is *creating* with science' - [ ] Innovators dilemma. An interesting book that discusses, well, the innovators dilemma. ⏬ ⏳ 2025-02-24 📅 2025-02-28 -- [ ] Look up Pancake. Language that is good for drivers but also easy to distill proofs. 🛫 2025-02-24 📅 2025-02-28 +- [ ] Look up Pancake. Language that is good for drivers but also easy to distill proofs. 🔽 🛫 2025-02-24 📅 2025-02-28 diff --git a/300s School/NUCE 2113 - Radiation Detection and Measurement/!Things That Need Done.md b/300s School/NUCE 2113 - Radiation Detection and Measurement/!Things That Need Done.md index b28b0b30d..84b1f62bd 100644 --- a/300s School/NUCE 2113 - Radiation Detection and Measurement/!Things That Need Done.md +++ b/300s School/NUCE 2113 - Radiation Detection and Measurement/!Things That Need Done.md @@ -1,9 +1,12 @@ # Homework - +- [ ] Homework 4 #NUCE2113 ⏫ 📅 2025-03-11 # Lab Reports - [x] Lab Report 2 #NUCE2113 ⏫ ⏳ 2025-02-03 📅 2025-02-04 ✅ 2025-02-04 - [x] Lab Report 3 #NUCE2113 ⏳ 2025-02-05 📅 2025-02-11 ✅ 2025-02-10 - [x] Lab Report 4 #NUCE2113 ⏳ 2025-02-12 📅 2025-02-18 ✅ 2025-02-17 - [x] Lab Report 5 #NUCE2113 🔼 ⏳ 2025-02-19 📅 2025-02-25 ✅ 2025-02-25 - [<] Lab Report 6 #NUCE2113 ⏫ ⏳ 2025-03-05 📅 2025-03-11 -- [ ] Lab Report 7 #NUCE2113 ⏫ ⏳ 2025-03-12 📅 2025-03-18 \ No newline at end of file +- [ ] Lab Report 7 #NUCE2113 ⏫ ⏳ 2025-03-12 📅 2025-03-18 + +# Midterm +- [ ] Midterm #NUCE2113 🔺 📅 2025-03-18 ⏳ 2025-03-14 \ No newline at end of file diff --git a/5 Thesis/Things to Do.md b/5 Thesis/Things to Do.md index b0bcbb633..b6d0ffdd4 100644 --- a/5 Thesis/Things to Do.md +++ b/5 Thesis/Things to Do.md @@ -1,6 +1,6 @@ Follow up tasks: - [-] What is the state of the art for wireless control? #Thesis ❌ 2025-01-24 -- [<] What has happened so far with verifying assembly code? #Thesis 🔽 ⏳ 2025-01-29 📅 2025-02-06 +- [-] What has happened so far with verifying assembly code? #Thesis 🔽 ⏳ 2025-01-29 📅 2025-02-06 ❌ 2025-03-10 - [?] How does Rust compile into binary? #Thesis ⏬ ⏳ 2025-01-28 📅 2025-02-11 ```dataview task diff --git a/900s Calendars/Learning/Learning - README.md b/900s Calendars/Learning/Learning - README.md index 1d06058de..9350fca60 100644 --- a/900s Calendars/Learning/Learning - README.md +++ b/900s Calendars/Learning/Learning - README.md @@ -15,7 +15,7 @@ - [[2025-03-06 ME2046 more HW3.md]] - [[2025-03-07 HW2 NUCE 2113.md]] - [[2025-03-10 Laboratory 6 Report.md]] -- [[2025-03-13 ME2046 Exam]] +- [[2025-03-13 ME2046 Exam.md]] ## Summary