From 0193cf1a8b82a1769d2b4a0d4c1f7c13ceb53bf8 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Mon, 31 Mar 2025 16:11:20 +0200 Subject: [PATCH] fix: fix the handling of constant parameters in function bodies --- CoqOfRust/alloc/boxed/convert.v | 16 +- CoqOfRust/alloc/collections/btree/map.v | 10 +- CoqOfRust/alloc/collections/btree/set.v | 10 +- .../alloc/collections/vec_deque/into_iter.v | 58 +-- CoqOfRust/alloc/collections/vec_deque/mod.v | 17 +- CoqOfRust/alloc/rc.v | 2 +- CoqOfRust/alloc/sync.v | 2 +- CoqOfRust/alloc/vec/into_iter.v | 45 +-- CoqOfRust/alloc/vec/is_zero.v | 5 +- CoqOfRust/alloc/vec/mod.v | 23 +- CoqOfRust/alloy_primitives/bits/fixed.v | 233 +----------- CoqOfRust/alloy_primitives/map/fixed.v | 35 +- .../alloy_primitives/signed/conversions.v | 100 +---- CoqOfRust/alloy_primitives/signed/int.v | 31 +- CoqOfRust/alloy_primitives/signed/ops.v | 79 +--- CoqOfRust/alloy_primitives/signed/utils.v | 93 +---- CoqOfRust/core/array/iter.v | 2 +- CoqOfRust/core/array/mod.v | 30 +- CoqOfRust/core/escape.v | 7 +- CoqOfRust/core/iter/adapters/array_chunks.v | 71 +--- CoqOfRust/core/iter/adapters/copied.v | 42 +- CoqOfRust/core/iter/adapters/filter.v | 10 +- CoqOfRust/core/iter/adapters/filter_map.v | 7 +- CoqOfRust/core/iter/adapters/flatten.v | 42 +- CoqOfRust/core/iter/adapters/map_windows.v | 113 +----- CoqOfRust/core/ptr/const_ptr.v | 7 +- CoqOfRust/core/ptr/mut_ptr.v | 7 +- CoqOfRust/core/slice/iter.v | 5 +- CoqOfRust/core/slice/mod.v | 241 ++---------- CoqOfRust/core/slice/sort/stable/mod.v | 4 +- CoqOfRust/core/unicode/unicode_data.v | 24 +- CoqOfRust/revm/revm_interpreter/gas/calc.v | 17 +- .../revm_interpreter/instructions/contract.v | 14 +- .../revm/revm_interpreter/instructions/host.v | 18 +- .../revm_interpreter/instructions/stack.v | 42 +- .../revm/revm_interpreter/interpreter/stack.v | 27 +- CoqOfRust/revm/revm_precompile/utilities.v | 31 +- CoqOfRust/ruint/add.v | 58 +-- CoqOfRust/ruint/algorithms/gcd/matrix.v | 10 +- CoqOfRust/ruint/algorithms/gcd/mod.v | 20 +- CoqOfRust/ruint/base_convert.v | 35 +- CoqOfRust/ruint/bits.v | 360 +++--------------- CoqOfRust/ruint/bytes.v | 46 +-- CoqOfRust/ruint/fmt.v | 39 +- CoqOfRust/ruint/from.v | 304 +++------------ CoqOfRust/ruint/lib.v | 63 +-- CoqOfRust/ruint/modular.v | 21 +- CoqOfRust/ruint/mul.v | 116 +----- CoqOfRust/ruint/pow.v | 14 +- CoqOfRust/ruint/special.v | 11 +- lib/src/thir_expression.rs | 9 +- 51 files changed, 352 insertions(+), 2274 deletions(-) diff --git a/CoqOfRust/alloc/boxed/convert.v b/CoqOfRust/alloc/boxed/convert.v index 768acf069..74fc606bd 100644 --- a/CoqOfRust/alloc/boxed/convert.v +++ b/CoqOfRust/alloc/boxed/convert.v @@ -931,13 +931,7 @@ Module boxed. |) |) |); - M.borrow (| - Pointer.Kind.Ref, - get_constant (| - "alloc::boxed::convert::boxed_slice_as_array_unchecked::N", - Ty.path "usize" - |) - |) + M.borrow (| Pointer.Kind.Ref, M.alloc (| N |) |) ] |), [ @@ -1161,9 +1155,7 @@ Module boxed. |) ] |), - M.read (| - get_constant (| "alloc::boxed::convert::N", Ty.path "usize" |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1286,9 +1278,7 @@ Module boxed. |), [ M.borrow (| Pointer.Kind.Ref, vec |) ] |), - M.read (| - get_constant (| "alloc::boxed::convert::N", Ty.path "usize" |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/alloc/collections/btree/map.v b/CoqOfRust/alloc/collections/btree/map.v index d1b446107..08ccc5752 100644 --- a/CoqOfRust/alloc/collections/btree/map.v +++ b/CoqOfRust/alloc/collections/btree/map.v @@ -22642,15 +22642,7 @@ Module collections. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloc::collections::btree::map::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| N, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| diff --git a/CoqOfRust/alloc/collections/btree/set.v b/CoqOfRust/alloc/collections/btree/set.v index 1885bc18c..4c2ad1660 100644 --- a/CoqOfRust/alloc/collections/btree/set.v +++ b/CoqOfRust/alloc/collections/btree/set.v @@ -7451,15 +7451,7 @@ Module collections. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloc::collections::btree::set::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| N, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| diff --git a/CoqOfRust/alloc/collections/vec_deque/into_iter.v b/CoqOfRust/alloc/collections/vec_deque/into_iter.v index beb464477..7bbf8e363 100644 --- a/CoqOfRust/alloc/collections/vec_deque/into_iter.v +++ b/CoqOfRust/alloc/collections/vec_deque/into_iter.v @@ -1373,12 +1373,7 @@ Module collections. |) ] |), - M.read (| - get_constant (| - "alloc::collections::vec_deque::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := @@ -1415,12 +1410,7 @@ Module collections. ] |); M.read (| raw_arr_ptr |); - M.read (| - get_constant (| - "alloc::collections::vec_deque::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) + N ] |) |) in @@ -1457,12 +1447,7 @@ Module collections. "inner" |) |); - M.read (| - get_constant (| - "alloc::collections::vec_deque::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) + N ] |) |) @@ -1481,15 +1466,7 @@ Module collections. |) in M.write (| β, - BinOp.Wrap.sub (| - M.read (| β |), - M.read (| - get_constant (| - "alloc::collections::vec_deque::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) - |) + BinOp.Wrap.sub (| M.read (| β |), N |) |) |) in M.return_ (| @@ -1590,12 +1567,7 @@ Module collections. let~ remaining : Ty.path "usize" := M.alloc (| BinOp.Wrap.sub (| - M.read (| - get_constant (| - "alloc::collections::vec_deque::into_iter::next_chunk::N", - Ty.path "usize" - |) - |), + N, M.call_closure (| Ty.path "usize", M.get_associated_function (| @@ -1741,12 +1713,7 @@ Module collections. "inner" |) |); - M.read (| - get_constant (| - "alloc::collections::vec_deque::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) + N ] |) |) @@ -1763,18 +1730,7 @@ Module collections. "alloc::collections::vec_deque::VecDeque", "len" |) in - M.write (| - β, - BinOp.Wrap.sub (| - M.read (| β |), - M.read (| - get_constant (| - "alloc::collections::vec_deque::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) - |) - |) + M.write (| β, BinOp.Wrap.sub (| M.read (| β |), N |) |) |) in M.alloc (| Value.StructTuple diff --git a/CoqOfRust/alloc/collections/vec_deque/mod.v b/CoqOfRust/alloc/collections/vec_deque/mod.v index dac5981aa..104a73bc3 100644 --- a/CoqOfRust/alloc/collections/vec_deque/mod.v +++ b/CoqOfRust/alloc/collections/vec_deque/mod.v @@ -19513,11 +19513,7 @@ Module collections. [], [] |), - [ - M.read (| - get_constant (| "alloc::collections::vec_deque::N", Ty.path "usize" |) - |) - ] + [ N ] |) |) in let~ arr : @@ -19622,12 +19618,7 @@ Module collections. |), [ M.borrow (| Pointer.Kind.Ref, deq |) ] |); - M.read (| - get_constant (| - "alloc::collections::vec_deque::N", - Ty.path "usize" - |) - |) + N ] |) |) in @@ -19654,9 +19645,7 @@ Module collections. "alloc::collections::vec_deque::VecDeque", "len" |), - M.read (| - get_constant (| "alloc::collections::vec_deque::N", Ty.path "usize" |) - |) + N |) |) in deq diff --git a/CoqOfRust/alloc/rc.v b/CoqOfRust/alloc/rc.v index 6aa728f81..170550030 100644 --- a/CoqOfRust/alloc/rc.v +++ b/CoqOfRust/alloc/rc.v @@ -12714,7 +12714,7 @@ Module rc. |) ] |), - M.read (| get_constant (| "alloc::rc::N", Ty.path "usize" |) |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/alloc/sync.v b/CoqOfRust/alloc/sync.v index ccd13b699..6918ba6f7 100644 --- a/CoqOfRust/alloc/sync.v +++ b/CoqOfRust/alloc/sync.v @@ -17655,7 +17655,7 @@ Module sync. |) ] |), - M.read (| get_constant (| "alloc::sync::N", Ty.path "usize" |) |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/alloc/vec/into_iter.v b/CoqOfRust/alloc/vec/into_iter.v index 4b33cc7de..9e8829dbf 100644 --- a/CoqOfRust/alloc/vec/into_iter.v +++ b/CoqOfRust/alloc/vec/into_iter.v @@ -1928,15 +1928,7 @@ Module vec. (let γ := M.use (M.alloc (| - BinOp.lt (| - M.read (| len |), - M.read (| - get_constant (| - "alloc::vec::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) - |) + BinOp.lt (| M.read (| len |), N |) |)) in let _ := M.is_constant_or_break_match (| @@ -2032,12 +2024,7 @@ Module vec. "end" |) |); - M.read (| - get_constant (| - "alloc::vec::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) + N ] |) |) @@ -2097,19 +2084,7 @@ Module vec. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| len |), - M.read (| - get_constant (| - "alloc::vec::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.lt (| M.read (| len |), N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -2288,12 +2263,7 @@ Module vec. |), [ M.borrow (| Pointer.Kind.MutRef, raw_ary |) ] |)); - M.read (| - get_constant (| - "alloc::vec::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) + N ] |) |) in @@ -2321,12 +2291,7 @@ Module vec. "ptr" |) |); - M.read (| - get_constant (| - "alloc::vec::into_iter::next_chunk::N", - Ty.path "usize" - |) - |) + N ] |) |) diff --git a/CoqOfRust/alloc/vec/is_zero.v b/CoqOfRust/alloc/vec/is_zero.v index fa619a1c6..76db7aa58 100644 --- a/CoqOfRust/alloc/vec/is_zero.v +++ b/CoqOfRust/alloc/vec/is_zero.v @@ -1173,10 +1173,7 @@ Module vec. ltac:(M.monadic (let self := M.alloc (| self |) in LogicalOp.and (| - BinOp.le (| - M.read (| get_constant (| "alloc::vec::is_zero::N", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 16 - |), + BinOp.le (| N, Value.Integer IntegerKind.Usize 16 |), ltac:(M.monadic (M.call_closure (| Ty.path "bool", diff --git a/CoqOfRust/alloc/vec/mod.v b/CoqOfRust/alloc/vec/mod.v index f5aecf8b5..7693f9f32 100644 --- a/CoqOfRust/alloc/vec/mod.v +++ b/CoqOfRust/alloc/vec/mod.v @@ -7812,12 +7812,7 @@ Module vec. [], [] |), - [ - M.read (| len |); - M.read (| - get_constant (| "alloc::vec::N", Ty.path "usize" |) - |) - ] + [ M.read (| len |); N ] |); M.borrow (| Pointer.Kind.Ref, @@ -7847,12 +7842,7 @@ Module vec. [], [] |), - [ - M.read (| len |); - M.read (| - get_constant (| "alloc::vec::N", Ty.path "usize" |) - |) - ] + [ M.read (| len |); N ] |); M.call_closure (| Ty.path "usize", @@ -7862,12 +7852,7 @@ Module vec. [], [] |), - [ - M.read (| cap |); - M.read (| - get_constant (| "alloc::vec::N", Ty.path "usize" |) - |) - ] + [ M.read (| cap |); N ] |) ] |))) @@ -11157,7 +11142,7 @@ Module vec. |), [ M.borrow (| Pointer.Kind.Ref, vec |) ] |), - M.read (| get_constant (| "alloc::vec::N", Ty.path "usize" |) |) + N |) |)) in let _ := diff --git a/CoqOfRust/alloy_primitives/bits/fixed.v b/CoqOfRust/alloy_primitives/bits/fixed.v index 1b0e46f4a..7f5a7e023 100644 --- a/CoqOfRust/alloy_primitives/bits/fixed.v +++ b/CoqOfRust/alloy_primitives/bits/fixed.v @@ -4445,15 +4445,7 @@ Module bits. M.use (M.alloc (| LogicalOp.or (| - BinOp.le (| - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 4 - |), + BinOp.le (| N, Value.Integer IntegerKind.Usize 4 |), ltac:(M.monadic (UnOp.not (| M.call_closure (| @@ -4771,21 +4763,10 @@ Module bits. [ ("start", BinOp.Wrap.sub (| - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |), + N, Value.Integer IntegerKind.Usize 2 |)); - ("end_", - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |)) + ("end_", N) ] ] |) @@ -5865,17 +5846,7 @@ Module bits. ltac:(M.monadic (let γ := M.use - (M.alloc (| - BinOp.gt (| - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |)) in + (M.alloc (| BinOp.gt (| N, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := @@ -5883,15 +5854,7 @@ Module bits. M.write (| M.SubPointer.get_array_field (| bytes, - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| N, Value.Integer IntegerKind.Usize 1 |) |), M.read (| x |) |) @@ -5954,9 +5917,7 @@ Module bits. : M := let Self : Ty.t := Self N in match ε, τ, α with - | [], [], [] => - ltac:(M.monadic - (M.read (| get_constant (| "alloy_primitives::bits::fixed::N", Ty.path "usize" |) |))) + | [], [], [] => ltac:(M.monadic N) | _, _, _ => M.impossible "wrong number of arguments" end. @@ -6005,30 +5966,7 @@ Module bits. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.eq (| - BinOp.Wrap.add (| - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::concat_const::M", - Ty.path "usize" - |) - |) - |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::concat_const::Z", - Ty.path "usize" - |) - |) - |) - |) + UnOp.not (| BinOp.eq (| BinOp.Wrap.add (| N, M_ |), Z |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -6085,19 +6023,7 @@ Module bits. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::concat_const::Z", - Ty.path "usize" - |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.lt (| M.read (| i |), Z |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := @@ -6113,17 +6039,7 @@ Module bits. ltac:(M.monadic (let γ := M.use - (M.alloc (| - BinOp.ge (| - M.read (| i |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |) - |) - |)) in + (M.alloc (| BinOp.ge (| M.read (| i |), N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), @@ -6135,15 +6051,7 @@ Module bits. "alloy_primitives::bits::fixed::FixedBytes", 0 |), - BinOp.Wrap.sub (| - M.read (| i |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |) - |) + BinOp.Wrap.sub (| M.read (| i |), N |) |))); fun γ => ltac:(M.monadic @@ -6359,10 +6267,7 @@ Module bits. M.deref (| M.borrow (| Pointer.Kind.Ref, - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) + M.alloc (| N |) |) |) |) @@ -6433,20 +6338,7 @@ Module bits. fun γ => ltac:(M.monadic (let γ := - M.use - (M.alloc (| - UnOp.not (| - BinOp.le (| - M.read (| len |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |) - |) - |) - |)) in + M.use (M.alloc (| UnOp.not (| BinOp.le (| M.read (| len |), N |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -6504,10 +6396,7 @@ Module bits. M.deref (| M.borrow (| Pointer.Kind.Ref, - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) + M.alloc (| N |) |) |) |) @@ -6593,18 +6482,7 @@ Module bits. M.borrow (| Pointer.Kind.MutRef, bytes |); Value.StructRecord "core::ops::range::RangeFrom" - [ - ("start", - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |), - M.read (| len |) - |)) - ] + [ ("start", BinOp.Wrap.sub (| N, M.read (| len |) |)) ] ] |) |) @@ -6666,20 +6544,7 @@ Module bits. fun γ => ltac:(M.monadic (let γ := - M.use - (M.alloc (| - UnOp.not (| - BinOp.le (| - M.read (| len |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |) - |) - |) - |)) in + M.use (M.alloc (| UnOp.not (| BinOp.le (| M.read (| len |), N |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -6737,10 +6602,7 @@ Module bits. M.deref (| M.borrow (| Pointer.Kind.Ref, - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) + M.alloc (| N |) |) |) |) @@ -7071,19 +6933,7 @@ Module bits. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.lt (| M.read (| i |), N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), @@ -7306,19 +7156,7 @@ Module bits. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.lt (| M.read (| i |), N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := @@ -7430,19 +7268,7 @@ Module bits. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.lt (| M.read (| i |), N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := @@ -7554,19 +7380,7 @@ Module bits. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| - "alloy_primitives::bits::fixed::N", - Ty.path "usize" - |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.lt (| M.read (| i |), N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := @@ -7678,12 +7492,7 @@ Module bits. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (get_constant (| - "alloy_primitives::bits::fixed::fmt_hex::UPPER", - Ty.path "bool" - |)) in + (let γ := M.use (M.alloc (| UPPER |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| diff --git a/CoqOfRust/alloy_primitives/map/fixed.v b/CoqOfRust/alloy_primitives/map/fixed.v index fdcd046fd..49015f8c7 100644 --- a/CoqOfRust/alloy_primitives/map/fixed.v +++ b/CoqOfRust/alloy_primitives/map/fixed.v @@ -755,13 +755,7 @@ Module map. |) |) |); - M.borrow (| - Pointer.Kind.Ref, - get_constant (| - "alloy_primitives::map::fixed::N", - Ty.path "usize" - |) - |) + M.borrow (| Pointer.Kind.Ref, M.alloc (| N |) |) ] |), [ @@ -875,12 +869,7 @@ Module map. |) ] |), - M.read (| - get_constant (| - "alloy_primitives::map::fixed::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := @@ -914,17 +903,7 @@ Module map. ltac:(M.monadic (let γ := M.use - (M.alloc (| - BinOp.gt (| - M.read (| - get_constant (| - "alloy_primitives::map::fixed::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 32 - |) - |)) in + (M.alloc (| BinOp.gt (| N, Value.Integer IntegerKind.Usize 32 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := M.alloc (| @@ -1024,13 +1003,7 @@ Module map. Value.Tuple [ M.borrow (| Pointer.Kind.Ref, i |); - M.borrow (| - Pointer.Kind.Ref, - get_constant (| - "alloy_primitives::map::fixed::N", - Ty.path "usize" - |) - |) + M.borrow (| Pointer.Kind.Ref, M.alloc (| N |) |) ] |), [ diff --git a/CoqOfRust/alloy_primitives/signed/conversions.v b/CoqOfRust/alloy_primitives/signed/conversions.v index 717855d76..cd6c3586f 100644 --- a/CoqOfRust/alloy_primitives/signed/conversions.v +++ b/CoqOfRust/alloy_primitives/signed/conversions.v @@ -1820,15 +1820,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1977,15 +1969,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -2134,15 +2118,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -2291,15 +2267,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -2448,15 +2416,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -2605,15 +2565,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -2762,15 +2714,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -2914,15 +2858,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -3071,15 +3007,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -3230,15 +3158,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::conversions::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/alloy_primitives/signed/int.v b/CoqOfRust/alloy_primitives/signed/int.v index 9432b9d28..0068ff341 100644 --- a/CoqOfRust/alloy_primitives/signed/int.v +++ b/CoqOfRust/alloy_primitives/signed/int.v @@ -915,15 +915,7 @@ Module signed. let Self : Ty.t := Self BITS LIMBS in ltac:(M.monadic (M.alloc (| - M.call_closure (| - Ty.path "u64", - M.get_function (| "ruint::mask", [], [] |), - [ - M.read (| - get_constant (| "alloy_primitives::signed::int::BITS", Ty.path "usize" |) - |) - ] - |) + M.call_closure (| Ty.path "u64", M.get_function (| "ruint::mask", [], [] |), [ BITS ] |) |))). Global Instance AssociatedConstant_value_MASK : @@ -946,11 +938,7 @@ Module signed. M.call_closure (| Ty.path "u64", M.get_function (| "alloy_primitives::signed::utils::sign_bit", [], [] |), - [ - M.read (| - get_constant (| "alloy_primitives::signed::int::BITS", Ty.path "usize" |) - |) - ] + [ BITS ] |) |))). @@ -969,8 +957,7 @@ Module signed. (α : list Value.t) : M := let Self : Ty.t := Self BITS LIMBS in - ltac:(M.monadic - (get_constant (| "alloy_primitives::signed::int::BITS", Ty.path "usize" |))). + ltac:(M.monadic (M.alloc (| BITS |))). Global Instance AssociatedConstant_value_BITS : forall (BITS LIMBS : Value.t), @@ -1525,17 +1512,7 @@ Module signed. ltac:(M.monadic (let γ := M.use - (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::int::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |)) in + (M.alloc (| BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| Value.Bool false |))); fun γ => diff --git a/CoqOfRust/alloy_primitives/signed/ops.v b/CoqOfRust/alloy_primitives/signed/ops.v index 5d4d60a34..f8971afdf 100644 --- a/CoqOfRust/alloy_primitives/signed/ops.v +++ b/CoqOfRust/alloy_primitives/signed/ops.v @@ -92,15 +92,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::ops::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -491,15 +483,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::ops::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -4556,12 +4540,7 @@ Module signed. let~ is_exp_odd : Ty.path "bool" := M.alloc (| LogicalOp.and (| - BinOp.ne (| - M.read (| - get_constant (| "alloy_primitives::signed::ops::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |), + BinOp.ne (| BITS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic (BinOp.eq (| BinOp.Wrap.rem (| @@ -4823,15 +4802,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::ops::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -5777,15 +5748,7 @@ Module signed. Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic - (BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::ops::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |))) + (BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |))) |) |)) in let _ := @@ -5808,15 +5771,7 @@ Module signed. (M.alloc (| BinOp.ge (| M.read (| rhs |), - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "alloy_primitives::signed::ops::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| BITS, Value.Integer IntegerKind.Usize 1 |) |) |)) in let _ := @@ -6033,17 +5988,7 @@ Module signed. [], [ Ty.path "usize" ] |), - [ - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "alloy_primitives::signed::ops::BITS", - Ty.path "usize" - |) - |), - M.read (| rhs |) - |) - ] + [ BinOp.Wrap.sub (| BITS, M.read (| rhs |) |) ] |) ] |); @@ -6166,15 +6111,7 @@ Module signed. LogicalOp.or (| BinOp.eq (| M.read (| rhs |), Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic - (BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::ops::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |))) + (BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |))) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/alloy_primitives/signed/utils.v b/CoqOfRust/alloy_primitives/signed/utils.v index 6c3cb5bb8..6082cd718 100644 --- a/CoqOfRust/alloy_primitives/signed/utils.v +++ b/CoqOfRust/alloy_primitives/signed/utils.v @@ -140,15 +140,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::utils::twos_complement::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -248,15 +240,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::utils::const_eq::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -336,18 +320,7 @@ Module signed. fun γ => ltac:(M.monadic (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| - "alloy_primitives::signed::utils::const_eq::LIMBS", - Ty.path "usize" - |) - |) - |) - |)) in + M.use (M.alloc (| BinOp.lt (| M.read (| i |), LIMBS |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), @@ -459,15 +432,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::utils::max::LIMBS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| LIMBS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -508,15 +473,7 @@ Module signed. let β := M.SubPointer.get_array_field (| limbs, - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "alloy_primitives::signed::utils::max::LIMBS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, @@ -539,15 +496,7 @@ Module signed. let β := M.SubPointer.get_array_field (| limbs, - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "alloy_primitives::signed::utils::max::LIMBS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, @@ -621,15 +570,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::utils::min::LIMBS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| LIMBS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -663,15 +604,7 @@ Module signed. M.write (| M.SubPointer.get_array_field (| limbs, - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "alloy_primitives::signed::utils::min::LIMBS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |), M.read (| get_associated_constant (| @@ -777,15 +710,7 @@ Module signed. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "alloy_primitives::signed::utils::one::LIMBS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| LIMBS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/core/array/iter.v b/CoqOfRust/core/array/iter.v index a5b259e3a..649555ad6 100644 --- a/CoqOfRust/core/array/iter.v +++ b/CoqOfRust/core/array/iter.v @@ -100,7 +100,7 @@ Module array. [], [] |), - [ M.read (| get_constant (| "core::array::iter::N", Ty.path "usize" |) |) ] + [ N ] |)) ] |) diff --git a/CoqOfRust/core/array/mod.v b/CoqOfRust/core/array/mod.v index 910198c37..723f40068 100644 --- a/CoqOfRust/core/array/mod.v +++ b/CoqOfRust/core/array/mod.v @@ -23,10 +23,7 @@ Module array. M.call_closure (| Ty.apply (Ty.path "core::iter::sources::repeat_n::RepeatN") [] [ T ], M.get_function (| "core::iter::sources::repeat_n::repeat_n", [], [ T ] |), - [ - M.read (| val |); - M.read (| get_constant (| "core::array::repeat::N", Ty.path "usize" |) |) - ] + [ M.read (| val |); N ] |) ] |))) @@ -6181,14 +6178,7 @@ Module array. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| get_constant (| "core::array::N", Ty.path "usize" |) |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.lt (| M.read (| i |), N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := @@ -6305,14 +6295,7 @@ Module array. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| get_constant (| "core::array::N", Ty.path "usize" |) |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.lt (| M.read (| i |), N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := @@ -6908,12 +6891,7 @@ Module array. 0 |) |), - M.read (| - get_constant (| - "core::array::try_from_trusted_iterator::N", - Ty.path "usize" - |) - |) + N |) |) |)) in diff --git a/CoqOfRust/core/escape.v b/CoqOfRust/core/escape.v index b7c95f7e6..f7e22faeb 100644 --- a/CoqOfRust/core/escape.v +++ b/CoqOfRust/core/escape.v @@ -907,12 +907,7 @@ Module escape. "core::ops::range::Range" [ ("start", M.cast (Ty.path "u8") (M.read (| start |))); - ("end_", - M.cast - (Ty.path "u8") - (M.read (| - get_constant (| "core::escape::escape_unicode::N", Ty.path "usize" |) - |))) + ("end_", M.cast (Ty.path "u8") N) ] ] |) diff --git a/CoqOfRust/core/iter/adapters/array_chunks.v b/CoqOfRust/core/iter/adapters/array_chunks.v index ac5d6f481..1e22da1a3 100644 --- a/CoqOfRust/core/iter/adapters/array_chunks.v +++ b/CoqOfRust/core/iter/adapters/array_chunks.v @@ -257,17 +257,7 @@ Module iter. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| - "core::iter::adapters::array_chunks::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -595,12 +585,7 @@ Module iter. |) ] |), - M.read (| - get_constant (| - "core::iter::adapters::array_chunks::N", - Ty.path "usize" - |) - |) + N |) |) in let~ remainder : @@ -1092,15 +1077,7 @@ Module iter. M.alloc (| Value.Tuple [ - BinOp.Wrap.div (| - M.read (| lower |), - M.read (| - get_constant (| - "core::iter::adapters::array_chunks::N", - Ty.path "usize" - |) - |) - |); + BinOp.Wrap.div (| M.read (| lower |), N |); M.call_closure (| Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ], M.get_associated_function (| @@ -1130,15 +1107,7 @@ Module iter. fun γ => ltac:(M.monadic (let n := M.copy (| γ |) in - BinOp.Wrap.div (| - M.read (| n |), - M.read (| - get_constant (| - "core::iter::adapters::array_chunks::N", - Ty.path "usize" - |) - |) - |))) + BinOp.Wrap.div (| M.read (| n |), N |))) ] |))) | _ => M.impossible "wrong number of arguments" @@ -1192,9 +1161,7 @@ Module iter. |) ] |), - M.read (| - get_constant (| "core::iter::adapters::array_chunks::N", Ty.path "usize" |) - |) + N |))) | _, _, _ => M.impossible "wrong number of arguments" end. @@ -2356,9 +2323,7 @@ Module iter. |) ] |), - M.read (| - get_constant (| "core::iter::adapters::array_chunks::N", Ty.path "usize" |) - |) + N |))) | _, _, _ => M.impossible "wrong number of arguments" end. @@ -2403,9 +2368,7 @@ Module iter. |) ] |), - M.read (| - get_constant (| "core::iter::adapters::array_chunks::N", Ty.path "usize" |) - |) + N |))) | _, _, _ => M.impossible "wrong number of arguments" end. @@ -2612,12 +2575,7 @@ Module iter. (M.alloc (| BinOp.ge (| BinOp.Wrap.sub (| M.read (| inner_len |), M.read (| i |) |), - M.read (| - get_constant (| - "core::iter::adapters::array_chunks::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := @@ -2779,18 +2737,7 @@ Module iter. let~ _ : Ty.tuple [] := M.alloc (| let β := i in - M.write (| - β, - BinOp.Wrap.add (| - M.read (| β |), - M.read (| - get_constant (| - "core::iter::adapters::array_chunks::N", - Ty.path "usize" - |) - |) - |) - |) + M.write (| β, BinOp.Wrap.add (| M.read (| β |), N |) |) |) in M.alloc (| Value.Tuple [] |))); fun γ => diff --git a/CoqOfRust/core/iter/adapters/copied.v b/CoqOfRust/core/iter/adapters/copied.v index 0c9db21e9..0b30eaac3 100644 --- a/CoqOfRust/core/iter/adapters/copied.v +++ b/CoqOfRust/core/iter/adapters/copied.v @@ -1410,15 +1410,7 @@ Module iter. (let γ := M.use (M.alloc (| - BinOp.lt (| - M.read (| len |), - M.read (| - get_constant (| - "core::iter::adapters::copied::N", - Ty.path "usize" - |) - |) - |) + BinOp.lt (| M.read (| len |), N |) |)) in let _ := M.is_constant_or_break_match (| @@ -1538,12 +1530,7 @@ Module iter. Pointer.Kind.MutRef, M.deref (| M.read (| self |) |) |); - M.read (| - get_constant (| - "core::iter::adapters::copied::N", - Ty.path "usize" - |) - |) + N ] |) |), @@ -1585,19 +1572,7 @@ Module iter. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| len |), - M.read (| - get_constant (| - "core::iter::adapters::copied::N", - Ty.path "usize" - |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.lt (| M.read (| len |), N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), @@ -1833,9 +1808,7 @@ Module iter. |), [ M.borrow (| Pointer.Kind.MutRef, raw_array |) ] |)); - M.read (| - get_constant (| "core::iter::adapters::copied::N", Ty.path "usize" |) - |) + N ] |) |) in @@ -1862,12 +1835,7 @@ Module iter. [], [] |), - [ - M.borrow (| Pointer.Kind.MutRef, M.deref (| M.read (| self |) |) |); - M.read (| - get_constant (| "core::iter::adapters::copied::N", Ty.path "usize" |) - |) - ] + [ M.borrow (| Pointer.Kind.MutRef, M.deref (| M.read (| self |) |) |); N ] |) |), [ diff --git a/CoqOfRust/core/iter/adapters/filter.v b/CoqOfRust/core/iter/adapters/filter.v index 8ca54edec..a4d173f89 100644 --- a/CoqOfRust/core/iter/adapters/filter.v +++ b/CoqOfRust/core/iter/adapters/filter.v @@ -444,15 +444,7 @@ Module iter. (let γ := M.use (M.alloc (| - BinOp.lt (| - M.read (| initialized |), - M.read (| - get_constant (| - "core::iter::adapters::filter::next_chunk_dropless::N", - Ty.path "usize" - |) - |) - |) + BinOp.lt (| M.read (| initialized |), N |) |)) in let _ := M.is_constant_or_break_match (| diff --git a/CoqOfRust/core/iter/adapters/filter_map.v b/CoqOfRust/core/iter/adapters/filter_map.v index 2e7777dac..9411957a2 100644 --- a/CoqOfRust/core/iter/adapters/filter_map.v +++ b/CoqOfRust/core/iter/adapters/filter_map.v @@ -991,12 +991,7 @@ Module iter. "initialized" |) |), - M.read (| - get_constant (| - "core::iter::adapters::filter_map::next_chunk::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := diff --git a/CoqOfRust/core/iter/adapters/flatten.v b/CoqOfRust/core/iter/adapters/flatten.v index 1dc15e334..6bd35e5a7 100644 --- a/CoqOfRust/core/iter/adapters/flatten.v +++ b/CoqOfRust/core/iter/adapters/flatten.v @@ -1364,11 +1364,7 @@ Module iter. [], [] |), - [ - M.read (| - get_constant (| "core::iter::adapters::flatten::N", Ty.path "usize" |) - |) - ] + [ N ] |) |))). @@ -1412,11 +1408,7 @@ Module iter. [], [] |), - [ - M.read (| - get_constant (| "core::iter::adapters::flatten::N", Ty.path "usize" |) - |) - ] + [ N ] |) |))). @@ -6853,15 +6845,7 @@ Module iter. : M := let Self : Ty.t := Self N T in match ε, τ, α with - | [], [], [] => - ltac:(M.monadic - (Value.StructTuple - "core::option::Option::Some" - [ - M.read (| - get_constant (| "core::iter::adapters::flatten::N", Ty.path "usize" |) - |) - ])) + | [], [], [] => ltac:(M.monadic (Value.StructTuple "core::option::Option::Some" [ N ])) | _, _, _ => M.impossible "wrong number of arguments" end. @@ -6893,15 +6877,7 @@ Module iter. : M := let Self : Ty.t := Self N T in match ε, τ, α with - | [], [], [] => - ltac:(M.monadic - (Value.StructTuple - "core::option::Option::Some" - [ - M.read (| - get_constant (| "core::iter::adapters::flatten::N", Ty.path "usize" |) - |) - ])) + | [], [], [] => ltac:(M.monadic (Value.StructTuple "core::option::Option::Some" [ N ])) | _, _, _ => M.impossible "wrong number of arguments" end. @@ -6933,15 +6909,7 @@ Module iter. : M := let Self : Ty.t := Self N T in match ε, τ, α with - | [], [], [] => - ltac:(M.monadic - (Value.StructTuple - "core::option::Option::Some" - [ - M.read (| - get_constant (| "core::iter::adapters::flatten::N", Ty.path "usize" |) - |) - ])) + | [], [], [] => ltac:(M.monadic (Value.StructTuple "core::option::Option::Some" [ N ])) | _, _, _ => M.impossible "wrong number of arguments" end. diff --git a/CoqOfRust/core/iter/adapters/map_windows.v b/CoqOfRust/core/iter/adapters/map_windows.v index ddb3a23a3..cf170407e 100644 --- a/CoqOfRust/core/iter/adapters/map_windows.v +++ b/CoqOfRust/core/iter/adapters/map_windows.v @@ -109,17 +109,7 @@ Module iter. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -232,15 +222,7 @@ Module iter. [], [] |), - [ - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |); - Value.Integer IntegerKind.Usize 2 - ] + [ N; Value.Integer IntegerKind.Usize 2 ] |) |) |) @@ -1127,12 +1109,7 @@ Module iter. [ M.read (| lo |); BinOp.Wrap.sub (| - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |), + N, Value.Integer IntegerKind.Usize 1 |) ] @@ -1185,12 +1162,7 @@ Module iter. [ M.read (| hi |); BinOp.Wrap.sub (| - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |), + N, Value.Integer IntegerKind.Usize 1 @@ -1690,21 +1662,11 @@ Module iter. "start" |) |), - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |) + N |), BinOp.Wrap.mul (| Value.Integer IntegerKind.Usize 2, - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |) + N |) |) |) @@ -1888,21 +1850,11 @@ Module iter. "start" |) |), - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |) + N |), BinOp.Wrap.mul (| Value.Integer IntegerKind.Usize 2, - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |) + N |) |) |) @@ -2175,21 +2127,11 @@ Module iter. "start" |) |), - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |) + N |), BinOp.Wrap.mul (| Value.Integer IntegerKind.Usize 2, - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |) + N |) |) |) @@ -2243,12 +2185,7 @@ Module iter. "start" |) |), - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := @@ -2320,15 +2257,7 @@ Module iter. ] |)); M.read (| buffer_mut_ptr |); - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| N, Value.Integer IntegerKind.Usize 1 |) ] |) |) in @@ -2377,12 +2306,7 @@ Module iter. [ M.read (| buffer_mut_ptr |); BinOp.Wrap.sub (| - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |), + N, Value.Integer IntegerKind.Usize 1 |) ] @@ -2508,12 +2432,7 @@ Module iter. "start" |) |), - M.read (| - get_constant (| - "core::iter::adapters::map_windows::N", - Ty.path "usize" - |) - |) + N |) ] |) @@ -3003,9 +2922,7 @@ Module iter. |) ] |); - M.read (| - get_constant (| "core::iter::adapters::map_windows::N", Ty.path "usize" |) - |) + N ] |) |) in diff --git a/CoqOfRust/core/ptr/const_ptr.v b/CoqOfRust/core/ptr/const_ptr.v index d5ae8d1b2..61eb45dc9 100644 --- a/CoqOfRust/core/ptr/const_ptr.v +++ b/CoqOfRust/core/ptr/const_ptr.v @@ -2557,12 +2557,7 @@ Module ptr. |), [ M.read (| self |) ] |), - M.read (| - get_constant (| - "core::ptr::const_ptr::as_array::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/core/ptr/mut_ptr.v b/CoqOfRust/core/ptr/mut_ptr.v index efca86864..832bdd2db 100644 --- a/CoqOfRust/core/ptr/mut_ptr.v +++ b/CoqOfRust/core/ptr/mut_ptr.v @@ -2823,12 +2823,7 @@ Module ptr. |), [ M.read (| self |) ] |), - M.read (| - get_constant (| - "core::ptr::mut_ptr::as_mut_array::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/core/slice/iter.v b/CoqOfRust/core/slice/iter.v index 236d17d04..ba7be22d3 100644 --- a/CoqOfRust/core/slice/iter.v +++ b/CoqOfRust/core/slice/iter.v @@ -16469,10 +16469,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| slice |) |) |) ] |); - BinOp.Wrap.sub (| - M.read (| get_constant (| "core::slice::iter::N", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| N, Value.Integer IntegerKind.Usize 1 |) ] |) |) in diff --git a/CoqOfRust/core/slice/mod.v b/CoqOfRust/core/slice/mod.v index 0d268966f..4d6056687 100644 --- a/CoqOfRust/core/slice/mod.v +++ b/CoqOfRust/core/slice/mod.v @@ -944,9 +944,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| "core::slice::first_chunk::N", Ty.path "usize" |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1058,9 +1056,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| "core::slice::first_chunk_mut::N", Ty.path "usize" |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1185,12 +1181,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| - "core::slice::split_first_chunk::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1212,15 +1203,7 @@ Module slice. [], [] |), - [ - M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |); - M.read (| - get_constant (| - "core::slice::split_first_chunk::N", - Ty.path "usize" - |) - |) - ] + [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |); N ] |) |), [ @@ -1355,12 +1338,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| - "core::slice::split_first_chunk_mut::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1382,15 +1360,7 @@ Module slice. [], [] |), - [ - M.borrow (| Pointer.Kind.MutRef, M.deref (| M.read (| self |) |) |); - M.read (| - get_constant (| - "core::slice::split_first_chunk_mut::N", - Ty.path "usize" - |) - |) - ] + [ M.borrow (| Pointer.Kind.MutRef, M.deref (| M.read (| self |) |) |); N ] |) |), [ @@ -1527,9 +1497,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| "core::slice::split_last_chunk::N", Ty.path "usize" |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1564,12 +1532,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| - "core::slice::split_last_chunk::N", - Ty.path "usize" - |) - |) + N |) ] |) @@ -1706,12 +1669,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| - "core::slice::split_last_chunk_mut::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1746,12 +1704,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| - "core::slice::split_last_chunk_mut::N", - Ty.path "usize" - |) - |) + N |) ] |) @@ -1880,9 +1833,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| "core::slice::last_chunk::N", Ty.path "usize" |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1924,9 +1875,7 @@ Module slice. |) ] |), - M.read (| - get_constant (| "core::slice::last_chunk::N", Ty.path "usize" |) - |) + N |) ] |) @@ -2043,9 +1992,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| "core::slice::last_chunk_mut::N", Ty.path "usize" |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -2100,12 +2047,7 @@ Module slice. |) ] |), - M.read (| - get_constant (| - "core::slice::last_chunk_mut::N", - Ty.path "usize" - |) - |) + N |) ] |) @@ -2681,9 +2623,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| "core::slice::as_array::N", Ty.path "usize" |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -2774,9 +2714,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| - get_constant (| "core::slice::as_mut_array::N", Ty.path "usize" |) - |) + N |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -3751,12 +3689,7 @@ Module slice. [] |), [ - M.read (| - get_constant (| - "core::slice::as_chunks_unchecked::N", - Ty.path "usize" - |) - |); + N; M.call_closure (| Ty.path "usize", M.get_associated_function (| @@ -3790,9 +3723,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |); - M.read (| - get_constant (| "core::slice::as_chunks_unchecked::N", Ty.path "usize" |) - |) + N ] |) |) in @@ -3878,14 +3809,7 @@ Module slice. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| "core::slice::as_chunks::N", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -3937,9 +3861,9 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| get_constant (| "core::slice::as_chunks::N", Ty.path "usize" |) |) + N |), - M.read (| get_constant (| "core::slice::as_chunks::N", Ty.path "usize" |) |) + N |) |) in M.match_operator (| @@ -4048,14 +3972,7 @@ Module slice. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| "core::slice::as_rchunks::N", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -4106,7 +4023,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| get_constant (| "core::slice::as_rchunks::N", Ty.path "usize" |) |) + N |) |) in M.match_operator (| @@ -4137,12 +4054,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - BinOp.Wrap.mul (| - M.read (| len |), - M.read (| - get_constant (| "core::slice::as_rchunks::N", Ty.path "usize" |) - |) - |) + BinOp.Wrap.mul (| M.read (| len |), N |) |) ] |) @@ -4227,14 +4139,7 @@ Module slice. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| "core::slice::array_chunks::N", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -4352,12 +4257,7 @@ Module slice. [] |), [ - M.read (| - get_constant (| - "core::slice::as_chunks_unchecked_mut::N", - Ty.path "usize" - |) - |); + N; M.call_closure (| Ty.path "usize", M.get_associated_function (| @@ -4396,12 +4296,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |); - M.read (| - get_constant (| - "core::slice::as_chunks_unchecked_mut::N", - Ty.path "usize" - |) - |) + N ] |) |) in @@ -4507,17 +4402,7 @@ Module slice. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| - "core::slice::as_chunks_mut::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -4569,9 +4454,9 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| get_constant (| "core::slice::as_chunks_mut::N", Ty.path "usize" |) |) + N |), - M.read (| get_constant (| "core::slice::as_chunks_mut::N", Ty.path "usize" |) |) + N |) |) in M.match_operator (| @@ -4693,17 +4578,7 @@ Module slice. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| - "core::slice::as_rchunks_mut::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -4754,7 +4629,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - M.read (| get_constant (| "core::slice::as_rchunks_mut::N", Ty.path "usize" |) |) + N |) |) in M.match_operator (| @@ -4785,12 +4660,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |), - BinOp.Wrap.mul (| - M.read (| len |), - M.read (| - get_constant (| "core::slice::as_rchunks_mut::N", Ty.path "usize" |) - |) - |) + BinOp.Wrap.mul (| M.read (| len |), N |) |) ] |) @@ -4885,17 +4755,7 @@ Module slice. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| - "core::slice::array_chunks_mut::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -4978,17 +4838,7 @@ Module slice. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| - "core::slice::array_windows::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -14794,16 +14644,7 @@ Module slice. [ Value.StructRecord "core::ops::range::Range" - [ - ("start", Value.Integer IntegerKind.Usize 0); - ("end_", - M.read (| - get_constant (| - "core::slice::get_many_unchecked_mut::N", - Ty.path "usize" - |) - |)) - ] + [ ("start", Value.Integer IntegerKind.Usize 0); ("end_", N) ] ] |) |), @@ -15853,7 +15694,7 @@ Module slice. |) ] |); - M.read (| get_constant (| "core::slice::N", Ty.path "usize" |) |) + N ] |); M.borrow (| @@ -15888,7 +15729,7 @@ Module slice. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| self |) |) |) ] |); - M.read (| get_constant (| "core::slice::N", Ty.path "usize" |) |) + N ] |) |))) @@ -16031,9 +15872,7 @@ Module slice. |) ] |); - M.read (| - get_constant (| "core::slice::N", Ty.path "usize" |) - |) + N ] |); M.borrow (| @@ -16073,7 +15912,7 @@ Module slice. |) ] |); - M.read (| get_constant (| "core::slice::N", Ty.path "usize" |) |) + N ] |) |))) diff --git a/CoqOfRust/core/slice/sort/stable/mod.v b/CoqOfRust/core/slice/sort/stable/mod.v index e4bc543e4..3d330e27d 100644 --- a/CoqOfRust/core/slice/sort/stable/mod.v +++ b/CoqOfRust/core/slice/sort/stable/mod.v @@ -663,9 +663,7 @@ Module slice. let~ len : Ty.path "usize" := M.alloc (| BinOp.Wrap.div (| - M.read (| - get_constant (| "core::slice::sort::stable::N", Ty.path "usize" |) - |), + N, M.call_closure (| Ty.path "usize", M.get_function (| "core::mem::size_of", [], [ T ] |), diff --git a/CoqOfRust/core/unicode/unicode_data.v b/CoqOfRust/core/unicode/unicode_data.v index 08d67dd6d..3f8051cab 100644 --- a/CoqOfRust/core/unicode/unicode_data.v +++ b/CoqOfRust/core/unicode/unicode_data.v @@ -71,29 +71,9 @@ Module unicode. (BinOp.Wrap.div (| M.read (| needle |), Value.Integer IntegerKind.U32 64 |)) |) in let~ chunk_map_idx : Ty.path "usize" := - M.alloc (| - BinOp.Wrap.div (| - M.read (| bucket_idx |), - M.read (| - get_constant (| - "core::unicode::unicode_data::bitset_search::CHUNK_SIZE", - Ty.path "usize" - |) - |) - |) - |) in + M.alloc (| BinOp.Wrap.div (| M.read (| bucket_idx |), CHUNK_SIZE |) |) in let~ chunk_piece : Ty.path "usize" := - M.alloc (| - BinOp.Wrap.rem (| - M.read (| bucket_idx |), - M.read (| - get_constant (| - "core::unicode::unicode_data::bitset_search::CHUNK_SIZE", - Ty.path "usize" - |) - |) - |) - |) in + M.alloc (| BinOp.Wrap.rem (| M.read (| bucket_idx |), CHUNK_SIZE |) |) in let~ chunk_idx : Ty.path "u8" := M.copy (| M.match_operator (| diff --git a/CoqOfRust/revm/revm_interpreter/gas/calc.v b/CoqOfRust/revm/revm_interpreter/gas/calc.v index a2853f0fb..b5aed7030 100644 --- a/CoqOfRust/revm/revm_interpreter/gas/calc.v +++ b/CoqOfRust/revm/revm_interpreter/gas/calc.v @@ -2389,10 +2389,7 @@ Module gas. |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in - get_constant (| - "revm_interpreter::gas::calc::istanbul_sstore_cost::SLOAD_GAS", - Ty.path "u64" - |))); + M.alloc (| SLOAD_GAS |))); fun γ => ltac:(M.monadic (M.match_operator (| @@ -2476,16 +2473,8 @@ Module gas. M.read (| γ |), Value.Bool true |) in - get_constant (| - "revm_interpreter::gas::calc::istanbul_sstore_cost::SSTORE_RESET_GAS", - Ty.path "u64" - |))); - fun γ => - ltac:(M.monadic - (get_constant (| - "revm_interpreter::gas::calc::istanbul_sstore_cost::SLOAD_GAS", - Ty.path "u64" - |))) + M.alloc (| SSTORE_RESET_GAS |))); + fun γ => ltac:(M.monadic (M.alloc (| SLOAD_GAS |))) ] |))) ] diff --git a/CoqOfRust/revm/revm_interpreter/instructions/contract.v b/CoqOfRust/revm/revm_interpreter/instructions/contract.v index a13a46981..28cc4a35a 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/contract.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/contract.v @@ -6341,12 +6341,7 @@ Module instructions. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (get_constant (| - "revm_interpreter::instructions::contract::create::IS_CREATE2", - Ty.path "bool" - |)) in + (let γ := M.use (M.alloc (| IS_CREATE2 |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := @@ -7516,12 +7511,7 @@ Module instructions. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (get_constant (| - "revm_interpreter::instructions::contract::create::IS_CREATE2", - Ty.path "bool" - |)) in + (let γ := M.use (M.alloc (| IS_CREATE2 |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), diff --git a/CoqOfRust/revm/revm_interpreter/instructions/host.v b/CoqOfRust/revm/revm_interpreter/instructions/host.v index 79621ef7a..766eaad7f 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/host.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/host.v @@ -6499,16 +6499,7 @@ Module instructions. [], [] |), - [ - M.cast - (Ty.path "u8") - (M.read (| - get_constant (| - "revm_interpreter::instructions::host::log::N", - Ty.path "usize" - |) - |)); - M.cast (Ty.path "u64") (M.read (| len |)) + [ M.cast (Ty.path "u8") N; M.cast (Ty.path "u64") (M.read (| len |)) ] |) |), @@ -7230,12 +7221,7 @@ Module instructions. |) ] |), - M.read (| - get_constant (| - "revm_interpreter::instructions::host::log::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := diff --git a/CoqOfRust/revm/revm_interpreter/instructions/stack.v b/CoqOfRust/revm/revm_interpreter/instructions/stack.v index 20ae308a0..f6341d229 100644 --- a/CoqOfRust/revm/revm_interpreter/instructions/stack.v +++ b/CoqOfRust/revm/revm_interpreter/instructions/stack.v @@ -894,12 +894,7 @@ Module instructions. "bytecode" |) |); - M.read (| - get_constant (| - "revm_interpreter::instructions::stack::push::N", - Ty.path "usize" - |) - |) + N ] |) |) in @@ -945,14 +940,7 @@ Module instructions. "bytecode" |) |); - M.cast - (Ty.path "isize") - (M.read (| - get_constant (| - "revm_interpreter::instructions::stack::push::N", - Ty.path "usize" - |) - |)) + M.cast (Ty.path "isize") N ] |) |) in @@ -1136,12 +1124,7 @@ Module instructions. "stack" |) |); - M.read (| - get_constant (| - "revm_interpreter::instructions::stack::dup::N", - Ty.path "usize" - |) - |) + N ] |) |) @@ -1338,17 +1321,7 @@ Module instructions. (let γ := M.use (M.alloc (| - UnOp.not (| - BinOp.ne (| - M.read (| - get_constant (| - "revm_interpreter::instructions::stack::swap::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) - |) + UnOp.not (| BinOp.ne (| N, Value.Integer IntegerKind.Usize 0 |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1400,12 +1373,7 @@ Module instructions. |) |); Value.Integer IntegerKind.Usize 0; - M.read (| - get_constant (| - "revm_interpreter::instructions::stack::swap::N", - Ty.path "usize" - |) - |) + N ] |) |) diff --git a/CoqOfRust/revm/revm_interpreter/interpreter/stack.v b/CoqOfRust/revm/revm_interpreter/interpreter/stack.v index 3a59fb212..6f7a86f65 100644 --- a/CoqOfRust/revm/revm_interpreter/interpreter/stack.v +++ b/CoqOfRust/revm/revm_interpreter/interpreter/stack.v @@ -1304,12 +1304,7 @@ Module interpreter. |) ] |), - M.read (| - get_constant (| - "revm_interpreter::interpreter::stack::popn::N", - Ty.path "usize" - |) - |) + N |) |)) in let _ := @@ -1399,15 +1394,7 @@ Module interpreter. |) ] |), - BinOp.Wrap.add (| - M.read (| - get_constant (| - "revm_interpreter::interpreter::stack::popn_top::POPN", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.add (| POPN, Value.Integer IntegerKind.Usize 1 |) |) |)) in let _ := @@ -2158,15 +2145,7 @@ Module interpreter. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "revm_interpreter::interpreter::stack::popn::N", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| N, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/revm/revm_precompile/utilities.v b/CoqOfRust/revm/revm_precompile/utilities.v index 377529dc9..871c7a1ea 100644 --- a/CoqOfRust/revm/revm_precompile/utilities.v +++ b/CoqOfRust/revm/revm_precompile/utilities.v @@ -195,17 +195,7 @@ Module utilities. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| data |) |) |); - Value.StructRecord - "core::ops::range::RangeTo" - [ - ("end_", - M.read (| - get_constant (| - "revm_precompile::utilities::right_pad::LEN", - Ty.path "usize" - |) - |)) - ] + Value.StructRecord "core::ops::range::RangeTo" [ ("end_", LEN) ] ] |) |) in @@ -558,17 +548,7 @@ Module utilities. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| data |) |) |); - Value.StructRecord - "core::ops::range::RangeTo" - [ - ("end_", - M.read (| - get_constant (| - "revm_precompile::utilities::left_pad::LEN", - Ty.path "usize" - |) - |)) - ] + Value.StructRecord "core::ops::range::RangeTo" [ ("end_", LEN) ] ] |) |) in @@ -678,12 +658,7 @@ Module utilities. [ ("start", BinOp.Wrap.sub (| - M.read (| - get_constant (| - "revm_precompile::utilities::left_pad::LEN", - Ty.path "usize" - |) - |), + LEN, M.call_closure (| Ty.path "usize", M.get_associated_function (| diff --git a/CoqOfRust/ruint/add.v b/CoqOfRust/ruint/add.v index b3f83fae8..e17dc0f1d 100644 --- a/CoqOfRust/ruint/add.v +++ b/CoqOfRust/ruint/add.v @@ -333,12 +333,7 @@ Module add. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::add::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -377,15 +372,7 @@ Module add. fun γ => ltac:(M.monadic (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| "ruint::add::LIMBS", Ty.path "usize" |) - |) - |) - |)) in + M.use (M.alloc (| BinOp.lt (| M.read (| i |), LIMBS |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), @@ -495,12 +482,7 @@ Module add. "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::add::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) |), M.read (| @@ -518,10 +500,7 @@ Module add. let β := M.SubPointer.get_array_field (| M.SubPointer.get_struct_record_field (| self, "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::add::LIMBS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, @@ -641,12 +620,7 @@ Module add. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::add::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -685,15 +659,7 @@ Module add. fun γ => ltac:(M.monadic (let γ := - M.use - (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| "ruint::add::LIMBS", Ty.path "usize" |) - |) - |) - |)) in + M.use (M.alloc (| BinOp.lt (| M.read (| i |), LIMBS |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), @@ -803,12 +769,7 @@ Module add. "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::add::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) |), M.read (| @@ -826,10 +787,7 @@ Module add. let β := M.SubPointer.get_array_field (| M.SubPointer.get_struct_record_field (| self, "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::add::LIMBS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, diff --git a/CoqOfRust/ruint/algorithms/gcd/matrix.v b/CoqOfRust/ruint/algorithms/gcd/matrix.v index f5cfaecd8..45f34853a 100644 --- a/CoqOfRust/ruint/algorithms/gcd/matrix.v +++ b/CoqOfRust/ruint/algorithms/gcd/matrix.v @@ -587,15 +587,7 @@ Module algorithms. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "ruint::algorithms::gcd::matrix::apply::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| diff --git a/CoqOfRust/ruint/algorithms/gcd/mod.v b/CoqOfRust/ruint/algorithms/gcd/mod.v index ddef05092..5393ce8f9 100644 --- a/CoqOfRust/ruint/algorithms/gcd/mod.v +++ b/CoqOfRust/ruint/algorithms/gcd/mod.v @@ -421,15 +421,7 @@ Module algorithms. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| - "ruint::algorithms::gcd::gcd_extended::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1241,15 +1233,7 @@ Module algorithms. M.use (M.alloc (| LogicalOp.or (| - BinOp.eq (| - M.read (| - get_constant (| - "ruint::algorithms::gcd::inv_mod::BITS", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |), + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic (M.call_closure (| Ty.path "bool", diff --git a/CoqOfRust/ruint/base_convert.v b/CoqOfRust/ruint/base_convert.v index fe80fc43e..71ea4e582 100644 --- a/CoqOfRust/ruint/base_convert.v +++ b/CoqOfRust/ruint/base_convert.v @@ -999,12 +999,7 @@ Module base_convert. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::base_convert::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1512,12 +1507,7 @@ Module base_convert. "limbs" |), BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::base_convert::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, Value.Integer IntegerKind.Usize 1 @@ -1612,12 +1602,7 @@ Module base_convert. "limbs" |), BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::base_convert::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, Value.Integer IntegerKind.Usize 1 @@ -2273,12 +2258,7 @@ Module base_convert. ltac:(M.monadic (LogicalOp.and (| BinOp.ne (| - M.read (| - get_constant (| - "ruint::base_convert::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic @@ -2291,12 +2271,7 @@ Module base_convert. "limbs" |), BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::base_convert::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, Value.Integer IntegerKind.Usize 1 diff --git a/CoqOfRust/ruint/bits.v b/CoqOfRust/ruint/bits.v index a78dff126..484b2be3f 100644 --- a/CoqOfRust/ruint/bits.v +++ b/CoqOfRust/ruint/bits.v @@ -37,16 +37,7 @@ Module bits. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.ge (| - M.read (| index |), - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.ge (| M.read (| index |), BITS |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -140,16 +131,7 @@ Module bits. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.ge (| - M.read (| index |), - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.ge (| M.read (| index |), BITS |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| @@ -457,12 +439,7 @@ Module bits. M.use (M.alloc (| BinOp.ne (| - BinOp.Wrap.rem (| - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 64 - |), + BinOp.Wrap.rem (| BITS, Value.Integer IntegerKind.Usize 64 |), Value.Integer IntegerKind.Usize 0 |) |)) in @@ -484,12 +461,7 @@ Module bits. M.borrow (| Pointer.Kind.MutRef, self |); BinOp.Wrap.sub (| Value.Integer IntegerKind.Usize 64, - BinOp.Wrap.rem (| - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 64 - |) + BinOp.Wrap.rem (| BITS, Value.Integer IntegerKind.Usize 64 |) |) ] |) @@ -645,7 +617,7 @@ Module bits. end)) ] |); - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |); + BITS; M.closure (fun γ => ltac:(M.monadic @@ -734,15 +706,7 @@ Module bits. |) |), BinOp.Wrap.sub (| - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), - M.read (| n |) - |), + BinOp.Wrap.sub (| LIMBS, M.read (| n |) |), Value.Integer IntegerKind.Usize 1 |) |) @@ -936,7 +900,7 @@ Module bits. end)) ] |); - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |); + BITS; M.closure (fun γ => ltac:(M.monadic @@ -1130,7 +1094,7 @@ Module bits. end)) ] |); - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |); + BITS; M.closure (fun γ => ltac:(M.monadic @@ -1366,7 +1330,7 @@ Module bits. ltac:(M.monadic (let self := M.alloc (| self |) in BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |), + BITS, M.call_closure (| Ty.path "usize", M.get_associated_function (| @@ -1404,7 +1368,7 @@ Module bits. ltac:(M.monadic (let self := M.alloc (| self |) in BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |), + BITS, M.call_closure (| Ty.path "usize", M.get_associated_function (| @@ -2024,14 +1988,7 @@ Module bits. ltac:(M.monadic (let γ := M.use - (M.alloc (| - BinOp.ge (| - M.read (| limbs |), - M.read (| - get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) - |) - |) - |)) in + (M.alloc (| BinOp.ge (| M.read (| limbs |), LIMBS |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), @@ -2154,21 +2111,10 @@ Module bits. [ ("start", BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, M.read (| limbs |) |)); - ("end_", - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |)) + ("end_", LIMBS) ] ] |) @@ -2288,12 +2234,7 @@ Module bits. |), BinOp.Wrap.sub (| BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, M.read (| limbs |) |), Value.Integer IntegerKind.Usize 1 @@ -2386,13 +2327,7 @@ Module bits. "core::ops::range::Range" [ ("start", M.read (| limbs |)); - ("end_", - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |)) + ("end_", LIMBS) ] ] |) @@ -2499,13 +2434,7 @@ Module bits. limbs |) |), - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path - "usize" - |) - |) + LIMBS |))) |) |) @@ -2778,12 +2707,7 @@ Module bits. "limbs" |), BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in @@ -2839,20 +2763,8 @@ Module bits. Value.StructRecord "core::ops::range::Range" [ - ("start", - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), - M.read (| limbs |) - |)); - ("end_", - M.read (| - get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) - |)) + ("start", BinOp.Wrap.sub (| LIMBS, M.read (| limbs |) |)); + ("end_", LIMBS) ] ] |) @@ -2964,15 +2876,7 @@ Module bits. "limbs" |), BinOp.Wrap.sub (| - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), - M.read (| limbs |) - |), + BinOp.Wrap.sub (| LIMBS, M.read (| limbs |) |), Value.Integer IntegerKind.Usize 1 |) |) @@ -3016,15 +2920,7 @@ Module bits. "limbs" |), BinOp.Wrap.sub (| - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), - M.read (| limbs |) - |), + BinOp.Wrap.sub (| LIMBS, M.read (| limbs |) |), Value.Integer IntegerKind.Usize 1 |) |) @@ -3115,13 +3011,7 @@ Module bits. M.read (| limbs |), Value.Integer IntegerKind.Usize 1 |)); - ("end_", - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |)) + ("end_", LIMBS) ] ] |) @@ -3208,12 +3098,7 @@ Module bits. M.read (| i |), M.read (| limbs |) |), - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |) + LIMBS |), ltac:(M.monadic (BinOp.lt (| @@ -3226,12 +3111,7 @@ Module bits. IntegerKind.Usize 1 |), - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |) + LIMBS |))) |) |) @@ -3544,12 +3424,7 @@ Module bits. "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, @@ -3760,14 +3635,7 @@ Module bits. ltac:(M.monadic (let γ := M.use - (M.alloc (| - BinOp.ge (| - M.read (| limbs |), - M.read (| - get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) - |) - |) - |)) in + (M.alloc (| BinOp.ge (| M.read (| limbs |), LIMBS |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), @@ -4020,12 +3888,7 @@ Module bits. Value.Integer IntegerKind.Usize 0); ("end_", BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, M.read (| limbs |) |)) ] @@ -4184,12 +4047,7 @@ Module bits. [ ("start", BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, M.read (| limbs |) |)) ] @@ -4223,12 +4081,7 @@ Module bits. "limbs" |), BinOp.Wrap.sub (| - BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) - |), - M.read (| limbs |) - |), + BinOp.Wrap.sub (| LIMBS, M.read (| limbs |) |), Value.Integer IntegerKind.Usize 1 |) |) @@ -4271,15 +4124,7 @@ Module bits. ("start", Value.Integer IntegerKind.Usize 0); ("end_", BinOp.Wrap.sub (| - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), - M.read (| limbs |) - |), + BinOp.Wrap.sub (| LIMBS, M.read (| limbs |) |), Value.Integer IntegerKind.Usize 1 |)) ] @@ -4361,12 +4206,7 @@ Module bits. M.read (| i |), M.read (| limbs |) |), - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |) + LIMBS |), ltac:(M.monadic (BinOp.lt (| @@ -4379,12 +4219,7 @@ Module bits. IntegerKind.Usize 1 |), - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |) + LIMBS |))) |) |) @@ -4619,12 +4454,7 @@ Module bits. "limbs" |), BinOp.Wrap.sub (| - BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) - |), - M.read (| limbs |) - |), + BinOp.Wrap.sub (| LIMBS, M.read (| limbs |) |), Value.Integer IntegerKind.Usize 1 |) |), @@ -4636,12 +4466,7 @@ Module bits. "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) |), M.read (| bits |) @@ -4694,15 +4519,7 @@ Module bits. "core::ops::range::RangeFrom" [ ("start", - BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::bits::LIMBS", - Ty.path "usize" - |) - |), - M.read (| limbs |) - |)) + BinOp.Wrap.sub (| LIMBS, M.read (| limbs |) |)) ] ] |) @@ -4807,12 +4624,7 @@ Module bits. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -4846,10 +4658,7 @@ Module bits. |), [ M.borrow (| Pointer.Kind.Ref, self |); - BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| BITS, Value.Integer IntegerKind.Usize 1 |) ] |) |) in @@ -4921,12 +4730,7 @@ Module bits. [], [] |), - [ - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |); - M.read (| rhs |) - ] + [ BITS; M.read (| rhs |) ] |) ] |) @@ -4983,12 +4787,7 @@ Module bits. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -5011,12 +4810,7 @@ Module bits. ] |) in let~ rhs : Ty.path "usize" := - M.alloc (| - BinOp.Wrap.rem (| - M.read (| rhs |), - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |) - |) - |) in + M.alloc (| BinOp.Wrap.rem (| M.read (| rhs |), BITS |) |) in M.alloc (| M.call_closure (| Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [], @@ -5054,13 +4848,7 @@ Module bits. [], [] |), - [ - M.read (| self |); - BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |), - M.read (| rhs |) - |) - ] + [ M.read (| self |); BinOp.Wrap.sub (| BITS, M.read (| rhs |) |) ] |) ] |) @@ -5110,12 +4898,7 @@ Module bits. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -5138,12 +4921,7 @@ Module bits. ] |) in let~ rhs : Ty.path "usize" := - M.alloc (| - BinOp.Wrap.rem (| - M.read (| rhs |), - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |) - |) - |) in + M.alloc (| BinOp.Wrap.rem (| M.read (| rhs |), BITS |) |) in M.alloc (| M.call_closure (| Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [], @@ -5153,13 +4931,7 @@ Module bits. [], [] |), - [ - M.read (| self |); - BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::bits::BITS", Ty.path "usize" |) |), - M.read (| rhs |) - |) - ] + [ M.read (| self |); BinOp.Wrap.sub (| BITS, M.read (| rhs |) |) ] |) |) |))) @@ -5218,12 +4990,7 @@ Module bits. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -5363,10 +5130,7 @@ Module bits. let β := M.SubPointer.get_array_field (| M.SubPointer.get_struct_record_field (| self, "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, @@ -5558,11 +5322,7 @@ Module bits. [ Value.StructRecord "core::ops::range::Range" - [ - ("start", Value.Integer IntegerKind.Usize 0); - ("end_", - M.read (| get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) |)) - ] + [ ("start", Value.Integer IntegerKind.Usize 0); ("end_", LIMBS) ] ] |) |), @@ -6050,11 +5810,7 @@ Module bits. [ Value.StructRecord "core::ops::range::Range" - [ - ("start", Value.Integer IntegerKind.Usize 0); - ("end_", - M.read (| get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) |)) - ] + [ ("start", Value.Integer IntegerKind.Usize 0); ("end_", LIMBS) ] ] |) |), @@ -6542,11 +6298,7 @@ Module bits. [ Value.StructRecord "core::ops::range::Range" - [ - ("start", Value.Integer IntegerKind.Usize 0); - ("end_", - M.read (| get_constant (| "ruint::bits::LIMBS", Ty.path "usize" |) |)) - ] + [ ("start", Value.Integer IntegerKind.Usize 0); ("end_", LIMBS) ] ] |) |), @@ -6977,12 +6729,7 @@ Module bits. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -7149,12 +6896,7 @@ Module bits. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::bits::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/ruint/bytes.v b/CoqOfRust/ruint/bytes.v index 6f61bc761..a6762668a 100644 --- a/CoqOfRust/ruint/bytes.v +++ b/CoqOfRust/ruint/bytes.v @@ -18,10 +18,7 @@ Module bytes. ltac:(M.monadic (M.alloc (| BinOp.Wrap.div (| - BinOp.Wrap.add (| - M.read (| get_constant (| "ruint::bytes::BITS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 7 - |), + BinOp.Wrap.add (| BITS, Value.Integer IntegerKind.Usize 7 |), Value.Integer IntegerKind.Usize 8 |) |))). @@ -447,12 +444,7 @@ Module bytes. (M.alloc (| UnOp.not (| BinOp.eq (| - M.read (| - get_constant (| - "ruint::bytes::to_le_bytes::BYTES", - Ty.path "usize" - |) - |), + BYTES, M.read (| get_associated_constant (| Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [], @@ -1045,12 +1037,7 @@ Module bytes. (M.alloc (| UnOp.not (| BinOp.eq (| - M.read (| - get_constant (| - "ruint::bytes::from_be_bytes::BYTES", - Ty.path "usize" - |) - |), + BYTES, M.read (| get_associated_constant (| Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [], @@ -1416,15 +1403,7 @@ Module bytes. (let γ := M.use (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| - "ruint::bytes::LIMBS", - Ty.path "usize" - |) - |) - |) + BinOp.lt (| M.read (| i |), LIMBS |) |)) in let _ := M.is_constant_or_break_match (| @@ -1815,12 +1794,7 @@ Module bytes. (M.alloc (| UnOp.not (| BinOp.eq (| - M.read (| - get_constant (| - "ruint::bytes::from_le_bytes::BYTES", - Ty.path "usize" - |) - |), + BYTES, M.read (| get_associated_constant (| Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [], @@ -2159,15 +2133,7 @@ Module bytes. (let γ := M.use (M.alloc (| - BinOp.lt (| - M.read (| i |), - M.read (| - get_constant (| - "ruint::bytes::LIMBS", - Ty.path "usize" - |) - |) - |) + BinOp.lt (| M.read (| i |), LIMBS |) |)) in let _ := M.is_constant_or_break_match (| diff --git a/CoqOfRust/ruint/fmt.v b/CoqOfRust/ruint/fmt.v index 83b9e94c3..9c6a0d698 100644 --- a/CoqOfRust/ruint/fmt.v +++ b/CoqOfRust/ruint/fmt.v @@ -212,12 +212,7 @@ Module fmt. M.use (M.alloc (| LogicalOp.or (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::fmt::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |), + BinOp.eq (| LIMBS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic (M.call_closure (| Ty.path "bool", @@ -793,12 +788,7 @@ Module fmt. M.use (M.alloc (| LogicalOp.or (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::fmt::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |), + BinOp.eq (| LIMBS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic (M.call_closure (| Ty.path "bool", @@ -1321,12 +1311,7 @@ Module fmt. M.use (M.alloc (| LogicalOp.or (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::fmt::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |), + BinOp.eq (| LIMBS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic (M.call_closure (| Ty.path "bool", @@ -1849,12 +1834,7 @@ Module fmt. M.use (M.alloc (| LogicalOp.or (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::fmt::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |), + BinOp.eq (| LIMBS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic (M.call_closure (| Ty.path "bool", @@ -2377,12 +2357,7 @@ Module fmt. M.use (M.alloc (| LogicalOp.or (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::fmt::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |), + BinOp.eq (| LIMBS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic (M.call_closure (| Ty.path "bool", @@ -3235,9 +3210,7 @@ Module fmt. ] |) |), - M.read (| - get_constant (| "ruint::fmt::SIZE", Ty.path "usize" |) - |) + SIZE |) |)) in let _ := diff --git a/CoqOfRust/ruint/from.v b/CoqOfRust/ruint/from.v index 743950453..03b77a3dd 100644 --- a/CoqOfRust/ruint/from.v +++ b/CoqOfRust/ruint/from.v @@ -3026,12 +3026,7 @@ Module from. [ Value.StructTuple "ruint::from::ToUintError::ValueTooLarge" - [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); - M.read (| n |) - ] + [ BITS; M.read (| n |) ] ] |))); fun γ => @@ -3207,9 +3202,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS_DST", Ty.path "usize" |) - |); + BITS_DST; M.read (| n |); M.read (| get_associated_constant (| @@ -3307,12 +3300,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.le (| - M.read (| - get_constant (| "ruint::from::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.le (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -3364,12 +3352,7 @@ Module from. M.use (M.alloc (| BinOp.eq (| - M.read (| - get_constant (| - "ruint::from::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, Value.Integer IntegerKind.Usize 1 |) |)) in @@ -3411,12 +3394,7 @@ Module from. Value.StructTuple "ruint::from::ToUintError::ValueTooLarge" [ - M.read (| - get_constant (| - "ruint::from::BITS", - Ty.path "usize" - |) - |); + BITS; M.call_closure (| Ty.apply (Ty.path "ruint::Uint") @@ -3451,12 +3429,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| LIMBS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| @@ -3787,15 +3760,7 @@ Module from. [ Value.StructTuple "ruint::from::ToUintError::ValueTooLarge" - [ - M.read (| - get_constant (| - "ruint::from::BITS", - Ty.path "usize" - |) - |); - M.read (| n |) - ] + [ BITS; M.read (| n |) ] ])) ] |))) @@ -3906,9 +3871,7 @@ Module from. Value.StructTuple "ruint::from::ToUintError::ValueTooLarge" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.call_closure (| Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [], M.get_associated_function (| @@ -4436,15 +4399,7 @@ Module from. (M.alloc (| Value.StructTuple "ruint::from::ToUintError::ValueNegative" - [ - M.read (| - get_constant (| - "ruint::from::BITS", - Ty.path "usize" - |) - |); - M.read (| n |) - ] + [ BITS; M.read (| n |) ] |))) | _ => M.impossible "wrong number of arguments" end) @@ -4657,15 +4612,7 @@ Module from. (M.alloc (| Value.StructTuple "ruint::from::ToUintError::ValueNegative" - [ - M.read (| - get_constant (| - "ruint::from::BITS", - Ty.path "usize" - |) - |); - M.read (| n |) - ] + [ BITS; M.read (| n |) ] |))) | _ => M.impossible "wrong number of arguments" end) @@ -4878,15 +4825,7 @@ Module from. (M.alloc (| Value.StructTuple "ruint::from::ToUintError::ValueNegative" - [ - M.read (| - get_constant (| - "ruint::from::BITS", - Ty.path "usize" - |) - |); - M.read (| n |) - ] + [ BITS; M.read (| n |) ] |))) | _ => M.impossible "wrong number of arguments" end) @@ -5099,15 +5038,7 @@ Module from. (M.alloc (| Value.StructTuple "ruint::from::ToUintError::ValueNegative" - [ - M.read (| - get_constant (| - "ruint::from::BITS", - Ty.path "usize" - |) - |); - M.read (| n |) - ] + [ BITS; M.read (| n |) ] |))) | _ => M.impossible "wrong number of arguments" end) @@ -5320,15 +5251,7 @@ Module from. (M.alloc (| Value.StructTuple "ruint::from::ToUintError::ValueNegative" - [ - M.read (| - get_constant (| - "ruint::from::BITS", - Ty.path "usize" - |) - |); - M.read (| n |) - ] + [ BITS; M.read (| n |) ] |))) | _ => M.impossible "wrong number of arguments" end) @@ -5541,15 +5464,7 @@ Module from. (M.alloc (| Value.StructTuple "ruint::from::ToUintError::ValueNegative" - [ - M.read (| - get_constant (| - "ruint::from::BITS", - Ty.path "usize" - |) - |); - M.read (| n |) - ] + [ BITS; M.read (| n |) ] |))) | _ => M.impossible "wrong number of arguments" end) @@ -5733,11 +5648,7 @@ Module from. [ Value.StructTuple "ruint::from::ToUintError::NotANumber" - [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |) - ] + [ BITS ] ] |) |) @@ -5897,12 +5808,7 @@ Module from. [ Value.StructTuple "ruint::from::ToUintError::ValueNegative" - [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); - M.read (| wrapped |) - ] + [ BITS; M.read (| wrapped |) ] ] |) |) @@ -6047,12 +5953,7 @@ Module from. [ Value.StructTuple "ruint::from::ToUintError::ValueTooLarge" - [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); - M.read (| wrapped |) - ] + [ BITS; M.read (| wrapped |) ] ] |) |) @@ -6270,9 +6171,7 @@ Module from. Value.StructTuple "ruint::from::ToUintError::ValueTooLarge" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.read (| get_associated_constant (| Ty.apply (Ty.path "ruint::Uint") [ BITS; LIMBS ] [], @@ -6566,15 +6465,7 @@ Module from. [ Value.StructTuple "ruint::from::ToUintError::ValueTooLarge" - [ - M.read (| - get_constant (| - "ruint::from::BITS", - Ty.path "usize" - |) - |); - M.read (| n |) - ] + [ BITS; M.read (| n |) ] ] |))); fun γ => @@ -6777,12 +6668,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -6839,9 +6725,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.call_closure (| Ty.path "bool", M.get_associated_function (| @@ -7022,12 +6906,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -7091,9 +6970,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.cast (Ty.path "i8") (M.read (| @@ -7275,12 +7152,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -7344,9 +7216,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.cast (Ty.path "u8") (M.read (| @@ -7529,12 +7399,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -7598,9 +7463,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.cast (Ty.path "i16") (M.read (| @@ -7783,12 +7646,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -7852,9 +7710,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.cast (Ty.path "u16") (M.read (| @@ -8037,12 +7893,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -8106,9 +7957,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.cast (Ty.path "i32") (M.read (| @@ -8291,12 +8140,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -8360,9 +8204,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.cast (Ty.path "u32") (M.read (| @@ -8545,12 +8387,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -8614,9 +8451,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.cast (Ty.path "i64") (M.read (| @@ -8799,12 +8634,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -8868,9 +8698,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.read (| M.use (M.SubPointer.get_array_field (| @@ -9053,12 +8881,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -9122,9 +8945,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.cast (Ty.path "isize") (M.read (| @@ -9309,12 +9130,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -9378,9 +9194,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.cast (Ty.path "usize") (M.read (| @@ -9564,12 +9378,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -9612,12 +9421,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.le (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 64 - |) + BinOp.le (| BITS, Value.Integer IntegerKind.Usize 64 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -9700,9 +9504,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.read (| result |); M.read (| get_associated_constant (| @@ -9847,12 +9649,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -9895,12 +9692,7 @@ Module from. (let γ := M.use (M.alloc (| - BinOp.le (| - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 64 - |) + BinOp.le (| BITS, Value.Integer IntegerKind.Usize 64 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -9983,9 +9775,7 @@ Module from. Value.StructTuple "ruint::from::FromUintError::Overflow" [ - M.read (| - get_constant (| "ruint::from::BITS", Ty.path "usize" |) - |); + BITS; M.read (| result |); M.read (| get_associated_constant (| diff --git a/CoqOfRust/ruint/lib.v b/CoqOfRust/ruint/lib.v index da21a132a..26c448dd9 100644 --- a/CoqOfRust/ruint/lib.v +++ b/CoqOfRust/ruint/lib.v @@ -254,7 +254,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. M.call_closure (| Ty.path "usize", M.get_function (| "ruint::nlimbs", [], [] |), - [ M.read (| get_constant (| "ruint::BITS", Ty.path "usize" |) |) ] + [ BITS ] |) |) in let~ _ : Ty.tuple [] := @@ -265,15 +265,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. fun γ => ltac:(M.monadic (let γ := - M.use - (M.alloc (| - UnOp.not (| - BinOp.eq (| - M.read (| get_constant (| "ruint::LIMBS", Ty.path "usize" |) |), - M.read (| limbs |) - |) - |) - |)) in + M.use (M.alloc (| UnOp.not (| BinOp.eq (| LIMBS, M.read (| limbs |) |) |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| M.never_to_any (| @@ -334,11 +326,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. let Self : Ty.t := Self BITS LIMBS in ltac:(M.monadic (M.alloc (| - M.call_closure (| - Ty.path "u64", - M.get_function (| "ruint::mask", [], [] |), - [ M.read (| get_constant (| "ruint::BITS", Ty.path "usize" |) |) ] - |) + M.call_closure (| Ty.path "u64", M.get_function (| "ruint::mask", [], [] |), [ BITS ] |) |))). Global Instance AssociatedConstant_value_MASK : @@ -356,7 +344,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. (α : list Value.t) : M := let Self : Ty.t := Self BITS LIMBS in - ltac:(M.monadic (get_constant (| "ruint::BITS", Ty.path "usize" |))). + ltac:(M.monadic (M.alloc (| BITS |))). Global Instance AssociatedConstant_value_BITS : forall (BITS LIMBS : Value.t), @@ -448,23 +436,14 @@ Module Impl_ruint_Uint_BITS_LIMBS. fun γ => ltac:(M.monadic (let γ := - M.use - (M.alloc (| - BinOp.gt (| - M.read (| get_constant (| "ruint::BITS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 0 - |) - |)) in + M.use (M.alloc (| BinOp.gt (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := M.alloc (| let β := M.SubPointer.get_array_field (| limbs, - BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::LIMBS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, @@ -644,10 +623,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. M.use (M.alloc (| LogicalOp.and (| - BinOp.gt (| - M.read (| get_constant (| "ruint::BITS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 0 - |), + BinOp.gt (| BITS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic (BinOp.ne (| M.read (| @@ -1014,7 +990,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. |), [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| slice |) |) |) ] |), - M.read (| get_constant (| "ruint::LIMBS", Ty.path "usize" |) |) + LIMBS |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1122,10 +1098,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. [], [] |), - [ - M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| slice |) |) |); - M.read (| get_constant (| "ruint::LIMBS", Ty.path "usize" |) |) - ] + [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| slice |) |) |); LIMBS ] |) |), [ @@ -1236,12 +1209,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. (let γ := M.use (M.alloc (| - BinOp.gt (| - M.read (| - get_constant (| "ruint::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.gt (| LIMBS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| @@ -1260,12 +1228,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. M.SubPointer.get_array_field (| limbs, BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::LIMBS", - Ty.path "usize" - |) - |), + LIMBS, Value.Integer IntegerKind.Usize 1 |) |) @@ -1289,9 +1252,7 @@ Module Impl_ruint_Uint_BITS_LIMBS. M.SubPointer.get_array_field (| limbs, BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::LIMBS", Ty.path "usize" |) - |), + LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in diff --git a/CoqOfRust/ruint/modular.v b/CoqOfRust/ruint/modular.v index 474dd0377..d69bd3496 100644 --- a/CoqOfRust/ruint/modular.v +++ b/CoqOfRust/ruint/modular.v @@ -415,12 +415,7 @@ Module modular. M.call_closure (| Ty.path "usize", M.get_function (| "ruint::nlimbs", [], [] |), - [ - BinOp.Wrap.mul (| - Value.Integer IntegerKind.Usize 2, - M.read (| get_constant (| "ruint::modular::BITS", Ty.path "usize" |) |) - |) - ] + [ BinOp.Wrap.mul (| Value.Integer IntegerKind.Usize 2, BITS |) ] |) |) in let~ _ : Ty.tuple [] := @@ -447,12 +442,7 @@ Module modular. BinOp.ge (| BinOp.Wrap.mul (| Value.Integer IntegerKind.Usize 2, - M.read (| - get_constant (| - "ruint::modular::LIMBS", - Ty.path "usize" - |) - |) + LIMBS |), M.read (| product_len |) |) @@ -1059,12 +1049,7 @@ Module modular. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::modular::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/ruint/mul.v b/CoqOfRust/ruint/mul.v index 92e75da5a..0986861c7 100644 --- a/CoqOfRust/ruint/mul.v +++ b/CoqOfRust/ruint/mul.v @@ -165,12 +165,7 @@ Module mul. ltac:(M.monadic (let γ := M.use - (M.alloc (| - BinOp.gt (| - M.read (| get_constant (| "ruint::mul::BITS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 0 - |) - |)) in + (M.alloc (| BinOp.gt (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := M.alloc (| @@ -187,12 +182,7 @@ Module mul. "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::mul::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) |), M.read (| @@ -214,12 +204,7 @@ Module mul. "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::mul::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, @@ -406,12 +391,7 @@ Module mul. ltac:(M.monadic (let γ := M.use - (M.alloc (| - BinOp.gt (| - M.read (| get_constant (| "ruint::mul::BITS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 0 - |) - |)) in + (M.alloc (| BinOp.gt (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := M.alloc (| @@ -422,12 +402,7 @@ Module mul. "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| - get_constant (| "ruint::mul::LIMBS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, @@ -514,12 +489,7 @@ Module mul. M.use (M.alloc (| LogicalOp.or (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::mul::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |), + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |), ltac:(M.monadic (BinOp.eq (| BinOp.bit_and @@ -1171,12 +1141,7 @@ Module mul. (let γ := M.use (M.alloc (| - BinOp.lt (| - M.read (| correct_limbs |), - M.read (| - get_constant (| "ruint::mul::LIMBS", Ty.path "usize" |) - |) - |) + BinOp.lt (| M.read (| correct_limbs |), LIMBS |) |)) in let _ := M.is_constant_or_break_match (| @@ -1272,10 +1237,7 @@ Module mul. let β := M.SubPointer.get_array_field (| M.SubPointer.get_struct_record_field (| result, "ruint::Uint", "limbs" |), - BinOp.Wrap.sub (| - M.read (| get_constant (| "ruint::mul::LIMBS", Ty.path "usize" |) |), - Value.Integer IntegerKind.Usize 1 - |) + BinOp.Wrap.sub (| LIMBS, Value.Integer IntegerKind.Usize 1 |) |) in M.write (| β, @@ -1342,23 +1304,10 @@ Module mul. M.alloc (| Value.Tuple [ + M.borrow (| Pointer.Kind.Ref, M.alloc (| BITS_RES |) |); M.borrow (| Pointer.Kind.Ref, - get_constant (| "ruint::mul::widening_mul::BITS_RES", Ty.path "usize" |) - |); - M.borrow (| - Pointer.Kind.Ref, - M.alloc (| - BinOp.Wrap.add (| - M.read (| get_constant (| "ruint::mul::BITS", Ty.path "usize" |) |), - M.read (| - get_constant (| - "ruint::mul::widening_mul::BITS_RHS", - Ty.path "usize" - |) - |) - |) - |) + M.alloc (| BinOp.Wrap.add (| BITS, BITS_RHS |) |) |) ] |), @@ -1443,24 +1392,14 @@ Module mul. M.alloc (| Value.Tuple [ - M.borrow (| - Pointer.Kind.Ref, - get_constant (| "ruint::mul::widening_mul::LIMBS_RES", Ty.path "usize" |) - |); + M.borrow (| Pointer.Kind.Ref, M.alloc (| LIMBS_RES |) |); M.borrow (| Pointer.Kind.Ref, M.alloc (| M.call_closure (| Ty.path "usize", M.get_function (| "ruint::nlimbs", [], [] |), - [ - M.read (| - get_constant (| - "ruint::mul::widening_mul::BITS_RES", - Ty.path "usize" - |) - |) - ] + [ BITS_RES ] |) |) |) @@ -1613,15 +1552,7 @@ Module mul. (let γ := M.use (M.alloc (| - BinOp.gt (| - M.read (| - get_constant (| - "ruint::mul::widening_mul::LIMBS_RES", - Ty.path "usize" - |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.gt (| LIMBS_RES, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in let~ _ : Ty.tuple [] := @@ -1657,12 +1588,7 @@ Module mul. "limbs" |), BinOp.Wrap.sub (| - M.read (| - get_constant (| - "ruint::mul::widening_mul::LIMBS_RES", - Ty.path "usize" - |) - |), + LIMBS_RES, Value.Integer IntegerKind.Usize 1 |) |) @@ -1764,12 +1690,7 @@ Module mul. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::mul::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -1886,12 +1807,7 @@ Module mul. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::mul::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/ruint/pow.v b/CoqOfRust/ruint/pow.v index a9cae5ade..6860b046a 100644 --- a/CoqOfRust/ruint/pow.v +++ b/CoqOfRust/ruint/pow.v @@ -127,12 +127,7 @@ Module pow. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::pow::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in @@ -521,12 +516,7 @@ Module pow. (let γ := M.use (M.alloc (| - BinOp.eq (| - M.read (| - get_constant (| "ruint::pow::BITS", Ty.path "usize" |) - |), - Value.Integer IntegerKind.Usize 0 - |) + BinOp.eq (| BITS, Value.Integer IntegerKind.Usize 0 |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in diff --git a/CoqOfRust/ruint/special.v b/CoqOfRust/ruint/special.v index 829781606..fc725c5e0 100644 --- a/CoqOfRust/ruint/special.v +++ b/CoqOfRust/ruint/special.v @@ -179,16 +179,7 @@ Module special. [ fun γ => ltac:(M.monadic - (let γ := - M.use - (M.alloc (| - BinOp.ge (| - M.read (| exp |), - M.read (| - get_constant (| "ruint::special::BITS", Ty.path "usize" |) - |) - |) - |)) in + (let γ := M.use (M.alloc (| BinOp.ge (| M.read (| exp |), BITS |) |)) in let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in M.alloc (| diff --git a/lib/src/thir_expression.rs b/lib/src/thir_expression.rs index 57ff48387..4e1946c82 100644 --- a/lib/src/thir_expression.rs +++ b/lib/src/thir_expression.rs @@ -1202,13 +1202,10 @@ pub(crate) fn compile_expr<'a>( _ => Rc::new(Expr::GetConstant { path, return_ty }), } } - thir::ExprKind::ConstParam { def_id, .. } => { - let return_ty = compile_type(env, &expr.span, generics, &expr.ty); + thir::ExprKind::ConstParam { param, .. } => { + let name = to_valid_coq_name(IsValue::No, param.name.as_str()); - Rc::new(Expr::GetConstant { - path: compile_def_id(env, *def_id), - return_ty, - }) + Expr::local_var(name.as_str()).alloc() } thir::ExprKind::StaticRef { def_id, .. } => { let return_ty = compile_type(env, &expr.span, generics, &expr.ty);