@@ -20,6 +20,7 @@ use crate::types::Final;
2020use crate :: { analysis, Ihr } ;
2121use crate :: { Cmr , FailEntropy , Value } ;
2222use frame:: Frame ;
23+ use simplicity_sys:: ffi:: UWORD ;
2324
2425pub use self :: limits:: LimitError ;
2526
@@ -242,7 +243,12 @@ impl BitMachine {
242243 Ok ( tracker)
243244 }
244245
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 > > (
246252 & mut self ,
247253 program : & RedeemNode < J > ,
248254 env : & J :: Environment ,
@@ -371,7 +377,7 @@ impl BitMachine {
371377 }
372378 }
373379 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 ) ?,
375381 node:: Inner :: Word ( value) => self . write_value ( value. as_value ( ) ) ,
376382 node:: Inner :: Fail ( entropy) => {
377383 return Err ( ExecutionError :: ReachedFailNode ( * entropy) )
@@ -408,7 +414,12 @@ impl BitMachine {
408414 }
409415 }
410416
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 > {
412423 use crate :: ffi:: c_jets:: frame_ffi:: { c_readBit, c_writeBit, CFrameItem } ;
413424 use crate :: ffi:: c_jets:: uword_width;
414425 use crate :: ffi:: ffi:: UWORD ;
@@ -494,13 +505,15 @@ impl BitMachine {
494505 let output_width = jet. target_ty ( ) . to_bit_width ( ) ;
495506 // Input buffer is implicitly referenced by input read frame!
496507 // 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) } ;
498509 let ( mut output_write_frame, output_buffer) = unsafe { get_output_frame ( output_width) } ;
499510
500511 let jet_fn = jet. c_jet_ptr ( ) ;
501512 let c_env = J :: c_jet_env ( env) ;
502513 let success = jet_fn ( & mut output_write_frame, input_read_frame, c_env) ;
503514
515+ tracker. track_jet_call ( & jet, & input_buffer, & output_buffer, success) ;
516+
504517 if !success {
505518 Err ( JetFailed )
506519 } else {
@@ -510,25 +523,33 @@ impl BitMachine {
510523 }
511524}
512525
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.
515527///
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 ,
517529/// and it is implemented for [`NoTracker`], which is a dummy tracker that is
518530/// optimized out by the compiler.
519531///
520532/// The trait enables us to turn tracking on or off depending on a generic parameter.
521- trait CaseTracker {
533+ pub trait ExecTracker < J : Jet > {
522534 /// Track the execution of the left branch of the case node with the given `ihr`.
523535 fn track_left ( & mut self , ihr : Ihr ) ;
524536
525537 /// Track the execution of the right branch of the case node with the given `ihr`.
526538 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+ ) ;
527548}
528549
529550/// Tracker of executed left and right branches for each case node.
530551#[ derive( Clone , Debug , Default ) ]
531- pub ( crate ) struct SetTracker {
552+ pub struct SetTracker {
532553 left : HashSet < Ihr > ,
533554 right : HashSet < Ihr > ,
534555}
@@ -545,23 +566,28 @@ impl SetTracker {
545566 }
546567}
547568
569+ /// Tracker that does not do anything (noop).
548570#[ derive( Copy , Clone , Debug ) ]
549- struct NoTracker ;
571+ pub struct NoTracker ;
550572
551- impl CaseTracker for SetTracker {
573+ impl < J : Jet > ExecTracker < J > for SetTracker {
552574 fn track_left ( & mut self , ihr : Ihr ) {
553575 self . left . insert ( ihr) ;
554576 }
555577
556578 fn track_right ( & mut self , ihr : Ihr ) {
557579 self . right . insert ( ihr) ;
558580 }
581+
582+ fn track_jet_call ( & mut self , _: & J , _: & [ UWORD ] , _: & [ UWORD ] , _: bool ) { }
559583}
560584
561- impl CaseTracker for NoTracker {
585+ impl < J : Jet > ExecTracker < J > for NoTracker {
562586 fn track_left ( & mut self , _: Ihr ) { }
563587
564588 fn track_right ( & mut self , _: Ihr ) { }
589+
590+ fn track_jet_call ( & mut self , _: & J , _: & [ UWORD ] , _: & [ UWORD ] , _: bool ) { }
565591}
566592
567593/// Errors related to simplicity Execution
0 commit comments