Merge pull request #232 from formal-land/guillaume-claret@translate-axiom-mode-public

Translate axiom mode as public

Author: clarus

.github/workflows/rust.yml

@@ -33,7 +33,7 @@ jobs:
         python run_tests.py --output-path ./coq_translation/default/
     - name: Translate Rust examples (axiomatized)
       run: |
-        python run_tests.py --axiomatize --output-path ./coq_translation/axiomatized/
+        python run_tests.py --axiomatize --axiomatize-public --output-path ./coq_translation/axiomatized/
     - name: Translate Ink! library
       run: |
         cd CoqOfRust

CoqOfRust/CoqOfRust.v

@@ -196,6 +196,7 @@ Require CoqOfRust.core.hash.
 Require CoqOfRust.core.iter.
 Require CoqOfRust.core.marker.
 Require CoqOfRust.core.mem.
+Require CoqOfRust.core.num.
 Require CoqOfRust.core.option.
 Require CoqOfRust.core.primitive.
 Require CoqOfRust.core.result.
@@ -216,6 +217,7 @@ Module core.
   Export CoqOfRust.core.iter.
   Export CoqOfRust.core.marker.
   Export CoqOfRust.core.mem.
+  Export CoqOfRust.core.num.
   Export CoqOfRust.core.option.
   Export CoqOfRust.core.primitive.
   Export CoqOfRust.core.result.
@@ -815,7 +817,6 @@ Require CoqOfRust._std.io.
 (* Require CoqOfRust._std.iter. *)
 (* Require Import CoqOfRust._std.iter_type. *)
 (* Require Import CoqOfRust._std.net. *)
-Require Import CoqOfRust._std.num.
 Require Import CoqOfRust._std.ops.
 (* Require Import CoqOfRust._std.os. *)
 Require Import CoqOfRust._std.panic.
@@ -854,7 +855,6 @@ Module std.
   Module io := _std.io.
   (* Module iter := _std.iter. *)
   (* Module net := _std.net. *)
-  Module num := _std.num.
   Module ops := _std.ops.
   (* Module os := _std.os. *)
   Module panic := _std.panic.

CoqOfRust/blacklist.txt

@@ -143,74 +143,30 @@ examples/unsafe_operations/inline_assembly_symbol_operands_and_abi_clobbers.v
 examples/unsafe_operations/inline_assembly.v
 examples/unsafe_operations/raw_pointers.v
 examples/variable_bindings/declare_first.v
-examples_axiomatized/conversion/from.v
-examples_axiomatized/conversion/into.v
-examples_axiomatized/conversion/try_from_and_try_into.v
-examples_axiomatized/conversion/try_from_and_try_into.v
 examples_axiomatized/custom_types/enums_testcase_linked_list.v
-examples_axiomatized/custom_types/structures.v
 examples_axiomatized/error_handling/boxing_errors.v
-examples_axiomatized/error_handling/early_returns.v
-examples_axiomatized/error_handling/introducing_question_mark_is_an_replacement_for_deprecated_try.v
-examples_axiomatized/error_handling/introducing_question_mark.v
-examples_axiomatized/error_handling/map_in_result_via_combinators.v
-examples_axiomatized/error_handling/map_in_result_via_match.v
-examples_axiomatized/error_handling/multiple_error_types.v
 examples_axiomatized/error_handling/other_uses_of_question_mark.v
-examples_axiomatized/error_handling/pulling_results_out_of_options_with_stop_error_processing.v
-examples_axiomatized/error_handling/pulling_results_out_of_options.v
-examples_axiomatized/error_handling/result_use_in_main.v
 examples_axiomatized/error_handling/unpacking_options_via_question_mark.v
 examples_axiomatized/error_handling/wrapping_errors.v
 examples_axiomatized/functions/functions_closures_as_input_parameters.v
 examples_axiomatized/functions/functions_closures_as_output_parameters.v
 examples_axiomatized/functions/functions_closures_input_functions.v
 examples_axiomatized/functions/functions_closures_type_anonymity_define_and_use.v
-examples_axiomatized/functions/functions_closures_type_anonymity_define.v
-examples_axiomatized/generics/generics_associated_types_problem.v
-examples_axiomatized/generics/generics_associated_types_problem.v
-examples_axiomatized/generics/generics_associated_types_solution.v
-examples_axiomatized/generics/generics_associated_types_solution.v
-examples_axiomatized/generics/generics_bounds_test_case_empty_bounds.v
 examples_axiomatized/generics/generics_bounds.v
-examples_axiomatized/generics/generics_functions.v
-examples_axiomatized/generics/generics_functions.v
 examples_axiomatized/generics/generics_implementation.v
-examples_axiomatized/generics/generics_multiple_bounds.v
-examples_axiomatized/generics/generics_phantom_type_test_case_unit_clarification.v
-examples_axiomatized/generics/generics_phantom_type.v
-examples_axiomatized/generics/generics.v
-examples_axiomatized/generics/generics.v
 examples_axiomatized/modules/struct_visibility.v
-examples_axiomatized/modules/super_and_self.v
-examples_axiomatized/modules/the_use_as_declaration.v
 examples_axiomatized/modules/visibility.v
-examples_axiomatized/primitives/arrays_and_slices.v
-examples_axiomatized/scoping_rules/scoping_rules_borrowing_mutablity.v
-examples_axiomatized/scoping_rules/scoping_rules_borrowing_the_ref_pattern.v
-examples_axiomatized/scoping_rules/scoping_rules_lifetimes_bounds.v
-examples_axiomatized/scoping_rules/scoping_rules_lifetimes_structs.v
-examples_axiomatized/scoping_rules/scoping_rules_lifetimes_traits.v
 examples_axiomatized/scoping_rules/scoping_rules_ownership_and_rules_partial_moves.v
 examples_axiomatized/scoping_rules/scoping_rules_raii_desctructor.v
-examples_axiomatized/std_library_types/box_stack_heap.v
-examples_axiomatized/std_library_types/hash_map_alternate_or_custom_key_types.v
 examples_axiomatized/std_misc/file_io_read_lines_efficient_method.v
 examples_axiomatized/std_misc/file_io_read_lines.v
 examples_axiomatized/std_misc/filesystem_operations.v
 examples_axiomatized/std_misc/foreign_function_interface.v
 examples_axiomatized/subtle.v
-examples_axiomatized/subtle.v
-examples_axiomatized/traits/clone.v
-examples_axiomatized/traits/derive.v
-examples_axiomatized/traits/derive.v
 examples_axiomatized/traits/drop.v
-examples_axiomatized/traits/hash.v
 examples_axiomatized/traits/impl_trait_as_return_type.v
 examples_axiomatized/traits/iterators.v
 examples_axiomatized/traits/returning_traits_with_dyn.v
-examples_axiomatized/traits/returning_traits_with_dyn.v
-examples_axiomatized/traits/returning_traits_with_dyn.v
 examples_axiomatized/traits/supertraits.v
 ink/erc20.v
 _std/iter_type.v

CoqOfRust/_std/num.v renamed to CoqOfRust/core/num.v

@@ -99,23 +99,25 @@ Module NonZeroUsize.
 End NonZeroUsize.
 Definition NonZeroUsize := NonZeroUsize.t.
 
-(* pub struct ParseFloatError { /* private fields */ } *)
-Module ParseFloatError.
-  Parameter t : Set.
-End ParseFloatError.
-Definition ParseFloatError := ParseFloatError.t.
-
-(* pub struct ParseIntError { /* private fields */ } *)
-Module ParseIntError.
-  Parameter t : Set.
-End ParseIntError.
-Definition ParseIntError := ParseIntError.t.
-
-(* pub struct TryFromIntError(_); *)
-Module TryFromIntError.
-  Parameter t : Set.
-End TryFromIntError.
-Definition TryFromIntError := TryFromIntError.t.
+Module error.
+  (* pub struct ParseFloatError { /* private fields */ } *)
+  Module ParseFloatError.
+    Parameter t : Set.
+  End ParseFloatError.
+  Definition ParseFloatError := ParseFloatError.t.
+
+  (* pub struct ParseIntError { /* private fields */ } *)
+  Module ParseIntError.
+    Parameter t : Set.
+  End ParseIntError.
+  Definition ParseIntError := ParseIntError.t.
+
+  (* pub struct TryFromIntError(_); *)
+  Module TryFromIntError.
+    Parameter t : Set.
+  End TryFromIntError.
+  Definition TryFromIntError := TryFromIntError.t.
+End error.
 
 (* pub struct Wrapping<T>(pub T); *)
 Module Wrapping.

cli/src/main.rs

@@ -13,6 +13,9 @@ struct Translate {
     /// Axiomatize the definitions
     #[arg(long, value_name = "axiomatize", default_value_t = false)]
     axiomatize: bool,
+    /// Axiomatize the definitions with everything as public
+    #[arg(long, value_name = "axiomatize_public", default_value_t = false)]
+    axiomatize_public: bool,
     /// Generate the "reorder" section of the configuration file
     #[arg(long, value_name = "generate_reorder", default_value_t = false)]
     generate_reorder: bool,
@@ -61,6 +64,7 @@ fn main() {
                 path: t.path,
                 output: t.output_path,
                 axiomatize: t.axiomatize,
+                axiomatize_public: t.axiomatize_public,
                 generate_reorder: t.generate_reorder,
                 configuration_file: t.configuration_file,
             });

coq-of-rust-config.json

@@ -2,17 +2,6 @@
   "axiomatize": false,
   "debug_reorder": false,
   "impl_ignore_axioms": [
-    "examples/conversion/converting_to_string.rs",
-    "examples/error_handling/combinators_and_then.rs",
-    "examples/error_handling/combinators_map.rs",
-    "examples/error_handling/defining_an_error_type.rs",
-    "examples/error_handling/unpacking_options_and_defaults_via_get_or_insert.rs",
-    "examples/error_handling/unpacking_options_and_defaults_via_get_or_insert_with.rs",
-    "examples/error_handling/unpacking_options_and_defaults_via_or_else.rs",
-    "examples/error_handling/unpacking_options_and_defaults_via_or.rs",
-    "examples/primitives/tuples.rs",
-    "examples/std_library_types/result_chaining_with_question_mark.rs",
-    "examples/traits/operator_overloading.rs",
     "ink",
     "ink_env",
     "ink_storage"

coq_translation/axiomatized/examples/attributes/dead_code.v

@@ -1,4 +1,12 @@
 (* Generated by coq-of-rust *)
 Require Import CoqOfRust.CoqOfRust.
 
+Parameter used_function : forall `{H' : State.Trait}, M (H := H') unit.
 
+(* #[allow(dead_code)] - function was ignored by the compiler *)
+Parameter unused_function : forall `{H' : State.Trait}, M (H := H') unit.
+
+Parameter noisy_unused_function : forall `{H' : State.Trait}, M (H := H') unit.
+
+(* #[allow(dead_code)] - function was ignored by the compiler *)
+Parameter main : forall `{H' : State.Trait}, M (H := H') unit.

coq_translation/axiomatized/examples/cargo/concurrent_tests.v

@@ -1,4 +1,16 @@
 (* Generated by coq-of-rust *)
 Require Import CoqOfRust.CoqOfRust.
 
+Parameter foo :
+    forall `{H' : State.Trait} {A : Set},
+    (core.option.Option A) -> M (H := H') unit.
 
+Module tests.
+  Parameter test_file : forall `{H' : State.Trait}, M (H := H') unit.
+  
+  Parameter test_file_also : forall `{H' : State.Trait}, M (H := H') unit.
+End tests.
+
+Parameter test_file : forall `{H' : State.Trait}, M (H := H') unit.
+
+Parameter test_file_also : forall `{H' : State.Trait}, M (H := H') unit.

coq_translation/axiomatized/examples/conversion/converting_to_string.v

@@ -1,4 +1,38 @@
 (* Generated by coq-of-rust *)
 Require Import CoqOfRust.CoqOfRust.
 
+Module Circle.
+  Unset Primitive Projections.
+  Record t : Set := {
+    radius : i32;
+  }.
+  Global Set Primitive Projections.
+  
+  Global Instance Get_radius : Notation.Dot "radius" := {
+    Notation.dot '(Build_t x0) := x0;
+  }.
+  Global Instance Get_AF_radius : Notation.DoubleColon t "radius" := {
+    Notation.double_colon '(Build_t x0) := x0;
+  }.
+End Circle.
+Definition Circle : Set := Circle.t.
 
+Module Impl_core_fmt_Display_for_converting_to_string_Circle.
+  Definition Self := converting_to_string.Circle.
+  
+  Parameter fmt :
+      forall `{H' : State.Trait},
+      (ref Self) -> (mut_ref core.fmt.Formatter) -> M (H := H') core.fmt.Result.
+  
+  Global Instance Method_fmt `{H' : State.Trait} : Notation.Dot "fmt" := {
+    Notation.dot := fmt;
+  }.
+  
+  Global Instance I : core.fmt.Display.Trait Self := {
+    core.fmt.Display.fmt `{H' : State.Trait} := fmt;
+  }.
+  Global Hint Resolve I : core.
+End Impl_core_fmt_Display_for_converting_to_string_Circle.
+
+(* #[allow(dead_code)] - function was ignored by the compiler *)
+Parameter main : forall `{H' : State.Trait}, M (H := H') unit.

coq_translation/axiomatized/examples/conversion/from.v

@@ -1,6 +1,22 @@
 (* Generated by coq-of-rust *)
 Require Import CoqOfRust.CoqOfRust.
 
+Module Number.
+  Unset Primitive Projections.
+  Record t : Set := {
+    value : i32;
+  }.
+  Global Set Primitive Projections.
+  
+  Global Instance Get_value : Notation.Dot "value" := {
+    Notation.dot '(Build_t x0) := x0;
+  }.
+  Global Instance Get_AF_value : Notation.DoubleColon t "value" := {
+    Notation.double_colon '(Build_t x0) := x0;
+  }.
+End Number.
+Definition Number : Set := Number.t.
+
 Module Impl_core_convert_From_for_from_Number.
   Definition Self := from.Number.
 
@@ -16,3 +32,6 @@ Module Impl_core_convert_From_for_from_Number.
   }.
   Global Hint Resolve I : core.
 End Impl_core_convert_From_for_from_Number.
+
+(* #[allow(dead_code)] - function was ignored by the compiler *)
+Parameter main : forall `{H' : State.Trait}, M (H := H') unit.