diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-27 15:22:37 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-27 15:22:37 +0200 |
| commit | 9d3103177c6838541f3a21caa6716381a50dc817 (patch) | |
| tree | 5302d332dff219d7a43337e0da59d589872e2175 /kvx/SelectOpproof.v | |
| parent | d71e693e1b4844453f4b3c6356e514e8da4162e8 (diff) | |
| download | compcert-kvx-9d3103177c6838541f3a21caa6716381a50dc817.tar.gz compcert-kvx-9d3103177c6838541f3a21caa6716381a50dc817.zip | |
generate insf
Diffstat (limited to 'kvx/SelectOpproof.v')
| -rw-r--r-- | kvx/SelectOpproof.v | 64 |
1 files changed, 32 insertions, 32 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index 1d9f3f91..0ede1e2d 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -839,40 +839,40 @@ Proof. ** unfold Int.max_unsigned, Int.modulus. simpl. lia. - * apply DEFAULT. - + clear Risbitfield. - clear zstop. - set (zstop := (int_highest_bit nmask)). - destruct (is_bitfield _ _) eqn:Risbitfield. - ++ destruct (and_dec _ _) as [[Rmask Rnmask] | ]. - * subst y. subst x. - TrivialExists. simpl. f_equal. - rewrite Val.or_commut. - unfold insf. - rewrite Risbitfield. - rewrite Rmask. - rewrite Rnmask. - simpl. - unfold bitfield_mask. - subst zstart. - rewrite (Val.or_commut (Val.and v0 _)). - rewrite (Val.or_commut (Val.and v0 _)). - destruct v1; simpl; trivial. - unfold Int.ltu, Int.iwordsize, Int.zwordsize. - rewrite Int.unsigned_repr. - ** rewrite Int.unsigned_repr. - *** simpl. - rewrite Int.shl_zero. - reflexivity. - *** simpl. - unfold Int.max_unsigned, Int.modulus. + * clear Risbitfield. clear o. + clear zstop. + set (zstop := (int_highest_bit nmask)). + destruct (is_bitfield _ _) eqn:Risbitfield. + ++ destruct (and_dec _ _) as [[Rmask Rnmask] | ]. + ** subst y. subst x. + TrivialExists. simpl. f_equal. + rewrite Val.or_commut. + unfold insf. + rewrite Risbitfield. + rewrite Rmask. + rewrite Rnmask. + simpl. + unfold bitfield_mask. + subst zstart. + rewrite (Val.or_commut (Val.and v0 _)). + rewrite (Val.or_commut (Val.and v0 _)). + destruct v1; simpl; trivial. + unfold Int.ltu, Int.iwordsize, Int.zwordsize. + rewrite Int.unsigned_repr. + *** rewrite Int.unsigned_repr. + **** simpl. + rewrite Int.shl_zero. + reflexivity. + **** simpl. + unfold Int.max_unsigned, Int.modulus. + simpl. + lia. + *** unfold Int.max_unsigned, Int.modulus. simpl. lia. - ** unfold Int.max_unsigned, Int.modulus. - simpl. - lia. - * apply DEFAULT. - ++ apply DEFAULT. + ** apply DEFAULT. + ++ apply DEFAULT. + + apply DEFAULT. - apply DEFAULT. Qed. |