Skip to content

Handle constants like functions #709

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Mar 31, 2025
Merged

Handle constants like functions #709

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
82 changes: 20 additions & 62 deletions CoqOfRust/M.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ Module Pointer.
Module Kind.
Inductive t : Set :=
(** The address kind for the allocation primitive. This is later converted to proper pointer
kinds. *)
kinds. This is not a native Rust kind of pointer. *)
| Raw
| Ref
| MutRef
Expand All @@ -149,7 +149,7 @@ Module Pointer.

Definition to_ty_path (kind : t) : string :=
match kind with
| Raw => "raw" (* it should appear as it is not possible to manipulate raw pointers in Rust *)
| Raw => "*"
| Ref => "&"
| MutRef => "&mut"
| ConstPointer => "*const"
Expand Down Expand Up @@ -275,12 +275,22 @@ End Value.

Module Primitive.
Inductive t : Set :=
| StateAlloc (value : Value.t)
| StateRead (pointer : Value.t)
| StateWrite (pointer : Value.t) (value : Value.t)
| GetSubPointer (pointer : Value.t) (index : Pointer.Index.t)
| AreEqual (value1 value2 : Value.t)
| GetFunction (path : string) (generic_consts : list Value.t) (generic_tys : list Ty.t)
| StateAlloc
(value : Value.t)
| StateRead
(pointer : Value.t)
| StateWrite
(pointer : Value.t)
(value : Value.t)
| GetSubPointer
(pointer : Value.t)
(index : Pointer.Index.t)
| AreEqual
(value1 value2 : Value.t)
| GetFunction
(path : string)
(generic_consts : list Value.t)
(generic_tys : list Ty.t)
| GetAssociatedFunction
(ty : Ty.t)
(name : string)
Expand Down Expand Up @@ -376,7 +386,6 @@ End PolymorphicFunction.

Module InstanceField.
Inductive t : Set :=
| Constant (constant : Value.t)
| Method (method : PolymorphicFunction.t)
| Ty (ty : Ty.t).
End InstanceField.
Expand All @@ -400,7 +409,7 @@ Module IsFunction.
(function : PolymorphicFunction.t),
Prop.

Class Trait
Class C
(trait_name : string)
(function : PolymorphicFunction.t) :
Prop := {
Expand All @@ -415,7 +424,7 @@ Module IsAssociatedFunction.
(function : PolymorphicFunction.t),
Prop.

Class Trait
Class C
(Self : Ty.t)
(function_name : string)
(function : PolymorphicFunction.t) :
Expand All @@ -424,22 +433,6 @@ Module IsAssociatedFunction.
}.
End IsAssociatedFunction.

Module IsAssociatedConstant.
Parameter t : forall
(Self : Ty.t)
(constant_name : string)
(constant : Value.t),
Prop.

Class Trait
(Self : Ty.t)
(constant_name : string)
(constant : Value.t) :
Prop := {
is_associated_constant : t Self constant_name constant;
}.
End IsAssociatedConstant.

Parameter IsProvidedMethod :
forall
(trait_name : string)
Expand Down Expand Up @@ -664,8 +657,6 @@ Definition get_sub_pointer (pointer : Value.t) (index : Pointer.Index.t) : M :=
Definition are_equal (value1 value2 : Value.t) : M :=
call_primitive (Primitive.AreEqual value1 value2).

Parameter get_constant : string -> Value.t.

Definition get_function (path : string) (generic_consts : list Value.t) (generic_tys : list Ty.t) :
M :=
call_primitive (Primitive.GetFunction path generic_consts generic_tys).
Expand Down Expand Up @@ -896,36 +887,3 @@ Parameter struct_record_update : Value.t -> list (string * Value.t) -> Value.t.
Parameter unevaluated_const : Value.t -> Value.t.

Parameter yield : Value.t -> M.

Fixpoint run_constant (constant : M) : Value.t :=
match constant with
| LowM.Pure value =>
match value with
| inl value => value
| inr _ => Value.Error "expected a success value"
end
| LowM.CallPrimitive primitive k =>
let value :=
match primitive with
| Primitive.StateAlloc value =>
Value.Pointer {|
Pointer.kind := Pointer.Kind.Raw;
Pointer.core := Pointer.Core.Immediate value;
|}
| Primitive.StateRead pointer =>
match pointer with
| Value.Pointer {|
Pointer.kind := Pointer.Kind.Raw;
Pointer.core := Pointer.Core.Immediate value;
|} =>
value
| _ => Value.Error "expected an immediate raw pointer"
end
| _ => Value.Error "unhandled primitive"
end in
run_constant (k value)
| LowM.CallClosure _ _ _ _ => Value.Error "unexpected closure call"
| LowM.Let _ _ _ => Value.Error "unexpected let"
| LowM.Loop _ _ _ => Value.Error "unexpected loop"
| LowM.Impossible _ => Value.Error "impossible"
end.
67 changes: 38 additions & 29 deletions CoqOfRust/alloc/alloc.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,33 +5,34 @@ Module alloc.
Parameter __rust_alloc : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Global Instance Instance_IsFunction___rust_alloc :
M.IsFunction.Trait "alloc::alloc::__rust_alloc" __rust_alloc.
M.IsFunction.C "alloc::alloc::__rust_alloc" __rust_alloc.
Admitted.

Parameter __rust_dealloc : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Global Instance Instance_IsFunction___rust_dealloc :
M.IsFunction.Trait "alloc::alloc::__rust_dealloc" __rust_dealloc.
M.IsFunction.C "alloc::alloc::__rust_dealloc" __rust_dealloc.
Admitted.

Parameter __rust_realloc : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Global Instance Instance_IsFunction___rust_realloc :
M.IsFunction.Trait "alloc::alloc::__rust_realloc" __rust_realloc.
M.IsFunction.C "alloc::alloc::__rust_realloc" __rust_realloc.
Admitted.

Parameter __rust_alloc_zeroed : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Global Instance Instance_IsFunction___rust_alloc_zeroed :
M.IsFunction.Trait "alloc::alloc::__rust_alloc_zeroed" __rust_alloc_zeroed.
M.IsFunction.C "alloc::alloc::__rust_alloc_zeroed" __rust_alloc_zeroed.
Admitted.

Parameter __rust_no_alloc_shim_is_unstable : Value.t.
Parameter __rust_no_alloc_shim_is_unstable : PolymorphicFunction.t.

Axiom Constant___rust_no_alloc_shim_is_unstable :
(M.get_constant "alloc::alloc::__rust_no_alloc_shim_is_unstable") =
Global Instance Instance_IsConstant___rust_no_alloc_shim_is_unstable :
M.IsFunction.C
"alloc::alloc::__rust_no_alloc_shim_is_unstable"
__rust_no_alloc_shim_is_unstable.
Global Hint Rewrite Constant___rust_no_alloc_shim_is_unstable : constant_rewrites.
Admitted.

(* StructTuple
{
Expand Down Expand Up @@ -157,7 +158,10 @@ Module alloc.
Pointer.Kind.Ref,
M.deref (|
M.read (|
M.get_constant "alloc::alloc::__rust_no_alloc_shim_is_unstable"
get_constant (|
"alloc::alloc::__rust_no_alloc_shim_is_unstable",
Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ]
|)
|)
|)
|)
Expand Down Expand Up @@ -198,7 +202,7 @@ Module alloc.
| _, _, _ => M.impossible "wrong number of arguments"
end.

Global Instance Instance_IsFunction_alloc : M.IsFunction.Trait "alloc::alloc::alloc" alloc.
Global Instance Instance_IsFunction_alloc : M.IsFunction.C "alloc::alloc::alloc" alloc.
Admitted.
Global Typeclasses Opaque alloc.

Expand Down Expand Up @@ -238,7 +242,7 @@ Module alloc.
| _, _, _ => M.impossible "wrong number of arguments"
end.

Global Instance Instance_IsFunction_dealloc : M.IsFunction.Trait "alloc::alloc::dealloc" dealloc.
Global Instance Instance_IsFunction_dealloc : M.IsFunction.C "alloc::alloc::dealloc" dealloc.
Admitted.
Global Typeclasses Opaque dealloc.

Expand Down Expand Up @@ -280,7 +284,7 @@ Module alloc.
| _, _, _ => M.impossible "wrong number of arguments"
end.

Global Instance Instance_IsFunction_realloc : M.IsFunction.Trait "alloc::alloc::realloc" realloc.
Global Instance Instance_IsFunction_realloc : M.IsFunction.C "alloc::alloc::realloc" realloc.
Admitted.
Global Typeclasses Opaque realloc.

Expand Down Expand Up @@ -314,7 +318,10 @@ Module alloc.
Pointer.Kind.Ref,
M.deref (|
M.read (|
M.get_constant "alloc::alloc::__rust_no_alloc_shim_is_unstable"
get_constant (|
"alloc::alloc::__rust_no_alloc_shim_is_unstable",
Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ]
|)
|)
|)
|)
Expand Down Expand Up @@ -356,7 +363,7 @@ Module alloc.
end.

Global Instance Instance_IsFunction_alloc_zeroed :
M.IsFunction.Trait "alloc::alloc::alloc_zeroed" alloc_zeroed.
M.IsFunction.C "alloc::alloc::alloc_zeroed" alloc_zeroed.
Admitted.
Global Typeclasses Opaque alloc_zeroed.

Expand Down Expand Up @@ -696,7 +703,7 @@ Module alloc.
end.

Global Instance AssociatedFunction_alloc_impl :
M.IsAssociatedFunction.Trait Self "alloc_impl" alloc_impl.
M.IsAssociatedFunction.C Self "alloc_impl" alloc_impl.
Admitted.
Global Typeclasses Opaque alloc_impl.

Expand Down Expand Up @@ -1471,7 +1478,7 @@ Module alloc.
end.

Global Instance AssociatedFunction_grow_impl :
M.IsAssociatedFunction.Trait Self "grow_impl" grow_impl.
M.IsAssociatedFunction.C Self "grow_impl" grow_impl.
Admitted.
Global Typeclasses Opaque grow_impl.
End Impl_alloc_alloc_Global.
Expand Down Expand Up @@ -2554,14 +2561,14 @@ Module alloc.
end.

Global Instance Instance_IsFunction_exchange_malloc :
M.IsFunction.Trait "alloc::alloc::exchange_malloc" exchange_malloc.
M.IsFunction.C "alloc::alloc::exchange_malloc" exchange_malloc.
Admitted.
Global Typeclasses Opaque exchange_malloc.

Parameter __rust_alloc_error_handler : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Global Instance Instance_IsFunction___rust_alloc_error_handler :
M.IsFunction.Trait "alloc::alloc::__rust_alloc_error_handler" __rust_alloc_error_handler.
M.IsFunction.C "alloc::alloc::__rust_alloc_error_handler" __rust_alloc_error_handler.
Admitted.

(*
Expand Down Expand Up @@ -2613,7 +2620,7 @@ Module alloc.
end.

Global Instance Instance_IsFunction_handle_alloc_error :
M.IsFunction.Trait "alloc::alloc::handle_alloc_error" handle_alloc_error.
M.IsFunction.C "alloc::alloc::handle_alloc_error" handle_alloc_error.
Admitted.
Global Typeclasses Opaque handle_alloc_error.

Expand Down Expand Up @@ -2666,7 +2673,7 @@ Module alloc.
end.

Global Instance Instance_IsFunction_ct_error :
M.IsFunction.Trait "alloc::alloc::handle_alloc_error::ct_error" ct_error.
M.IsFunction.C "alloc::alloc::handle_alloc_error::ct_error" ct_error.
Admitted.
Global Typeclasses Opaque ct_error.

Expand Down Expand Up @@ -2712,7 +2719,7 @@ Module alloc.
end.

Global Instance Instance_IsFunction_rt_error :
M.IsFunction.Trait "alloc::alloc::handle_alloc_error::rt_error" rt_error.
M.IsFunction.C "alloc::alloc::handle_alloc_error::rt_error" rt_error.
Admitted.
Global Typeclasses Opaque rt_error.
End handle_alloc_error.
Expand Down Expand Up @@ -2756,8 +2763,10 @@ Module alloc.
M.read (|
M.deref (|
M.read (|
M.get_constant
"alloc::alloc::__alloc_error_handler::__rdl_oom::__rust_alloc_error_handler_should_panic"
get_constant (|
"alloc::alloc::__alloc_error_handler::__rdl_oom::__rust_alloc_error_handler_should_panic",
Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ]
|)
|)
|)
|),
Expand Down Expand Up @@ -2901,18 +2910,18 @@ Module alloc.
end.

Global Instance Instance_IsFunction___rdl_oom :
M.IsFunction.Trait "alloc::alloc::__alloc_error_handler::__rdl_oom" __rdl_oom.
M.IsFunction.C "alloc::alloc::__alloc_error_handler::__rdl_oom" __rdl_oom.
Admitted.
Global Typeclasses Opaque __rdl_oom.

Module __rdl_oom.
Parameter __rust_alloc_error_handler_should_panic : Value.t.
Parameter __rust_alloc_error_handler_should_panic : PolymorphicFunction.t.

Axiom Constant___rust_alloc_error_handler_should_panic :
(M.get_constant
"alloc::alloc::__alloc_error_handler::__rdl_oom::__rust_alloc_error_handler_should_panic") =
Global Instance Instance_IsConstant___rust_alloc_error_handler_should_panic :
M.IsFunction.C
"alloc::alloc::__alloc_error_handler::__rdl_oom::__rust_alloc_error_handler_should_panic"
__rust_alloc_error_handler_should_panic.
Global Hint Rewrite Constant___rust_alloc_error_handler_should_panic : constant_rewrites.
Admitted.
End __rdl_oom.
End __alloc_error_handler.
End alloc.
8 changes: 4 additions & 4 deletions CoqOfRust/alloc/borrow.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -433,7 +433,7 @@ Module borrow.

Global Instance AssociatedFunction_is_borrowed :
forall (B : Ty.t),
M.IsAssociatedFunction.Trait (Self B) "is_borrowed" (is_borrowed B).
M.IsAssociatedFunction.C (Self B) "is_borrowed" (is_borrowed B).
Admitted.
Global Typeclasses Opaque is_borrowed.

Expand Down Expand Up @@ -465,7 +465,7 @@ Module borrow.

Global Instance AssociatedFunction_is_owned :
forall (B : Ty.t),
M.IsAssociatedFunction.Trait (Self B) "is_owned" (is_owned B).
M.IsAssociatedFunction.C (Self B) "is_owned" (is_owned B).
Admitted.
Global Typeclasses Opaque is_owned.

Expand Down Expand Up @@ -644,7 +644,7 @@ Module borrow.

Global Instance AssociatedFunction_to_mut :
forall (B : Ty.t),
M.IsAssociatedFunction.Trait (Self B) "to_mut" (to_mut B).
M.IsAssociatedFunction.C (Self B) "to_mut" (to_mut B).
Admitted.
Global Typeclasses Opaque to_mut.

Expand Down Expand Up @@ -705,7 +705,7 @@ Module borrow.

Global Instance AssociatedFunction_into_owned :
forall (B : Ty.t),
M.IsAssociatedFunction.Trait (Self B) "into_owned" (into_owned B).
M.IsAssociatedFunction.C (Self B) "into_owned" (into_owned B).
Admitted.
Global Typeclasses Opaque into_owned.
End Impl_alloc_borrow_Cow_B.
Expand Down
Loading
Loading