Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[sp2019latest] Adapt to coq/coq#18590 #1827

Merged
merged 1 commit into from
Mar 12, 2024
Merged

[sp2019latest] Adapt to coq/coq#18590 #1827

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions src/Algebra/Group.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,10 +97,10 @@ Section GroupByIsomorphism.

Class isomorphic_groups :=
{
isomorphic_groups_group_G :> @group G EQ OP ID INV;
isomorphic_groups_group_H :> @group H eq op id inv;
isomorphic_groups_hom_GH :> @Monoid.is_homomorphism G EQ OP H eq op phi;
isomorphic_groups_hom_HG :> @Monoid.is_homomorphism H eq op G EQ OP phi';
isomorphic_groups_group_G :: @group G EQ OP ID INV;
isomorphic_groups_group_H :: @group H eq op id inv;
isomorphic_groups_hom_GH :: @Monoid.is_homomorphism G EQ OP H eq op phi;
isomorphic_groups_hom_HG :: @Monoid.is_homomorphism H eq op G EQ OP phi';
}.

Lemma group_by_isomorphism
Expand Down Expand Up @@ -144,10 +144,10 @@ Section CommutativeGroupByIsomorphism.

Class isomorphic_commutative_groups :=
{
isomorphic_commutative_groups_group_G :> @commutative_group G EQ OP ID INV;
isomorphic_commutative_groups_group_H :> @commutative_group H eq op id inv;
isomorphic_commutative_groups_hom_GH :> @Monoid.is_homomorphism G EQ OP H eq op phi;
isomorphic_commutative_groups_hom_HG :> @Monoid.is_homomorphism H eq op G EQ OP phi';
isomorphic_commutative_groups_group_G :: @commutative_group G EQ OP ID INV;
isomorphic_commutative_groups_group_H :: @commutative_group H eq op id inv;
isomorphic_commutative_groups_hom_GH :: @Monoid.is_homomorphism G EQ OP H eq op phi;
isomorphic_commutative_groups_hom_HG :: @Monoid.is_homomorphism H eq op G EQ OP phi';
}.

Lemma commutative_group_by_isomorphism
Expand Down
122 changes: 61 additions & 61 deletions src/LegacyArithmetic/Interface.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,16 +163,16 @@ Section InstructionGallery.

Class is_spread_left_immediate (sprl : spread_left_immediate) :=
{
decode_fst_spread_left_immediate :> forall r count,
decode_fst_spread_left_immediate :: forall r count,
0 <= count < n
-> decode (fst (sprl r count)) =~> (decode r << count) mod 2^n;
decode_snd_spread_left_immediate :> forall r count,
decode_snd_spread_left_immediate :: forall r count,
0 <= count < n
-> decode (snd (sprl r count)) =~> (decode r << count) >> n

}.

Class mask_keep_low := { mkl :> W -> imm -> W }.
Class mask_keep_low := { mkl :: W -> imm -> W }.
Global Coercion mkl : mask_keep_low >-> Funclass.

Class is_mask_keep_low (mkl : mask_keep_low) :=
Expand All @@ -184,7 +184,7 @@ Section InstructionGallery.

Class is_bitwise_and (and : bitwise_and) :=
{
decode_bitwise_and :> forall x y, decode (and x y) <~=~> Z.land (decode x) (decode y)
decode_bitwise_and :: forall x y, decode (and x y) <~=~> Z.land (decode x) (decode y)
}.

(** Quoting http://www.felixcloutier.com/x86/AND.html:
Expand All @@ -197,16 +197,16 @@ Section InstructionGallery.

Class is_bitwise_and_with_CF (andf : bitwise_and_with_CF) :=
{
decode_snd_bitwise_and_with_CF :> forall x y, decode (snd (andf x y)) <~=~> Z.land (decode x) (decode y);
fst_bitwise_and_with_CF :> forall x y, fst (andf x y) =~> false
decode_snd_bitwise_and_with_CF :: forall x y, decode (snd (andf x y)) <~=~> Z.land (decode x) (decode y);
fst_bitwise_and_with_CF :: forall x y, fst (andf x y) =~> false
}.

Class bitwise_or := { or : W -> W -> W }.
Global Coercion or : bitwise_or >-> Funclass.

Class is_bitwise_or (or : bitwise_or) :=
{
decode_bitwise_or :> forall x y, decode (or x y) <~=~> Z.lor (decode x) (decode y)
decode_bitwise_or :: forall x y, decode (or x y) <~=~> Z.lor (decode x) (decode y)
}.

(** Quoting http://www.felixcloutier.com/x86/OR.html:
Expand All @@ -219,8 +219,8 @@ Section InstructionGallery.

Class is_bitwise_or_with_CF (orf : bitwise_or_with_CF) :=
{
decode_snd_bitwise_or_with_CF :> forall x y, decode (snd (orf x y)) <~=~> Z.lor (decode x) (decode y);
fst_bitwise_or_with_CF :> forall x y, fst (orf x y) =~> false
decode_snd_bitwise_or_with_CF :: forall x y, decode (snd (orf x y)) <~=~> Z.lor (decode x) (decode y);
fst_bitwise_or_with_CF :: forall x y, fst (orf x y) =~> false
}.

Local Notation bit b := (if b then 1 else 0).
Expand All @@ -230,17 +230,17 @@ Section InstructionGallery.

Class is_add_with_carry (adc : add_with_carry) :=
{
bit_fst_add_with_carry :> forall x y c, bit (fst (adc x y c)) <~=~> (decode x + decode y + bit c) >> n;
decode_snd_add_with_carry :> forall x y c, decode (snd (adc x y c)) <~=~> (decode x + decode y + bit c) mod (2^n)
bit_fst_add_with_carry :: forall x y c, bit (fst (adc x y c)) <~=~> (decode x + decode y + bit c) >> n;
decode_snd_add_with_carry :: forall x y c, decode (snd (adc x y c)) <~=~> (decode x + decode y + bit c) mod (2^n)
}.

Class sub_with_carry := { subc : W -> W -> bool -> bool * W }.
Global Coercion subc : sub_with_carry >-> Funclass.

Class is_sub_with_carry (subc:W->W->bool->bool*W) :=
{
fst_sub_with_carry :> forall x y c, fst (subc x y c) <~=~> ((decode x - decode y - bit c) <? 0);
decode_snd_sub_with_carry :> forall x y c, decode (snd (subc x y c)) <~=~> (decode x - decode y - bit c) mod 2^n
fst_sub_with_carry :: forall x y c, fst (subc x y c) <~=~> ((decode x - decode y - bit c) <? 0);
decode_snd_sub_with_carry :: forall x y c, decode (snd (subc x y c)) <~=~> (decode x - decode y - bit c) mod 2^n
}.

Class multiply := { mul : W -> W -> W }.
Expand Down Expand Up @@ -279,17 +279,17 @@ Section InstructionGallery.
forall x y, decode (mulhwhh x y) <~=~> ((decode x >> w) * (decode y >> w)) mod 2^n.
Class is_mul_double (muldw : multiply_double) :=
{
decode_fst_mul_double :>
decode_fst_mul_double ::
forall x y, decode (fst (muldw x y)) =~> (decode x * decode y) mod 2^n;
decode_snd_mul_double :>
decode_snd_mul_double ::
forall x y, decode (snd (muldw x y)) =~> (decode x * decode y) >> n
}.

Class is_mul_double_with_CF (muldwf : multiply_double_with_CF) :=
{
decode_fst_mul_double_with_CF :>
decode_fst_mul_double_with_CF ::
forall x y, decode (fst (snd (muldwf x y))) =~> (decode x * decode y) mod 2^n;
decode_snd_mul_double_with_CF :>
decode_snd_mul_double_with_CF ::
forall x y, decode (snd (snd (muldwf x y))) =~> (decode x * decode y) >> n
}.

Expand Down Expand Up @@ -388,34 +388,34 @@ Module fancy_machine.
Class instructions (n : Z) :=
{
W : Type (* [n]-bit word *);
decode :> decoder n W;
ldi :> load_immediate W;
shrd :> shift_right_doubleword_immediate W;
shl :> shift_left_immediate W;
shr :> shift_right_immediate W;
adc :> add_with_carry W;
subc :> sub_with_carry W;
mulhwll :> multiply_low_low W;
mulhwhl :> multiply_high_low W;
mulhwhh :> multiply_high_high W;
selc :> select_conditional W;
addm :> add_modulo W
decode :: decoder n W;
ldi :: load_immediate W;
shrd :: shift_right_doubleword_immediate W;
shl :: shift_left_immediate W;
shr :: shift_right_immediate W;
adc :: add_with_carry W;
subc :: sub_with_carry W;
mulhwll :: multiply_low_low W;
mulhwhl :: multiply_high_low W;
mulhwhh :: multiply_high_high W;
selc :: select_conditional W;
addm :: add_modulo W
}.

Class arithmetic {n_over_two} (ops:instructions (2 * n_over_two)) :=
{
decode_range :> is_decode decode;
load_immediate :> is_load_immediate ldi;
shift_right_doubleword_immediate :> is_shift_right_doubleword_immediate shrd;
shift_left_immediate :> is_shift_left_immediate shl;
shift_right_immediate :> is_shift_right_immediate shr;
add_with_carry :> is_add_with_carry adc;
sub_with_carry :> is_sub_with_carry subc;
multiply_low_low :> is_mul_low_low n_over_two mulhwll;
multiply_high_low :> is_mul_high_low n_over_two mulhwhl;
multiply_high_high :> is_mul_high_high n_over_two mulhwhh;
select_conditional :> is_select_conditional selc;
add_modulo :> is_add_modulo addm
decode_range :: is_decode decode;
load_immediate :: is_load_immediate ldi;
shift_right_doubleword_immediate :: is_shift_right_doubleword_immediate shrd;
shift_left_immediate :: is_shift_left_immediate shl;
shift_right_immediate :: is_shift_right_immediate shr;
add_with_carry :: is_add_with_carry adc;
sub_with_carry :: is_sub_with_carry subc;
multiply_low_low :: is_mul_low_low n_over_two mulhwll;
multiply_high_low :: is_mul_high_low n_over_two mulhwhl;
multiply_high_high :: is_mul_high_high n_over_two mulhwhh;
select_conditional :: is_select_conditional selc;
add_modulo :: is_add_modulo addm
}.
End fancy_machine.

Expand All @@ -425,30 +425,30 @@ Module x86.
Class instructions (n : Z) :=
{
W : Type (* [n]-bit word *);
decode :> decoder n W;
ldi :> load_immediate W;
shrdf :> shift_right_doubleword_immediate_with_CF W;
shlf :> shift_left_immediate_with_CF W;
shrf :> shift_right_immediate_with_CF W;
adc :> add_with_carry W;
subc :> sub_with_carry W;
muldwf :> multiply_double_with_CF W;
selc :> select_conditional W;
orf :> bitwise_or_with_CF W
decode :: decoder n W;
ldi :: load_immediate W;
shrdf :: shift_right_doubleword_immediate_with_CF W;
shlf :: shift_left_immediate_with_CF W;
shrf :: shift_right_immediate_with_CF W;
adc :: add_with_carry W;
subc :: sub_with_carry W;
muldwf :: multiply_double_with_CF W;
selc :: select_conditional W;
orf :: bitwise_or_with_CF W
}.

Class arithmetic {n} (ops:instructions n) :=
{
decode_range :> is_decode decode;
load_immediate :> is_load_immediate ldi;
shift_right_doubleword_immediate_with_CF :> is_shift_right_doubleword_immediate_with_CF shrdf;
shift_left_immediate_with_CF :> is_shift_left_immediate_with_CF shlf;
shift_right_immediate_with_CF :> is_shift_right_immediate_with_CF shrf;
add_with_carry :> is_add_with_carry adc;
sub_with_carry :> is_sub_with_carry subc;
multiply_double_with_CF :> is_mul_double_with_CF muldwf;
select_conditional :> is_select_conditional selc;
bitwise_or_with_CF :> is_bitwise_or_with_CF orf
decode_range :: is_decode decode;
load_immediate :: is_load_immediate ldi;
shift_right_doubleword_immediate_with_CF :: is_shift_right_doubleword_immediate_with_CF shrdf;
shift_left_immediate_with_CF :: is_shift_left_immediate_with_CF shlf;
shift_right_immediate_with_CF :: is_shift_right_immediate_with_CF shrf;
add_with_carry :: is_add_with_carry adc;
sub_with_carry :: is_sub_with_carry subc;
multiply_double_with_CF :: is_mul_double_with_CF muldwf;
select_conditional :: is_select_conditional selc;
bitwise_or_with_CF :: is_bitwise_or_with_CF orf
}.
End x86.

Expand Down