From a1f1b728cc6c5b9546e48fbf8bb1b43a258fa0dd Mon Sep 17 00:00:00 2001
From: "Tate, Hongliang Tian" <tate.thl@antgroup.com>
Date: Thu, 21 Jul 2022 00:22:28 -0700
Subject: [PATCH] Update docs

---
 docs/book.toml                                |  2 +-
 docs/src/README.md                            | 20 ++++++-
 .../capabilities/type_level_programming.md    | 52 -------------------
 3 files changed, 20 insertions(+), 54 deletions(-)

diff --git a/docs/book.toml b/docs/book.toml
index bed5cf0b..7a7ed560 100644
--- a/docs/book.toml
+++ b/docs/book.toml
@@ -6,4 +6,4 @@ src = "src"
 title = "KxOS: A Secure, Fast, and Modern OS in Rust"
 
 [rust]
-edition = "2021"
\ No newline at end of file
+edition = "2021"
diff --git a/docs/src/README.md b/docs/src/README.md
index 886bd47b..4342eba1 100644
--- a/docs/src/README.md
+++ b/docs/src/README.md
@@ -1,3 +1,17 @@
+<!-- 
+# Table of Content
+
+1. Introduction
+2. Design
+   1. Privilege Separation
+      1. Case Study 1: Syscall Workflow
+      2. Case Study 2: Drivers for Virtio Devices on PCI
+   2. Everything as a Capability
+      1. Type-Level Programming in Rust
+      2. CapComp: Zero-Cost Capabilities and Component
+   3. (More content...)
+-->
+
 # Introduction
 
 This document describes KxOS, a secure, fast, and modern OS written in Rust.
@@ -78,4 +92,8 @@ is allowed to have _unsafe_ Rust code. Furthermore, we propose the idea of _ever
 
 **3. Fast user-mode development.** Traditional OS kernels like Linux are hard to develop, test, and debug. Kernel development involves countless rounds of programming, failing, and rebooting on bare-metal or virtual machines. This way of life is unproductive and painful. Such a pain point is also recognized and partially addressed by [research work](https://www.usenix.org/conference/fast21/presentation/miller), but we think we can do more. In this spirit, we design the OS core to provide high-level APIs that are largely independent of the underlying hardware and implement it with two targets: one target is as part of a regular OS in kernel space and the other is as a library OS in user space. This way, all the OS components of KxOS, which are stacked above the OS core, can be developed, tested, and debugged in user space, which is more friendly to developers than kernel space.
 
-**4. High-fidelity Linux ABI.** An OS without usable applications is useless. So we believe it is important for KxOS to fit in an established and thriving ecosystem of software, such as the one around Linux. This is why we conclude that KxOS should aim at implementing high-fidelity Linux ABI, including the system calls, the proc file system, etc. 
+**4. High-fidelity Linux ABI.** An OS without usable applications is useless. So we believe it is important for KxOS to fit in an established and thriving ecosystem of software, such as the one around Linux. This is why we conclude that KxOS should aim at implementing high-fidelity Linux ABI, including the system calls, the proc file system, etc.
+
+**5. TEEs as top-tier targets.** (Todo)
+
+**6. Reservation-based OOM prevention.** (Todo)
diff --git a/docs/src/capabilities/type_level_programming.md b/docs/src/capabilities/type_level_programming.md
index ee0e3879..7ca3a7f7 100644
--- a/docs/src/capabilities/type_level_programming.md
+++ b/docs/src/capabilities/type_level_programming.md
@@ -362,58 +362,6 @@ pub type SetContainOp<Set, Item> = <Set as SetContain<Item>>::Output;
 
 Note: needs to implement `SameAs` for all possible item types (e.g., among `A` through `D`).
 
-### Where are the boundaries for TLP?
-
-#### Expressiveness: practically unlimited.
-
-![[Pasted image 20210825015426.png]]
-
----
-
-![[Pasted image 20210825015401.png]]
-
-#### Ergonomics: probably fixable.
-
-An example from the `typ` crate.
-
-```rust
-typ! {
-	fn BinaryGcd<lhs, rhs>(lhs: Unsigned, rhs: Unsigned) -> Unsigned {
-		if lhs == rhs {
-			lhs
-		} else if lhs == 0u {
-			rhs
-		} else if rhs == 0u {
-			lhs
-		} else {
-			if lhs % 2u == 1u {
-				if rhs % 2u == 1u {
-					if lhs > rhs {
-						let sub: Unsigned = lhs - rhs;
-						BinaryGcd(sub, rhs)
-					} else {
-						let sub: Unsigned = rhs - lhs;
-						BinaryGcd(sub, lhs)
-					}
-				} else {
-					let div: Unsigned = rhs / 2u;
-					BinaryGcd(lhs, div)
-				}
-			} else {
-				if rhs % 2u == 1u {
-					let div: Unsigned = lhs / 2u;
-					BinaryGcd(div, rhs)
-				} else {
-					let ldiv: Unsigned = lhs / 2u;
-					let rdiv: Unsigned = rhs / 2u;
-					BinaryGcd(ldiv, rdiv) * 2u
-				}
-			}
-		}
-	}
-}
-```
-
 ## An Application of TLP
 
 ### Capabilities in Rust