os
This commit is contained in:
commit
29f7c07e4c
3
.obsidian/app.json
vendored
3
.obsidian/app.json
vendored
@ -8,5 +8,6 @@
|
||||
},
|
||||
"alwaysUpdateLinks": true,
|
||||
"useMarkdownLinks": true,
|
||||
"promptDelete": false
|
||||
"promptDelete": false,
|
||||
"readableLineLength": false
|
||||
}
|
||||
2
.obsidian/graph.json
vendored
2
.obsidian/graph.json
vendored
@ -46,6 +46,6 @@
|
||||
"repelStrength": 10,
|
||||
"linkStrength": 1,
|
||||
"linkDistance": 250,
|
||||
"scale": 0.665400791557209,
|
||||
"scale": 0.9981011873358133,
|
||||
"close": false
|
||||
}
|
||||
272
.obsidian/workspace.json
vendored
272
.obsidian/workspace.json
vendored
@ -1,272 +0,0 @@
|
||||
{
|
||||
"main": {
|
||||
"id": "0e274d9edc8c2fe9",
|
||||
"type": "split",
|
||||
"children": [
|
||||
{
|
||||
"id": "0f03a1a547c0e7e7",
|
||||
"type": "tabs",
|
||||
"children": [
|
||||
{
|
||||
"id": "76bee43de3990bf8",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "markdown",
|
||||
"state": {
|
||||
"file": "Software Engineering/TA Meeting 1.md",
|
||||
"mode": "source",
|
||||
"source": false
|
||||
},
|
||||
"icon": "lucide-file",
|
||||
"title": "TA Meeting 1"
|
||||
}
|
||||
},
|
||||
{
|
||||
"id": "f76f297000da99ca",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "release-notes",
|
||||
"state": {
|
||||
"currentVersion": "1.8.9"
|
||||
},
|
||||
"icon": "lucide-book-up",
|
||||
"title": "Release Notes 1.8.9"
|
||||
}
|
||||
}
|
||||
],
|
||||
"currentTab": 1
|
||||
}
|
||||
],
|
||||
"direction": "vertical"
|
||||
},
|
||||
"left": {
|
||||
"id": "14a8ed1946809664",
|
||||
"type": "split",
|
||||
"children": [
|
||||
{
|
||||
"id": "92972e07e7778c7e",
|
||||
"type": "tabs",
|
||||
"children": [
|
||||
{
|
||||
"id": "56bef0584922cba9",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "file-explorer",
|
||||
"state": {
|
||||
"sortOrder": "alphabetical",
|
||||
"autoReveal": false
|
||||
},
|
||||
"icon": "lucide-folder-closed",
|
||||
"title": "Files"
|
||||
}
|
||||
},
|
||||
{
|
||||
"id": "919f0d89f8f5c3bb",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "search",
|
||||
"state": {
|
||||
"query": "",
|
||||
"matchingCase": false,
|
||||
"explainSearch": false,
|
||||
"collapseAll": false,
|
||||
"extraContext": false,
|
||||
"sortOrder": "alphabetical"
|
||||
},
|
||||
"icon": "lucide-search",
|
||||
"title": "Search"
|
||||
}
|
||||
},
|
||||
{
|
||||
"id": "b590c125634ae7e4",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "bookmarks",
|
||||
"state": {},
|
||||
"icon": "lucide-bookmark",
|
||||
"title": "Bookmarks"
|
||||
}
|
||||
}
|
||||
]
|
||||
}
|
||||
],
|
||||
"direction": "horizontal",
|
||||
"width": 234.5
|
||||
},
|
||||
"right": {
|
||||
"id": "fd4347e6b5300816",
|
||||
"type": "split",
|
||||
"children": [
|
||||
{
|
||||
"id": "5d827a80e07e299e",
|
||||
"type": "tabs",
|
||||
"children": [
|
||||
{
|
||||
"id": "10adbcc903d0c352",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "backlink",
|
||||
"state": {
|
||||
"file": "Extracurricular/Circuitree/Committee Market/discussion/Macro pad.md",
|
||||
"collapseAll": false,
|
||||
"extraContext": false,
|
||||
"sortOrder": "alphabetical",
|
||||
"showSearch": false,
|
||||
"searchQuery": "",
|
||||
"backlinkCollapsed": false,
|
||||
"unlinkedCollapsed": true
|
||||
},
|
||||
"icon": "links-coming-in",
|
||||
"title": "Backlinks for Macro pad"
|
||||
}
|
||||
},
|
||||
{
|
||||
"id": "d61fc22784bbd3b0",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "outgoing-link",
|
||||
"state": {
|
||||
"file": "Extracurricular/Circuitree/Committee Market/discussion/Macro pad.md",
|
||||
"linksCollapsed": false,
|
||||
"unlinkedCollapsed": true
|
||||
},
|
||||
"icon": "links-going-out",
|
||||
"title": "Outgoing links from Macro pad"
|
||||
}
|
||||
},
|
||||
{
|
||||
"id": "c6317bbbe070400b",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "tag",
|
||||
"state": {
|
||||
"sortOrder": "frequency",
|
||||
"useHierarchy": true
|
||||
},
|
||||
"icon": "lucide-tags",
|
||||
"title": "Tags"
|
||||
}
|
||||
},
|
||||
{
|
||||
"id": "9fea917e949ad714",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "outline",
|
||||
"state": {
|
||||
"file": "Extracurricular/Circuitree/Committee Market/discussion/Macro pad.md"
|
||||
},
|
||||
"icon": "lucide-list",
|
||||
"title": "Outline of Macro pad"
|
||||
}
|
||||
},
|
||||
{
|
||||
"id": "e195b03d8630d307",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "QUICKSHARE_SIDE_VIEW",
|
||||
"state": {},
|
||||
"icon": "lucide-file",
|
||||
"title": "Plugin no longer active"
|
||||
}
|
||||
},
|
||||
{
|
||||
"id": "ac10c8e987c0e736",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "git-view",
|
||||
"state": {},
|
||||
"icon": "git-pull-request",
|
||||
"title": "Source Control"
|
||||
}
|
||||
},
|
||||
{
|
||||
"id": "9a5124aa0b3cede4",
|
||||
"type": "leaf",
|
||||
"state": {
|
||||
"type": "transcript-view",
|
||||
"state": {},
|
||||
"icon": "lucide-file",
|
||||
"title": "Plugin no longer active"
|
||||
}
|
||||
}
|
||||
],
|
||||
"currentTab": 5
|
||||
}
|
||||
],
|
||||
"direction": "horizontal",
|
||||
"width": 200,
|
||||
"collapsed": true
|
||||
},
|
||||
"left-ribbon": {
|
||||
"hiddenItems": {
|
||||
"switcher:Open quick switcher": false,
|
||||
"graph:Open graph view": false,
|
||||
"canvas:Create new canvas": false,
|
||||
"daily-notes:Open today's daily note": false,
|
||||
"templates:Insert template": false,
|
||||
"command-palette:Open command palette": false,
|
||||
"obsidian-excalidraw-plugin:Create new drawing": false,
|
||||
"table-editor-obsidian:Advanced Tables Toolbar": false,
|
||||
"obsidian-git:Open Git source control": false,
|
||||
"obsidian-advanced-slides:Show Slide Preview": false,
|
||||
"omnisearch:Omnisearch": false
|
||||
}
|
||||
},
|
||||
"active": "f76f297000da99ca",
|
||||
"lastOpenFiles": [
|
||||
"Software Engineering/TA Meeting 1.md",
|
||||
"Fundamentals of Electronics/Introductory Lecture.md",
|
||||
"Introduction to Machine Learning/Introductory lecture.md",
|
||||
"Fundamentals of Electronics",
|
||||
"Pasted image 20250113151159.png",
|
||||
"Advanced Algorithms/Graph Algorithms.md",
|
||||
"Advanced Algorithms/Graphs.md",
|
||||
"Introduction to Machine Learning/image.png",
|
||||
"Extracurricular/Circuitree/Committee Market/Macro pad.md",
|
||||
"Extracurricular/Circuitree/Committee Market/discussion/Committee market ideas.md",
|
||||
"Extracurricular/Circuitree/Committee Market/discussion/CA.md",
|
||||
"Extracurricular/Misc/Plan.md",
|
||||
"Extracurricular/Misc/Proposed Routine Plan.canvas",
|
||||
"Extracurricular/Misc/Ideas.md",
|
||||
"Functional Programming/Eq and Num.md",
|
||||
"Functional Programming/Proofs.md",
|
||||
"Operating Systems/Introductory lecture.md",
|
||||
"Discrete Structures/Relations and Digraphs.md",
|
||||
"Operating Systems/assets/Pasted image 20250204103541.png",
|
||||
"Software Engineering/Introductory Lecture.md",
|
||||
"Discrete Structures/Recurrence relations.md",
|
||||
"Discrete Structures/Mathematical Proofs (Induction).md",
|
||||
"Discrete Structures/Counting.md",
|
||||
"Introduction to Machine Learning",
|
||||
"Operating Systems/assets/image.png",
|
||||
"Operating Systems/image.png",
|
||||
"Operating Systems/assets",
|
||||
"conflict-files-obsidian-git.md",
|
||||
"Statistics and Probability/Mock exam run 1.md",
|
||||
"Operating Systems",
|
||||
"Statistics and Probability/Support Lecture.md",
|
||||
"Software Engineering",
|
||||
"Functional Programming/Drawing 2024-12-24 17.52.22.excalidraw.md",
|
||||
"Extracurricular/satQuest/Meeting Dec 18.md",
|
||||
"Extracurricular/satQuest/img/Pasted image 20241218122110.png",
|
||||
"Excalidraw/Drawing 2024-12-11 23.27.51.excalidraw.md",
|
||||
"Discrete Structures/Midterm/attempt 2.md",
|
||||
"Discrete Structures/Midterm/attempt 1.md",
|
||||
"Discrete Structures/Midterm",
|
||||
"Extracurricular/satQuest/img/Pasted image 20241206134156.png",
|
||||
"Untitled.canvas",
|
||||
"Advanced Algorithms/Pasted image 20241203234600.png",
|
||||
"Excalidraw",
|
||||
"Extracurricular/satQuest/img/Pasted image 20241206134213.png",
|
||||
"Extracurricular/satQuest/img/Pasted image 20241206134207.png",
|
||||
"Extracurricular/satQuest/img",
|
||||
"Advanced Algorithms/assets/pnp",
|
||||
"Advanced Algorithms/assets/graph",
|
||||
"Web Engineering/canvae/server_client.canvas",
|
||||
"Advanced Programming/projects/second/Refactoring.canvas",
|
||||
"Advanced Programming/assets/assignment/assignment_organization.canvas",
|
||||
"Advanced Programming/assets/spring/Beans.canvas",
|
||||
"Advanced Programming/assets/assignment/assignment_app.canvas",
|
||||
"Extracurricular/Circuitree/Committee Market/discussion/Proposed showcase infra.canvas"
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,18 @@
|
||||
|
||||
```mermaid
|
||||
sequenceDiagram
|
||||
Prototype ->> Order: Meeting with everyone
|
||||
Order ->> Prepare: Not everyone has to be present
|
||||
```
|
||||
|
||||
|
||||
|
||||
## Next week
|
||||
- Early, need to organize a meeting to build the antenna
|
||||
- Purchase the materials right after
|
||||
- Schedule the event
|
||||
|
||||
|
||||
|
||||
## All times
|
||||
- Create slides
|
||||
@ -22,6 +22,16 @@
|
||||
"color": "6",
|
||||
"label": "Productivity"
|
||||
},
|
||||
{
|
||||
"id": "37abaca3fa89fb9b",
|
||||
"type": "text",
|
||||
"text": "Better mental and productivity",
|
||||
"styleAttributes": {},
|
||||
"x": 799,
|
||||
"y": 681,
|
||||
"width": 294,
|
||||
"height": 60
|
||||
},
|
||||
{
|
||||
"id": "6dc127fe4098cce8",
|
||||
"type": "text",
|
||||
@ -42,16 +52,6 @@
|
||||
"width": 250,
|
||||
"height": 60
|
||||
},
|
||||
{
|
||||
"id": "2b76b4366e7d7447",
|
||||
"type": "text",
|
||||
"text": "Consistency in terms of Uni",
|
||||
"styleAttributes": {},
|
||||
"x": 713,
|
||||
"y": 354,
|
||||
"width": 280,
|
||||
"height": 60
|
||||
},
|
||||
{
|
||||
"id": "5159e3993f95efcb",
|
||||
"type": "text",
|
||||
@ -112,16 +112,6 @@
|
||||
"width": 283,
|
||||
"height": 60
|
||||
},
|
||||
{
|
||||
"id": "37abaca3fa89fb9b",
|
||||
"type": "text",
|
||||
"text": "Better mental and productivity",
|
||||
"styleAttributes": {},
|
||||
"x": 799,
|
||||
"y": 681,
|
||||
"width": 294,
|
||||
"height": 60
|
||||
},
|
||||
{
|
||||
"id": "3aa369dab5e52be1",
|
||||
"type": "text",
|
||||
@ -161,6 +151,16 @@
|
||||
"y": 800,
|
||||
"width": 181,
|
||||
"height": 60
|
||||
},
|
||||
{
|
||||
"id": "2b76b4366e7d7447",
|
||||
"type": "text",
|
||||
"text": "Consistency in terms of Uni",
|
||||
"styleAttributes": {},
|
||||
"x": 713,
|
||||
"y": 354,
|
||||
"width": 280,
|
||||
"height": 60
|
||||
}
|
||||
],
|
||||
"edges": [
|
||||
|
||||
55
Languages & Machines/Introduction.md
Normal file
55
Languages & Machines/Introduction.md
Normal file
@ -0,0 +1,55 @@
|
||||
---
|
||||
type: theoretical
|
||||
ty:
|
||||
---
|
||||
|
||||
## The foundations of computation
|
||||
Looking for answers for basic questions like:
|
||||
- Computability?
|
||||
- Power $\leftrightarrow$ Programming constructs?
|
||||
|
||||
Which leads us to fundamental concepts like:
|
||||
- State
|
||||
- Transitions
|
||||
- Non-determinism
|
||||
- Undecideability
|
||||
|
||||
|
||||
## Models
|
||||
### Finite memory
|
||||
Finite automata, regexp
|
||||
|
||||
### Finite memory with stack
|
||||
Push down automata
|
||||
|
||||
### Unrestricted
|
||||
Turing machines
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
## Grammars
|
||||
|
||||
|
||||
|
||||
|
||||
On a higher level, it seems like grammars and machines are very different, but parsing a language (a set of strings) is quite similar to computation.
|
||||
|
||||
## State-based systems and glossary
|
||||
An FSM can be a specification for OOP.
|
||||
|
||||
- States ($q_0,\ldots, q_n$)
|
||||
- Transitions ($a,b,c,\ldots,z$)
|
||||
- We can interpret the transitions as class methods and specify the sequences of allowed invocations - **typestate**
|
||||
|
||||
|
||||
|
||||
## Notation
|
||||
- $x \in X, X\subseteq Y$
|
||||
- $\forall x \in X: P(x), \exists x \in X: P(x)$
|
||||
- $R \subseteq X \times Y$ is a relation between $X$ and $Y$
|
||||
- $xRy \equiv (x,y) \in R$
|
||||
- $G = (V, E)$, where $E \subseteq V\times V$ is a directed graph
|
||||
|
||||
Part of [Relations and Digraphs](Relations%20and%20Digraphs.md)
|
||||
61
Languages & Machines/Regular languages.md
Normal file
61
Languages & Machines/Regular languages.md
Normal file
@ -0,0 +1,61 @@
|
||||
---
|
||||
type: math
|
||||
---
|
||||
## Induction
|
||||
Similar (if not the same) to:
|
||||
- [Mathematical Proofs (Induction)](Mathematical%20Proofs%20(Induction).md)
|
||||
- [Structural Proofs](Proofs.md)
|
||||
|
||||
|
||||
- Base case $0\in \mathbb{N}$
|
||||
- Inductive step - if $n\in \mathbb{N} \implies n+1\in \mathbb{N}$
|
||||
- We allow a finite number of steps
|
||||
|
||||
|
||||
I.e.
|
||||
Given $f (n) = n(n + 1)$ for all $n\in N$, then $f (n)$ is even.
|
||||
|
||||
**Base case:** $f(0) = 0\times 1 = 0$, which is even
|
||||
**I.S.:**
|
||||
$$
|
||||
f(n+1) = (n+1)(n+2)= n(n+1)+2(n+1) = f(n) + 2(n+1) \blacksquare
|
||||
$$
|
||||
|
||||
## Strings and Languages
|
||||
Literally the same as [Mathematical Data Structures](Mathematical%20Data%20Structures.md), but on strings
|
||||
|
||||
How to define the reversal of a string, inductively?
|
||||
|
||||
|
||||
Let $w$ be a finite string. We define $w^R$ by induction on $|w|$:
|
||||
|
||||
**B.C.:**
|
||||
$|w| = 0$, then, trivially, $w = \epsilon \therefore w^R = \epsilon$
|
||||
|
||||
**I.S.:**
|
||||
$|w| = n \geq 1$, so $w = u a$ with $|u| = n-1$,
|
||||
|
||||
|
||||
## Operations on strings
|
||||
- Concatenation (associative)
|
||||
- Substring, prefix, suffix
|
||||
- Replication (exponentiation): a string concatenated with itself
|
||||
- Reversal ($u^R$)
|
||||
|
||||
## Operations on languages
|
||||
- Lifting operations on strings to languages
|
||||
- Concatenation of languages
|
||||
- Kleene star - $V^*$ -> smallest superset[^1] of V that contains the empty string and is closed under concatenation, i.e. one or more repetitions
|
||||
- Reversal
|
||||
|
||||
## Regular sets / languages
|
||||
This used to be in DS, but I don't have it in this repo.
|
||||
|
||||
Recursively defined over an alphabet $\Sigma$ from
|
||||
- $\emptyset$
|
||||
- $\{\epsilon\}$
|
||||
- $\{a\} | \forall a \in \Sigma$
|
||||
|
||||
Regex is a notatio nto denote regular languages, i.e.:
|
||||
|
||||
[^1]: The opposite of a subset - a set which contains all elements of another (and possibly more)
|
||||
|
Before Width: | Height: | Size: 7.5 KiB After Width: | Height: | Size: 7.5 KiB |
BIN
Languages & Machines/assets/Pasted image 20250414190100.png
Normal file
BIN
Languages & Machines/assets/Pasted image 20250414190100.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 225 KiB |
BIN
Languages & Machines/assets/Pasted image 20250414190119.png
Normal file
BIN
Languages & Machines/assets/Pasted image 20250414190119.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 37 KiB |
BIN
Languages & Machines/assets/Pasted image 20250414190144.png
Normal file
BIN
Languages & Machines/assets/Pasted image 20250414190144.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 95 KiB |
BIN
Languages & Machines/assets/Pasted image 20250414190229.png
Normal file
BIN
Languages & Machines/assets/Pasted image 20250414190229.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 894 KiB |
24
Software Engineering/Initial Questions.md
Normal file
24
Software Engineering/Initial Questions.md
Normal file
@ -0,0 +1,24 @@
|
||||
|
||||
### Logistics
|
||||
- Will we have access to an overview of the project roadmap, including deliverables?\
|
||||
> **No. It is a research project, hence no deliverables and such.**
|
||||
- Do you need us to use specific project management tools (e.g. GitHub, Jira, etc.)?
|
||||
- How often are you available? Is it possible to have weekly progress reports?
|
||||
> Every week is good.
|
||||
### Formal Verification
|
||||
- What is the expected level of background in Coq or formal methods?
|
||||
> It's possible to catch up to speed in a couple of months
|
||||
- Can you explain the process by which a smart contract's safety properties will be validated formally?
|
||||
- Are there any existing case studies or example proofs we might refer to for a better understanding of the expected output?
|
||||
> You will be linked to existing projects
|
||||
- Define the contract verification criteria
|
||||
### Project scope clarifications
|
||||
- Among the seven smart contracts being verified, which ones do you expect us to work on, and why those?
|
||||
- Which technologies are we going to be introduced to, if any? Will we have access to guides for Coq and Solidity?
|
||||
- How do you envision the high-level Coq framework integrating with existing Solidity projects?
|
||||
|
||||
### Optional
|
||||
|
||||
- How much of the formal verification process will be based on axioms versus fully constructive proofs?
|
||||
- Could you elaborate on the notion of “high-level primitives” (e.g., identity, item, property) and how flexible they need to be for different types of contracts?
|
||||
- Could you specify what you mean by "real numbers and integer approximations"? Is it related to precision with math? How does that impact the security of a smart contract? Practical example?
|
||||
33
Software Engineering/Meeting.md
Normal file
33
Software Engineering/Meeting.md
Normal file
@ -0,0 +1,33 @@
|
||||
## Intro
|
||||
- Formalland 2 years old
|
||||
- Formal verification for code, proofs
|
||||
- Find a way to fully specify smart contracts
|
||||
- Formal verification as means of security (no bugs -> no stealing)
|
||||
- Alternatives include:
|
||||
- Testing (Unit, Value)
|
||||
- Human expertise
|
||||
- Quite niche in the field of computer science
|
||||
- We can be sure that the program follows intended behavior after verification
|
||||
|
||||
|
||||
## Smart contracts
|
||||
- Notion of users
|
||||
- Admin - owner
|
||||
- We need to look through some examples [here](https://formal.land/docs/tools/coq-of-solidity/specification-project) to get a feel for them.
|
||||
- Motivated by bugs [listed here](https://github.com/kadenzipfel/smart-contract-vulnerabilities)
|
||||
|
||||
### Example of Smart Contract
|
||||
- Stablecoins (USDC)
|
||||
- Possible specification(?) is to state that the amount of coins is fixed
|
||||
|
||||
## Work
|
||||
- Solidity
|
||||
- VSC online
|
||||
|
||||
### Questions during the meeting
|
||||
- What is the difference between a user and an admin in the context of smart contracts?
|
||||
|
||||
- You mentioned that one possible specification is to state that the amount of coins is fixed. How does that relate to formal verification? To our project?
|
||||
|
||||
- Is the idea to design a DSL? Could you elaborate on the specifics? Do you have a write-up about it or do we need to come up with it?
|
||||
> Yes. We want to simplify formal verification of smart contracts by creating a DSL.
|
||||
2
Software Engineering/Reqirements.md
Normal file
2
Software Engineering/Reqirements.md
Normal file
@ -0,0 +1,2 @@
|
||||
|
||||
End goal: Represent all 7 smart contracts in our DSL
|
||||
17
conflict-files-obsidian-git.md
Normal file
17
conflict-files-obsidian-git.md
Normal file
@ -0,0 +1,17 @@
|
||||
# Conflicts
|
||||
Please resolve them and commit them using the commands `Git: Commit all changes` followed by `Git: Push`
|
||||
(This file will automatically be deleted before commit)
|
||||
[[#Additional Instructions]] available below file list
|
||||
|
||||
- Not a file: .obsidian/workspace.json
|
||||
|
||||
# Additional Instructions
|
||||
I strongly recommend to use "Source mode" for viewing the conflicted files. For simple conflicts, in each file listed above replace every occurrence of the following text blocks with the desired text.
|
||||
|
||||
```diff
|
||||
<<<<<<< HEAD
|
||||
File changes in local repository
|
||||
=======
|
||||
File changes in remote repository
|
||||
>>>>>>> origin/main
|
||||
```
|
||||
Loading…
x
Reference in New Issue
Block a user