@@ -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,20 +523,28 @@ 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.
@@ -548,20 +569,24 @@ impl SetTracker {
548569#[ derive( Copy , Clone , Debug ) ]
549570struct NoTracker ;
550571
551- impl CaseTracker for SetTracker {
572+ impl < J : Jet > ExecTracker < J > for SetTracker {
552573 fn track_left ( & mut self , ihr : Ihr ) {
553574 self . left . insert ( ihr) ;
554575 }
555576
556577 fn track_right ( & mut self , ihr : Ihr ) {
557578 self . right . insert ( ihr) ;
558579 }
580+
581+ fn track_jet_call ( & mut self , _: & J , _: & [ UWORD ] , _: & [ UWORD ] , _: bool ) { }
559582}
560583
561- impl CaseTracker for NoTracker {
584+ impl < J : Jet > ExecTracker < J > for NoTracker {
562585 fn track_left ( & mut self , _: Ihr ) { }
563586
564587 fn track_right ( & mut self , _: Ihr ) { }
588+
589+ fn track_jet_call ( & mut self , _: & J , _: & [ UWORD ] , _: & [ UWORD ] , _: bool ) { }
565590}
566591
567592/// Errors related to simplicity Execution
0 commit comments