diff --git a/CoqOfRust/alloc/links/raw_vec.v b/CoqOfRust/alloc/links/raw_vec.v new file mode 100644 index 000000000..992db6395 --- /dev/null +++ b/CoqOfRust/alloc/links/raw_vec.v @@ -0,0 +1,55 @@ +Require Import CoqOfRust.CoqOfRust. +Require Import links.M. +Require Import alloc.links.alloc. +Require Import alloc.raw_vec. + +Module RawVec. + Parameter t : Set -> Set -> Set. + + Parameter to_value : forall {T A : Set}, t T A -> Value.t. + + Global Instance IsLink (T A : Set) `(Link T) `(Link A) : Link (t T A) := { + Φ := Ty.apply (Ty.path "alloc::raw_vec::RawVec") [] [Φ T; Φ A]; + φ := to_value; + }. + + Definition of_ty (T' A' : Ty.t) : + OfTy.t T' -> + OfTy.t A' -> + OfTy.t (Ty.apply (Ty.path "alloc::raw_vec::RawVec") [] [T'; A']). + Proof. + intros [T] [A]. + eapply OfTy.Make with (A := t T A). + subst. + reflexivity. + Defined. + Smpl Add apply of_ty : of_ty. +End RawVec. + +Module Impl_RawVec_T_A. + Definition Self (T A : Set) `{Link T} `{Link A} : Set := + RawVec.t T A. + + (* + pub const fn new_in(alloc: A) -> Self + *) + Instance run_new_in {T A : Set} `{Link T} `{Link A} (alloc : A) : + Run.Trait + (raw_vec.Impl_alloc_raw_vec_RawVec_T_A.new_in (Φ T) (Φ A)) [] [] [φ alloc] + (Self T A). + Admitted. +End Impl_RawVec_T_A. +Export Impl_RawVec_T_A. + +Module Impl_RawVec_T. + Definition Self (T : Set) `{Link T} : Set := + RawVec.t T Global.t. + + (* + pub const fn new() -> Self + *) + Instance run_new {T : Set} `{Link T} : + Run.Trait (raw_vec.Impl_alloc_raw_vec_RawVec_T_alloc_alloc_Global.new (Φ T)) [] [] [] (Self T). + Admitted. +End Impl_RawVec_T. +Export Impl_RawVec_T. diff --git a/CoqOfRust/alloc/vec/links/mod.v b/CoqOfRust/alloc/vec/links/mod.v index c68cbab67..58c02ebf6 100644 --- a/CoqOfRust/alloc/vec/links/mod.v +++ b/CoqOfRust/alloc/vec/links/mod.v @@ -2,23 +2,32 @@ Require Import CoqOfRust.CoqOfRust. Require Import alloc.vec.mod. Require Import links.M. Require Import alloc.links.alloc. +Require Import alloc.links.raw_vec. Require Import core.links.clone. Require Import core.links.default. Require Import core.links.option. Require Import core.ops.links.deref. Require Import core.ops.links.index. +(* +pub struct Vec { + buf: RawVec, + len: usize, +} +*) Module Vec. Record t {T A : Set} : Set := { - value : list T; + buf : RawVec.t T A; + len : Usize.t; }. Arguments t : clear implicits. - Parameter to_value : forall {T A : Set}, t T A -> Value.t. - Global Instance IsLink (T A : Set) `(Link T) `(Link A) : Link (t T A) := { Φ := Ty.apply (Ty.path "alloc::vec::Vec") [] [Φ T; Φ A]; - φ := to_value; + φ x := Value.StructRecord "alloc::vec::Vec" [] [Φ T; Φ A] [ + ("buf", φ x.(buf)); + ("len", φ x.(len)) + ]; }. Definition of_ty (T' A' : Ty.t) : @@ -32,6 +41,40 @@ Module Vec. reflexivity. Defined. Smpl Add apply of_ty : of_ty. + + Lemma of_value_with {T A : Set} `{Link T} `{Link A} + (buf' : Value.t) (buf : RawVec.t T A) + (len' : Value.t) (len : Usize.t) : + buf' = φ buf -> + len' = φ len -> + Value.StructRecord "alloc::vec::Vec" [] [Φ T; Φ A] [("buf", buf'); ("len", len')] = + φ ({| buf := buf; len := len |} : t T A). + Proof. + now intros; subst. + Qed. + Smpl Add unshelve eapply of_value_with : of_value. + + Definition of_value + (T' A' : Ty.t) + (H_T : OfTy.t T') + (H_A : OfTy.t A') + (buf' : Value.t) (buf : RawVec.t (OfTy.get_Set H_T) (OfTy.get_Set H_A)) + (len' : Value.t) (len : Usize.t) : + buf' = φ buf -> + len' = φ len -> + OfValue.t (Value.StructRecord "alloc::vec::Vec" [] [T'; A'] [ + ("buf", buf'); + ("len", len') + ]). + Proof. + intros. + destruct H_T as [T]. + destruct H_A as [A]. + eapply OfValue.Make with (value := Build_t T A buf len). + subst. + reflexivity. + Defined. + Smpl Add unshelve eapply of_value : of_value. End Vec. Module Impl_Clone_for_Vec. @@ -80,7 +123,14 @@ Module Impl_Vec_T. *) Instance run_new {T : Set} `{Link T} : Run.Trait (vec.Impl_alloc_vec_Vec_T_alloc_alloc_Global.new (Φ T)) [] [] [] (Self T). - Admitted. + Proof. + constructor. + run_symbolic. + 2: { + change (Ty.path "alloc::alloc::Global") with (Φ Global.t). + repeat smpl of_value. + } + Defined. (* pub fn with_capacity(capacity: usize) -> Self *) Instance run_with_capacity {T : Set} `{Link T} (capacity : Usize.t) : diff --git a/CoqOfRust/examples/axiomatized/examples/custom/loops.err b/CoqOfRust/examples/axiomatized/examples/custom/loops.err new file mode 100644 index 000000000..e69de29bb diff --git a/CoqOfRust/examples/axiomatized/examples/custom/loops.v b/CoqOfRust/examples/axiomatized/examples/custom/loops.v new file mode 100644 index 000000000..cad0f0c4f --- /dev/null +++ b/CoqOfRust/examples/axiomatized/examples/custom/loops.v @@ -0,0 +1,23 @@ +(* Generated by coq-of-rust *) +Require Import CoqOfRust.CoqOfRust. + +Parameter sum_checked : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_sum_checked : M.IsFunction.C "loops::sum_checked" sum_checked. +Admitted. + +Parameter reverse_in_place : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_reverse_in_place : + M.IsFunction.C "loops::reverse_in_place" reverse_in_place. +Admitted. + +Parameter is_sorted : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_is_sorted : M.IsFunction.C "loops::is_sorted" is_sorted. +Admitted. + +Parameter max_array : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_max_array : M.IsFunction.C "loops::max_array" max_array. +Admitted. diff --git a/CoqOfRust/examples/axiomatized/examples/custom/loops_free.err b/CoqOfRust/examples/axiomatized/examples/custom/loops_free.err new file mode 100644 index 000000000..e69de29bb diff --git a/CoqOfRust/examples/axiomatized/examples/custom/loops_free.v b/CoqOfRust/examples/axiomatized/examples/custom/loops_free.v new file mode 100644 index 000000000..edeb347fb --- /dev/null +++ b/CoqOfRust/examples/axiomatized/examples/custom/loops_free.v @@ -0,0 +1,38 @@ +(* Generated by coq-of-rust *) +Require Import CoqOfRust.CoqOfRust. + +Parameter max2 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_max2 : M.IsFunction.C "loops_free::max2" max2. +Admitted. + +Parameter abs_i32 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_abs_i32 : M.IsFunction.C "loops_free::abs_i32" abs_i32. +Admitted. + +Parameter bool_and : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_bool_and : M.IsFunction.C "loops_free::bool_and" bool_and. +Admitted. + +Parameter get_or_zero : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_get_or_zero : + M.IsFunction.C "loops_free::get_or_zero" get_or_zero. +Admitted. + +Parameter eq2 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_eq2 : M.IsFunction.C "loops_free::eq2" eq2. +Admitted. + +Parameter eq_pair : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_eq_pair : M.IsFunction.C "loops_free::eq_pair" eq_pair. +Admitted. + +Parameter min3 : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M. + +Global Instance Instance_IsFunction_min3 : M.IsFunction.C "loops_free::min3" min3. +Admitted. diff --git a/CoqOfRust/examples/default/examples/custom/loops.err b/CoqOfRust/examples/default/examples/custom/loops.err new file mode 100644 index 000000000..e69de29bb diff --git a/CoqOfRust/examples/default/examples/custom/loops.v b/CoqOfRust/examples/default/examples/custom/loops.v new file mode 100644 index 000000000..56fd7a5cd --- /dev/null +++ b/CoqOfRust/examples/default/examples/custom/loops.v @@ -0,0 +1,645 @@ +(* Generated by coq-of-rust *) +Require Import CoqOfRust.CoqOfRust. + +(* +pub fn sum_checked(xs: &[u32]) -> Option { + let mut acc: u32 = 0; + let mut i: usize = 0; + // Invariant idea (Coq): + // - 0 <= i <= xs.len() + // - acc = sum(xs[0..i]) and never overflowed + while i < xs.len() { + match acc.checked_add(xs[i]) { + Some(v) => acc = v, + None => return None, + } + i += 1; + } + Some(acc) +} +*) +Definition sum_checked (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ xs ] => + ltac:(M.monadic + (let xs := + M.alloc (| + Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u32" ] ], + xs + |) in + M.catch_return (Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ]) (| + ltac:(M.monadic + (M.read (| + let~ acc : Ty.path "u32" := Value.Integer IntegerKind.U32 0 in + let~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in + let~ _ : Ty.tuple [] := + M.read (| + M.loop (| + Ty.tuple [], + ltac:(M.monadic + (M.alloc (| + Ty.tuple [], + M.match_operator (| + Ty.tuple [], + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.lt, + [ + M.read (| i |); + M.call_closure (| + Ty.path "usize", + M.get_associated_function (| + Ty.apply (Ty.path "slice") [] [ Ty.path "u32" ], + "len", + [], + [] + |), + [ + M.borrow (| + Pointer.Kind.Ref, + M.deref (| M.read (| xs |) |) + |) + ] + |) + ] + |) + |)) in + let _ := + is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.read (| + let~ _ : Ty.tuple [] := + M.match_operator (| + Ty.tuple [], + M.alloc (| + Ty.apply + (Ty.path "core::option::Option") + [] + [ Ty.path "u32" ], + M.call_closure (| + Ty.apply + (Ty.path "core::option::Option") + [] + [ Ty.path "u32" ], + M.get_associated_function (| + Ty.path "u32", + "checked_add", + [], + [] + |), + [ + M.read (| acc |); + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| xs |) |), + M.read (| i |) + |) + |) + ] + |) + |), + [ + fun γ => + ltac:(M.monadic + (let γ0_0 := + M.SubPointer.get_struct_tuple_field (| + γ, + "core::option::Option::Some", + 0 + |) in + let v := M.copy (| Ty.path "u32", γ0_0 |) in + M.write (| acc, M.read (| v |) |))); + fun γ => + ltac:(M.monadic + (let _ := + M.is_struct_tuple (| + γ, + "core::option::Option::None" + |) in + M.never_to_any (| + M.read (| + M.return_ (| + Value.StructTuple + "core::option::Option::None" + [] + [ Ty.path "u32" ] + [] + |) + |) + |))) + ] + |) in + let~ _ : Ty.tuple [] := + let β := i in + M.write (| + β, + M.call_closure (| + Ty.path "usize", + BinOp.Wrap.add, + [ M.read (| β |); Value.Integer IntegerKind.Usize 1 ] + |) + |) in + M.alloc (| Ty.tuple [], Value.Tuple [] |) + |))); + fun γ => + ltac:(M.monadic + (M.never_to_any (| + M.read (| + let~ _ : Ty.tuple [] := + M.never_to_any (| M.read (| M.break (||) |) |) in + M.alloc (| Ty.tuple [], Value.Tuple [] |) + |) + |))) + ] + |) + |))) + |) + |) in + M.alloc (| + Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ], + Value.StructTuple + "core::option::Option::Some" + [] + [ Ty.path "u32" ] + [ M.read (| acc |) ] + |) + |))) + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_sum_checked : M.IsFunction.C "loops::sum_checked" sum_checked. +Admitted. +Global Typeclasses Opaque sum_checked. + +(* +pub fn reverse_in_place(xs: &mut [i32]) { + if xs.len() == 0 { return; } + let mut l: usize = 0; + let mut r: usize = xs.len() - 1; + // Invariant idea: + // - xs[0..l] and xs[r+1..] are already reversed wrt original + // - l <= r + 1 + while l < r { + let tmp = xs[l]; + xs[l] = xs[r]; + xs[r] = tmp; + l += 1; + r -= 1; + } +} +*) +Definition reverse_in_place (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ xs ] => + ltac:(M.monadic + (let xs := + M.alloc (| + Ty.apply (Ty.path "&mut") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "i32" ] ], + xs + |) in + M.catch_return (Ty.tuple []) (| + ltac:(M.monadic + (M.read (| + let~ _ : Ty.tuple [] := + M.match_operator (| + Ty.tuple [], + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.eq, + [ + M.call_closure (| + Ty.path "usize", + M.get_associated_function (| + Ty.apply (Ty.path "slice") [] [ Ty.path "i32" ], + "len", + [], + [] + |), + [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| xs |) |) |) ] + |); + Value.Integer IntegerKind.Usize 0 + ] + |) + |)) in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.never_to_any (| M.read (| M.return_ (| Value.Tuple [] |) |) |))); + fun γ => ltac:(M.monadic (Value.Tuple [])) + ] + |) in + let~ l : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in + let~ r : Ty.path "usize" := + M.call_closure (| + Ty.path "usize", + BinOp.Wrap.sub, + [ + M.call_closure (| + Ty.path "usize", + M.get_associated_function (| + Ty.apply (Ty.path "slice") [] [ Ty.path "i32" ], + "len", + [], + [] + |), + [ M.borrow (| Pointer.Kind.Ref, M.deref (| M.read (| xs |) |) |) ] + |); + Value.Integer IntegerKind.Usize 1 + ] + |) in + M.loop (| + Ty.tuple [], + ltac:(M.monadic + (M.alloc (| + Ty.tuple [], + M.match_operator (| + Ty.tuple [], + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.lt, + [ M.read (| l |); M.read (| r |) ] + |) + |)) in + let _ := + is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.read (| + let~ tmp : Ty.path "i32" := + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| xs |) |), + M.read (| l |) + |) + |) in + let~ _ : Ty.tuple [] := + M.write (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| xs |) |), + M.read (| l |) + |), + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| xs |) |), + M.read (| r |) + |) + |) + |) in + let~ _ : Ty.tuple [] := + M.write (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| xs |) |), + M.read (| r |) + |), + M.read (| tmp |) + |) in + let~ _ : Ty.tuple [] := + let β := l in + M.write (| + β, + M.call_closure (| + Ty.path "usize", + BinOp.Wrap.add, + [ M.read (| β |); Value.Integer IntegerKind.Usize 1 ] + |) + |) in + let~ _ : Ty.tuple [] := + let β := r in + M.write (| + β, + M.call_closure (| + Ty.path "usize", + BinOp.Wrap.sub, + [ M.read (| β |); Value.Integer IntegerKind.Usize 1 ] + |) + |) in + M.alloc (| Ty.tuple [], Value.Tuple [] |) + |))); + fun γ => + ltac:(M.monadic + (M.never_to_any (| + M.read (| + let~ _ : Ty.tuple [] := + M.never_to_any (| M.read (| M.break (||) |) |) in + M.alloc (| Ty.tuple [], Value.Tuple [] |) + |) + |))) + ] + |) + |))) + |) + |))) + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_reverse_in_place : + M.IsFunction.C "loops::reverse_in_place" reverse_in_place. +Admitted. +Global Typeclasses Opaque reverse_in_place. + +(* +pub fn is_sorted(xs: &[i32]) -> bool { + let mut i: usize = 1; + // Invariant idea: + // - prefix xs[0..i] is sorted (pairwise non-decreasing) + while i < xs.len() { + if xs[i - 1] > xs[i] { return false; } + i += 1; + } + true +} +*) +Definition is_sorted (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ xs ] => + ltac:(M.monadic + (let xs := + M.alloc (| + Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "i32" ] ], + xs + |) in + M.catch_return (Ty.path "bool") (| + ltac:(M.monadic + (M.read (| + let~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 1 in + let~ _ : Ty.tuple [] := + M.read (| + M.loop (| + Ty.tuple [], + ltac:(M.monadic + (M.alloc (| + Ty.tuple [], + M.match_operator (| + Ty.tuple [], + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.lt, + [ + M.read (| i |); + M.call_closure (| + Ty.path "usize", + M.get_associated_function (| + Ty.apply (Ty.path "slice") [] [ Ty.path "i32" ], + "len", + [], + [] + |), + [ + M.borrow (| + Pointer.Kind.Ref, + M.deref (| M.read (| xs |) |) + |) + ] + |) + ] + |) + |)) in + let _ := + is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.read (| + let~ _ : Ty.tuple [] := + M.match_operator (| + Ty.tuple [], + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.gt, + [ + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| xs |) |), + M.call_closure (| + Ty.path "usize", + BinOp.Wrap.sub, + [ + M.read (| i |); + Value.Integer IntegerKind.Usize 1 + ] + |) + |) + |); + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| xs |) |), + M.read (| i |) + |) + |) + ] + |) + |)) in + let _ := + is_constant_or_break_match (| + M.read (| γ |), + Value.Bool true + |) in + M.never_to_any (| + M.read (| M.return_ (| Value.Bool false |) |) + |))); + fun γ => ltac:(M.monadic (Value.Tuple [])) + ] + |) in + let~ _ : Ty.tuple [] := + let β := i in + M.write (| + β, + M.call_closure (| + Ty.path "usize", + BinOp.Wrap.add, + [ M.read (| β |); Value.Integer IntegerKind.Usize 1 ] + |) + |) in + M.alloc (| Ty.tuple [], Value.Tuple [] |) + |))); + fun γ => + ltac:(M.monadic + (M.never_to_any (| + M.read (| + let~ _ : Ty.tuple [] := + M.never_to_any (| M.read (| M.break (||) |) |) in + M.alloc (| Ty.tuple [], Value.Tuple [] |) + |) + |))) + ] + |) + |))) + |) + |) in + M.alloc (| Ty.path "bool", Value.Bool true |) + |))) + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_is_sorted : M.IsFunction.C "loops::is_sorted" is_sorted. +Admitted. +Global Typeclasses Opaque is_sorted. + +(* +pub fn max_array(a: &[i32; N]) -> i32 { + let mut m = a[0]; + let mut i: usize = 1; + // Invariant idea: + // - m = max(a[0..i]) + while i < N { + if a[i] > m { m = a[i]; } + i += 1; + } + m +} +*) +Definition max_array (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [ N ], [], [ a ] => + ltac:(M.monadic + (let a := + M.alloc (| + Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ Ty.path "i32" ] ], + a + |) in + M.read (| + let~ m : Ty.path "i32" := + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| a |) |), + Value.Integer IntegerKind.Usize 0 + |) + |) in + let~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 1 in + let~ _ : Ty.tuple [] := + M.read (| + M.loop (| + Ty.tuple [], + ltac:(M.monadic + (M.alloc (| + Ty.tuple [], + M.match_operator (| + Ty.tuple [], + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| Ty.path "bool", BinOp.lt, [ M.read (| i |); N ] |) + |)) in + let _ := + is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.read (| + let~ _ : Ty.tuple [] := + M.match_operator (| + Ty.tuple [], + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.gt, + [ + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| a |) |), + M.read (| i |) + |) + |); + M.read (| m |) + ] + |) + |)) in + let _ := + is_constant_or_break_match (| + M.read (| γ |), + Value.Bool true + |) in + M.read (| + let~ _ : Ty.tuple [] := + M.write (| + m, + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| a |) |), + M.read (| i |) + |) + |) + |) in + M.alloc (| Ty.tuple [], Value.Tuple [] |) + |))); + fun γ => ltac:(M.monadic (Value.Tuple [])) + ] + |) in + let~ _ : Ty.tuple [] := + let β := i in + M.write (| + β, + M.call_closure (| + Ty.path "usize", + BinOp.Wrap.add, + [ M.read (| β |); Value.Integer IntegerKind.Usize 1 ] + |) + |) in + M.alloc (| Ty.tuple [], Value.Tuple [] |) + |))); + fun γ => + ltac:(M.monadic + (M.never_to_any (| + M.read (| + let~ _ : Ty.tuple [] := + M.never_to_any (| M.read (| M.break (||) |) |) in + M.alloc (| Ty.tuple [], Value.Tuple [] |) + |) + |))) + ] + |) + |))) + |) + |) in + m + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_max_array : M.IsFunction.C "loops::max_array" max_array. +Admitted. +Global Typeclasses Opaque max_array. diff --git a/CoqOfRust/examples/default/examples/custom/loops_free.err b/CoqOfRust/examples/default/examples/custom/loops_free.err new file mode 100644 index 000000000..e69de29bb diff --git a/CoqOfRust/examples/default/examples/custom/loops_free.v b/CoqOfRust/examples/default/examples/custom/loops_free.v new file mode 100644 index 000000000..29853d8a9 --- /dev/null +++ b/CoqOfRust/examples/default/examples/custom/loops_free.v @@ -0,0 +1,385 @@ +(* Generated by coq-of-rust *) +Require Import CoqOfRust.CoqOfRust. + +(* +pub fn max2(a: u32, b: u32) -> u32 { + if a < b { b } else { a } +} +*) +Definition max2 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ a; b ] => + ltac:(M.monadic + (let a := M.alloc (| Ty.path "u32", a |) in + let b := M.alloc (| Ty.path "u32", b |) in + M.match_operator (| + Ty.path "u32", + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.lt, + [ M.read (| a |); M.read (| b |) ] + |) + |)) in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.read (| b |))); + fun γ => ltac:(M.monadic (M.read (| a |))) + ] + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_max2 : M.IsFunction.C "loops_free::max2" max2. +Admitted. +Global Typeclasses Opaque max2. + +(* +pub fn abs_i32(x: i32) -> i32 { + if x < 0 { -x } else { x } +} +*) +Definition abs_i32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ x ] => + ltac:(M.monadic + (let x := M.alloc (| Ty.path "i32", x |) in + M.match_operator (| + Ty.path "i32", + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.lt, + [ M.read (| x |); Value.Integer IntegerKind.I32 0 ] + |) + |)) in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + UnOp.neg (| M.read (| x |) |))); + fun γ => ltac:(M.monadic (M.read (| x |))) + ] + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_abs_i32 : M.IsFunction.C "loops_free::abs_i32" abs_i32. +Admitted. +Global Typeclasses Opaque abs_i32. + +(* +pub fn bool_and(a: bool, b: bool) -> bool { + if a { + if b { true } else { false } + } else { + false + } +} +*) +Definition bool_and (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ a; b ] => + ltac:(M.monadic + (let a := M.alloc (| Ty.path "bool", a |) in + let b := M.alloc (| Ty.path "bool", b |) in + M.match_operator (| + Ty.path "bool", + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := M.use a in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.match_operator (| + Ty.path "bool", + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := M.use b in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + Value.Bool true)); + fun γ => ltac:(M.monadic (Value.Bool false)) + ] + |))); + fun γ => ltac:(M.monadic (Value.Bool false)) + ] + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_bool_and : M.IsFunction.C "loops_free::bool_and" bool_and. +Admitted. +Global Typeclasses Opaque bool_and. + +(* +pub fn get_or_zero(xs: &[u32; 4], i: usize) -> u32 { + if i < 4 { xs[i] } else { 0 } +} +*) +Definition get_or_zero (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ xs; i ] => + ltac:(M.monadic + (let xs := + M.alloc (| + Ty.apply + (Ty.path "&") + [] + [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u32" ] ], + xs + |) in + let i := M.alloc (| Ty.path "usize", i |) in + M.match_operator (| + Ty.path "u32", + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.lt, + [ M.read (| i |); Value.Integer IntegerKind.Usize 4 ] + |) + |)) in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.read (| + M.SubPointer.get_array_field (| M.deref (| M.read (| xs |) |), M.read (| i |) |) + |))); + fun γ => ltac:(M.monadic (Value.Integer IntegerKind.U32 0)) + ] + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_get_or_zero : + M.IsFunction.C "loops_free::get_or_zero" get_or_zero. +Admitted. +Global Typeclasses Opaque get_or_zero. + +(* +pub fn eq2(a: &[u32; 2], b: &[u32; 2]) -> bool { + if a[0] == b[0] && a[1] == b[1] { + true + } else { + false + } +} +*) +Definition eq2 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ a; b ] => + ltac:(M.monadic + (let a := + M.alloc (| + Ty.apply + (Ty.path "&") + [] + [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u32" ] ], + a + |) in + let b := + M.alloc (| + Ty.apply + (Ty.path "&") + [] + [ Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 2 ] [ Ty.path "u32" ] ], + b + |) in + M.match_operator (| + Ty.path "bool", + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + LogicalOp.and (| + M.call_closure (| + Ty.path "bool", + BinOp.eq, + [ + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| a |) |), + Value.Integer IntegerKind.Usize 0 + |) + |); + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| b |) |), + Value.Integer IntegerKind.Usize 0 + |) + |) + ] + |), + ltac:(M.monadic + (M.call_closure (| + Ty.path "bool", + BinOp.eq, + [ + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| a |) |), + Value.Integer IntegerKind.Usize 1 + |) + |); + M.read (| + M.SubPointer.get_array_field (| + M.deref (| M.read (| b |) |), + Value.Integer IntegerKind.Usize 1 + |) + |) + ] + |))) + |) + |)) in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + Value.Bool true)); + fun γ => ltac:(M.monadic (Value.Bool false)) + ] + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_eq2 : M.IsFunction.C "loops_free::eq2" eq2. +Admitted. +Global Typeclasses Opaque eq2. + +(* +pub fn eq_pair(x: (u32, u32), y: (u32, u32)) -> bool { + if x.0 == y.0 && x.1 == y.1 { true } else { false } +} +*) +Definition eq_pair (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ x; y ] => + ltac:(M.monadic + (let x := M.alloc (| Ty.tuple [ Ty.path "u32"; Ty.path "u32" ], x |) in + let y := M.alloc (| Ty.tuple [ Ty.path "u32"; Ty.path "u32" ], y |) in + M.match_operator (| + Ty.path "bool", + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + LogicalOp.and (| + M.call_closure (| + Ty.path "bool", + BinOp.eq, + [ + M.read (| M.SubPointer.get_tuple_field (| x, 0 |) |); + M.read (| M.SubPointer.get_tuple_field (| y, 0 |) |) + ] + |), + ltac:(M.monadic + (M.call_closure (| + Ty.path "bool", + BinOp.eq, + [ + M.read (| M.SubPointer.get_tuple_field (| x, 1 |) |); + M.read (| M.SubPointer.get_tuple_field (| y, 1 |) |) + ] + |))) + |) + |)) in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + Value.Bool true)); + fun γ => ltac:(M.monadic (Value.Bool false)) + ] + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_eq_pair : M.IsFunction.C "loops_free::eq_pair" eq_pair. +Admitted. +Global Typeclasses Opaque eq_pair. + +(* +pub fn min3(a: u32, b: u32, c: u32) -> u32 { + let m = if a < b { a } else { b }; + if m < c { m } else { c } +} +*) +Definition min3 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M := + match ε, τ, α with + | [], [], [ a; b; c ] => + ltac:(M.monadic + (let a := M.alloc (| Ty.path "u32", a |) in + let b := M.alloc (| Ty.path "u32", b |) in + let c := M.alloc (| Ty.path "u32", c |) in + M.read (| + let~ m : Ty.path "u32" := + M.match_operator (| + Ty.path "u32", + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.lt, + [ M.read (| a |); M.read (| b |) ] + |) + |)) in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.read (| a |))); + fun γ => ltac:(M.monadic (M.read (| b |))) + ] + |) in + M.alloc (| + Ty.path "u32", + M.match_operator (| + Ty.path "u32", + M.alloc (| Ty.tuple [], Value.Tuple [] |), + [ + fun γ => + ltac:(M.monadic + (let γ := + M.use + (M.alloc (| + Ty.path "bool", + M.call_closure (| + Ty.path "bool", + BinOp.lt, + [ M.read (| m |); M.read (| c |) ] + |) + |)) in + let _ := is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in + M.read (| m |))); + fun γ => ltac:(M.monadic (M.read (| c |))) + ] + |) + |) + |))) + | _, _, _ => M.impossible "wrong number of arguments" + end. + +Global Instance Instance_IsFunction_min3 : M.IsFunction.C "loops_free::min3" min3. +Admitted. +Global Typeclasses Opaque min3. diff --git a/CoqOfRust/revm/revm_bytecode/links/eof.v b/CoqOfRust/revm/revm_bytecode/links/eof.v index e479a6f31..40bb34f7e 100644 --- a/CoqOfRust/revm/revm_bytecode/links/eof.v +++ b/CoqOfRust/revm/revm_bytecode/links/eof.v @@ -162,6 +162,9 @@ Module Impl_Eof. (* pub fn decode(raw: Bytes) -> Result *) Instance run_decode (raw : Bytes.t) : Run.Trait eof.Impl_revm_bytecode_eof_Eof.decode [] [] [φ raw] (Result.t Self EofDecodeError.t). + Proof. + constructor. + run_symbolic. Admitted. End Impl_Eof. Export Impl_Eof.