@@ -220,19 +220,19 @@ impl<'a> DefaultTracker<'a> {
220220 match output. clone ( ) {
221221 NodeOutput :: Success ( mut output_frame) => {
222222 let target_ty = & node. arrow ( ) . target ;
223+ let jet_target_ty = resolve_jet_type ( & target_type ( jet) ) ;
223224
224225 // Skip the leading bit when the frame has extra padding.
225- // This occurs because jets are wrapped in AssertL (a Case combinator),
226- // which adds structure to the output frame for some jets.
227- if output_frame . len ( ) > target_ty . bit_width ( ) {
226+ // This occurs because some jets (like eq_64 etc.) are wrapped in AssertL (a Case combinator),
227+ // see compile::with_debug_symbol
228+ if target_ty . as_sum ( ) . is_some ( ) {
228229 let _ = output_frame. next ( ) ;
229230 }
230231
231232 let output_value = SimValue :: from_padded_bits ( & mut output_frame, target_ty)
232233 . expect ( "output from bit machine is always well-formed" ) ;
233234
234- let target_ty = resolve_jet_type ( & target_type ( jet) ) ;
235- Value :: reconstruct ( & StructuralValue :: from ( output_value) , & target_ty)
235+ Value :: reconstruct ( & StructuralValue :: from ( output_value) , & jet_target_ty)
236236 }
237237 _ => None ,
238238 }
@@ -524,4 +524,52 @@ mod tests {
524524 Some ( "Some((Right(0x6d521c38ec1ea15734ae22b7c46064412829c0d0579f0a713d1c04ede979026f), Right(1000)))" )
525525 ) ;
526526 }
527+ const TEST_ARITHMETIC_JETS : & str = r#"
528+ fn main() {
529+
530+ let x: u32 = 5;
531+ let y: u32 = 4;
532+
533+ let sum: (bool, u32) = jet::add_32(x, y);
534+ let prod: u64 = jet::multiply_32(x, y);
535+
536+ assert!(jet::eq_64(prod, 20));
537+ }
538+ "# ;
539+
540+ #[ test]
541+ fn test_arith_jet_trace_regression ( ) {
542+ let env = create_test_env ( ) ;
543+
544+ let program = TemplateProgram :: new ( TEST_ARITHMETIC_JETS ) . unwrap ( ) ;
545+ let program = program. instantiate ( Arguments :: default ( ) , true ) . unwrap ( ) ;
546+ let satisfied = program. satisfy ( WitnessValues :: default ( ) ) . unwrap ( ) ;
547+
548+ let ( mut tracker, _, jet_store) = create_test_tracker ( & satisfied. debug_symbols ) ;
549+
550+ let _ = satisfied. redeem ( ) . prune_with_tracker ( & env, & mut tracker) ;
551+
552+ let jets = jet_store. borrow ( ) ;
553+
554+ assert_eq ! (
555+ jets. get( "add_32" ) . unwrap( ) . 0 ,
556+ Some ( vec![ "5" . to_string( ) , "4" . to_string( ) ] )
557+ ) ;
558+ assert_eq ! (
559+ jets. get( "add_32" ) . unwrap( ) . 1 ,
560+ Some ( "(false, 9)" . to_string( ) )
561+ ) ;
562+
563+ assert_eq ! (
564+ jets. get( "multiply_32" ) . unwrap( ) . 0 ,
565+ Some ( vec![ "5" . to_string( ) , "4" . to_string( ) ] )
566+ ) ;
567+ assert_eq ! ( jets. get( "multiply_32" ) . unwrap( ) . 1 , Some ( "20" . to_string( ) ) ) ;
568+
569+ assert_eq ! (
570+ jets. get( "eq_64" ) . unwrap( ) . 0 ,
571+ Some ( vec![ "20" . to_string( ) , "20" . to_string( ) ] )
572+ ) ;
573+ assert_eq ! ( jets. get( "eq_64" ) . unwrap( ) . 1 , Some ( "true" . to_string( ) ) ) ;
574+ }
527575}
0 commit comments