@@ -149,21 +149,30 @@ eth_friend(?1, ?2, ?3, ?4) = and<
149149## Another perspective
150150When 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.
152+ - A * statement* can be seen as the * constraints* of a traditional zk-circuit,
153+ which can be true or false.
154+ - A * predicate* is a relation formula, which when filled with values becomes a
155+ * statement* .
153156- An * operation* comprises the deduction rules, which are rules used to deduce
154157 new statements from previous statements or used to construct new statements
155158 from values.
156159
157-
158160$$
159- statement \cong predicate \cong constraints\\
161+ predicate \cong circuit/relation to be fulfilled\\
162+ statement \cong constraints filled with the witness\\
160163operations \cong deduction~rules
161164$$
162165
163166
167+ 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)
171+
172+
164173
165174<div style =" display :flex ;margin-left :-60px ;" >
166- <div style =" padding :10px ;max-width :50% ;" >
175+ <div style =" padding :10px ;max-width :50% ; border-right : 1 px solid #ccc ; " >
167176
168177So, for example, for the given predicate:
169178
@@ -181,9 +190,11 @@ IsWood(item, private: ingreds,inputs,key)=AND(
181190We can view it as:
182191
183192The * statement* ` IsWood(item) ` is ` true ` if and only if:<br >
184- $\exists$ ` ingreds ` , ` inputs ` , ` key `
193+ $\exists$ ` item ` , ` ingreds ` , ` inputs ` , ` key `
185194 such that the following statements hold:
186- ` ItemDef ` , ` Equal ` , ` DictContains ` .
195+ - ` ItemDef(0x1234, ingreds, inputs, key) `
196+ - ` Equal(inputs, {}) `
197+ - ` DictContains(ingreds, "blueprint", "wood") `
187198
188199</div >
189200</div >
0 commit comments