diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index c9cf42b93..8c1617fb0 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -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 diff --git a/CoqOfRust/alloc/collections/vec_deque/into_iter.v b/CoqOfRust/alloc/collections/vec_deque/into_iter.v index 90e9767de..62a67a378 100644 --- a/CoqOfRust/alloc/collections/vec_deque/into_iter.v +++ b/CoqOfRust/alloc/collections/vec_deque/into_iter.v @@ -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", diff --git a/CoqOfRust/alloc/str.v b/CoqOfRust/alloc/str.v index d18cacd92..32cbdc2db 100644 --- a/CoqOfRust/alloc/str.v +++ b/CoqOfRust/alloc/str.v @@ -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 (| diff --git a/CoqOfRust/alloc/string.v b/CoqOfRust/alloc/string.v index ec6fa2c1f..9dd53217f 100644 --- a/CoqOfRust/alloc/string.v +++ b/CoqOfRust/alloc/string.v @@ -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 |) @@ -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 (| @@ -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 |) diff --git a/CoqOfRust/alloc/vec/into_iter.v b/CoqOfRust/alloc/vec/into_iter.v index 5927de1e6..d02824630 100644 --- a/CoqOfRust/alloc/vec/into_iter.v +++ b/CoqOfRust/alloc/vec/into_iter.v @@ -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", diff --git a/CoqOfRust/alloy_primitives/bits/address.v b/CoqOfRust/alloy_primitives/bits/address.v index 174498746..0918278bd 100644 --- a/CoqOfRust/alloy_primitives/bits/address.v +++ b/CoqOfRust/alloy_primitives/bits/address.v @@ -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 [], @@ -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 |), diff --git a/CoqOfRust/alloy_primitives/bits/fixed.v b/CoqOfRust/alloy_primitives/bits/fixed.v index 2daea6c98..6c7f6c3ff 100644 --- a/CoqOfRust/alloy_primitives/bits/fixed.v +++ b/CoqOfRust/alloy_primitives/bits/fixed.v @@ -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 @@ -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 : @@ -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 (| @@ -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. @@ -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 (| diff --git a/CoqOfRust/alloy_primitives/bits/function.v b/CoqOfRust/alloy_primitives/bits/function.v index c4f9c452f..c8746d0cb 100644 --- a/CoqOfRust/alloy_primitives/bits/function.v +++ b/CoqOfRust/alloy_primitives/bits/function.v @@ -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 [], @@ -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 [], diff --git a/CoqOfRust/alloy_primitives/bits/links/fixed.v b/CoqOfRust/alloy_primitives/bits/links/fixed.v index cef1f3c4a..2914b5a2a 100644 --- a/CoqOfRust/alloy_primitives/bits/links/fixed.v +++ b/CoqOfRust/alloy_primitives/bits/links/fixed.v @@ -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 := @@ -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. diff --git a/CoqOfRust/alloy_primitives/bytes/links/mod.v b/CoqOfRust/alloy_primitives/bytes/links/mod.v index b64632d51..6fba7d417 100644 --- a/CoqOfRust/alloy_primitives/bytes/links/mod.v +++ b/CoqOfRust/alloy_primitives/bytes/links/mod.v @@ -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. @@ -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. diff --git a/CoqOfRust/alloy_primitives/signature/primitive_sig.v b/CoqOfRust/alloy_primitives/signature/primitive_sig.v index 8e35bc0e6..be0262748 100644 --- a/CoqOfRust/alloy_primitives/signature/primitive_sig.v +++ b/CoqOfRust/alloy_primitives/signature/primitive_sig.v @@ -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 [], diff --git a/CoqOfRust/alloy_primitives/signature/sig.v b/CoqOfRust/alloy_primitives/signature/sig.v index 01be83023..20cb26b98 100644 --- a/CoqOfRust/alloy_primitives/signature/sig.v +++ b/CoqOfRust/alloy_primitives/signature/sig.v @@ -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 [], diff --git a/CoqOfRust/alloy_primitives/signed/utils.v b/CoqOfRust/alloy_primitives/signed/utils.v index 07d5dfc46..a1278985f 100644 --- a/CoqOfRust/alloy_primitives/signed/utils.v +++ b/CoqOfRust/alloy_primitives/signed/utils.v @@ -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" |) |), @@ -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 (| @@ -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" @@ -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 |), diff --git a/CoqOfRust/bytes/buf/buf_impl.v b/CoqOfRust/bytes/buf/buf_impl.v index 12f70e0f8..d1933dd93 100644 --- a/CoqOfRust/bytes/buf/buf_impl.v +++ b/CoqOfRust/bytes/buf/buf_impl.v @@ -1066,7 +1066,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 2 |) in @@ -1437,7 +1437,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 2 |) in @@ -1808,7 +1808,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 2 |) in @@ -2174,7 +2174,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 2 |) in @@ -2545,7 +2545,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 2 |) in @@ -2916,7 +2916,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 2 |) in @@ -3282,7 +3282,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in @@ -3653,7 +3653,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in @@ -4024,7 +4024,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in @@ -4390,7 +4390,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in @@ -4761,7 +4761,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in @@ -5132,7 +5132,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in @@ -5498,7 +5498,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -5869,7 +5869,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -6240,7 +6240,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -6606,7 +6606,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -6977,7 +6977,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -7348,7 +7348,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -7714,7 +7714,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 16 |) in @@ -8085,7 +8085,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 16 |) in @@ -8456,7 +8456,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 16 |) in @@ -8822,7 +8822,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 16 |) in @@ -9193,7 +9193,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 16 |) in @@ -9564,7 +9564,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 16 |) in @@ -9700,7 +9700,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -9800,7 +9800,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -10062,7 +10062,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -10162,7 +10162,7 @@ Module buf. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in diff --git a/CoqOfRust/bytes/links/bytes.v b/CoqOfRust/bytes/links/bytes.v index 144dc5acb..316cb3874 100644 --- a/CoqOfRust/bytes/links/bytes.v +++ b/CoqOfRust/bytes/links/bytes.v @@ -36,6 +36,14 @@ Module Impl_Bytes. bytes.Impl_bytes_bytes_Bytes.len [] [] [ φ self ] Usize.t. Admitted. + + (* pub fn clear(&mut self) *) + Instance run_clear (self : Ref.t Pointer.Kind.MutRef Self) : + Run.Trait bytes.Impl_bytes_bytes_Bytes.clear [] [] [φ self] unit. + Proof. + constructor. + run_symbolic. + Admitted. End Impl_Bytes. Export Impl_Bytes. diff --git a/CoqOfRust/core/array/iter.v b/CoqOfRust/core/array/iter.v index dd6f73ce1..216bba91d 100644 --- a/CoqOfRust/core/array/iter.v +++ b/CoqOfRust/core/array/iter.v @@ -260,7 +260,7 @@ Module array. (Ty.path "array") [ N ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ] := - repeat (| + lib.repeat (| M.read (| get_constant (| "core::array::iter::empty_discriminant", @@ -2201,7 +2201,7 @@ Module array. [ T ] [ ("data", - repeat (| + lib.repeat (| M.read (| get_constant (| "core::array::iter::clone_discriminant", diff --git a/CoqOfRust/core/escape.v b/CoqOfRust/core/escape.v index fdaa0eb7d..cfed0bf35 100644 --- a/CoqOfRust/core/escape.v +++ b/CoqOfRust/core/escape.v @@ -89,7 +89,10 @@ Module escape. M.read (| get_constant (| "core::escape::backslash_discriminant", Ty.tuple [] |) |) in let~ output : Ty.apply (Ty.path "array") [ N ] [ Ty.path "core::ascii::ascii_char::AsciiChar" ] := - repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [] [] [], N |) in + lib.repeat (| + Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [] [] [], + N + |) in let~ _ : Ty.tuple [] := M.write (| M.SubPointer.get_array_field (| output, Value.Integer IntegerKind.Usize 0 |), @@ -150,7 +153,10 @@ Module escape. M.read (| get_constant (| "core::escape::hex_escape_discriminant", Ty.tuple [] |) |) in let~ output : Ty.apply (Ty.path "array") [ N ] [ Ty.path "core::ascii::ascii_char::AsciiChar" ] := - repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [] [] [], N |) in + lib.repeat (| + Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [] [] [], + N + |) in let~ hi : Ty.path "core::ascii::ascii_char::AsciiChar" := M.read (| M.SubPointer.get_array_field (| @@ -253,7 +259,10 @@ Module escape. M.read (| get_constant (| "core::escape::verbatim_discriminant", Ty.tuple [] |) |) in let~ output : Ty.apply (Ty.path "array") [ N ] [ Ty.path "core::ascii::ascii_char::AsciiChar" ] := - repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [] [] [], N |) in + lib.repeat (| + Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [] [] [], + N + |) in let~ _ : Ty.tuple [] := M.write (| M.SubPointer.get_array_field (| output, Value.Integer IntegerKind.Usize 0 |), @@ -517,7 +526,7 @@ Module escape. ltac:(M.monadic (let~ arr : Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 256 ] [ Ty.path "u8" ] := - repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 256 |) in + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 256 |) in let~ idx : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in let~ _ : Ty.tuple [] := M.read (| @@ -784,7 +793,10 @@ Module escape. |) in let~ output : Ty.apply (Ty.path "array") [ N ] [ Ty.path "core::ascii::ascii_char::AsciiChar" ] := - repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [] [] [], N |) in + lib.repeat (| + Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [] [] [], + N + |) in let~ _ : Ty.tuple [] := M.write (| M.SubPointer.get_array_field (| output, Value.Integer IntegerKind.Usize 3 |), @@ -1388,7 +1400,7 @@ Module escape. [] [ ("data", - repeat (| + lib.repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [] [] [], N |)); diff --git a/CoqOfRust/core/fmt/float.v b/CoqOfRust/core/fmt/float.v index f9c826e59..d679e7f3e 100644 --- a/CoqOfRust/core/fmt/float.v +++ b/CoqOfRust/core/fmt/float.v @@ -179,7 +179,7 @@ Module fmt. [ Value.Integer IntegerKind.Usize 1024 ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -202,7 +202,7 @@ Module fmt. [] [ Ty.path "core::num::fmt::Part" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") @@ -357,7 +357,7 @@ Module fmt. [ Value.Integer IntegerKind.Usize 17 ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -380,7 +380,7 @@ Module fmt. [] [ Ty.path "core::num::fmt::Part" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") @@ -668,7 +668,7 @@ Module fmt. [ Value.Integer IntegerKind.Usize 1024 ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -691,7 +691,7 @@ Module fmt. [] [ Ty.path "core::num::fmt::Part" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") @@ -848,7 +848,7 @@ Module fmt. [ Value.Integer IntegerKind.Usize 17 ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -871,7 +871,7 @@ Module fmt. [] [ Ty.path "core::num::fmt::Part" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") diff --git a/CoqOfRust/core/fmt/mod.v b/CoqOfRust/core/fmt/mod.v index 568d7dbde..346f6c675 100644 --- a/CoqOfRust/core/fmt/mod.v +++ b/CoqOfRust/core/fmt/mod.v @@ -479,7 +479,7 @@ Module fmt. M.borrow (| Pointer.Kind.MutRef, M.alloc (| - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) @@ -5357,7 +5357,7 @@ Module fmt. [ Value.Integer IntegerKind.Usize 5 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 5 |) in @@ -14715,7 +14715,7 @@ Module fmt. M.borrow (| Pointer.Kind.MutRef, M.alloc (| - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) diff --git a/CoqOfRust/core/fmt/num.v b/CoqOfRust/core/fmt/num.v index 8e9620811..3ba0f6208 100644 --- a/CoqOfRust/core/fmt/num.v +++ b/CoqOfRust/core/fmt/num.v @@ -826,7 +826,7 @@ Module fmt. [ Value.Integer IntegerKind.Usize 128 ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -6829,7 +6829,7 @@ Module fmt. [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -7648,7 +7648,7 @@ Module fmt. [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -8467,7 +8467,7 @@ Module fmt. [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -9286,7 +9286,7 @@ Module fmt. [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -10105,7 +10105,7 @@ Module fmt. [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| @@ -11448,7 +11448,7 @@ Module fmt. [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") @@ -11935,7 +11935,7 @@ Module fmt. [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") @@ -15463,7 +15463,7 @@ Module fmt. [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") @@ -15949,7 +15949,7 @@ Module fmt. [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") @@ -18466,7 +18466,7 @@ Module fmt. [ Value.Integer IntegerKind.Usize 39 ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ] ] := - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| diff --git a/CoqOfRust/core/iter/adapters/copied.v b/CoqOfRust/core/iter/adapters/copied.v index 758b26e66..2009151c5 100644 --- a/CoqOfRust/core/iter/adapters/copied.v +++ b/CoqOfRust/core/iter/adapters/copied.v @@ -1360,7 +1360,7 @@ Module iter. [ N ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ] := - repeat (| + lib.repeat (| M.read (| get_constant (| "core::iter::adapters::copied::spec_next_chunk_discriminant", diff --git a/CoqOfRust/core/iter/adapters/filter.v b/CoqOfRust/core/iter/adapters/filter.v index 38f4ccccb..1af849322 100644 --- a/CoqOfRust/core/iter/adapters/filter.v +++ b/CoqOfRust/core/iter/adapters/filter.v @@ -170,7 +170,7 @@ Module iter. "Item" ] ] := - repeat (| + lib.repeat (| M.read (| get_constant (| "core::iter::adapters::filter::next_chunk_dropless_discriminant", diff --git a/CoqOfRust/core/iter/adapters/filter_map.v b/CoqOfRust/core/iter/adapters/filter_map.v index 5df81b67a..df993f0a6 100644 --- a/CoqOfRust/core/iter/adapters/filter_map.v +++ b/CoqOfRust/core/iter/adapters/filter_map.v @@ -582,7 +582,7 @@ Module iter. (Ty.path "array") [ N ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ B ] ] := - repeat (| + lib.repeat (| M.read (| get_constant (| "core::iter::adapters::filter_map::next_chunk_discriminant", diff --git a/CoqOfRust/core/iter/adapters/map_windows.v b/CoqOfRust/core/iter/adapters/map_windows.v index c9099d964..5f84b2bcc 100644 --- a/CoqOfRust/core/iter/adapters/map_windows.v +++ b/CoqOfRust/core/iter/adapters/map_windows.v @@ -1518,7 +1518,7 @@ Module iter. |) ] |); - repeat (| + lib.repeat (| M.read (| get_constant (| "core::iter::adapters::map_windows::try_from_iter_discriminant", @@ -2745,7 +2745,7 @@ Module iter. ("buffer", Value.Array [ - repeat (| + lib.repeat (| M.read (| get_constant (| "core::iter::adapters::map_windows::clone_discriminant", @@ -2754,7 +2754,7 @@ Module iter. |), N |); - repeat (| + lib.repeat (| M.read (| get_constant (| "core::iter::adapters::map_windows::clone_discriminant", diff --git a/CoqOfRust/core/iter/traits/links/iterator.v b/CoqOfRust/core/iter/traits/links/iterator.v index 97afab2a4..9d3b1f495 100644 --- a/CoqOfRust/core/iter/traits/links/iterator.v +++ b/CoqOfRust/core/iter/traits/links/iterator.v @@ -6,6 +6,7 @@ Require Import core.links.array. Require Import core.links.option. Require Import core.links.result. Require Import core.num.links.nonzero. +Require Import core.ops.links.function. (* pub trait Iterator *) Module Iterator. @@ -192,6 +193,18 @@ Module Iterator. where Self: Sized, F: FnMut(Self::Item) -> bool { ... } *) + Definition Run_any + (Self : Set) `{Link Self} + (Item : Set) `{Link Item} : + Set := + TraitMethod.C (trait Self) "any" (fun method => + forall + (F : Set) `{Link F} + (self : Ref.t Pointer.Kind.MutRef Self) + (f : F) + `(FnMut.Run F Item bool), + Run.Trait method [] [Φ F] [φ self; φ f] bool + ). (* fn find

(&mut self, predicate: P) -> Option @@ -323,5 +336,6 @@ Module Iterator. count : Run_count Self; last : Run_last Self Item; advance_by : Run_advance_by Self; + any : Run_any Self Item; }. End Iterator. diff --git a/CoqOfRust/core/links/option.v b/CoqOfRust/core/links/option.v index b1ff72329..8e51449e0 100644 --- a/CoqOfRust/core/links/option.v +++ b/CoqOfRust/core/links/option.v @@ -32,12 +32,15 @@ Module Option. Proof. now intros; subst. Qed. Smpl Add apply of_value_with_None : of_value. - Lemma of_value_with_Some {A : Set} `{Link A} (value : A) value' : + Lemma of_value_with_Some + A' (A : Set) `{Link A} + value' (value : A) : + A' = Φ A -> value' = φ value -> - Value.StructTuple "core::option::Option::Some" [] [Φ A] [value'] = + Value.StructTuple "core::option::Option::Some" [] [A'] [value'] = φ (Some value). Proof. intros; subst; reflexivity. Qed. - Smpl Add apply of_value_with_Some : of_value. + Smpl Add unshelve eapply of_value_with_Some : of_value. Definition of_value_None A' : OfTy.t A' -> @@ -49,13 +52,14 @@ Module Option. Defined. Smpl Add unshelve eapply of_value_None : of_value. - Definition of_value_Some A' value' : - forall - (of_value_value : OfValue.t value'), - A' = Φ (OfValue.get_Set of_value_value) -> + Definition of_value_Some A' value' + (H_A' : OfTy.t A') + (value : OfTy.get_Set H_A') : + value' = φ value -> OfValue.t (Value.StructTuple "core::option::Option::Some" [] [A'] [value']). Proof. - intros [A ? value] **. + intros. + destruct H_A' as [A]. eapply OfValue.Make with (A := option A) (value := Some value). now subst. Defined. @@ -178,3 +182,13 @@ Module Impl_Try_for_Option. Admitted. End Impl_Try_for_Option. Export Impl_Try_for_Option. + +(* impl ops::FromResidual> for Option *) +Module Impl_FromResidual_Infallible_for_Option. + Definition Self (T : Set) : Set := + option T. + + Instance run (T : Set) `{Link T} : FromResidual.Run (Self T) (option Infallible.t). + Admitted. +End Impl_FromResidual_Infallible_for_Option. +Export Impl_FromResidual_Infallible_for_Option. diff --git a/CoqOfRust/core/mem/maybe_uninit.v b/CoqOfRust/core/mem/maybe_uninit.v index 8e0237951..f366c60d2 100644 --- a/CoqOfRust/core/mem/maybe_uninit.v +++ b/CoqOfRust/core/mem/maybe_uninit.v @@ -241,7 +241,7 @@ Module mem. match ε, τ, α with | [ N ], [], [] => ltac:(M.monadic - (repeat (| + (lib.repeat (| M.read (| get_constant (| "core::mem::maybe_uninit::uninit_array_discriminant", diff --git a/CoqOfRust/core/net/display_buffer.v b/CoqOfRust/core/net/display_buffer.v index 35cd27bb1..61010da46 100644 --- a/CoqOfRust/core/net/display_buffer.v +++ b/CoqOfRust/core/net/display_buffer.v @@ -39,7 +39,7 @@ Module net. [] [ ("buf", - repeat (| + lib.repeat (| M.call_closure (| Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ Ty.path "u8" ], M.get_associated_function (| diff --git a/CoqOfRust/core/net/parser.v b/CoqOfRust/core/net/parser.v index 63048f9bc..7c49cae51 100644 --- a/CoqOfRust/core/net/parser.v +++ b/CoqOfRust/core/net/parser.v @@ -3327,7 +3327,7 @@ Module net. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in @@ -3954,7 +3954,7 @@ Module net. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u16" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U16 0, Value.Integer IntegerKind.Usize 8 |) in @@ -4344,7 +4344,7 @@ Module net. (Ty.path "array") [ Value.Integer IntegerKind.Usize 7 ] [ Ty.path "u16" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U16 0, Value.Integer IntegerKind.Usize 7 |) in diff --git a/CoqOfRust/core/num/bignum.v b/CoqOfRust/core/num/bignum.v index 7a4cd1c2f..868d45bec 100644 --- a/CoqOfRust/core/num/bignum.v +++ b/CoqOfRust/core/num/bignum.v @@ -633,7 +633,10 @@ Module num. (Ty.path "array") [ Value.Integer IntegerKind.Usize 40 ] [ Ty.path "u32" ] := - repeat (| Value.Integer IntegerKind.U32 0, Value.Integer IntegerKind.Usize 40 |) in + lib.repeat (| + Value.Integer IntegerKind.U32 0, + Value.Integer IntegerKind.Usize 40 + |) in let~ _ : Ty.tuple [] := M.write (| M.SubPointer.get_array_field (| base, Value.Integer IntegerKind.Usize 0 |), @@ -678,7 +681,10 @@ Module num. (Ty.path "array") [ Value.Integer IntegerKind.Usize 40 ] [ Ty.path "u32" ] := - repeat (| Value.Integer IntegerKind.U32 0, Value.Integer IntegerKind.Usize 40 |) in + lib.repeat (| + Value.Integer IntegerKind.U32 0, + Value.Integer IntegerKind.Usize 40 + |) in let~ sz : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in let~ _ : Ty.tuple [] := M.read (| @@ -3889,7 +3895,7 @@ Module num. (Ty.path "array") [ Value.Integer IntegerKind.Usize 40 ] [ Ty.path "u32" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U32 0, Value.Integer IntegerKind.Usize 40 |) in @@ -6960,7 +6966,10 @@ Module num. (Ty.path "array") [ Value.Integer IntegerKind.Usize 3 ] [ Ty.path "u8" ] := - repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 3 |) in + lib.repeat (| + Value.Integer IntegerKind.U8 0, + Value.Integer IntegerKind.Usize 3 + |) in let~ _ : Ty.tuple [] := M.write (| M.SubPointer.get_array_field (| base, Value.Integer IntegerKind.Usize 0 |), @@ -7005,7 +7014,10 @@ Module num. (Ty.path "array") [ Value.Integer IntegerKind.Usize 3 ] [ Ty.path "u8" ] := - repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 3 |) in + lib.repeat (| + Value.Integer IntegerKind.U8 0, + Value.Integer IntegerKind.Usize 3 + |) in let~ sz : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in let~ _ : Ty.tuple [] := M.read (| @@ -10299,7 +10311,7 @@ Module num. (Ty.path "array") [ Value.Integer IntegerKind.Usize 3 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 3 |) in diff --git a/CoqOfRust/core/num/dec2flt/common.v b/CoqOfRust/core/num/dec2flt/common.v index d67dca046..f3288ed20 100644 --- a/CoqOfRust/core/num/dec2flt/common.v +++ b/CoqOfRust/core/num/dec2flt/common.v @@ -28,7 +28,10 @@ Module num. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in + lib.repeat (| + Value.Integer IntegerKind.U8 0, + Value.Integer IntegerKind.Usize 8 + |) in let~ _ : Ty.tuple [] := M.call_closure (| Ty.tuple [], diff --git a/CoqOfRust/core/num/dec2flt/decimal.v b/CoqOfRust/core/num/dec2flt/decimal.v index 2ce708cfc..3339356dd 100644 --- a/CoqOfRust/core/num/dec2flt/decimal.v +++ b/CoqOfRust/core/num/dec2flt/decimal.v @@ -191,7 +191,7 @@ Module num. ("decimal_point", Value.Integer IntegerKind.I32 0); ("truncated", Value.Bool false); ("digits", - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 768 |)) diff --git a/CoqOfRust/core/num/int_sqrt.v b/CoqOfRust/core/num/int_sqrt.v index 4f06b8fd2..361fdcf96 100644 --- a/CoqOfRust/core/num/int_sqrt.v +++ b/CoqOfRust/core/num/int_sqrt.v @@ -14,7 +14,7 @@ Module num. (Ty.path "array") [ Value.Integer IntegerKind.Usize 256 ] [ Ty.tuple [ Ty.path "u8"; Ty.path "u8" ] ] := - repeat (| + lib.repeat (| Value.Tuple [ Value.Integer IntegerKind.U8 0; Value.Integer IntegerKind.U8 0 ], Value.Integer IntegerKind.Usize 256 |) in diff --git a/CoqOfRust/core/num/links/mod.v b/CoqOfRust/core/num/links/mod.v index 057fee558..2b24c5373 100644 --- a/CoqOfRust/core/num/links/mod.v +++ b/CoqOfRust/core/num/links/mod.v @@ -4,6 +4,19 @@ Require Import core.intrinsics.links.mod. Require Import core.links.array. Require Import core.num.mod. +Module Impl_u16. + Definition Self : Set := U16.t. + + (* pub const fn to_be_bytes(self) -> [u8; 2] *) + Instance run_to_be_bytes (self: Self) : + Run.Trait num.Impl_u16.to_be_bytes [] [] [ φ self ] (array.t U8.t {| Integer.value := 2 |}). + Proof. + constructor. + run_symbolic. + Admitted. +End Impl_u16. +Export Impl_u16. + Module Impl_u64. Definition Self : Set := U64.t. diff --git a/CoqOfRust/core/num/mod.v b/CoqOfRust/core/num/mod.v index 7106a2f07..a02b390ec 100644 --- a/CoqOfRust/core/num/mod.v +++ b/CoqOfRust/core/num/mod.v @@ -105077,7 +105077,7 @@ Module num. M.call_closure (| Ty.path "usize", M.get_associated_function (| Ty.path "usize", "from_ne_bytes", [], [] |), - [ repeat (| M.read (| x |), Value.Integer IntegerKind.Usize 8 |) ] + [ lib.repeat (| M.read (| x |), Value.Integer IntegerKind.Usize 8 |) ] |))) | _, _, _ => M.impossible "wrong number of arguments" end. diff --git a/CoqOfRust/core/ops/links/range.v b/CoqOfRust/core/ops/links/range.v index ead6ededd..4c4fd3e7c 100644 --- a/CoqOfRust/core/ops/links/range.v +++ b/CoqOfRust/core/ops/links/range.v @@ -1,6 +1,7 @@ Require Import CoqOfRust.CoqOfRust. Require Import CoqOfRust.links.M. Require Import core.links.cmp. +Require Import core.links.clone. Require Import core.ops.range. (* @@ -38,6 +39,15 @@ Module Range. Smpl Add eapply of_ty : of_ty. End Range. +Module Impl_Clone_for_Range. + Definition Self (Idx : Set) : Set := + Range.t Idx. + + Instance run (Idx : Set) `{Link Idx} : Clone.Run (Self Idx). + Admitted. +End Impl_Clone_for_Range. +Export Impl_Clone_for_Range. + Module Impl_Range. Definition Self (Idx : Set) : Set := Range.t Idx. diff --git a/CoqOfRust/core/slice/links/mod.v b/CoqOfRust/core/slice/links/mod.v index 4aa52dbbd..cc8bbf15b 100644 --- a/CoqOfRust/core/slice/links/mod.v +++ b/CoqOfRust/core/slice/links/mod.v @@ -59,6 +59,14 @@ Module Impl_Slice. run_symbolic. Defined. + (* pub fn iter(&self) -> Iter<'_, T> *) + Instance run_iter + (T : Set) `{Link T} + (self : Ref.t Pointer.Kind.Ref (Self T)) : + Run.Trait (slice.Impl_slice_T.iter (Φ T)) [] [] [φ self] + (Iter.t T). + Admitted. + (* pub fn iter_mut(&mut self) -> IterMut<'_, T> *) Instance run_iter_mut (T : Set) `{Link T} diff --git a/CoqOfRust/core/slice/sort/stable/mod.v b/CoqOfRust/core/slice/sort/stable/mod.v index dc6ac7e97..0650fe264 100644 --- a/CoqOfRust/core/slice/sort/stable/mod.v +++ b/CoqOfRust/core/slice/sort/stable/mod.v @@ -638,7 +638,7 @@ Module slice. [ ("_align", Value.Array []); ("storage", - repeat (| + lib.repeat (| M.read (| get_constant (| "core::slice::sort::stable::new_discriminant", diff --git a/CoqOfRust/core/str/iter.v b/CoqOfRust/core/str/iter.v index ff7845db5..f88b1e871 100644 --- a/CoqOfRust/core/str/iter.v +++ b/CoqOfRust/core/str/iter.v @@ -411,7 +411,7 @@ Module str. (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "bool" ] := - repeat (| + lib.repeat (| Value.Bool false, Value.Integer IntegerKind.Usize 32 |) in @@ -12309,7 +12309,7 @@ Module str. (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u16" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U16 0, Value.Integer IntegerKind.Usize 2 |) in diff --git a/CoqOfRust/core/str/pattern.v b/CoqOfRust/core/str/pattern.v index 1996bd40f..7be74fe43 100644 --- a/CoqOfRust/core/str/pattern.v +++ b/CoqOfRust/core/str/pattern.v @@ -4927,7 +4927,10 @@ Module str. (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~ utf8_size : Ty.path "u8" := M.call_closure (| Ty.path "u8", @@ -5102,7 +5105,7 @@ Module str. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in @@ -5191,7 +5194,7 @@ Module str. M.borrow (| Pointer.Kind.MutRef, M.alloc (| - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) @@ -5251,7 +5254,7 @@ Module str. M.borrow (| Pointer.Kind.MutRef, M.alloc (| - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) @@ -5311,7 +5314,7 @@ Module str. M.borrow (| Pointer.Kind.MutRef, M.alloc (| - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) @@ -5374,7 +5377,7 @@ Module str. M.borrow (| Pointer.Kind.MutRef, M.alloc (| - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) @@ -21130,7 +21133,7 @@ Module str. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u16" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U16 0, Value.Integer IntegerKind.Usize 4 |) in diff --git a/CoqOfRust/core/sync/atomic.v b/CoqOfRust/core/sync/atomic.v index cbb595692..3d49a3075 100644 --- a/CoqOfRust/core/sync/atomic.v +++ b/CoqOfRust/core/sync/atomic.v @@ -2511,7 +2511,9 @@ Module sync. (Ty.path "&mut") [] [ Ty.apply (Ty.path "core::sync::atomic::AtomicPtr") [] [ T ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -4205,7 +4207,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicI8" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -4330,7 +4334,9 @@ Module sync. (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicI8" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -5654,7 +5660,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicU8" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -5779,7 +5787,9 @@ Module sync. (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicU8" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -7113,7 +7123,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicI16" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -7238,7 +7250,9 @@ Module sync. (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicI16" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -8572,7 +8586,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicU16" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -8697,7 +8713,9 @@ Module sync. (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicU16" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -10031,7 +10049,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicI32" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -10156,7 +10176,9 @@ Module sync. (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicI32" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -11490,7 +11512,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicU32" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -11615,7 +11639,9 @@ Module sync. (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicU32" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -12949,7 +12975,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicI64" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -13074,7 +13102,9 @@ Module sync. (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicI64" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -14408,7 +14438,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicU64" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -14533,7 +14565,9 @@ Module sync. (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicU64" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -15867,7 +15901,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicIsize" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -15993,7 +16029,9 @@ Module sync. [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicIsize" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -17333,7 +17371,9 @@ Module sync. M.read (| M.match_operator (| Ty.apply (Ty.path "&mut") [] [ Ty.path "core::sync::atomic::AtomicUsize" ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic @@ -17459,7 +17499,9 @@ Module sync. [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "core::sync::atomic::AtomicUsize" ] ], - M.alloc (| repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) |), + M.alloc (| + lib.repeat (| Value.Tuple [], Value.Integer IntegerKind.Usize 0 |) + |), [ fun γ => ltac:(M.monadic diff --git a/CoqOfRust/examples/default/examples/custom/polymorphic_constants.v b/CoqOfRust/examples/default/examples/custom/polymorphic_constants.v index 9bf8bf3da..be6323fc1 100644 --- a/CoqOfRust/examples/default/examples/custom/polymorphic_constants.v +++ b/CoqOfRust/examples/default/examples/custom/polymorphic_constants.v @@ -90,7 +90,10 @@ Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := [ ("data", Value.Integer IntegerKind.I32 42); ("array", - repeat (| Value.Integer IntegerKind.I32 42, Value.Integer IntegerKind.Usize 3 |)) + lib.repeat (| + Value.Integer IntegerKind.I32 42, + Value.Integer IntegerKind.Usize 3 + |)) ] in let~ bar : Ty.apply diff --git a/CoqOfRust/examples/default/examples/ink_contracts/dns.v b/CoqOfRust/examples/default/examples/ink_contracts/dns.v index d665d88e8..ee8c82afa 100644 --- a/CoqOfRust/examples/default/examples/ink_contracts/dns.v +++ b/CoqOfRust/examples/default/examples/ink_contracts/dns.v @@ -627,7 +627,7 @@ Definition zero_address (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) [], [] |), - [ repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) ] + [ lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) ] |))) | _, _, _ => M.impossible "wrong number of arguments" end. diff --git a/CoqOfRust/examples/default/examples/ink_contracts/erc1155.v b/CoqOfRust/examples/default/examples/ink_contracts/erc1155.v index ce1512fd8..8e2da1bf6 100644 --- a/CoqOfRust/examples/default/examples/ink_contracts/erc1155.v +++ b/CoqOfRust/examples/default/examples/ink_contracts/erc1155.v @@ -446,7 +446,7 @@ Definition zero_address (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) [], [] |), - [ repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) ] + [ lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) ] |))) | _, _, _ => M.impossible "wrong number of arguments" end. diff --git a/CoqOfRust/examples/default/examples/ink_contracts/erc721.v b/CoqOfRust/examples/default/examples/ink_contracts/erc721.v index 742a74533..5c332bae2 100644 --- a/CoqOfRust/examples/default/examples/ink_contracts/erc721.v +++ b/CoqOfRust/examples/default/examples/ink_contracts/erc721.v @@ -1186,7 +1186,7 @@ Module Impl_erc721_Erc721. [] |), [ - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) @@ -2103,7 +2103,7 @@ Module Impl_erc721_Erc721. [] |), [ - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) @@ -3436,7 +3436,7 @@ Module Impl_erc721_Erc721. [] |), [ - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) diff --git a/CoqOfRust/examples/default/examples/ink_contracts/lang_err_integration_tests/constructors_return_value.v b/CoqOfRust/examples/default/examples/ink_contracts/lang_err_integration_tests/constructors_return_value.v index f939de753..a0246c1f9 100644 --- a/CoqOfRust/examples/default/examples/ink_contracts/lang_err_integration_tests/constructors_return_value.v +++ b/CoqOfRust/examples/default/examples/ink_contracts/lang_err_integration_tests/constructors_return_value.v @@ -424,7 +424,7 @@ Module Impl_constructors_return_value_ConstructorsReturnValue. [] |), [ - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) @@ -541,7 +541,7 @@ Module Impl_constructors_return_value_ConstructorsReturnValue. [] |), [ - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) diff --git a/CoqOfRust/examples/default/examples/ink_contracts/payment_channel.v b/CoqOfRust/examples/default/examples/ink_contracts/payment_channel.v index b7a50f1b4..170dc6f93 100644 --- a/CoqOfRust/examples/default/examples/ink_contracts/payment_channel.v +++ b/CoqOfRust/examples/default/examples/ink_contracts/payment_channel.v @@ -1032,7 +1032,7 @@ Module Impl_payment_channel_PaymentChannel. |) in let~ pub_key : Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 33 ] [ Ty.path "u8" ] := - repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 33 |) in + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 33 |) in let~ _ : Ty.tuple [] := M.call_closure (| Ty.tuple [], @@ -1101,7 +1101,7 @@ Module Impl_payment_channel_PaymentChannel. |) in let~ signature_account_id : Ty.apply (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 [], diff --git a/CoqOfRust/examples/default/examples/rust_book/primitives/arrays_and_slices.v b/CoqOfRust/examples/default/examples/rust_book/primitives/arrays_and_slices.v index 5f023d36c..86f92d451 100644 --- a/CoqOfRust/examples/default/examples/rust_book/primitives/arrays_and_slices.v +++ b/CoqOfRust/examples/default/examples/rust_book/primitives/arrays_and_slices.v @@ -244,7 +244,7 @@ Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := ] in let~ ys : Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 500 ] [ Ty.path "i32" ] := - repeat (| Value.Integer IntegerKind.I32 0, Value.Integer IntegerKind.Usize 500 |) in + lib.repeat (| Value.Integer IntegerKind.I32 0, Value.Integer IntegerKind.Usize 500 |) in let~ _ : Ty.tuple [] := M.read (| let~ _ : Ty.tuple [] := diff --git a/CoqOfRust/examples/default/examples/rust_book/unsafe_operations/inline_assembly_clobbered_registers.v b/CoqOfRust/examples/default/examples/rust_book/unsafe_operations/inline_assembly_clobbered_registers.v index b12e8e0b2..b51ae5ecb 100644 --- a/CoqOfRust/examples/default/examples/rust_book/unsafe_operations/inline_assembly_clobbered_registers.v +++ b/CoqOfRust/examples/default/examples/rust_book/unsafe_operations/inline_assembly_clobbered_registers.v @@ -43,7 +43,7 @@ Definition main (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := (M.read (| let~ name_buf : Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 12 ] [ Ty.path "u8" ] := - repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 12 |) in + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 12 |) in let~ _ : Ty.tuple [] := M.read (| let~ _ : Ty.tuple [] := M.read (| InlineAssembly |) in diff --git a/CoqOfRust/move_sui/translations/move_binary_format/deserializer.v b/CoqOfRust/move_sui/translations/move_binary_format/deserializer.v index 13623d381..7ced26d4b 100644 --- a/CoqOfRust/move_sui/translations/move_binary_format/deserializer.v +++ b/CoqOfRust/move_sui/translations/move_binary_format/deserializer.v @@ -709,7 +709,7 @@ Module deserializer. (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 2 |) in @@ -957,7 +957,7 @@ Module deserializer. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in @@ -1205,7 +1205,7 @@ Module deserializer. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in @@ -1453,7 +1453,7 @@ Module deserializer. (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 16 |) in @@ -1706,7 +1706,7 @@ Module deserializer. (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) in @@ -48789,7 +48789,7 @@ Module deserializer. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in diff --git a/CoqOfRust/move_sui/translations/move_binary_format/file_format_common.v b/CoqOfRust/move_sui/translations/move_binary_format/file_format_common.v index 6968dc688..fecaa7f81 100644 --- a/CoqOfRust/move_sui/translations/move_binary_format/file_format_common.v +++ b/CoqOfRust/move_sui/translations/move_binary_format/file_format_common.v @@ -4699,7 +4699,7 @@ Module file_format_common. (Ty.path "array") [ Value.Integer IntegerKind.Usize 1 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 1 |) in @@ -4880,7 +4880,7 @@ Module file_format_common. (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in diff --git a/CoqOfRust/move_sui/translations/move_core_types/account_address.v b/CoqOfRust/move_sui/translations/move_core_types/account_address.v index c9a83ac2c..7417ed2ae 100644 --- a/CoqOfRust/move_sui/translations/move_core_types/account_address.v +++ b/CoqOfRust/move_sui/translations/move_core_types/account_address.v @@ -376,7 +376,7 @@ Module account_address. "move_core_types::account_address::AccountAddress" [] [] - [ repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) ] + [ lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) ] |))). Global Instance AssociatedConstant_value_ZERO : M.IsAssociatedFunction.C Self "ZERO" value_ZERO. @@ -442,7 +442,7 @@ Module account_address. (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.write (| M.SubPointer.get_array_field (| @@ -497,7 +497,7 @@ Module account_address. (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.write (| M.SubPointer.get_array_field (| diff --git a/CoqOfRust/move_sui/translations/move_core_types/annotated_visitor.v b/CoqOfRust/move_sui/translations/move_core_types/annotated_visitor.v index fb47016b6..d8e023098 100644 --- a/CoqOfRust/move_sui/translations/move_core_types/annotated_visitor.v +++ b/CoqOfRust/move_sui/translations/move_core_types/annotated_visitor.v @@ -6875,7 +6875,7 @@ Module annotated_visitor. (M.alloc (| M.read (| let~ buf : 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 (| diff --git a/CoqOfRust/move_sui/translations/move_core_types/u256.v b/CoqOfRust/move_sui/translations/move_core_types/u256.v index 9a9f295b0..4512d0527 100644 --- a/CoqOfRust/move_sui/translations/move_core_types/u256.v +++ b/CoqOfRust/move_sui/translations/move_core_types/u256.v @@ -3145,7 +3145,7 @@ Module u256. (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 [], @@ -5759,7 +5759,7 @@ Module u256. (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 [], diff --git a/CoqOfRust/plonky3/field/array.v b/CoqOfRust/plonky3/field/array.v index 46454128d..c74f95014 100644 --- a/CoqOfRust/plonky3/field/array.v +++ b/CoqOfRust/plonky3/field/array.v @@ -460,7 +460,7 @@ Module array. [], [] |), - [ repeat (| M.read (| val |), N |) ] + [ lib.repeat (| M.read (| val |), N |) ] |))) | _, _, _ => M.impossible "wrong number of arguments" end. @@ -535,7 +535,7 @@ Module array. [ N ] [ F ] [ - repeat (| + lib.repeat (| M.read (| get_constant (| "p3_field::field::PrimeCharacteristicRing::ZERO", F |) |), N |) @@ -559,7 +559,7 @@ Module array. [ N ] [ F ] [ - repeat (| + lib.repeat (| M.read (| get_constant (| "p3_field::field::PrimeCharacteristicRing::ONE", F |) |), N |) @@ -583,7 +583,7 @@ Module array. [ N ] [ F ] [ - repeat (| + lib.repeat (| M.read (| get_constant (| "p3_field::field::PrimeCharacteristicRing::TWO", F |) |), N |) @@ -607,7 +607,7 @@ Module array. [ N ] [ F ] [ - repeat (| + lib.repeat (| M.read (| get_constant (| "p3_field::field::PrimeCharacteristicRing::NEG_ONE", F |) |), diff --git a/CoqOfRust/plonky3/field/extension/binomial_extension.v b/CoqOfRust/plonky3/field/extension/binomial_extension.v index 8f86d2b82..a24a20642 100644 --- a/CoqOfRust/plonky3/field/extension/binomial_extension.v +++ b/CoqOfRust/plonky3/field/extension/binomial_extension.v @@ -3498,7 +3498,7 @@ Module extension. [] |), [ - repeat (| + lib.repeat (| M.read (| get_constant (| "p3_field::field::PrimeCharacteristicRing::ZERO", A |) |), diff --git a/CoqOfRust/plonky3/field/extension/packed_binomial_extension.v b/CoqOfRust/plonky3/field/extension/packed_binomial_extension.v index 61fcbb90a..d961a9701 100644 --- a/CoqOfRust/plonky3/field/extension/packed_binomial_extension.v +++ b/CoqOfRust/plonky3/field/extension/packed_binomial_extension.v @@ -1436,7 +1436,7 @@ Module extension. [ F; PF ] [ ("value", - repeat (| + lib.repeat (| M.read (| get_constant (| "p3_field::field::PrimeCharacteristicRing::ZERO", PF |) |), diff --git a/CoqOfRust/plonky3/field/helpers.v b/CoqOfRust/plonky3/field/helpers.v index c04d42b8f..9c37176db 100644 --- a/CoqOfRust/plonky3/field/helpers.v +++ b/CoqOfRust/plonky3/field/helpers.v @@ -757,7 +757,7 @@ Module helpers. (Ty.path "array") [ D ] [ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ R ] ] := - repeat (| + lib.repeat (| M.read (| get_constant (| "p3_field::helpers::field_to_array_discriminant", diff --git a/CoqOfRust/plonky3/keccak_air/generation.v b/CoqOfRust/plonky3/keccak_air/generation.v index 13a59c9bc..f6ebf3143 100644 --- a/CoqOfRust/plonky3/keccak_air/generation.v +++ b/CoqOfRust/plonky3/keccak_air/generation.v @@ -1281,7 +1281,7 @@ Module generation. ] |), [ - repeat (| + lib.repeat (| Value.Integer IntegerKind.U64 0, Value.Integer IntegerKind.Usize 25 |); diff --git a/CoqOfRust/plonky3/util/lib.v b/CoqOfRust/plonky3/util/lib.v index 82f5a6776..38d4c15d4 100644 --- a/CoqOfRust/plonky3/util/lib.v +++ b/CoqOfRust/plonky3/util/lib.v @@ -316,7 +316,7 @@ Definition indices_arr (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) ltac:(M.monadic (M.read (| let~ indices_arr : Ty.apply (Ty.path "array") [ N ] [ Ty.path "usize" ] := - repeat (| Value.Integer IntegerKind.Usize 0, N |) in + lib.repeat (| Value.Integer IntegerKind.Usize 0, N |) in let~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in let~ _ : Ty.tuple [] := M.read (| @@ -2446,7 +2446,7 @@ Definition iter_next_chunk (ε : list Value.t) (τ : list Ty.t) (α : list Value "Item" ] ] := - repeat (| + lib.repeat (| M.read (| get_constant (| "p3_util::iter_next_chunk_discriminant", diff --git a/CoqOfRust/revm/revm_bytecode/eof/links/header.v b/CoqOfRust/revm/revm_bytecode/eof/links/header.v index 59df1affe..d5c6ac2b5 100644 --- a/CoqOfRust/revm/revm_bytecode/eof/links/header.v +++ b/CoqOfRust/revm/revm_bytecode/eof/links/header.v @@ -3,13 +3,14 @@ Require Import links.M. Require Import alloc.links.alloc. Require Import alloc.vec.links.mod. Require Import alloc.vec.links.mod. +Require Import core.links.result. Require Import revm_bytecode.eof.header. Module EofHeader. Record t : Set := { types_size: U16.t; - code_sizes: alloc.vec.links.mod.Vec.t U16.t alloc.links.alloc.Global.t; - container_sizes: alloc.vec.links.mod.Vec.t U16.t alloc.links.alloc.Global.t; + code_sizes: Vec.t U16.t Global.t; + container_sizes: Vec.t U16.t Global.t; data_size: U16.t; sum_code_sizes: Usize.t; sum_container_sizes: Usize.t; @@ -31,6 +32,145 @@ Module EofHeader. Definition of_ty : OfTy.t (Ty.path "revm_bytecode::eof::header::EofHeader"). Proof. eapply OfTy.Make with (A := t); reflexivity. Defined. Smpl Add apply of_ty : of_ty. + + Lemma of_value_with + types_size' types_size + code_sizes' code_sizes + container_sizes' container_sizes + data_size' data_size + sum_code_sizes' sum_code_sizes + sum_container_sizes' sum_container_sizes : + types_size' = φ types_size -> + code_sizes' = φ code_sizes -> + container_sizes' = φ container_sizes -> + data_size' = φ data_size -> + sum_code_sizes' = φ sum_code_sizes -> + sum_container_sizes' = φ sum_container_sizes -> + Value.StructRecord "revm_bytecode::eof::header::EofHeader" [] [] [ + ("types_size", types_size'); + ("code_sizes", code_sizes'); + ("container_sizes", container_sizes'); + ("data_size", data_size'); + ("sum_code_sizes", sum_code_sizes'); + ("sum_container_sizes", sum_container_sizes') + ] = + φ (Build_t types_size code_sizes container_sizes data_size sum_code_sizes sum_container_sizes). + Proof. + intros; now subst. + Qed. + Smpl Add unshelve eapply of_value_with : of_value. + + Definition of_value + types_size' (types_size : U16.t) + code_sizes' (code_sizes : Vec.t U16.t Global.t) + container_sizes' (container_sizes : Vec.t U16.t Global.t) + data_size' (data_size : U16.t) + sum_code_sizes' (sum_code_sizes : Usize.t) + sum_container_sizes' (sum_container_sizes : Usize.t) : + types_size' = φ types_size -> + code_sizes' = φ code_sizes -> + container_sizes' = φ container_sizes -> + data_size' = φ data_size -> + sum_code_sizes' = φ sum_code_sizes -> + sum_container_sizes' = φ sum_container_sizes -> + OfValue.t ( + Value.StructRecord "revm_bytecode::eof::header::EofHeader" [] [] [ + ("types_size", types_size'); + ("code_sizes", code_sizes'); + ("container_sizes", container_sizes'); + ("data_size", data_size'); + ("sum_code_sizes", sum_code_sizes'); + ("sum_container_sizes", sum_container_sizes') + ] + ). + Proof. econstructor; apply of_value_with; eassumption. Defined. + Smpl Add unshelve eapply of_value : of_value. + + Module SubPointer. + Definition get_types_size : SubPointer.Runner.t t + (Pointer.Index.StructRecord "revm_bytecode::eof::header::EofHeader" "types_size") := + {| + SubPointer.Runner.projection x := Some x.(types_size); + SubPointer.Runner.injection x y := Some (x <| types_size := y |>); + |}. + + Lemma get_types_size_is_valid : + SubPointer.Runner.Valid.t get_types_size. + Proof. + now constructor. + Qed. + Smpl Add apply get_types_size_is_valid : run_sub_pointer. + + Definition get_code_sizes : SubPointer.Runner.t t + (Pointer.Index.StructRecord "revm_bytecode::eof::header::EofHeader" "code_sizes") := + {| + SubPointer.Runner.projection x := Some x.(code_sizes); + SubPointer.Runner.injection x y := Some (x <| code_sizes := y |>); + |}. + + Lemma get_code_sizes_is_valid : + SubPointer.Runner.Valid.t get_code_sizes. + Proof. + now constructor. + Qed. + Smpl Add apply get_code_sizes_is_valid : run_sub_pointer. + + Definition get_container_sizes : SubPointer.Runner.t t + (Pointer.Index.StructRecord "revm_bytecode::eof::header::EofHeader" "container_sizes") := + {| + SubPointer.Runner.projection x := Some x.(container_sizes); + SubPointer.Runner.injection x y := Some (x <| container_sizes := y |>); + |}. + + Lemma get_container_sizes_is_valid : + SubPointer.Runner.Valid.t get_container_sizes. + Proof. + now constructor. + Qed. + Smpl Add apply get_container_sizes_is_valid : run_sub_pointer. + + Definition get_data_size : SubPointer.Runner.t t + (Pointer.Index.StructRecord "revm_bytecode::eof::header::EofHeader" "data_size") := + {| + SubPointer.Runner.projection x := Some x.(data_size); + SubPointer.Runner.injection x y := Some (x <| data_size := y |>); + |}. + + Lemma get_data_size_is_valid : + SubPointer.Runner.Valid.t get_data_size. + Proof. + now constructor. + Qed. + Smpl Add apply get_data_size_is_valid : run_sub_pointer. + + Definition get_sum_code_sizes : SubPointer.Runner.t t + (Pointer.Index.StructRecord "revm_bytecode::eof::header::EofHeader" "sum_code_sizes") := + {| + SubPointer.Runner.projection x := Some x.(sum_code_sizes); + SubPointer.Runner.injection x y := Some (x <| sum_code_sizes := y |>); + |}. + + Lemma get_sum_code_sizes_is_valid : + SubPointer.Runner.Valid.t get_sum_code_sizes. + Proof. + now constructor. + Qed. + Smpl Add apply get_sum_code_sizes_is_valid : run_sub_pointer. + + Definition get_sum_container_sizes : SubPointer.Runner.t t + (Pointer.Index.StructRecord "revm_bytecode::eof::header::EofHeader" "sum_container_sizes") := + {| + SubPointer.Runner.projection x := Some x.(sum_container_sizes); + SubPointer.Runner.injection x y := Some (x <| sum_container_sizes := y |>); + |}. + + Lemma get_sum_container_sizes_is_valid : + SubPointer.Runner.Valid.t get_sum_container_sizes. + Proof. + now constructor. + Qed. + Smpl Add apply get_sum_container_sizes_is_valid : run_sub_pointer. + End SubPointer. End EofHeader. Module Impl_EofHeader. @@ -43,10 +183,23 @@ Module Impl_EofHeader. Run.Trait header.eof.header.Impl_revm_bytecode_eof_header_EofHeader.size [] [] [φ self] Usize.t. Admitted. + (* pub fn eof_size(&self) -> usize *) + Instance run_eof_size (self : Ref.t Pointer.Kind.Ref Self) : + Run.Trait header.eof.header.Impl_revm_bytecode_eof_header_EofHeader.eof_size [] [] [φ self] + Usize.t. + Admitted. + (* pub fn encode(&self, buffer: &mut Vec) *) Instance run_encode (self : Ref.t Pointer.Kind.Ref Self) (buffer : Ref.t Pointer.Kind.MutPointer (Vec.t U8.t Global.t)) : Run.Trait header.eof.header.Impl_revm_bytecode_eof_header_EofHeader.encode [] [] [φ self; φ buffer] unit. Admitted. + + (* pub fn decode(input: &[u8]) -> Result<(Self, &[u8]), EofDecodeError> *) + Instance run_decode (input : Ref.t Pointer.Kind.Ref (list U8.t)) : + Run.Trait header.eof.header.Impl_revm_bytecode_eof_header_EofHeader.decode [] [] [φ input] + (Result.t Self (Ref.t Pointer.Kind.Ref (list U8.t))). + Admitted. End Impl_EofHeader. +Export Impl_EofHeader. diff --git a/CoqOfRust/revm/revm_bytecode/opcode.v b/CoqOfRust/revm/revm_bytecode/opcode.v index 0cbddbf93..5425f75d3 100644 --- a/CoqOfRust/revm/revm_bytecode/opcode.v +++ b/CoqOfRust/revm/revm_bytecode/opcode.v @@ -3942,7 +3942,7 @@ Module opcode. [] [ Ty.path "revm_bytecode::opcode::OpCodeInfo" ] ] := - repeat (| + lib.repeat (| Value.StructTuple "core::option::Option::None" [] diff --git a/CoqOfRust/revm/revm_interpreter/instructions.v b/CoqOfRust/revm/revm_interpreter/instructions.v index fd7e13d64..ff6632801 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions.v +++ b/CoqOfRust/revm/revm_interpreter/instructions.v @@ -111,7 +111,7 @@ Module instructions. ] (Ty.tuple []) ] := - repeat (| + lib.repeat (| M.read (| M.use (M.alloc (| diff --git a/CoqOfRust/revm/revm_interpreter/instructions/data.v b/CoqOfRust/revm/revm_interpreter/instructions/data.v index 274c2528b..3d7a563c3 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/data.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/data.v @@ -533,7 +533,7 @@ Module instructions. (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) in @@ -952,7 +952,7 @@ Module instructions. (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) in diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract.v index 570cd33ef..854576d76 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/contract.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract.v @@ -38,376 +38,16 @@ Require Import ruint.links.cmp. Require Import ruint.links.from. Require Import ruint.links.lib. -(* -pub fn eofcreate( - interpreter: &mut Interpreter, - _host: &mut H, -) -*) -Instance run_eofcreate - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (_host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.eofcreate [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE eqn:?. - destruct run_StackTrait_for_Stack. - destruct run_MemoryTrait_for_Memory. - destruct run_LoopControl_for_Control. - destruct run_Immediates_for_Bytecode. - destruct run_Jumps_for_Bytecode. - destruct run_EofContainer_for_Bytecode. - destruct run_InputsTrait_for_Input. - destruct run_RuntimeFlag_for_RuntimeFlag. - destruct Impl_Clone_for_Bytes.run. - destruct Impl_Default_for_Bytes.run. - destruct links.mod.Impl_Deref_for_Bytes.run. - destruct (Impl_Into_for_From_T.run Impl_From_Vec_u8_for_Bytes.run). - run_symbolic. -Admitted. - -(* -pub fn return_contract( - interpreter: &mut Interpreter, - _host: &mut H, -) -*) -Instance run_return_contract - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (_host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.return_contract [] [ Φ H; Φ WIRE ] [ φ interpreter; φ _host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE. - destruct run_StackTrait_for_Stack. - destruct run_LoopControl_for_Control. - destruct run_Immediates_for_Bytecode. - destruct run_EofContainer_for_Bytecode. - destruct run_RuntimeFlag_for_RuntimeFlag. - destruct Impl_Clone_for_Bytes.run. - destruct links.mod.Impl_Deref_for_Bytes.run. - destruct bytes.Impl_Deref_for_Bytes.run. - do 100 try run_symbolic_one_step. - (* Too slow. Maybe a non-linear part in the proof. *) -Admitted. - -(* -pub fn extcall_input(interpreter: &mut Interpreter) -> Option -*) -Instance run_extcall_input - {WIRE : Set} `{Link WIRE} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) : - Run.Trait - instructions.contract.extcall_input [] [ Φ WIRE ] [ φ interpreter ] - (option Bytes.t). -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE eqn:?. - destruct run_StackTrait_for_Stack. - destruct run_MemoryTrait_for_Memory. - destruct (Impl_Try_for_Option.run Bytes.t). - destruct run_FromResidual_for_Self. - destruct (Impl_Try_for_Option.run (Range.t Usize.t)). - destruct (Impl_AsRef_for_Slice.run U8.t). - run_symbolic. -Admitted. - -(* -pub fn extcall_gas_calc( - interpreter: &mut Interpreter, - host: &mut H, - target: Address, - transfers_value: bool, -) -> Option -*) -Instance run_extcall_gas_calc - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (host : Ref.t Pointer.Kind.MutRef H) - (target : Address.t) - (transfers_value : bool) : - Run.Trait - instructions.contract.extcall_gas_calc - [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host; φ target; φ transfers_value ] - (option U64.t). -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE. - destruct run_StackTrait_for_Stack. - destruct run_LoopControl_for_Control. - destruct run_RuntimeFlag_for_RuntimeFlag. - destruct run_Host_for_H. - run_symbolic. -Admitted. - -(* -pub fn pop_extcall_target_address( - interpreter: &mut Interpreter, -) -> Option

-*) -Instance run_pop_extcall_target_address - {WIRE : Set} `{Link WIRE} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) : - Run.Trait - instructions.contract.pop_extcall_target_address [] [ Φ WIRE ] [ φ interpreter ] - (option Address.t). -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE. - destruct run_StackTrait_for_Stack. - destruct Impl_From_U256_for_FixedBytes_32.run. - destruct (Impl_Iterator_for_Iter.run U8.t). - run_symbolic. -Admitted. - -(* -pub fn extcall( - interpreter: &mut Interpreter, - host: &mut H, -) -*) -Instance run_extcall - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.extcall [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE eqn:?. - destruct run_StackTrait_for_Stack. - destruct run_LoopControl_for_Control. - destruct run_InputsTrait_for_Input. - destruct run_RuntimeFlag_for_RuntimeFlag. - run_symbolic. -Admitted. - -(* -pub fn extdelegatecall( - interpreter: &mut Interpreter, - host: &mut H, -) -*) -Instance run_extdelegatecall - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.extdelegatecall [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE eqn:?. - destruct run_LoopControl_for_Control. - destruct run_InputsTrait_for_Input. - destruct run_RuntimeFlag_for_RuntimeFlag. - run_symbolic. -Admitted. - -(* -pub fn extstaticcall( - interpreter: &mut Interpreter, - host: &mut H, -) -*) -Instance run_extstaticcall - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.extstaticcall [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE eqn:?. - destruct run_LoopControl_for_Control. - destruct run_InputsTrait_for_Input. - destruct run_RuntimeFlag_for_RuntimeFlag. - run_symbolic. -Admitted. - -(* -pub fn create( - interpreter: &mut Interpreter, - host: &mut H, -) -*) -Instance run_create - (IS_CREATE2 : bool) - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.create [ φ IS_CREATE2 ] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE. - destruct run_StackTrait_for_Stack. - destruct run_MemoryTrait_for_Memory. - destruct run_LoopControl_for_Control. - destruct run_InputsTrait_for_Input. - destruct run_RuntimeFlag_for_RuntimeFlag. - destruct run_Host_for_H. - destruct run_CfgGetter_for_Self. - destruct run_Cfg_for_Cfg. - destruct (Impl_AsRef_for_Slice.run U8.t). - run_symbolic. -Admitted. - -(* -pub fn call( - interpreter: &mut Interpreter, - host: &mut H, -) -*) -Instance run_call - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.call [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE eqn:?. - destruct run_StackTrait_for_Stack. - destruct run_LoopControl_for_Control. - destruct run_InputsTrait_for_Input. - destruct run_RuntimeFlag_for_RuntimeFlag. - destruct run_Host_for_H. - destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}). - destruct Impl_IntoAddress_for_U256.run. - run_symbolic. -Admitted. - -(* -pub fn call_code( - interpreter: &mut Interpreter, - host: &mut H, -) -*) -Instance run_call_code - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.call_code [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE eqn:?. - destruct run_StackTrait_for_Stack. - destruct run_MemoryTrait_for_Memory. - destruct run_LoopControl_for_Control. - destruct run_InputsTrait_for_Input. - destruct run_RuntimeFlag_for_RuntimeFlag. - destruct run_Host_for_H. - destruct Impl_From_U256_for_FixedBytes_32.run. - destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}). - run_symbolic. -Admitted. - - -(* -pub fn delegate_call( - interpreter: &mut Interpreter, - host: &mut H, -) -*) -Instance run_delegate_call - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.delegate_call [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE eqn:?. - destruct run_StackTrait_for_Stack. - destruct run_LoopControl_for_Control. - destruct run_InputsTrait_for_Input. - destruct run_RuntimeFlag_for_RuntimeFlag. - destruct run_Host_for_H. - destruct Impl_From_U256_for_FixedBytes_32.run. - destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}). - run_symbolic. -Admitted. - -(* -pub fn static_call( - interpreter: &mut Interpreter, - host: &mut H, -) -*) -Instance run_static_call - {WIRE H : Set} `{Link WIRE} `{Link H} - {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} - {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} - (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) - (run_Host_for_H : Host.Run H H_types) - (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) - (host : Ref.t Pointer.Kind.MutRef H) : - Run.Trait - instructions.contract.static_call [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] - unit. -Proof. - constructor. - destruct run_InterpreterTypes_for_WIRE eqn:?. - destruct run_StackTrait_for_Stack. - destruct run_LoopControl_for_Control. - destruct run_InputsTrait_for_Input. - destruct run_RuntimeFlag_for_RuntimeFlag. - destruct run_Host_for_H. - destruct Impl_From_U256_for_FixedBytes_32.run. - destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}). - run_symbolic. -Admitted. +Require Export revm.revm_interpreter.instructions.links.contract.call_code. +Require Export revm.revm_interpreter.instructions.links.contract.call. +Require Export revm.revm_interpreter.instructions.links.contract.create. +Require Export revm.revm_interpreter.instructions.links.contract.delegate_call. +Require Export revm.revm_interpreter.instructions.links.contract.eofcreate. +Require Export revm.revm_interpreter.instructions.links.contract.extcall_gas_calc. +Require Export revm.revm_interpreter.instructions.links.contract.extcall_input. +Require Export revm.revm_interpreter.instructions.links.contract.extcall. +Require Export revm.revm_interpreter.instructions.links.contract.extdelegatecall. +Require Export revm.revm_interpreter.instructions.links.contract.extstaticcall. +Require Export revm.revm_interpreter.instructions.links.contract.pop_extcall_target_address. +Require Export revm.revm_interpreter.instructions.links.contract.return_contract. +Require Export revm.revm_interpreter.instructions.links.contract.static_call. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call.v new file mode 100644 index 000000000..fd9c7e042 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call.v @@ -0,0 +1,69 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn call( + interpreter: &mut Interpreter, + host: &mut H, +) +*) +Instance run_call + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.call [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE eqn:?. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + destruct run_InputsTrait_for_Input. + destruct run_RuntimeFlag_for_RuntimeFlag. + destruct run_Host_for_H. + destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}). + destruct Impl_IntoAddress_for_U256.run. + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call_code.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call_code.v new file mode 100644 index 000000000..391f26047 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/call_code.v @@ -0,0 +1,70 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn call_code( + interpreter: &mut Interpreter, + host: &mut H, +) +*) +Instance run_call_code + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.call_code [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE eqn:?. + destruct run_StackTrait_for_Stack. + destruct run_MemoryTrait_for_Memory. + destruct run_LoopControl_for_Control. + destruct run_InputsTrait_for_Input. + destruct run_RuntimeFlag_for_RuntimeFlag. + destruct run_Host_for_H. + destruct Impl_From_U256_for_FixedBytes_32.run. + destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}). + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/create.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/create.v new file mode 100644 index 000000000..03d123180 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/create.v @@ -0,0 +1,73 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn create( + interpreter: &mut Interpreter, + host: &mut H, +) +*) +Instance run_create + (IS_CREATE2 : bool) + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.create [ φ IS_CREATE2 ] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_MemoryTrait_for_Memory. + destruct run_LoopControl_for_Control. + destruct run_InputsTrait_for_Input. + destruct run_RuntimeFlag_for_RuntimeFlag. + destruct run_Host_for_H. + destruct run_CfgGetter_for_Self. + destruct run_Cfg_for_Cfg. + destruct (Impl_AsRef_for_Slice.run U8.t). + destruct run_Deref_for_Synthetic1. + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/delegate_call.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/delegate_call.v new file mode 100644 index 000000000..dd264c8aa --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/delegate_call.v @@ -0,0 +1,69 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn delegate_call( + interpreter: &mut Interpreter, + host: &mut H, +) +*) +Instance run_delegate_call + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.delegate_call [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE eqn:?. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + destruct run_InputsTrait_for_Input. + destruct run_RuntimeFlag_for_RuntimeFlag. + destruct run_Host_for_H. + destruct Impl_From_U256_for_FixedBytes_32.run. + destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}). + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/eofcreate.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/eofcreate.v new file mode 100644 index 000000000..3bd27c39e --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/eofcreate.v @@ -0,0 +1,73 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn eofcreate( + interpreter: &mut Interpreter, + _host: &mut H, +) +*) +Instance run_eofcreate + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.eofcreate [] [ Φ WIRE; Φ H ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE eqn:?. + destruct run_StackTrait_for_Stack. + destruct run_MemoryTrait_for_Memory. + destruct run_LoopControl_for_Control. + destruct run_Immediates_for_Bytecode. + destruct run_Jumps_for_Bytecode. + destruct run_EofContainer_for_Bytecode. + destruct run_InputsTrait_for_Input. + destruct run_RuntimeFlag_for_RuntimeFlag. + destruct Impl_Clone_for_Bytes.run. + destruct Impl_Default_for_Bytes.run. + destruct links.mod.Impl_Deref_for_Bytes.run. + destruct (Impl_Into_for_From_T.run Impl_From_Vec_u8_for_Bytes.run). + destruct run_Deref_for_Synthetic. + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall.v new file mode 100644 index 000000000..9b1968cf1 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall.v @@ -0,0 +1,69 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.links.contract.extcall_gas_calc. +Require Import revm.revm_interpreter.instructions.links.contract.extcall_input. +Require Import revm.revm_interpreter.instructions.links.contract.pop_extcall_target_address. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn extcall( + interpreter: &mut Interpreter, + host: &mut H, +) +*) +Instance run_extcall + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.extcall [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE eqn:?. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + destruct run_InputsTrait_for_Input. + destruct run_RuntimeFlag_for_RuntimeFlag. + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall_gas_calc.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall_gas_calc.v new file mode 100644 index 000000000..244820817 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall_gas_calc.v @@ -0,0 +1,73 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn extcall_gas_calc( + interpreter: &mut Interpreter, + host: &mut H, + target: Address, + transfers_value: bool, +) -> Option +*) +Instance run_extcall_gas_calc + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (host : Ref.t Pointer.Kind.MutRef H) + (target : Address.t) + (transfers_value : bool) : + Run.Trait + instructions.contract.extcall_gas_calc + [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host; φ target; φ transfers_value ] + (option U64.t). +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + destruct run_RuntimeFlag_for_RuntimeFlag. + destruct run_ReturnData_for_ReturnData. + destruct run_Host_for_H. + destruct links.mod.Impl_DerefMut_for_Bytes.run. + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall_input.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall_input.v new file mode 100644 index 000000000..2372d619d --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extcall_input.v @@ -0,0 +1,65 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn extcall_input(interpreter: &mut Interpreter) -> Option +*) +Instance run_extcall_input + {WIRE : Set} `{Link WIRE} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) : + Run.Trait + instructions.contract.extcall_input [] [ Φ WIRE ] [ φ interpreter ] + (option alloy_primitives.bytes.links.mod.Bytes.t). +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE eqn:?. + destruct run_StackTrait_for_Stack. + destruct run_MemoryTrait_for_Memory. + destruct (Impl_Try_for_Option.run alloy_primitives.bytes.links.mod.Bytes.t). + destruct run_FromResidual_for_Self. + destruct (Impl_Try_for_Option.run (Range.t Usize.t)). + destruct (Impl_AsRef_for_Slice.run U8.t). + destruct run_Deref_for_Synthetic. + destruct (Impl_FromResidual_Infallible_for_Option.run alloy_primitives.bytes.links.mod.Bytes.t). + destruct (Impl_Clone_for_Range.run Usize.t). + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extdelegatecall.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extdelegatecall.v new file mode 100644 index 000000000..4c489038d --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extdelegatecall.v @@ -0,0 +1,68 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.links.contract.extcall_gas_calc. +Require Import revm.revm_interpreter.instructions.links.contract.extcall_input. +Require Import revm.revm_interpreter.instructions.links.contract.pop_extcall_target_address. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn extdelegatecall( + interpreter: &mut Interpreter, + host: &mut H, +) +*) +Instance run_extdelegatecall + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.extdelegatecall [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE eqn:?. + destruct run_LoopControl_for_Control. + destruct run_InputsTrait_for_Input. + destruct run_RuntimeFlag_for_RuntimeFlag. + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extstaticcall.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extstaticcall.v new file mode 100644 index 000000000..051a3a1d6 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/extstaticcall.v @@ -0,0 +1,68 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.links.contract.extcall_gas_calc. +Require Import revm.revm_interpreter.instructions.links.contract.extcall_input. +Require Import revm.revm_interpreter.instructions.links.contract.pop_extcall_target_address. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn extstaticcall( + interpreter: &mut Interpreter, + host: &mut H, +) +*) +Instance run_extstaticcall + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.extstaticcall [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE eqn:?. + destruct run_LoopControl_for_Control. + destruct run_InputsTrait_for_Input. + destruct run_RuntimeFlag_for_RuntimeFlag. + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/pop_extcall_target_address.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/pop_extcall_target_address.v new file mode 100644 index 000000000..35a6d8955 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/pop_extcall_target_address.v @@ -0,0 +1,64 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import core.slice.links.mod. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn pop_extcall_target_address( + interpreter: &mut Interpreter, +) -> Option
+*) +Instance run_pop_extcall_target_address + {WIRE : Set} `{Link WIRE} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) : + Run.Trait + instructions.contract.pop_extcall_target_address [] [ Φ WIRE ] [ φ interpreter ] + (option Address.t). +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + destruct Impl_From_U256_for_FixedBytes_32.run. + destruct (Impl_Iterator_for_Iter.run U8.t). + destruct (Impl_Index_for_FixedBytes_N.run {| Integer.value := 32 |} (RangeTo.t Usize.t)). + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/return_contract.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/return_contract.v new file mode 100644 index 000000000..b50245ede --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/return_contract.v @@ -0,0 +1,72 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.eof.links.header. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn return_contract( + interpreter: &mut Interpreter, + _host: &mut H, +) +*) +Instance run_return_contract + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (_host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.return_contract [] [ Φ H; Φ WIRE ] [ φ interpreter; φ _host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE. + destruct run_StackTrait_for_Stack. + destruct run_MemoryTrait_for_Memory. + destruct run_LoopControl_for_Control. + destruct run_Immediates_for_Bytecode. + destruct run_EofContainer_for_Bytecode. + destruct run_RuntimeFlag_for_RuntimeFlag. + destruct Impl_Clone_for_Bytes.run. + destruct links.mod.Impl_Deref_for_Bytes.run. + destruct bytes.Impl_Deref_for_Bytes.run. + destruct (Impl_AsRef_for_Slice.run U8.t). + destruct run_Deref_for_Synthetic1. + Time run_symbolic. +Admitted. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/contract/static_call.v b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/static_call.v new file mode 100644 index 000000000..e4fa16896 --- /dev/null +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/contract/static_call.v @@ -0,0 +1,69 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import CoqOfRust.links.M. +Require Import alloc.links.boxed. +Require Import alloc.links.slice. +Require Import alloy_primitives.bits.links.address. +Require Import alloy_primitives.bits.links.fixed. +Require Import alloy_primitives.bytes.links.mod. +Require Import alloy_primitives.utils.links.mod. +Require Import bytes.links.bytes. +Require Import core.convert.links.mod. +Require Import core.fmt.links.mod. +Require Import core.links.borrow. +Require Import core.links.cmp. +Require Import core.links.option. +Require Import core.links.panicking. +Require Import core.links.result. +Require Import core.num.links.mod. +Require Import core.ops.links.control_flow. +Require Import core.ops.links.range. +Require Import core.slice.links.iter. +Require Import revm.revm_bytecode.links.eof. +Require Import revm.revm_context_interface.links.cfg. +Require Import revm.revm_context_interface.links.host. +Require Import revm.revm_interpreter.gas.links.calc. +Require Import revm.revm_interpreter.gas.links.constants. +Require Import revm.revm_interpreter.interpreter_action.links.call_inputs. +Require Import revm.revm_interpreter.interpreter_action.links.eof_create_inputs. +Require Import revm.revm_interpreter.interpreter.links.shared_memory. +Require Import revm.revm_interpreter.links.gas. +Require Import revm.revm_interpreter.links.interpreter. +Require Import revm.revm_interpreter.links.interpreter_types. +Require Import revm.revm_interpreter.instructions.contract.links.call_helpers. +Require Import revm.revm_interpreter.instructions.contract. +Require Import revm.revm_interpreter.instructions.links.utility. +Require Import revm.revm_specification.links.hardfork. +Require Import ruint.links.bytes. +Require Import ruint.links.cmp. +Require Import ruint.links.from. +Require Import ruint.links.lib. + +(* +pub fn static_call( + interpreter: &mut Interpreter, + host: &mut H, +) +*) +Instance run_static_call + {WIRE H : Set} `{Link WIRE} `{Link H} + {WIRE_types : InterpreterTypes.Types.t} `{InterpreterTypes.Types.AreLinks WIRE_types} + {H_types : Host.Types.t} `{Host.Types.AreLinks H_types} + (run_InterpreterTypes_for_WIRE : InterpreterTypes.Run WIRE WIRE_types) + (run_Host_for_H : Host.Run H H_types) + (interpreter : Ref.t Pointer.Kind.MutRef (Interpreter.t WIRE WIRE_types)) + (host : Ref.t Pointer.Kind.MutRef H) : + Run.Trait + instructions.contract.static_call [] [ Φ WIRE; Φ H ] [ φ interpreter; φ host ] + unit. +Proof. + constructor. + destruct run_InterpreterTypes_for_WIRE eqn:?. + destruct run_StackTrait_for_Stack. + destruct run_LoopControl_for_Control. + destruct run_InputsTrait_for_Input. + destruct run_RuntimeFlag_for_RuntimeFlag. + destruct run_Host_for_H. + destruct Impl_From_U256_for_FixedBytes_32.run. + destruct (TryFrom_Uint_for_u64.run {| Integer.value := 256 |} {| Integer.value := 4 |}). + run_symbolic. +Defined. diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/count_admitted.py b/CoqOfRust/revm/revm_interpreter/instructions/links/count_admitted.py index ce36e4f9e..97aae7763 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/count_admitted.py +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/count_admitted.py @@ -9,38 +9,47 @@ admitted = 0 defined = 0 -for file in sorted(os.listdir(".")): - if file.endswith(".v"): - # Mardown title - print() - print(f"## {file.replace('.v', '').capitalize()}") - print() - with open(file, "r") as f: - for index, line in enumerate(f): - # print(line) - if "Instance run_" in line: - total += 1 - # Get the name of the instance - instance_name = line.split("Instance run_")[1].split("]")[0].strip() - # Get the first word of the instance name - instance_name = instance_name.split(" ")[0] - # To know if it is admitted, we need to know which word appears first - # in the lines after: - # "Admitted" or "Defined" - isAdmitted = False - with open(file, "r") as f: - for following_line in list(f)[index + 1 :]: - if "Admitted" in following_line: - isAdmitted = True - break - if "Defined" in following_line: - break - emoji = "[ ]" if isAdmitted else "[x]" - if isAdmitted: - admitted += 1 - else: - defined += 1 - print(f"- {emoji} `{instance_name}`") + +def count_in_folder(folder: str): + for file in sorted(os.listdir(folder)): + if file.endswith(".v"): + # Mardown title + print() + folder_in_title = "" if folder == "." else folder.capitalize() + "/" + print(f"## {folder_in_title}{file.replace('.v', '').capitalize()}") + print() + with open(os.path.join(folder, file), "r") as f: + for index, line in enumerate(f): + # print(line) + if "Instance run_" in line: + global total + total += 1 + # Get the name of the instance + instance_name = line.split("Instance run_")[1].split("]")[0].strip() + # Get the first word of the instance name + instance_name = instance_name.split(" ")[0] + # To know if it is admitted, we need to know which word appears first + # in the lines after: + # "Admitted" or "Defined" + isAdmitted = False + with open(os.path.join(folder, file), "r") as f: + for following_line in list(f)[index + 1 :]: + if "Admitted" in following_line: + isAdmitted = True + break + if "Defined" in following_line: + break + emoji = "[ ]" if isAdmitted else "[x]" + if isAdmitted: + global admitted + admitted += 1 + else: + global defined + defined += 1 + print(f"- {emoji} `{instance_name}`") + +count_in_folder(".") +count_in_folder("contract") print() print("## Summary") diff --git a/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md b/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md index 7c5096539..bdcd5bee9 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md +++ b/CoqOfRust/revm/revm_interpreter/instructions/links/progress_on_links.md @@ -45,19 +45,6 @@ ## Contract -- [ ] `eofcreate` -- [ ] `return_contract` -- [ ] `extcall_input` -- [ ] `extcall_gas_calc` -- [ ] `pop_extcall_target_address` -- [ ] `extcall` -- [ ] `extdelegatecall` -- [ ] `extstaticcall` -- [ ] `create` -- [ ] `call` -- [ ] `call_code` -- [ ] `delegate_call` -- [ ] `static_call` ## Control @@ -161,9 +148,61 @@ - [ ] `cast_slice_to_u256` +## Contract/Call + +- [x] `call` + +## Contract/Call_code + +- [x] `call_code` + +## Contract/Create + +- [x] `create` + +## Contract/Delegate_call + +- [x] `delegate_call` + +## Contract/Eofcreate + +- [x] `eofcreate` + +## Contract/Extcall + +- [x] `extcall` + +## Contract/Extcall_gas_calc + +- [x] `extcall_gas_calc` + +## Contract/Extcall_input + +- [x] `extcall_input` + +## Contract/Extdelegatecall + +- [x] `extdelegatecall` + +## Contract/Extstaticcall + +- [x] `extstaticcall` + +## Contract/Pop_extcall_target_address + +- [x] `pop_extcall_target_address` + +## Contract/Return_contract + +- [ ] `return_contract` + +## Contract/Static_call + +- [x] `static_call` + ## Summary - Total: 120 -- Admitted: 33 -- Defined: 87 -- Percentage: 72.50% +- Admitted: 21 +- Defined: 99 +- Percentage: 82.50% diff --git a/CoqOfRust/revm/revm_interpreter/instructions/system.v b/CoqOfRust/revm/revm_interpreter/instructions/system.v index 58fd15603..651e2251a 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/system.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/system.v @@ -6394,7 +6394,7 @@ Module instructions. (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) in diff --git a/CoqOfRust/revm/revm_interpreter/instructions/utility.v b/CoqOfRust/revm/revm_interpreter/instructions/utility.v index a42bfae43..fb49a2b79 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/utility.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/utility.v @@ -1070,7 +1070,7 @@ Module instructions. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in diff --git a/CoqOfRust/revm/revm_interpreter/interpreter/stack.v b/CoqOfRust/revm/revm_interpreter/interpreter/stack.v index 9cc211f8e..f1d8beca7 100644 --- a/CoqOfRust/revm/revm_interpreter/interpreter/stack.v +++ b/CoqOfRust/revm/revm_interpreter/interpreter/stack.v @@ -2432,7 +2432,7 @@ Module interpreter. M.never_to_any (| M.read (| M.return_ (| - repeat (| + lib.repeat (| M.read (| get_associated_constant (| Ty.apply @@ -2475,7 +2475,7 @@ Module interpreter. ] [] ] := - repeat (| + lib.repeat (| M.read (| get_associated_constant (| Ty.apply @@ -5594,7 +5594,7 @@ Module interpreter. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 8 |) in diff --git a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v index b325ea1b4..a461f07ac 100644 --- a/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v +++ b/CoqOfRust/revm/revm_interpreter/links/interpreter_types.v @@ -166,7 +166,7 @@ Module MemoryTrait. TraitMethod.C (trait Self) "slice" (fun method => forall (self : Ref.t Pointer.Kind.Ref Self) - (range : Ref.t Pointer.Kind.Ref (range.Range.t Usize.t)), + (range : range.Range.t Usize.t), Run.Trait method [] [] [ φ self; φ range ] Synthetic ). diff --git a/CoqOfRust/revm/revm_precompile/blake2.v b/CoqOfRust/revm/revm_precompile/blake2.v index d768ffa70..d71e5524a 100644 --- a/CoqOfRust/revm/revm_precompile/blake2.v +++ b/CoqOfRust/revm/revm_precompile/blake2.v @@ -510,7 +510,7 @@ Module blake2. (Ty.path "array") [ Value.Integer IntegerKind.Usize 8 ] [ Ty.path "u64" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U64 0, Value.Integer IntegerKind.Usize 8 |) in @@ -519,7 +519,7 @@ Module blake2. (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u64" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U64 0, Value.Integer IntegerKind.Usize 16 |) in @@ -1471,7 +1471,7 @@ Module blake2. (Ty.path "array") [ Value.Integer IntegerKind.Usize 64 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 64 |) in @@ -2394,7 +2394,10 @@ Module blake2. (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u64" ] := - repeat (| Value.Integer IntegerKind.U64 0, Value.Integer IntegerKind.Usize 16 |) in + lib.repeat (| + Value.Integer IntegerKind.U64 0, + Value.Integer IntegerKind.Usize 16 + |) in let~ _ : Ty.tuple [] := M.call_closure (| Ty.tuple [], diff --git a/CoqOfRust/revm/revm_precompile/bls12_381/g1_msm.v b/CoqOfRust/revm/revm_precompile/bls12_381/g1_msm.v index 88e11aefe..ded1d4141 100644 --- a/CoqOfRust/revm/revm_precompile/bls12_381/g1_msm.v +++ b/CoqOfRust/revm/revm_precompile/bls12_381/g1_msm.v @@ -1580,7 +1580,7 @@ Module bls12_381. [] |), [ - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 128 |) diff --git a/CoqOfRust/revm/revm_precompile/bls12_381/g2.v b/CoqOfRust/revm/revm_precompile/bls12_381/g2.v index 70a03cf42..5fe14d461 100644 --- a/CoqOfRust/revm/revm_precompile/bls12_381/g2.v +++ b/CoqOfRust/revm/revm_precompile/bls12_381/g2.v @@ -1415,11 +1415,11 @@ Module bls12_381. [ Ty.path "u8" ] ] ] := - repeat (| + lib.repeat (| M.borrow (| Pointer.Kind.Ref, M.alloc (| - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 48 |) diff --git a/CoqOfRust/revm/revm_precompile/bls12_381/g2_msm.v b/CoqOfRust/revm/revm_precompile/bls12_381/g2_msm.v index 11c3946ad..80f95391e 100644 --- a/CoqOfRust/revm/revm_precompile/bls12_381/g2_msm.v +++ b/CoqOfRust/revm/revm_precompile/bls12_381/g2_msm.v @@ -1580,7 +1580,7 @@ Module bls12_381. [] |), [ - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 256 |) diff --git a/CoqOfRust/revm/revm_precompile/bn128.v b/CoqOfRust/revm/revm_precompile/bn128.v index 78e8f6a36..bf295ed5a 100644 --- a/CoqOfRust/revm/revm_precompile/bn128.v +++ b/CoqOfRust/revm/revm_precompile/bn128.v @@ -2407,7 +2407,7 @@ Module bn128. (Ty.path "array") [ Value.Integer IntegerKind.Usize 64 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 64 |) in @@ -3118,7 +3118,7 @@ Module bn128. (Ty.path "array") [ Value.Integer IntegerKind.Usize 64 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 64 |) in diff --git a/CoqOfRust/revm/revm_precompile/hash.v b/CoqOfRust/revm/revm_precompile/hash.v index 22e0356b1..2ff6accf3 100644 --- a/CoqOfRust/revm/revm_precompile/hash.v +++ b/CoqOfRust/revm/revm_precompile/hash.v @@ -585,7 +585,7 @@ Module hash. (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |) in diff --git a/CoqOfRust/revm/revm_precompile/utilities.v b/CoqOfRust/revm/revm_precompile/utilities.v index 622796613..5bf817347 100644 --- a/CoqOfRust/revm/revm_precompile/utilities.v +++ b/CoqOfRust/revm/revm_precompile/utilities.v @@ -273,7 +273,7 @@ Module utilities. fun γ => ltac:(M.monadic (let~ padded : Ty.apply (Ty.path "array") [ LEN ] [ Ty.path "u8" ] := - repeat (| Value.Integer IntegerKind.U8 0, LEN |) in + lib.repeat (| Value.Integer IntegerKind.U8 0, LEN |) in let~ _ : Ty.tuple [] := M.call_closure (| Ty.tuple [], @@ -640,7 +640,7 @@ Module utilities. fun γ => ltac:(M.monadic (let~ padded : Ty.apply (Ty.path "array") [ LEN ] [ Ty.path "u8" ] := - repeat (| Value.Integer IntegerKind.U8 0, LEN |) in + lib.repeat (| Value.Integer IntegerKind.U8 0, LEN |) in let~ _ : Ty.tuple [] := M.call_closure (| Ty.tuple [], diff --git a/CoqOfRust/ruint/bytes.v b/CoqOfRust/ruint/bytes.v index e650c3c54..bf990fc57 100644 --- a/CoqOfRust/ruint/bytes.v +++ b/CoqOfRust/ruint/bytes.v @@ -1454,7 +1454,7 @@ Module bytes. 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 let~ end_ : Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ] := M.read (| M.SubPointer.get_struct_record_field (| @@ -1661,7 +1661,7 @@ Module bytes. |) |) 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~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in let~ c : Ty.path "usize" := M.call_closure (| @@ -2328,7 +2328,7 @@ Module bytes. 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 let~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in let~ _ : Ty.tuple [] := @@ -2520,7 +2520,7 @@ Module bytes. |) |) 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~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in let~ _ : Ty.tuple [] := M.read (| diff --git a/CoqOfRust/ruint/from.v b/CoqOfRust/ruint/from.v index d82e611de..1d083c111 100644 --- a/CoqOfRust/ruint/from.v +++ b/CoqOfRust/ruint/from.v @@ -3432,7 +3432,7 @@ Module from. (Ty.path "array") [ LIMBS ] [ Ty.path "u64" ] := - repeat (| + lib.repeat (| Value.Integer IntegerKind.U64 0, LIMBS |) in @@ -3622,7 +3622,7 @@ Module from. |) |) 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 |), @@ -4022,7 +4022,7 @@ Module from. |) |) 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 |), diff --git a/CoqOfRust/ruint/lib.v b/CoqOfRust/ruint/lib.v index 9a86b4d1c..8511c2467 100644 --- a/CoqOfRust/ruint/lib.v +++ b/CoqOfRust/ruint/lib.v @@ -380,7 +380,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. [], [] |), - [ repeat (| Value.Integer IntegerKind.U64 0, LIMBS |) ] + [ lib.repeat (| Value.Integer IntegerKind.U64 0, LIMBS |) ] |) |))). @@ -431,7 +431,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. let Self : Ty.t := Self BITS LIMBS in ltac:(M.monadic (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" |) |), LIMBS |) in @@ -1066,7 +1066,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. |)) in let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) 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.call_closure (| Ty.tuple [], @@ -1181,7 +1181,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. let head := M.copy (| γ0_0 |) in let tail := M.copy (| γ0_1 |) 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.call_closure (| Ty.tuple [], diff --git a/CoqOfRust/ruint/modular.v b/CoqOfRust/ruint/modular.v index 7eb3a5a11..aa1e080bd 100644 --- a/CoqOfRust/ruint/modular.v +++ b/CoqOfRust/ruint/modular.v @@ -418,8 +418,8 @@ Module modular. [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u64" ] ] := - repeat (| - repeat (| + lib.repeat (| + lib.repeat (| Value.Integer IntegerKind.U64 0, Value.Integer IntegerKind.Usize 2 |), diff --git a/lib/src/thir_expression.rs b/lib/src/thir_expression.rs index 95be8dc7e..32c471c49 100644 --- a/lib/src/thir_expression.rs +++ b/lib/src/thir_expression.rs @@ -830,7 +830,7 @@ pub(crate) fn compile_expr<'a>( }) } thir::ExprKind::Repeat { value, count } => { - let func = Expr::local_var("repeat"); + let func = Expr::local_var("lib.repeat"); let args = vec![ compile_expr(env, generics, thir, value).read(), compile_const(env, &expr.span, count), @@ -1394,7 +1394,11 @@ fn compile_block<'a>( pub(crate) fn compile_const(env: &Env, span: &rustc_span::Span, const_: &Const) -> Rc { match &const_.kind() { - ConstKind::Param(param) => Expr::local_var(param.name.as_str()), + ConstKind::Param(param) => { + let name = to_valid_coq_name(IsValue::No, param.name.as_str()); + + Expr::local_var(name.as_str()) + } ConstKind::Infer(_) => Expr::local_var("InferConst"), ConstKind::Bound(_, _) => Expr::local_var("BoundConst"), ConstKind::Placeholder(_) => Expr::local_var("PlaceholderConst"),