fix arch-params-proof

Author: vbgl

proofs/compiler/arch_params_proof.v

@@ -1,4 +1,5 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
+From ITree Require Import ITree.
 Require Import
   compiler_util
   expr
@@ -58,6 +59,7 @@ Record h_lowering_params
         {E E0: Type -> Type}
         {wE : with_Error E E0}
         {rE : EventRels E0}
+        {rndE0 : RndEvent syscall_state -< E0}
         {p : prog}
         {ev : extra_val_t}
         (options : lowering_options)
@@ -109,6 +111,7 @@ Record h_lower_addressing_params
         {E E0: Type -> Type}
         {wE : with_Error E E0}
         {rE : EventRels E0}
+        {rndE0 : RndEvent syscall_state -< E0}
         {fresh_reg}
         {p p' : sprog}
         {ev fn},