Skip to content

Fix the diff in the CI in the code translation #743

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

Merged
merged 3 commits into from
May 31, 2025
Merged

Fix the diff in the CI in the code translation #743

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
55585b3
fix: avoid names collisions with M and repeat
clarus May 26, 2025
395c5c5
revm: more links for contract instructions
clarus May 31, 2025
276779a
ci: fix generation of the array translation
clarus May 31, 2025
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
2 changes: 2 additions & 0 deletions .github/workflows/rust.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,8 @@ jobs:
touch src/lib.rs
export RUST_MIN_STACK=800000000
time cargo coq-of-rust
sed -i 's/Module Impl_core_default_Default_where_core_default_Default_T_for_array_expr_T./(* Module Impl_core_default_Default_where_core_default_Default_T_for_array_expr_T./' src/array/mod.v
sed -i 's/End Impl_core_default_Default_where_core_default_Default_T_for_array_expr_T./End Impl_core_default_Default_where_core_default_Default_T_for_array_expr_T. *)/' src/array/mod.v
rsync -rcv src/ ../../../../CoqOfRust/core/ --include='*/' --include='*.v' --include='*.rs' --exclude='*'
cd ../../../..
endGroup
Expand Down
2 changes: 1 addition & 1 deletion CoqOfRust/alloc/collections/vec_deque/into_iter.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1345,7 +1345,7 @@ Module collections.
[ N ]
[ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
] :=
repeat (|
lib.repeat (|
M.read (|
get_constant (|
"alloc::collections::vec_deque::into_iter::next_chunk_discriminant",
Expand Down
2 changes: 1 addition & 1 deletion CoqOfRust/alloc/str.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8072,7 +8072,7 @@ Module str.
(Ty.path "array")
[ Value.Integer IntegerKind.Usize 16 ]
[ Ty.path "bool" ] :=
repeat (| Value.Bool false, Value.Integer IntegerKind.Usize 16 |) in
lib.repeat (| Value.Bool false, Value.Integer IntegerKind.Usize 16 |) in
let~ _ : Ty.tuple [] :=
M.read (|
M.loop (|
Expand Down
6 changes: 3 additions & 3 deletions CoqOfRust/alloc/string.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5703,7 +5703,7 @@ Module string.
M.borrow (|
Pointer.Kind.MutRef,
M.alloc (|
repeat (|
lib.repeat (|
Value.Integer IntegerKind.U8 0,
Value.Integer IntegerKind.Usize 4
|)
Expand Down Expand Up @@ -7806,7 +7806,7 @@ Module string.
|) in
let~ bits :
Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] :=
repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in
lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in
let~ bits :
Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] :=
M.call_closure (|
Expand Down Expand Up @@ -14847,7 +14847,7 @@ Module string.
M.borrow (|
Pointer.Kind.MutRef,
M.alloc (|
repeat (|
lib.repeat (|
Value.Integer IntegerKind.U8 0,
Value.Integer IntegerKind.Usize 4
|)
Expand Down
2 changes: 1 addition & 1 deletion CoqOfRust/alloc/vec/into_iter.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1899,7 +1899,7 @@ Module vec.
[ N ]
[ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ]
] :=
repeat (|
lib.repeat (|
M.read (|
get_constant (|
"alloc::vec::into_iter::next_chunk_discriminant",
Expand Down
10 changes: 8 additions & 2 deletions CoqOfRust/alloy_primitives/bits/address.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1093,7 +1093,10 @@ Module bits.
(Ty.path "array")
[ Value.Integer IntegerKind.Usize 32 ]
[ Ty.path "u8" ] :=
repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) in
lib.repeat (|
Value.Integer IntegerKind.U8 0,
Value.Integer IntegerKind.Usize 32
|) in
let~ _ : Ty.tuple [] :=
M.call_closure (|
Ty.tuple [],
Expand Down Expand Up @@ -2404,7 +2407,10 @@ Module bits.
(Ty.path "array")
[ Value.Integer IntegerKind.Usize 85 ]
[ Ty.path "u8" ] :=
repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 85 |) in
lib.repeat (|
Value.Integer IntegerKind.U8 0,
Value.Integer IntegerKind.Usize 85
|) in
let~ _ : Ty.tuple [] :=
M.write (|
M.SubPointer.get_array_field (| bytes, Value.Integer IntegerKind.Usize 0 |),
Expand Down
10 changes: 5 additions & 5 deletions CoqOfRust/alloy_primitives/bits/fixed.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4588,7 +4588,7 @@ Module bits.
(Ty.path "array")
[ Value.Integer IntegerKind.Usize 13 ]
[ Ty.path "u8" ] :=
repeat (|
lib.repeat (|
Value.Integer IntegerKind.U8 0,
Value.Integer IntegerKind.Usize 13
|) in
Expand Down Expand Up @@ -5868,7 +5868,7 @@ Module bits.
"alloy_primitives::bits::fixed::FixedBytes"
[ N ]
[]
[ repeat (| Value.Integer IntegerKind.U8 0, N |) ]
[ lib.repeat (| Value.Integer IntegerKind.U8 0, N |) ]
|))).

Global Instance AssociatedConstant_value_ZERO :
Expand Down Expand Up @@ -5924,7 +5924,7 @@ Module bits.
(let x := M.alloc (| x |) in
M.read (|
let~ bytes : Ty.apply (Ty.path "array") [ N ] [ Ty.path "u8" ] :=
repeat (| Value.Integer IntegerKind.U8 0, N |) in
lib.repeat (| Value.Integer IntegerKind.U8 0, N |) in
let~ _ : Ty.tuple [] :=
M.read (|
M.match_operator (|
Expand Down Expand Up @@ -5998,7 +5998,7 @@ Module bits.
"alloy_primitives::bits::fixed::FixedBytes"
[ N ]
[]
[ repeat (| M.read (| byte |), N |) ]))
[ lib.repeat (| M.read (| byte |), N |) ]))
| _, _, _ => M.impossible "wrong number of arguments"
end.

Expand Down Expand Up @@ -6130,7 +6130,7 @@ Module bits.
|)
|) in
let~ result : Ty.apply (Ty.path "array") [ Z ] [ Ty.path "u8" ] :=
repeat (| Value.Integer IntegerKind.U8 0, Z |) in
lib.repeat (| Value.Integer IntegerKind.U8 0, Z |) in
let~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in
let~ _ : Ty.tuple [] :=
M.read (|
Expand Down
10 changes: 8 additions & 2 deletions CoqOfRust/alloy_primitives/bits/function.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,10 @@ Module bits.
(Ty.path "array")
[ Value.Integer IntegerKind.Usize 32 ]
[ Ty.path "u8" ] :=
repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) in
lib.repeat (|
Value.Integer IntegerKind.U8 0,
Value.Integer IntegerKind.Usize 32
|) in
let~ _ : Ty.tuple [] :=
M.call_closure (|
Ty.tuple [],
Expand Down Expand Up @@ -331,7 +334,10 @@ Module bits.
(Ty.path "array")
[ Value.Integer IntegerKind.Usize 24 ]
[ Ty.path "u8" ] :=
repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 24 |) in
lib.repeat (|
Value.Integer IntegerKind.U8 0,
Value.Integer IntegerKind.Usize 24
|) in
let~ _ : Ty.tuple [] :=
M.call_closure (|
Ty.tuple [],
Expand Down
14 changes: 14 additions & 0 deletions CoqOfRust/alloy_primitives/bits/links/fixed.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Require Import alloy_primitives.bits.fixed.
Require Import core.convert.links.mod.
Require Import core.links.array.
Require Import core.links.borrow.
Require Import core.ops.links.index.

Module Impl_FixedBytes.
Definition Self (N: Usize.t) : Set :=
Expand Down Expand Up @@ -74,3 +75,16 @@ Module Impl_Borrow_Array_u8_N_for_FixedBytes_N.
Admitted.
End Impl_Borrow_Array_u8_N_for_FixedBytes_N.
Export Impl_Borrow_Array_u8_N_for_FixedBytes_N.

Module Impl_Index_for_FixedBytes_N.
Definition Self (N: Usize.t) : Set :=
FixedBytes.t N.

(* type Output = <[u8; N] as Index<__IdxT>>::Output *)
Definition Output : Set :=
list U8.t.

Instance run (N: Usize.t) (__IdxT : Set) `{Link __IdxT} : Index.Run (Self N) __IdxT Output.
Admitted.
End Impl_Index_for_FixedBytes_N.
Export Impl_Index_for_FixedBytes_N.
18 changes: 18 additions & 0 deletions CoqOfRust/alloy_primitives/bytes/links/mod.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,16 @@ Module Impl_Deref_for_Bytes.
End Impl_Deref_for_Bytes.
Export Impl_Deref_for_Bytes.

(* impl DerefMut for Bytes *)
Module Impl_DerefMut_for_Bytes.
Definition Self : Set :=
Bytes.t.

Instance run : DerefMut.Run Self bytes.Bytes.t.
Admitted.
End Impl_DerefMut_for_Bytes.
Export Impl_DerefMut_for_Bytes.

Module Impl_Bytes.
Definition Self : Set :=
Bytes.t.
Expand All @@ -92,6 +102,14 @@ Module Impl_Bytes.
constructor.
run_symbolic.
Admitted.

(* pub fn copy_from_slice(data: &[u8]) -> Self *)
Instance run_copy_from_slice (data : Ref.t Pointer.Kind.Ref (list U8.t)) :
Run.Trait bytes_.Impl_alloy_primitives_bytes__Bytes.copy_from_slice [] [] [ φ data ] Self.
Proof.
constructor.
run_symbolic.
Admitted.
End Impl_Bytes.
Export Impl_Bytes.

Expand Down
5 changes: 4 additions & 1 deletion CoqOfRust/alloy_primitives/signature/primitive_sig.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2013,7 +2013,10 @@ Module signature.
(Ty.path "array")
[ Value.Integer IntegerKind.Usize 65 ]
[ Ty.path "u8" ] :=
repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 65 |) in
lib.repeat (|
Value.Integer IntegerKind.U8 0,
Value.Integer IntegerKind.Usize 65
|) in
let~ _ : Ty.tuple [] :=
M.call_closure (|
Ty.tuple [],
Expand Down
5 changes: 4 additions & 1 deletion CoqOfRust/alloy_primitives/signature/sig.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2299,7 +2299,10 @@ Module signature.
(Ty.path "array")
[ Value.Integer IntegerKind.Usize 65 ]
[ Ty.path "u8" ] :=
repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 65 |) in
lib.repeat (|
Value.Integer IntegerKind.U8 0,
Value.Integer IntegerKind.Usize 65
|) in
let~ _ : Ty.tuple [] :=
M.call_closure (|
Ty.tuple [],
Expand Down
8 changes: 4 additions & 4 deletions CoqOfRust/alloy_primitives/signed/utils.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -513,7 +513,7 @@ Module signed.
|)
|) in
let~ limbs : Ty.apply (Ty.path "array") [ LIMBS ] [ Ty.path "u64" ] :=
repeat (|
lib.repeat (|
M.read (|
get_associated_constant (| Ty.path "u64", "MAX", Ty.path "u64" |)
|),
Expand Down Expand Up @@ -679,7 +679,7 @@ Module signed.
|)
|) in
let~ limbs : Ty.apply (Ty.path "array") [ LIMBS ] [ Ty.path "u64" ] :=
repeat (| Value.Integer IntegerKind.U64 0, LIMBS |) in
lib.repeat (| Value.Integer IntegerKind.U64 0, LIMBS |) in
let~ _ : Ty.tuple [] :=
M.write (|
M.SubPointer.get_array_field (|
Expand Down Expand Up @@ -743,7 +743,7 @@ Module signed.
ltac:(M.monadic
(M.read (|
let~ limbs : Ty.apply (Ty.path "array") [ LIMBS ] [ Ty.path "u64" ] :=
repeat (| Value.Integer IntegerKind.U64 0, LIMBS |) in
lib.repeat (| Value.Integer IntegerKind.U64 0, LIMBS |) in
M.alloc (|
Value.StructTuple
"alloy_primitives::signed::int::Signed"
Expand Down Expand Up @@ -839,7 +839,7 @@ Module signed.
|)
|) in
let~ limbs : Ty.apply (Ty.path "array") [ LIMBS ] [ Ty.path "u64" ] :=
repeat (| Value.Integer IntegerKind.U64 0, LIMBS |) in
lib.repeat (| Value.Integer IntegerKind.U64 0, LIMBS |) in
let~ _ : Ty.tuple [] :=
M.write (|
M.SubPointer.get_array_field (| limbs, Value.Integer IntegerKind.Usize 0 |),
Expand Down
Loading
Loading