Skip to content

Commit 8b8f1f1

Browse files
hellwolfhellwolf
committed
added data versioning article.
1 parent bf05f39 commit 8b8f1f1

File tree

6 files changed

+158
-2
lines changed

6 files changed

+158
-2
lines changed

‎content/docs/advanced/category-dsl.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,5 @@ template = "docs/page.html"
88
toc = true
99
lead = "There is no lambda, no variable in YulDSL."
1010
+++
11+
12+
(🚧 COMING SOON...)

‎content/docs/advanced/linear-types.md‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
+++
2+
title = "Using Linear Types in Yolc"
3+
date = 2025-05-19
4+
weight = 5
5+
template = "docs/page.html"
6+
7+
[extra]
8+
toc = true
9+
lead = "From linear lambda to data versioning."
10+
+++
11+
12+
(🚧 COMING SOON...)

‎content/docs/concepts/adt.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,5 @@ template = "docs/page.html"
77
[extra]
88
toc = true
99
+++
10+
11+
(🚧 COMING SOON...)

‎content/docs/concepts/data-versioning.md‎

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,144 @@ template = "docs/page.html"
66

77
[extra]
88
toc = true
9+
lead = "In two examples."
910
+++
11+
12+
Yolc has a unique safety feature called "data versioning." The key idea is that in compile time, Yolc tracks the state
13+
of the EVM when data was read, aka. versioning the data. Later on, if there is any chance that the state of the virtue
14+
machine is updated, then the previously read data must be considered outdated and shall not be used again.
15+
16+
Here are two inspiring examples to show how this safety feature can prevent bugs
17+
18+
## Example 1: Requiring "from != to"
19+
20+
In the following example, an innocuous ERC20 transfer function which does routinely:
21+
22+
1) Retrieve sender and receiver's balances.
23+
2) Calculate new balances.
24+
3) Do something with the new balances.
25+
4) Update balances.
26+
27+
```haskell
28+
transfer :: OmniFn (ADDR -> U256 -> BOOL)
29+
transfer = $lfn $ ylvm'pv
30+
\to amount -> LVM.do
31+
Ur from <- ycaller
32+
33+
-- ⛔ INCORRECT CODE, CANNOT PASS COMPILATION:
34+
Ur senderBalance <- ycall balanceOf (ver from)
35+
Ur receiverBalance <- ycall balanceOf (ver to)
36+
37+
-- calculate new balances
38+
Ur (newSenderBalance, newReceiverBalance) <- ywithrv
39+
@(U256 -> U256 -> U256 -> (U256, U256))
40+
(ver amount, senderBalance, receiverBalance)
41+
\amount' senderBalance' receiverBalance' ->
42+
be (senderBalance' - amount', receiverBalance' + amount')
43+
44+
-- Do something with the new balances and reuse later to avoid recalculation
45+
-- ...
46+
47+
-- WARNING: THIS IS WRONG
48+
-- Have you found the issue?
49+
balances #-> from <<:= newSenderBalance
50+
balances #-> to <<:= newReceiverBalance
51+
```
52+
53+
However, there is a deadly mistake: it should check that if "from != to".
54+
55+
In canonical ERC20 examples, it typically checks the condition. It may seem contrived, but in custom transfer
56+
implementations, where such intermediate values may seem an optimization, such a mistake can occur.
57+
58+
Nonetheless, with Yolc, it is a compile-time error:
59+
60+
```
61+
src/ERC20.hs:63:23: error: [GHC-22250]
62+
• Outdated data version
63+
• In a stmt of a 'do' block:
64+
balances #-> to <<:= newReceiverBalance
65+
...
66+
```
67+
68+
With **outdated data version**, what Yolc says is: "Since you don't provide a "run-time witness" (we will explain this
69+
concept in a future article) that 'from' not equal 'to', I have no choice but assume that newReceiverBalance may have
70+
changed since then." And Yolc throws an error instead.
71+
72+
Magic! But how can I write the correct code instead?
73+
74+
You can always rearrange the code, such that you perform the update after each reading:
75+
76+
```haskell
77+
Ur senderBalance <- ycall balanceOf (ver from)
78+
Ur newSenderBalance <- ywithrv_1 @(U256 -> U256 -> U256) (ver amount, senderBalance)
79+
\amount' senderBalance' -> senderBalance' - amount'
80+
balances #-> from <<:= newSenderBalance
81+
82+
Ur receiverBalance <- ycall balanceOf (ver to)
83+
Ur newReceiverBalance <- ywithrv_1 @(U256 -> U256 -> U256) (ver amount, receiverBalance)
84+
\amount' receiverBalance' -> receiverBalance' + amount'
85+
balances #-> to <<:= newReceiverBalance
86+
```
87+
88+
In a more general setting, there are two more solutions:
89+
90+
1) Provide a run-time witness in a type-safe way that compiler is happy with. We will explain this solution in a future
91+
article.
92+
2) Re-read the data! This solution is expensive, but always works.
93+
94+
## Example 2: Type-Safe "Checks Effects Interactions"
95+
96+
Another data version-related common bug is re-entrancy attack vulnerability, where the data you are using may be
97+
outdated due to an non-trusted external call may have altered it. Common Solidity practice such as "check effects
98+
interactions" provide a good guideline of how to prevent this from happening; open-zeppelin also provides
99+
reentrance-lock that serves as a hammer to the problem.
100+
101+
Yolc data version provides a type-safe solution to this, instead.
102+
103+
Here is a mint function:
104+
105+
```haskell
106+
mint :: OmniFn (ADDR -> U256 -> ())
107+
mint = $lfn $ ylvm'pv
108+
\to amount -> LVM.do
109+
Ur balanceBefore <- ycall balanceOf (ver to)
110+
111+
-- calculate new balance
112+
Ur newAmount <- ywithrv_1 @(U256 -> U256 -> U256)
113+
(balanceBefore, ver amount)
114+
(\x y -> x + y)
115+
116+
-- call **untrusted** external contract onTokenMinted
117+
ycall (to @-> onTokenMinted) (ver to) (ver amount)
118+
119+
-- update balance
120+
balances #-> to <<:= newAmount
121+
```
122+
123+
And it has a glaring re-entrancy vulnerability. It certainly didn't follow the "checks-effects-interactions"
124+
guideline. Again, Yolc catches it:
125+
126+
```
127+
src/ERC20.hs:85:21: error: [GHC-22250]
128+
• Outdated data version
129+
• In a stmt of a 'do' block: balances #-> to <<:= newAmount
130+
...
131+
```
132+
133+
We get the same **outdated data version** error!
134+
135+
# Under The Hood
136+
137+
Data versioning is only the beginning of how Yolc explores more type-level safety guarantees.
138+
139+
Under the hood, it is the [GHC's
140+
"LinearTypes"](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html) feature provides the horse
141+
power. One usage of linear types allows type-level enforcement of linearly transitioned state, a form of model checking
142+
closely related to Linear-time Temporal Logic (LTL). We will demonstrate such a claim in the future development Yolc.
143+
144+
Linear types is also closely related to uniqueness types. Some claims GHC's linearity-on-arrows is more general purpose
145+
than uniqueness types. An example of uniqueness type is the borrow-checker in Rust to ensure unique ownership of a
146+
resource handle enforced in type-level.
147+
148+
Read [here](/docs/advanced/linear-types) to learn more about how linear types is used in Yolc to internally for not just
149+
data versioning.

‎content/docs/concepts/edsl.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ template = "docs/page.html"
66

77
[extra]
88
toc = true
9-
lead = "This makes Yolc expressive."
9+
lead = "Haskell makes Yolc expressive."
1010
+++
1111

1212
# What Is Deep Embedding

‎content/docs/help/_index.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
+++
22
title = "Help"
33
sort_by = "weight"
4-
weight = 99
4+
weight = 40
55
draft = false
66
+++

0 commit comments

Comments
 (0)