vault backup: 2025-02-24 21:07:11
This commit is contained in:
parent
f8134b65ff
commit
42a3ecc817
3
.obsidian/plugins/colored-tags/data.json
vendored
3
.obsidian/plugins/colored-tags/data.json
vendored
@ -193,7 +193,8 @@
|
||||
"Haskell": 181,
|
||||
"Rust": 182,
|
||||
"LEAN": 183,
|
||||
"Email": 184
|
||||
"Email": 184,
|
||||
"Z": 185
|
||||
},
|
||||
"_version": 3
|
||||
}
|
||||
@ -8,6 +8,7 @@ sort by function task.created.format("dddd")
|
||||
# 😎 Tasks
|
||||
>[!danger] **Extreme Urgency Tasks**
|
||||
>```tasks
|
||||
>tags do not include #Z
|
||||
>not done
|
||||
>show urgency
|
||||
>filter by function task.urgency >16.999
|
||||
@ -17,17 +18,18 @@ sort by function task.created.format("dddd")
|
||||
|
||||
>[!warning] **High Urgency Tasks**
|
||||
>```tasks
|
||||
>tags do not include #Z
|
||||
>not done
|
||||
>show urgency
|
||||
>filter by function task.urgency >12.999 && task.urgency<17.0
|
||||
>group by tags
|
||||
>sort by urgency
|
||||
|
||||
> ```
|
||||
|
||||
>[!todo] **Medium Urgency Tasks**
|
||||
>```tasks
|
||||
>not done
|
||||
>tags do not include #Z
|
||||
>show urgency
|
||||
>filter by function task.urgency >7.999 && task.urgency<13.0
|
||||
>sort by urgency
|
||||
@ -37,6 +39,7 @@ sort by function task.created.format("dddd")
|
||||
>[!done] **Low Urgency Tasks**
|
||||
>```tasks
|
||||
>not done
|
||||
>tags do not include #Z
|
||||
>show urgency
|
||||
>filter by function task.urgency <8.0
|
||||
>sort by urgency
|
||||
|
||||
@ -10,10 +10,10 @@ tags:
|
||||
# Summary
|
||||
## What's the plan?
|
||||
- [x] TLA Learning Plan #TLA ⏫ ⏳ 2025-02-20 📅 2025-02-20 ✅ 2025-02-24
|
||||
- [ ] Do something with Robert's Email #Email 📅 2025-02-20 ⏳ 2025-02-20
|
||||
- [ ] Do something with Robert's Email #Email 🔽 ⏳ 2025-02-20 📅 2025-02-20
|
||||
- [x] Join union discord #Union ⏳ 2025-02-21 📅 2025-02-21 ✅ 2025-02-21
|
||||
- [ ] Invite Yiyang to signal chat #Union ⏳ 2025-02-21 📅 2025-02-21
|
||||
- [ ] Set up union github repo #Union ⏳ 2025-02-21 📅 2025-02-21
|
||||
- [ ] Invite Yiyang to signal chat #Union 🔽 ⏳ 2025-02-21 📅 2025-02-21
|
||||
- [ ] Set up union github repo #Union 🔽 ⏳ 2025-02-21 📅 2025-02-21
|
||||
|
||||
## What's the results!
|
||||
```tasks
|
||||
|
||||
@ -9,7 +9,7 @@ tags:
|
||||
[[ Weekly Note 2025-02-17]]
|
||||
# Summary
|
||||
## What's the plan?
|
||||
- [ ] Chess Graduate Student Tournament Plan #GSA
|
||||
- [ ] Chess Graduate Student Tournament Plan #GSA ⏳ 2025-02-26 📅 2025-02-28
|
||||
|
||||
## What's the results!
|
||||
```tasks
|
||||
|
||||
@ -9,7 +9,7 @@ tags:
|
||||
[[ Weekly Note 2025-02-17]]
|
||||
# Summary
|
||||
## What's the plan?
|
||||
- [ ] Investigate conference Robert mentioned "High Assurance Cyber Physical Something"
|
||||
- [ ] Investigate conference Robert mentioned "High Assurance Cyber Physical Something" #Thesis ⏳ 2025-02-24 📅 2025-02-28
|
||||
## What's the results!
|
||||
```tasks
|
||||
done 2025-02-24
|
||||
|
||||
@ -10,7 +10,7 @@ citekey: "ME2046_Sampled_Data_Analysis_Reading_Chapter_2pdf2254ME"
|
||||
## Tags:
|
||||
|
||||
|
||||
- ["] ME2046_Sampled_Data_Analysis_Reading_Chapter_2.pdf: 2254 ME 2046 SEC1000 DIGITAL CONTROL SYSTEMS #Reading
|
||||
- [x] ME2046_Sampled_Data_Analysis_Reading_Chapter_2.pdf: 2254 ME 2046 SEC1000 DIGITAL CONTROL SYSTEMS #Reading ✅ 2025-02-24
|
||||
|
||||
>[!seealso] Related Papers
|
||||
>
|
||||
|
||||
@ -28,7 +28,7 @@ pages: 63:1–63:30
|
||||
## Tags:
|
||||
|
||||
|
||||
- ["] A verified, efficient embedding of a verifiable assembly language #Reading
|
||||
- ["] A verified, efficient embedding of a verifiable assembly language #Reading ⏳ 2025-02-28 📅 2025-02-28
|
||||
|
||||
>[!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
|
||||
|
||||
@ -2,7 +2,7 @@
|
||||
|
||||
## Files
|
||||
- [[Assembly Canvas.canvas]]
|
||||
- [[Untitled.md]]
|
||||
- [[3-99 Research/Assembly/Untitled]]
|
||||
|
||||
## Summary
|
||||
|
||||
|
||||
@ -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
|
||||
- [?] What is a 'state' for a computer really? #Follow-Up #Haskell ⏳ 2025-02-28 📅 2025-02-28
|
||||
|
||||
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
|
||||
- [?] What is a 'monad' really? #Follow-Up #Haskell ⏳ 2025-02-28 📅 2025-02-28
|
||||
|
||||
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,6 +1,6 @@
|
||||
https://learnyouahaskell.github.io/chapters.html
|
||||
- [x] Chapter 1: Introduction #Haskell ⏳ 2025-02-18 📅 2025-02-12 ✅ 2025-02-19
|
||||
- [/] Chapter 2: Starting Out #Haskell ⏳ 2025-02-19 📅 2025-02-25
|
||||
- [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 4: Syntax in Functions #Haskell 📅 2025-03-05 ⏳ 2025-03-11
|
||||
- [ ] Chapter 5: Recursion #Haskell 📅 2025-03-12 ⏳ 2025-03-18
|
||||
|
||||
@ -7,6 +7,6 @@ Engineering is a step on top of science. Engineering is *creating* with science'
|
||||
|
||||
|
||||
|
||||
- [ ] Innovators dilemma. An interesting book that discusses, well, the innovators dilemma.
|
||||
- [ ] 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.
|
||||
- [ ] Look up Pancake. Language that is good for drivers but also easy to distill proofs. 🛫 2025-02-24 📅 2025-02-28
|
||||
|
||||
@ -4,4 +4,4 @@
|
||||
- [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
|
||||
- [/] Lab Report 5 #NUCE2113 ⏳ 2025-02-19 📅 2025-02-25
|
||||
- [/] Lab Report 5 #NUCE2113 🔼 ⏳ 2025-02-19 📅 2025-02-25
|
||||
@ -1,7 +1,7 @@
|
||||
# Table of Contents for 1 Ideas
|
||||
|
||||
## Files
|
||||
- [[Untitled.md]]
|
||||
- [[5 Thesis/1 Ideas/Untitled]]
|
||||
|
||||
## Summary
|
||||
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
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
|
||||
- [?] How does Rust compile into binary? #Thesis ⏳ 2025-01-28 📅 2025-02-11
|
||||
- [?] How does Rust compile into binary? #Thesis ⏬ ⏳ 2025-01-28 📅 2025-02-11
|
||||
```dataview
|
||||
task
|
||||
where contains(tags, "Thesis")
|
||||
|
||||
@ -6,8 +6,8 @@
|
||||
- [[2024-09-10 Nuclear Engineering Steering Committee - Conf Room A UClub.md]]
|
||||
- [[2025-02-24 Haskell Chapter 2.md]]
|
||||
- [[2025-02-24 LEAN.md]]
|
||||
- [[2025-02-25 Rust Chapter 2]]
|
||||
- [[2025-02-24 TLA Learning Plan and Notes.md]]
|
||||
- [[2025-02-25 Rust Chapter 2.md]]
|
||||
|
||||
## Summary
|
||||
|
||||
|
||||
@ -0,0 +1,4 @@
|
||||
```tasks
|
||||
tags include #Z
|
||||
group by tags
|
||||
```
|
||||
6
9999 Personal/Z/Untitled.canvas
Normal file
6
9999 Personal/Z/Untitled.canvas
Normal file
@ -0,0 +1,6 @@
|
||||
{
|
||||
"nodes":[
|
||||
{"id":"ceff3db39ffbb534","x":-340,"y":-320,"width":660,"height":440,"type":"text","text":"# The Dream 💘\n"}
|
||||
],
|
||||
"edges":[]
|
||||
}
|
||||
Loading…
x
Reference in New Issue
Block a user