@@ -13,7 +13,7 @@ mod serialize;
13
13
14
14
use crate :: dag:: { DagLike , MaxSharing } ;
15
15
use crate :: jet:: Jet ;
16
- use crate :: node:: { self , CommitNode } ;
16
+ use crate :: node:: { self , CommitNode , NoWitness } ;
17
17
use crate :: { Cmr , Imr , Value , WitnessNode } ;
18
18
19
19
use std:: collections:: HashMap ;
@@ -22,7 +22,6 @@ use std::sync::Arc;
22
22
23
23
pub use self :: error:: { Error , ErrorSet } ;
24
24
pub use self :: named_node:: NamedCommitNode ;
25
- pub use self :: parse:: parse;
26
25
27
26
/// Line/column pair
28
27
///
@@ -77,6 +76,12 @@ impl WitnessOrHole {
77
76
}
78
77
}
79
78
79
+ impl < ' a > From < & ' a NoWitness > for WitnessOrHole {
80
+ fn from ( _: & NoWitness ) -> Self {
81
+ WitnessOrHole :: Witness
82
+ }
83
+ }
84
+
80
85
#[ derive( Clone , Debug , PartialEq , Eq ) ]
81
86
pub struct Forest < J : Jet > {
82
87
roots : HashMap < Arc < str > , Arc < NamedCommitNode < J > > > ,
@@ -136,7 +141,6 @@ impl<J: Jet> Forest<J> {
136
141
let mut witness_lines = vec ! [ ] ;
137
142
let mut const_lines = vec ! [ ] ;
138
143
let mut program_lines = vec ! [ ] ;
139
- let mut disc_idx = 0 ;
140
144
// Pass 1: compute string data for every node
141
145
for root in self . roots . values ( ) {
142
146
for data in root. as_ref ( ) . post_order_iter :: < MaxSharing < _ > > ( ) {
@@ -161,9 +165,8 @@ impl<J: Jet> Forest<J> {
161
165
} else if let node:: Inner :: AssertL ( _, cmr) = node. inner ( ) {
162
166
expr_str. push_str ( " #" ) ;
163
167
expr_str. push_str ( & cmr. to_string ( ) ) ;
164
- } else if let node:: Inner :: Disconnect ( _, node:: NoDisconnect ) = node. inner ( ) {
165
- expr_str. push_str ( & format ! ( " ?disc_expr_{}" , disc_idx) ) ;
166
- disc_idx += 1 ;
168
+ } else if let node:: Inner :: Disconnect ( _, hole_name) = node. inner ( ) {
169
+ expr_str. push_str ( & format ! ( " ?{}" , hole_name) ) ;
167
170
}
168
171
169
172
let arrow = node. arrow ( ) ;
@@ -205,6 +208,9 @@ impl<J: Jet> Forest<J> {
205
208
ret
206
209
}
207
210
211
+ /// Convert the forest into a witness node.
212
+ ///
213
+ /// Succeeds if the forest contains a "main" root and returns `None` otherwise.
208
214
pub fn to_witness_node (
209
215
& self ,
210
216
witness : & HashMap < Arc < str > , Arc < Value > > ,
@@ -217,99 +223,160 @@ impl<J: Jet> Forest<J> {
217
223
#[ cfg( test) ]
218
224
mod tests {
219
225
use crate :: human_encoding:: Forest ;
220
- use crate :: jet:: Core ;
221
- use crate :: { Error , Value } ;
226
+ use crate :: jet:: { Core , Jet } ;
227
+ use crate :: { BitMachine , Value } ;
222
228
use std:: collections:: HashMap ;
223
229
use std:: sync:: Arc ;
224
230
225
- #[ test]
226
- fn to_witness_node_missing_witness ( ) {
227
- let s = "
228
- wit1 := witness : 1 -> 2^32
229
- wit2 := witness : 1 -> 2^32
231
+ fn assert_finalize_ok < J : Jet > (
232
+ s : & str ,
233
+ witness : & HashMap < Arc < str > , Arc < Value > > ,
234
+ env : & J :: Environment ,
235
+ ) {
236
+ let program = Forest :: < J > :: parse ( s)
237
+ . expect ( "Failed to parse human encoding" )
238
+ . to_witness_node ( witness)
239
+ . expect ( "Forest is missing expected root" )
240
+ . finalize ( )
241
+ . expect ( "Failed to finalize" ) ;
242
+ let mut mac = BitMachine :: for_program ( & program) ;
243
+ mac. exec ( & program, env) . expect ( "Failed to run program" ) ;
244
+ }
230
245
231
- wits_are_equal := comp (pair wit1 wit2) jet_eq_32 : 1 -> 2
232
- main := comp wits_are_equal jet_verify : 1 -> 1
233
- " ;
234
- let forest = Forest :: < Core > :: parse ( s) . unwrap ( ) ;
235
- let mut witness = HashMap :: new ( ) ;
236
- witness. insert ( Arc :: from ( "wit1" ) , Value :: u32 ( 1337 ) ) ;
237
-
238
- match forest. to_witness_node ( & witness) . unwrap ( ) . finalize ( ) {
239
- Ok ( _) => panic ! ( "Insufficient witness map should fail" ) ,
240
- Err ( Error :: IncompleteFinalization ) => { }
241
- Err ( error) => panic ! ( "Unexpected error {}" , error) ,
246
+ fn assert_finalize_err < J : Jet > (
247
+ s : & str ,
248
+ witness : & HashMap < Arc < str > , Arc < Value > > ,
249
+ env : & J :: Environment ,
250
+ err_msg : & ' static str ,
251
+ ) {
252
+ let program = match Forest :: < J > :: parse ( s)
253
+ . expect ( "Failed to parse human encoding" )
254
+ . to_witness_node ( witness)
255
+ . expect ( "Forest is missing expected root" )
256
+ . finalize ( )
257
+ {
258
+ Ok ( program) => program,
259
+ Err ( error) => {
260
+ assert_eq ! ( & error. to_string( ) , err_msg) ;
261
+ return ;
262
+ }
263
+ } ;
264
+ let mut mac = BitMachine :: for_program ( & program) ;
265
+ match mac. exec ( & program, env) {
266
+ Ok ( _) => panic ! ( "Execution is expected to fail" ) ,
267
+ Err ( error) => assert_eq ! ( & error. to_string( ) , err_msg) ,
242
268
}
243
269
}
244
270
245
271
#[ test]
246
- fn parse_duplicate_witness_in_disconnected_branch ( ) {
272
+ fn filled_witness ( ) {
247
273
let s = "
248
- wit1 := witness
249
- main := comp wit1 comp disconnect iden ?dis2 unit
250
-
251
- wit1 := witness
252
- dis2 := wit1
274
+ a := witness
275
+ b := witness
276
+ main := comp
277
+ comp
278
+ pair a b
279
+ jet_lt_8
280
+ jet_verify
253
281
" ;
254
282
255
- match Forest :: < Core > :: parse ( s ) {
256
- Ok ( _ ) => panic ! ( "Duplicate witness names should fail" ) ,
257
- Err ( set ) => {
258
- let errors : Vec < _ > = set . iter ( ) . collect ( ) ;
259
- assert_eq ! ( 1 , errors . len ( ) ) ;
260
- match errors [ 0 ] {
261
- super :: error :: Error :: NameRepeated { .. } => { }
262
- error => panic ! ( "Unexpected error {}" , error ) ,
263
- }
264
- }
265
- }
283
+ let a_less_than_b = HashMap :: from ( [
284
+ ( Arc :: from ( "a" ) , Value :: u8 ( 0x00 ) ) ,
285
+ ( Arc :: from ( "b" ) , Value :: u8 ( 0x01 ) ) ,
286
+ ] ) ;
287
+ assert_finalize_ok :: < Core > ( s , & a_less_than_b , & ( ) ) ;
288
+
289
+ let b_greater_equal_a = HashMap :: from ( [
290
+ ( Arc :: from ( "a" ) , Value :: u8 ( 0x01 ) ) ,
291
+ ( Arc :: from ( "b" ) , Value :: u8 ( 0x01 ) ) ,
292
+ ] ) ;
293
+ assert_finalize_err :: < Core > ( s , & b_greater_equal_a , & ( ) , "Jet failed during execution" ) ;
266
294
}
267
295
268
296
#[ test]
269
- fn to_witness_node_unfilled_hole ( ) {
270
- let s = "
271
- wit1 := witness
272
- main := comp wit1 comp disconnect iden ?dis2 unit
273
- " ;
274
- let forest = Forest :: < Core > :: parse ( s) . unwrap ( ) ;
275
- let witness = HashMap :: new ( ) ;
276
-
277
- match forest. to_witness_node ( & witness) . unwrap ( ) . finalize ( ) {
278
- Ok ( _) => panic ! ( "Duplicate witness names should fail" ) ,
279
- Err ( Error :: IncompleteFinalization ) => { }
280
- Err ( error) => panic ! ( "Unexpected error {}" , error) ,
281
- }
297
+ fn unfilled_witness ( ) {
298
+ let witness = HashMap :: from ( [ ( Arc :: from ( "wit1" ) , Value :: u32 ( 1337 ) ) ] ) ;
299
+ assert_finalize_err :: < Core > (
300
+ "
301
+ wit1 := witness : 1 -> 2^32
302
+ wit2 := witness : 1 -> 2^32
303
+
304
+ wits_are_equal := comp (pair wit1 wit2) jet_eq_32 : 1 -> 2
305
+ main := comp wits_are_equal jet_verify : 1 -> 1
306
+ " ,
307
+ & witness,
308
+ & ( ) ,
309
+ "unable to satisfy program" ,
310
+ ) ;
282
311
}
283
312
284
313
#[ test]
285
- fn to_witness_node_pruned_witness ( ) {
314
+ fn unfilled_witness_pruned ( ) {
286
315
let s = "
287
316
wit1 := witness
288
317
wit2 := witness
289
318
main := comp (pair wit1 unit) case unit wit2
290
319
" ;
291
- let forest = Forest :: < Core > :: parse ( s) . unwrap ( ) ;
292
- let mut witness = HashMap :: new ( ) ;
293
- witness. insert ( Arc :: from ( "wit1" ) , Value :: u1 ( 0 ) ) ;
294
-
295
- match forest. to_witness_node ( & witness) . unwrap ( ) . finalize ( ) {
296
- Ok ( _) => { }
297
- Err ( e) => panic ! ( "Unexpected error {}" , e) ,
298
- }
320
+ let wit2_is_pruned = HashMap :: from ( [ ( Arc :: from ( "wit1" ) , Value :: u1 ( 0 ) ) ] ) ;
321
+ assert_finalize_ok :: < Core > ( s, & wit2_is_pruned, & ( ) ) ;
322
+
323
+ let wit2_is_missing = HashMap :: from ( [ ( Arc :: from ( "wit1" ) , Value :: u1 ( 1 ) ) ] ) ;
324
+ // FIXME The finalization should fail
325
+ // This doesn't happen because we don't run the program,
326
+ // so we cannot always determine which nodes must be pruned
327
+ assert_finalize_err :: < Core > (
328
+ s,
329
+ & wit2_is_missing,
330
+ & ( ) ,
331
+ "Execution reached a pruned branch: bf12681a76fc7c00c63e583c25cc97237337d6aca30d3f4a664075445385c648"
332
+ ) ;
333
+
334
+ let wit2_is_present = HashMap :: from ( [
335
+ ( Arc :: from ( "wit1" ) , Value :: u1 ( 1 ) ) ,
336
+ ( Arc :: from ( "wit2" ) , Value :: unit ( ) ) ,
337
+ ] ) ;
338
+ assert_finalize_ok :: < Core > ( s, & wit2_is_present, & ( ) ) ;
339
+ }
299
340
300
- witness. insert ( Arc :: from ( "wit1" ) , Value :: u1 ( 1 ) ) ;
341
+ #[ test]
342
+ fn filled_hole ( ) {
343
+ let empty = HashMap :: new ( ) ;
344
+ assert_finalize_ok :: < Core > (
345
+ "
346
+ id1 := iden : 2^256 * 1 -> 2^256 * 1
347
+ main := comp (disconnect id1 ?hole) unit
348
+ hole := unit
349
+ " ,
350
+ & empty,
351
+ & ( ) ,
352
+ ) ;
353
+ }
301
354
302
- match forest. to_witness_node ( & witness) . unwrap ( ) . finalize ( ) {
303
- Ok ( _) => { }
304
- Err ( Error :: IncompleteFinalization ) => { }
305
- Err ( e) => panic ! ( "Unexpected error {}" , e) ,
306
- }
355
+ #[ test]
356
+ fn unfilled_hole ( ) {
357
+ let empty = HashMap :: new ( ) ;
358
+ assert_finalize_err :: < Core > (
359
+ "
360
+ wit1 := witness
361
+ main := comp wit1 comp disconnect iden ?dis2 unit
362
+ " ,
363
+ & empty,
364
+ & ( ) ,
365
+ "unable to satisfy program" ,
366
+ ) ;
367
+ }
307
368
308
- witness. insert ( Arc :: from ( "wit2" ) , Value :: unit ( ) ) ;
369
+ #[ test]
370
+ fn witness_name_override ( ) {
371
+ let s = "
372
+ wit1 := witness
373
+ wit2 := wit1
374
+ main := comp wit2 iden
375
+ " ;
376
+ let wit1_populated = HashMap :: from ( [ ( Arc :: from ( "wit1" ) , Value :: unit ( ) ) ] ) ;
377
+ assert_finalize_err :: < Core > ( s, & wit1_populated, & ( ) , "unable to satisfy program" ) ;
309
378
310
- match forest. to_witness_node ( & witness) . unwrap ( ) . finalize ( ) {
311
- Ok ( _) => { }
312
- Err ( e) => panic ! ( "Unexpected error {}" , e) ,
313
- }
379
+ let wit2_populated = HashMap :: from ( [ ( Arc :: from ( "wit2" ) , Value :: unit ( ) ) ] ) ;
380
+ assert_finalize_ok :: < Core > ( s, & wit2_populated, & ( ) ) ;
314
381
}
315
382
}
0 commit comments