@@ -20,6 +20,7 @@ use crate::types::Final;
20
20
use crate :: { analysis, Ihr } ;
21
21
use crate :: { Cmr , FailEntropy , Value } ;
22
22
use frame:: Frame ;
23
+ use simplicity_sys:: ffi:: UWORD ;
23
24
24
25
pub use self :: limits:: LimitError ;
25
26
@@ -242,7 +243,12 @@ impl BitMachine {
242
243
Ok ( tracker)
243
244
}
244
245
245
- fn exec_with_tracker < J : Jet , T : CaseTracker > (
246
+ /// Execute the given `program` on the Bit Machine, using the given environment and tracker.
247
+ ///
248
+ /// ## Precondition
249
+ ///
250
+ /// The Bit Machine is constructed via [`Self::for_program()`] to ensure enough space.
251
+ pub fn exec_with_tracker < J : Jet , T : ExecTracker < J > > (
246
252
& mut self ,
247
253
program : & RedeemNode < J > ,
248
254
env : & J :: Environment ,
@@ -371,7 +377,7 @@ impl BitMachine {
371
377
}
372
378
}
373
379
node:: Inner :: Witness ( value) => self . write_value ( value) ,
374
- node:: Inner :: Jet ( jet) => self . exec_jet ( * jet, env) ?,
380
+ node:: Inner :: Jet ( jet) => self . exec_jet ( * jet, env, tracker ) ?,
375
381
node:: Inner :: Word ( value) => self . write_value ( value. as_value ( ) ) ,
376
382
node:: Inner :: Fail ( entropy) => {
377
383
return Err ( ExecutionError :: ReachedFailNode ( * entropy) )
@@ -408,7 +414,12 @@ impl BitMachine {
408
414
}
409
415
}
410
416
411
- fn exec_jet < J : Jet > ( & mut self , jet : J , env : & J :: Environment ) -> Result < ( ) , JetFailed > {
417
+ fn exec_jet < J : Jet , T : ExecTracker < J > > (
418
+ & mut self ,
419
+ jet : J ,
420
+ env : & J :: Environment ,
421
+ tracker : & mut T ,
422
+ ) -> Result < ( ) , JetFailed > {
412
423
use crate :: ffi:: c_jets:: frame_ffi:: { c_readBit, c_writeBit, CFrameItem } ;
413
424
use crate :: ffi:: c_jets:: uword_width;
414
425
use crate :: ffi:: ffi:: UWORD ;
@@ -494,13 +505,15 @@ impl BitMachine {
494
505
let output_width = jet. target_ty ( ) . to_bit_width ( ) ;
495
506
// Input buffer is implicitly referenced by input read frame!
496
507
// Same goes for output buffer
497
- let ( input_read_frame, _input_buffer ) = unsafe { get_input_frame ( self , input_width) } ;
508
+ let ( input_read_frame, input_buffer ) = unsafe { get_input_frame ( self , input_width) } ;
498
509
let ( mut output_write_frame, output_buffer) = unsafe { get_output_frame ( output_width) } ;
499
510
500
511
let jet_fn = jet. c_jet_ptr ( ) ;
501
512
let c_env = J :: c_jet_env ( env) ;
502
513
let success = jet_fn ( & mut output_write_frame, input_read_frame, c_env) ;
503
514
515
+ tracker. track_jet_call ( & jet, & input_buffer, & output_buffer, success) ;
516
+
504
517
if !success {
505
518
Err ( JetFailed )
506
519
} else {
@@ -510,25 +523,33 @@ impl BitMachine {
510
523
}
511
524
}
512
525
513
- /// A type that keeps track of which case branches were executed
514
- /// during the execution of the Bit Machine.
526
+ /// A type that keeps track of Bit Machine execution.
515
527
///
516
- /// The trait is implemented for [`SetTracker`], which does the actual tracking ,
528
+ /// The trait is implemented for [`SetTracker`], that tracks which case branches were executed ,
517
529
/// and it is implemented for [`NoTracker`], which is a dummy tracker that is
518
530
/// optimized out by the compiler.
519
531
///
520
532
/// The trait enables us to turn tracking on or off depending on a generic parameter.
521
- trait CaseTracker {
533
+ pub trait ExecTracker < J : Jet > {
522
534
/// Track the execution of the left branch of the case node with the given `ihr`.
523
535
fn track_left ( & mut self , ihr : Ihr ) ;
524
536
525
537
/// Track the execution of the right branch of the case node with the given `ihr`.
526
538
fn track_right ( & mut self , ihr : Ihr ) ;
539
+
540
+ /// Track the execution of a `jet` call with the given `input_buffer`, `output_buffer`, and call result `success`.
541
+ fn track_jet_call (
542
+ & mut self ,
543
+ jet : & J ,
544
+ input_buffer : & [ UWORD ] ,
545
+ output_buffer : & [ UWORD ] ,
546
+ success : bool ,
547
+ ) ;
527
548
}
528
549
529
550
/// Tracker of executed left and right branches for each case node.
530
551
#[ derive( Clone , Debug , Default ) ]
531
- pub ( crate ) struct SetTracker {
552
+ pub struct SetTracker {
532
553
left : HashSet < Ihr > ,
533
554
right : HashSet < Ihr > ,
534
555
}
@@ -545,23 +566,28 @@ impl SetTracker {
545
566
}
546
567
}
547
568
569
+ /// Tracker that does not do anything (noop).
548
570
#[ derive( Copy , Clone , Debug ) ]
549
- struct NoTracker ;
571
+ pub struct NoTracker ;
550
572
551
- impl CaseTracker for SetTracker {
573
+ impl < J : Jet > ExecTracker < J > for SetTracker {
552
574
fn track_left ( & mut self , ihr : Ihr ) {
553
575
self . left . insert ( ihr) ;
554
576
}
555
577
556
578
fn track_right ( & mut self , ihr : Ihr ) {
557
579
self . right . insert ( ihr) ;
558
580
}
581
+
582
+ fn track_jet_call ( & mut self , _: & J , _: & [ UWORD ] , _: & [ UWORD ] , _: bool ) { }
559
583
}
560
584
561
- impl CaseTracker for NoTracker {
585
+ impl < J : Jet > ExecTracker < J > for NoTracker {
562
586
fn track_left ( & mut self , _: Ihr ) { }
563
587
564
588
fn track_right ( & mut self , _: Ihr ) { }
589
+
590
+ fn track_jet_call ( & mut self , _: & J , _: & [ UWORD ] , _: & [ UWORD ] , _: bool ) { }
565
591
}
566
592
567
593
/// Errors related to simplicity Execution
0 commit comments