Improve semantics of Oarray

proofs/compiler/stack_alloc_proof_1.v

@@ -7019,7 +7019,7 @@ Lemma fill_fill_mem table rmap vme m0 s1 s2 sr len addr l a :
   exists m2, fill_mem (emem s2) addr l = ok m2.
 Proof.
   move=> hvs hwf ok_addr.
-  rewrite /WArray.fill /fill_mem.
+  rewrite /WArray.fill /WArray.fill_aux /fill_mem.
   t_xrbindP=> /eqP hsize [i {}a] /= hfold _.
 
   have hvp: forall k, 0 <= k < len -> validw (emem s2) Aligned (addr + wrepr _ k)%R U8.

proofs/lang/sem_op_typed.v

@@ -189,10 +189,20 @@ Definition sem_opN_typed (o: opN) :
       let ty := curry (A := cint) (sz %/ pe) (λ vs, ok (wpack sz pe vs)) in
       ecast l (sem_prod l _) (esym (map_nseq _ _ _)) ty
   | Oarray len =>
-      let ty := curry (A := cword U8) (Pos.to_nat len) (λ bs, WArray.fill len (rev bs)) in
+      let ty := sem_prod_app (collect (Pos.to_nat len) [::]) (λ vs : seq (sem_t (cword U8)), WArray.fill len vs) in
       ecast l (sem_prod l _) (esym (map_nseq _ _ _)) ty
   | Ocombine_flags cf =>
       fun b0 b1 b2 b3 => ok (sem_combine_flags cf b0 b1 b2 b3)
   end.
 
+Lemma sem_opN_typed_ok (op: opN) :
+  sem_forall (@is_ok _ _) _ (sem_opN_typed op).
+Proof.
+  case: op => // [ ws pe | len ] /=; rewrite -> map_nseq => /=.
+  + by case: ws pe => - [].
+  apply: sem_forall_prod_app (size_collect (Pos.to_nat len) [::]) => bytes /=.
+  rewrite ssrnat.addn0 /WArray.fill => hlen; rewrite hlen eqxx /=.
+  by case/is_okP: (WArray.fill_aux_ok (Nat.eq_le_incl _ _ hlen)) => ? ->.
+Qed.
+
 End WITH_PARAMS.

proofs/lang/sem_type.v

@@ -148,6 +148,29 @@ Lemma sem_prod_ok_error {T: Type} (tin : seq ctype) (o : sem_prod tin T) e :
   sem_forall (fun et => et <> Error e) tin (sem_prod_ok tin o).
 Proof. by elim: tin o => /= [o | a l hrec o v]; eauto. Qed.
 
+Lemma sem_forall_m {T: Type} (P Q: T → Prop) (tin: seq ctype) (o: sem_prod tin T) :
+  (∀ t, P t → Q t) →
+  sem_forall P tin o →
+  sem_forall Q tin o.
+Proof. move => ?; elim: tin o => // t ts ih o h /= v; exact: ih. Qed.
+
+(* -------------------------------------------------------------------- *)
+Fixpoint collect {A: ctype} (n: nat) : seq (sem_t A) → sem_prod (nseq n A) (seq (sem_t A)) :=
+  match n return seq (sem_t A) → sem_prod (nseq n A) (seq (sem_t A)) with
+  | 0 => rev
+  | S n => λ (acc: seq (sem_t A)) (a : sem_t A), (collect n (a :: acc) : sem_prod (nseq n A) (seq (sem_t A)))
+  end.
+
+Lemma size_collect {A} n acc :
+  sem_forall (λ x, size x = n + size acc) (nseq n A) (collect n acc).
+Proof.
+  elim: n acc.
+  + by move => acc; rewrite /= size_rev.
+  move => n ih acc /= a /=.
+  move: ih => /(_ (a :: acc)) /=.
+  by apply: sem_forall_m => x; rewrite addSnnS.
+Qed.
+
 (* -------------------------------------------------------------------- *)
 
 Notation wmsf := (word msf_size).
@@ -212,3 +235,14 @@ Fixpoint app_sopn A ts : sem_prod ts (exec A) → seq T → exec A :=
   end.
 
 End APP.
+
+(* -------------------------------------------------------------------- *)
+Lemma sem_forall_prod_app {A B} (f: A → B) (P: A → Prop) (Q: B → Prop) tin x :
+  (∀ a, P a → Q (f a)) →
+  sem_forall P tin x →
+  sem_forall Q tin (sem_prod_app x f).
+Proof.
+  move => hpq.
+  elim: tin x; first by move => x; exact: hpq.
+  move => t ts ih o hPo /= v; exact: ih.
+Qed.