Bug: faulty control-flow reconstruction in ML-DSA

[msprotz]

Found while looking at something unrelated for @franziskuskiefer

If I dump the LLBC I receive from Charon while running cd libcrux/libcrux-ml-dsa && ./boring.sh on https://github.com/cryspen/libcrux/tree/franziskus/mldsa-c-ci (commit 26c593e) I get the following:

fn libcrux_ml_dsa::encoding::signature::{libcrux_ml_dsa::encoding::signature::Signature<SIMDUnit, COMMITMENT_HASH_SIZE, COLUMNS_IN_A, ROWS_IN_A>[TraitClause@0, TraitClause@1]}::deserialize<0, SIMDUnit, COMMITMENT_HASH_SIZE, COLUMNS_IN_A, ROWS_IN_A, GAMMA1_EXPONENT, GAMMA1_RING_ELEMENT_SIZE, MAX_ONES_IN_HINT, SIGNATURE_SIZE>(serialized^1 : &0 (@Array<u8, SIGNATURE_SIZE>)) -> core::result::Result<libcrux_ml_dsa::encoding::signature::Signature<SIMDUnit, COMMITMENT_HASH_SIZE, COLUMNS_IN_A, ROWS_IN_A>[TraitClause@0, TraitClause@1], libcrux_ml_dsa::types::VerificationError>[core::marker::Sized<libcrux_ml_dsa::encoding::signature::Signature<SIMDUnit, COMMITMENT_HASH_SIZE, COLUMNS_IN_A, ROWS_IN_A>[TraitClause@0, TraitClause@1]>, core::marker::Sized<libcrux_ml_dsa::types::VerificationError>]
  where
    [TraitClause@0]: core::marker::Sized<SIMDUnit>,
    [TraitClause@1]: libcrux_ml_dsa::simd::traits::Operations<SIMDUnit>,  
{
// ... lots of stuff ...
    loop {
      v@45 := copy i^41;
      v@44 := move v@45 < ROWS_IN_A;
      if (move v@44) {
        drop v@45;
        v@46 := copy malformed_hint^42;
        if (move v@46) {
          break 0
        }
        else {
          v@50 := copy i^41;
          v@49 := MAX_ONES_IN_HINT + move v@50;
          drop v@50;
          v@153 := &*(hint_serialized^8);
          v@154 := move @SliceIndexShared<'_, u8>(move v@153, copy v@49);
          v@48 := copy *(v@154);
          current_true_hints_seen^47 := cast<u8,usize> move v@48;
          drop v@48;
          fake_read current_true_hints_seen^47;
          drop v@49;
          v@53 := copy current_true_hints_seen^47;
          v@54 := copy previous_true_hints_seen^40;
          v@52 := move v@53 < move v@54;
          if (move v@52) {
            drop v@54;
            drop v@53
          }
          else {
            drop v@54;
            drop v@53;
            v@56 := copy previous_true_hints_seen^40;
            v@55 := move v@56 > MAX_ONES_IN_HINT;
            if (move v@55) {
              drop v@56
            }
            else {
              drop v@56;
              // BEGIN
              v@106 := ();
              v@51 := move v@106;
              drop v@55;
              drop v@52;
              drop v@51;
              j^57 := copy previous_true_hints_seen^40;
              fake_read j^57;
              loop {
                // lots of stuff
              };
              v@112 := ();
              v@58 := move v@112;
              drop v@78;
              drop v@60;
              drop v@59;
              drop v@58;
              v@79 := copy malformed_hint^42;
              if (move v@79) {
                v@113 := ();
                v@18 := move v@113
              }
              else {
                v@80 := copy current_true_hints_seen^47;
                previous_true_hints_seen^40 := move v@80;
                drop v@80;
                i^41 := copy i^41 + (1: usize : usize);
                v@114 := ();
                v@18 := move v@114
              };
              drop v@79;
              drop j^57;
              drop current_true_hints_seen^47;
              drop v@46;
              drop v@44;
              continue 0
              // END
            }
          };
          malformed_hint^42 := (true : bool);
          // BEGIN
          v@105 := ();
          v@51 := move v@105;
          drop v@55;
          drop v@52;
          drop v@51;
          j^57 := copy previous_true_hints_seen^40;
          fake_read j^57;
          loop {
            // lots of stuff
          };
          v@112 := ();
          v@58 := move v@112;
          drop v@78;
          drop v@60;
          drop v@59;
          drop v@58;
          v@79 := copy malformed_hint^42;
          if (move v@79) {
            v@113 := ();
            v@18 := move v@113
          }
          else {
            v@80 := copy current_true_hints_seen^47;
            previous_true_hints_seen^40 := move v@80;
            drop v@80;
            i^41 := copy i^41 + (1: usize : usize);
            v@114 := ();
            v@18 := move v@114
          };
          drop v@79;
          drop j^57;
          drop current_true_hints_seen^47;
          drop v@46;
          drop v@44;
          continue 0
          // END
        }
      }
      else {
        drop v@45;
        break 0
      }
    };

// ...

Note how the parts between BEGIN and END are repeated. (I snipped a bunch of irrelevant stuff in the middle but it's actually quite a large fragment.)

This is then throwing off my let-binding reconstruction phase that converts declare-then-assign into declare-in-the-right-location.

@sonmarcho I think this is pretty similar to the control-flow reconstruction issue I had on another internal project.

[Nadrieril]

Just checking: the reconstruction is semantically correct, right? It's just suboptimal?

Could you minimize the bug?

[msprotz]

Yes it is semantically correct, it just fails to reconstruct the original control-flow and I think one of the (large) basic blocks ends up being duplicated.

I'll try to minimize the bug, currently filing another one :-)