Add comments

charon/src/driver.rs

@@ -261,6 +261,8 @@ pub fn translate(
     // **WARNING**: this pass uses the fact that the dynamic checks introduced by Rustc use a
     // special "assert" construct. Because of this, it must happen *before* the
     // [reconstruct_asserts] pass. See the comments in [crate::remove_dynamic_checks].
+    // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this,
+    // it must happen before passes that insert statements like [simplify_constants].
     remove_dynamic_checks::transform(&mut ctx);
 
     // # Micro-pass: desugar the constants to other values/operands as much

charon/src/transform/remove_dynamic_checks.rs

@@ -74,7 +74,7 @@ fn remove_dynamic_checks(ctx: &mut TransCtx, block: &mut BlockData) {
         //   r := x checked.+ y;
         //   assert(move r.1 == false);
         // They only happen in constants because we compile with `-C opt-level=3`. They're tricky
-        // to remove so we leave them.
+        // to remove so we leave them for now.
         [.., Statement {
             content:
                 RawStatement::Assign(result, Rvalue::BinaryOp(BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul, ..)),