Skip to content

Commit 230d00e

Browse files
0xMushow0xMushow
committed
refactor: Replace PartialVMResult.t IntegerValue.t by PartialVMResult.t Z
1 parent 4f238d6 commit 230d00e

File tree

1 file changed

+42
-42
lines changed

1 file changed

+42
-42
lines changed

‎CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v‎

Lines changed: 42 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -1032,94 +1032,94 @@ Module IntegerValue.
10321032
| _, _ => Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10331033
end.
10341034

1035-
Definition cast_u8 (self : IntegerValue.t) : PartialVMResult.t IntegerValue.t :=
1035+
Definition cast_u8 (self : IntegerValue.t) : PartialVMResult.t Z :=
10361036
match self with
1037-
| IntegerValue.U8 l => Result.Ok (IntegerValue.U8 l)
1037+
| IntegerValue.U8 l => Result.Ok (l)
10381038
| IntegerValue.U16 l => if l <=? 2^8 - 1
1039-
then Result.Ok (IntegerValue.U8 l)
1039+
then Result.Ok (l)
10401040
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10411041
| IntegerValue.U32 l => if l <=? 2^8 - 1
1042-
then Result.Ok (IntegerValue.U8 l)
1042+
then Result.Ok (l)
10431043
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10441044
| IntegerValue.U64 l => if l <=? 2^8 - 1
1045-
then Result.Ok (IntegerValue.U8 l)
1045+
then Result.Ok (l)
10461046
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10471047
| IntegerValue.U128 l => if l <=? 2^8 - 1
1048-
then Result.Ok (IntegerValue.U8 l)
1048+
then Result.Ok ( l)
10491049
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10501050
| IntegerValue.U256 l => if l <=? 2^8 - 1
1051-
then Result.Ok (IntegerValue.U8 l)
1051+
then Result.Ok (l)
10521052
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10531053
end.
10541054

1055-
Definition cast_u16 (self : IntegerValue.t) : PartialVMResult.t IntegerValue.t :=
1055+
Definition cast_u16 (self : IntegerValue.t) : PartialVMResult.t Z :=
10561056
match self with
1057-
| IntegerValue.U8 l => Result.Ok (IntegerValue.U16 l)
1058-
| IntegerValue.U16 l => Result.Ok (IntegerValue.U16 l)
1057+
| IntegerValue.U8 l => Result.Ok (l)
1058+
| IntegerValue.U16 l => Result.Ok (l)
10591059
| IntegerValue.U32 l => if l <=? 2^16 - 1
1060-
then Result.Ok (IntegerValue.U16 l)
1060+
then Result.Ok (l)
10611061
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10621062
| IntegerValue.U64 l => if l <=? 2^16 - 1
1063-
then Result.Ok (IntegerValue.U16 l)
1063+
then Result.Ok (l)
10641064
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10651065
| IntegerValue.U128 l => if l <=? 2^16 - 1
1066-
then Result.Ok (IntegerValue.U16 l)
1066+
then Result.Ok (l)
10671067
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10681068
| IntegerValue.U256 l => if l <=? 2^16 - 1
1069-
then Result.Ok (IntegerValue.U16 l)
1069+
then Result.Ok (l)
10701070
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10711071
end.
10721072

1073-
Definition cast_u32 (self : IntegerValue.t) : PartialVMResult.t IntegerValue.t :=
1073+
Definition cast_u32 (self : IntegerValue.t) : PartialVMResult.t Z :=
10741074
match self with
1075-
| IntegerValue.U8 l => Result.Ok (IntegerValue.U32 l)
1076-
| IntegerValue.U16 l => Result.Ok (IntegerValue.U32 l)
1077-
| IntegerValue.U32 l => Result.Ok (IntegerValue.U32 l)
1075+
| IntegerValue.U8 l => Result.Ok (l)
1076+
| IntegerValue.U16 l => Result.Ok (l)
1077+
| IntegerValue.U32 l => Result.Ok (l)
10781078
| IntegerValue.U64 l => if l <=? 2^32 - 1
1079-
then Result.Ok (IntegerValue.U32 l)
1079+
then Result.Ok (l)
10801080
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10811081
| IntegerValue.U128 l => if l <=? 2^32 - 1
1082-
then Result.Ok (IntegerValue.U32 l)
1082+
then Result.Ok (l)
10831083
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10841084
| IntegerValue.U256 l => if l <=? 2^32 - 1
1085-
then Result.Ok (IntegerValue.U32 l)
1085+
then Result.Ok (l)
10861086
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10871087
end.
10881088

1089-
Definition cast_u64 (self : IntegerValue.t) : PartialVMResult.t IntegerValue.t :=
1089+
Definition cast_u64 (self : IntegerValue.t) : PartialVMResult.t Z :=
10901090
match self with
1091-
| IntegerValue.U8 l => Result.Ok (IntegerValue.U64 l)
1092-
| IntegerValue.U16 l => Result.Ok (IntegerValue.U64 l)
1093-
| IntegerValue.U32 l => Result.Ok (IntegerValue.U64 l)
1094-
| IntegerValue.U64 l => Result.Ok (IntegerValue.U64 l)
1091+
| IntegerValue.U8 l => Result.Ok (l)
1092+
| IntegerValue.U16 l => Result.Ok (l)
1093+
| IntegerValue.U32 l => Result.Ok (l)
1094+
| IntegerValue.U64 l => Result.Ok (l)
10951095
| IntegerValue.U128 l => if l <=? 2^64 - 1
1096-
then Result.Ok (IntegerValue.U64 l)
1096+
then Result.Ok (l)
10971097
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
10981098
| IntegerValue.U256 l => if l <=? 2^64 - 1
1099-
then Result.Ok (IntegerValue.U64 l)
1099+
then Result.Ok (l)
11001100
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
11011101
end.
11021102

1103-
Definition cast_u128 (self : IntegerValue.t) : PartialVMResult.t IntegerValue.t :=
1103+
Definition cast_u128 (self : IntegerValue.t) : PartialVMResult.t Z :=
11041104
match self with
1105-
| IntegerValue.U8 l => Result.Ok (IntegerValue.U128 l)
1106-
| IntegerValue.U16 l => Result.Ok (IntegerValue.U128 l)
1107-
| IntegerValue.U32 l => Result.Ok (IntegerValue.U128 l)
1108-
| IntegerValue.U64 l => Result.Ok (IntegerValue.U128 l)
1109-
| IntegerValue.U128 l => Result.Ok (IntegerValue.U128 l)
1105+
| IntegerValue.U8 l => Result.Ok (l)
1106+
| IntegerValue.U16 l => Result.Ok (l)
1107+
| IntegerValue.U32 l => Result.Ok (l)
1108+
| IntegerValue.U64 l => Result.Ok (l)
1109+
| IntegerValue.U128 l => Result.Ok (l)
11101110
| IntegerValue.U256 l => if l <=? 2^128 - 1
1111-
then Result.Ok (IntegerValue.U128 l)
1111+
then Result.Ok (l)
11121112
else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
11131113
end.
11141114

1115-
Definition cast_u256 (self : IntegerValue.t) : PartialVMResult.t IntegerValue.t :=
1115+
Definition cast_u256 (self : IntegerValue.t) : PartialVMResult.t Z :=
11161116
match self with
1117-
| IntegerValue.U8 l => Result.Ok (IntegerValue.U256 l)
1118-
| IntegerValue.U16 l => Result.Ok (IntegerValue.U256 l)
1119-
| IntegerValue.U32 l => Result.Ok (IntegerValue.U256 l)
1120-
| IntegerValue.U64 l => Result.Ok (IntegerValue.U256 l)
1121-
| IntegerValue.U128 l => Result.Ok (IntegerValue.U256 l)
1122-
| IntegerValue.U256 l => Result.Ok (IntegerValue.U256 l)
1117+
| IntegerValue.U8 l => Result.Ok (l)
1118+
| IntegerValue.U16 l => Result.Ok (l)
1119+
| IntegerValue.U32 l => Result.Ok (l)
1120+
| IntegerValue.U64 l => Result.Ok (l)
1121+
| IntegerValue.U128 l => Result.Ok (l)
1122+
| IntegerValue.U256 l => Result.Ok (l)
11231123
end.
11241124

11251125
End IntegerValue.

0 commit comments

Comments
 (0)