Skip to content

Commit ffbe94d

Browse files
committed
update example with @artwyman IsComposite suggestion & transitive_eq example
1 parent 28ea3e8 commit ffbe94d

File tree

1 file changed

+19
-18
lines changed

1 file changed

+19
-18
lines changed

book/src/simpleexample.md

Lines changed: 19 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -149,52 +149,53 @@ eth_friend(?1, ?2, ?3, ?4) = and<
149149
## Another perspective
150150
When working with statements and operations, it might be useful to see them from another perspective:
151151

152-
- A *statement* can be seen as the *constraints* of a traditional zk-circuit,
153-
which can be true or false.
154152
- A *predicate* is a relation formula, which when filled with values becomes a
155153
*statement*.
154+
- A *statement* can be seen as the *constraints* of a traditional zk-circuit,
155+
which can be true or false.
156156
- An *operation* comprises the deduction rules, which are rules used to deduce
157157
new statements from previous statements or used to construct new statements
158158
from values.
159159

160160
$$
161-
predicate \cong circuit/relation to be fulfilled\\
162-
statement \cong constraints filled with the witness\\
161+
predicate \cong circuit/relation~to~be~fulfilled\\
162+
statement \cong constraints~filled~with~the~witness\\
163163
operations \cong deduction~rules
164164
$$
165165

166166

167167
For example,
168-
- `Equal` for integers is a predicate.
169-
- `5 Equal 5` is a statement (true)
170-
- `5 Equal 4` is a statement (false)
168+
- `Equal` for integers is a *predicate*
169+
- `st_1 = Equal(A, B)` is a *statement*
170+
- `st_2 = Equal(B, C)` is a *statement*
171+
- `st_3 = TransitiveEqualFromStatements(st_1, st_2)` is an *operation*, which yields the statement `st_3 = Equal(A, C)`
172+
171173

172174

173175

174-
<div style="display:flex;margin-left:-60px;">
176+
<div style="display:flex;">
175177
<div style="padding:10px;max-width:50%; border-right:1px solid #ccc;">
176178

177179
So, for example, for the given predicate:
178180

179181
```
180-
IsWood(item, private: ingreds,inputs,key)=AND(
181-
ItemDef(item, ingreds, inputs, key)
182-
Equal(inputs, {{}})
183-
DictContains(ingreds, "blueprint", "wood")
184-
}
182+
IsComposite(n, private: a, b) = AND(
183+
ProductOf(n, a, b)
184+
GtFromEntries(a, 1)
185+
GtFromEntries(b, 1)
186+
)
185187
```
186188

187189
</div>
188190
<div style="padding:10px;max-width:45%;">
189191

190192
We can view it as:
191193

192-
The *statement* `IsWood(item)` is `true` if and only if:<br>
193-
$\exists$ `item`, `ingreds`, `inputs`, `key`
194+
The *statement* `IsComposite(n)` is `true` if and only if $\exists$ `n`, `a`, `b`
194195
such that the following statements hold:
195-
- `ItemDef(0x1234, ingreds, inputs, key)`
196-
- `Equal(inputs, {})`
197-
- `DictContains(ingreds, "blueprint", "wood")`
196+
- $n = a \cdot b$
197+
- $a > 1$
198+
- $b > 1$
198199

199200
</div>
200201
</div>

0 commit comments

Comments
 (0)