bump rupicola

Author: andres-erbsen

rupicola

@@ -110,7 +110,7 @@ Section Expr.
     fun c x y =>
       if literal_eqb x 0
       then if literal_eqb y (2^width - 1)
-           then expr.op bopname.add (expr.literal (-1))
+           then expr.op bopname.add (expr.op1 op1.opp (expr.literal 1))
                         (expr.op bopname.eq c (expr.literal 0))
            else base_make_error _
       else base_make_error _.

src/Bedrock/Field/Translation/Expr.v

@@ -54,6 +54,7 @@ Section Defs.
     | expr.literal _ => true
     | expr.var x => negb (String.eqb x ERROR)
     | expr.load _ a => error_free_expr a
+    | expr.op1 _ x => error_free_expr x
     | expr.op _ x y => (error_free_expr x && error_free_expr y)%bool
     | expr.inlinetable _ _ index => error_free_expr index
     | expr.ite c a b => (error_free_expr c && error_free_expr a && error_free_expr b)%bool

src/Bedrock/Field/Translation/Parameters/Defaults.v

@@ -706,7 +706,7 @@ Section Expr.
              equivalent_base rep.equiv rep.Z ident.literal] in *.
       cbv [WeakestPrecondition.dexpr ident.literal] in *.
       cbn [WeakestPrecondition.expr WeakestPrecondition.expr_body
-                                    Semantics.interp_binop].
+          Semantics.interp_binop Semantics.interp_op1].
       sepsimpl_hyps.
       eapply Proper_expr; [ | eassumption ].
       repeat intro; subst.
@@ -720,7 +720,8 @@ Section Expr.
         Z.ltb_to_lt; try lia.
       all:pull_Zmod.
       all:autorewrite with zsimplify_fast.
-      all:try reflexivity.
+      all:rewrite <-?word.ring_morph_opp, ?word.unsigned_of_Z.
+      all:cbv [word.wrap]; rewrite ?Zplus_mod_idemp_l, ?Zmod_mod; trivial.
       rewrite Z.mod_opp_l_nz
         by (rewrite ?Z.mod_1_l; auto with zarith).
       Z.rewrite_mod_small.

src/Bedrock/Field/Translation/Proofs/Expr.v

@@ -502,12 +502,11 @@ Section __.
          Memory := m;
          Locals := l;
          Functions := functions }>
-      cmd.seq (cmd.set var (expr.op bopname.sub (expr.literal (-1)) (expr.var x_var)))
+      cmd.seq (cmd.set var (expr.op1 op1.not (expr.var x_var)))
               k_impl
       <{ pred (nlet_eq [var] v k) }>.
   Proof using field_representaton word_ok.
     repeat (eexists; split; eauto).
-    apply word_not_impl.
   Qed.
   Hint Extern 10 => simple eapply compile_word_not; shelve : compiler.