Update chacha proof

clementblaudeau · clementblaudeau · commit 9533fe5ee6e9 · 2025-10-06T10:35:54.000+02:00
diff --git a/examples/lean_chacha20/proofs/lean/extraction/Lean_chacha20_manual_edit.lean b/examples/lean_chacha20/proofs/lean/extraction/Lean_chacha20_manual_edit.lean
@@ -749,7 +749,6 @@ theorem Lean_chacha20.chacha20_quarter_round_spec a b c d state:
   intros
   mvcgen [Lean_chacha20.chacha20_quarter_round,
           Lean_chacha20.chacha20_line,
-          Rust_primitives.Hax.Machine_int.bitxor,
           Result.ofOption, ]
   <;> try omega
 
