vault backup: 2025-03-10 10:44:32
This commit is contained in:
parent
c32cc84910
commit
c5f9d86559
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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.
|
||||
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
- [ ] Translate a MARVEL specification into a TLA+ module #Formal-methods #TLA ⛔ lofl94 ⏫ 📅 2025-03-04
|
||||
@ -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
|
||||
- [ ] Final Project Report #ME2046 ⏫ 📅 2025-04-24 ⏳ 2025-04-10
|
||||
|
||||
# Midterm
|
||||
- [ ] Midterm #ME2046 🔺 📅 2025-03-17 ⏳ 2025-03-14
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
- [ ] Lab Report 7 #NUCE2113 ⏫ ⏳ 2025-03-12 📅 2025-03-18
|
||||
|
||||
# Midterm
|
||||
- [ ] Midterm #NUCE2113 🔺 📅 2025-03-18 ⏳ 2025-03-14
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user