Skip to content

Commit 95b5d10

Browse files
romefellerromefeller
authored
Merge pull request #762 from formal-land/alexandre-oliveira@p-token-part3
Alexandre oliveira@p token part3
2 parents 082c124 + 4dd7825 commit 95b5d10

File tree

15 files changed

+2210
-2
lines changed

15 files changed

+2210
-2
lines changed

‎CoqOfRust/core/links/marker.v‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,4 +36,13 @@ End PointeeSized.
3636
Module PhantomData.
3737
Inductive t (T : Set) `{PointeeSized.Run T} : Set :=
3838
| Make.
39+
40+
Global Instance IsLink (T : Set) `{Link T} `{PointeeSized.Run T} : Link (t T) :=
41+
{ Φ := Ty.apply (Ty.path "core::marker::PhantomData") [] [Φ T];
42+
φ _ := Value.StructTuple "core::marker::PhantomData" [] [Φ T] []
43+
}.
44+
45+
Global Instance PointeeSized_Run_Ref {K A} `{Link A} `{PointeeSized.Run A}
46+
: PointeeSized.Run (Ref.t K A) :=
47+
{ dummy_empty_class := tt }.
3948
End PhantomData.

‎CoqOfRust/links/M.v‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -380,6 +380,17 @@ Module Str.
380380
Smpl Add apply of_value : of_value.
381381
End Str.
382382

383+
Module F64.
384+
Parameter t : Set.
385+
386+
Parameter to_value : t -> Value.t.
387+
388+
Global Instance IsLink : Link t := {
389+
Φ := Ty.path "f64";
390+
φ x := to_value x
391+
}.
392+
End F64.
393+
383394
(** A general type for references. Can be used for mutable or non-mutable references, as well as
384395
for unsafe pointers (we assume that the `unsafe` code is safe). *)
385396
Module Ref.

‎CoqOfRust/pinocchio/entrypoint/links/lazy.v‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
Require Import CoqOfRust.CoqOfRust.
2+
Require Import CoqOfRust.links.M.
3+
Require Import pinocchio.links.account_info.
4+
Require Import pinocchio.links.pubkey.
5+
Require Import pinocchio.links.lib.
6+
Require Import pinocchio.entrypoint.lazy.
7+
Require Import core.links.result.
8+
Require Import pinocchio.links.program_error.
9+
10+
Module InstructionContext.
11+
Record t : Set := {
12+
buffer : Ref.t Pointer.Kind.Raw U8.t;
13+
remaining: U64.t
14+
}.
15+
16+
Global Instance IsLink : Link t := {
17+
Φ := Ty.path "pinocchio::entrypoint::lazy::InstructionContext";
18+
φ x :=
19+
Value.StructRecord "pinocchio::entrypoint::lazy::InstructionContext" [] [] [
20+
("buffer", φ x.(buffer));
21+
("remaining", φ x.(remaining))
22+
];
23+
}.
24+
End InstructionContext.
25+
26+
Module MaybeAccount.
27+
Inductive t : Set :=
28+
| Account (a : AccountInfo.t)
29+
| Duplicated (i : U8.t).
30+
31+
Global Instance IsLink : Link t := {
32+
Φ := Ty.path "pinocchio::entrypoint::lazy::MaybeAccount";
33+
φ x :=
34+
match x with
35+
| Account a =>
36+
Value.StructTuple
37+
"pinocchio::entrypoint::lazy::MaybeAccount::Account" [] [] [φ a]
38+
| Duplicated i =>
39+
Value.StructTuple
40+
"pinocchio::entrypoint::lazy::MaybeAccount::Duplicated" [] [] [φ i]
41+
end;
42+
}.
43+
End MaybeAccount.
44+
45+
Module Impl_InstructionContext.
46+
Definition Self : Set := InstructionContext.t.
47+
48+
Instance run_new
49+
(input : Ref.t Pointer.Kind.Raw U8.t) :
50+
Run.Trait
51+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_InstructionContext.new
52+
[] [] [φ input] Self.
53+
Proof.
54+
constructor. admit.
55+
Admitted.
56+
57+
Instance run_new_unchecked
58+
(input : Ref.t Pointer.Kind.Raw U8.t) :
59+
Run.Trait
60+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_InstructionContext.new_unchecked
61+
[] [] [φ input] Self.
62+
Proof.
63+
constructor. admit.
64+
Admitted.
65+
66+
Instance run_next_account
67+
(self : Ref.t Pointer.Kind.Ref Self) :
68+
Run.Trait
69+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_InstructionContext.next_account
70+
[] [] [φ self] (Result.t MaybeAccount.t ProgramError.t).
71+
Proof.
72+
constructor. admit.
73+
Admitted.
74+
75+
Instance run_next_account_unchecked
76+
(self : Ref.t Pointer.Kind.Ref Self) :
77+
Run.Trait
78+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_InstructionContext.next_account_unchecked
79+
[] [] [φ self] MaybeAccount.t.
80+
Proof.
81+
constructor. admit.
82+
Admitted.
83+
84+
Instance run_remaining
85+
(self : Ref.t Pointer.Kind.Ref Self) :
86+
Run.Trait
87+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_InstructionContext.remaining
88+
[] [] [φ self] U64.t.
89+
Proof.
90+
constructor. admit.
91+
Admitted.
92+
93+
Instance run_instruction_data
94+
(self : Ref.t Pointer.Kind.Ref Self) :
95+
Run.Trait
96+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_InstructionContext.instruction_data
97+
[] [] [φ self] (Result.t (list (Integer.t IntegerKind.U8)) ProgramError.t).
98+
Proof.
99+
constructor. admit.
100+
Admitted.
101+
102+
Instance run_instruction_data_unchecked
103+
(self : Ref.t Pointer.Kind.Ref Self) :
104+
Run.Trait
105+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_InstructionContext.instruction_data_unchecked
106+
[] [] [φ self] (list (Integer.t IntegerKind.U8)).
107+
Proof.
108+
constructor. admit.
109+
Admitted.
110+
111+
Instance run_program_id
112+
(self : Ref.t Pointer.Kind.Ref Self) :
113+
Run.Trait
114+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_InstructionContext.program_id
115+
[] [] [φ self] (Result.t (Ref.t Pointer.Kind.Ref Pubkey.t) ProgramError.t).
116+
Proof.
117+
constructor. admit.
118+
Admitted.
119+
120+
Instance run_program_id_unchecked
121+
(self : Ref.t Pointer.Kind.Ref Self) :
122+
Run.Trait
123+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_InstructionContext.program_id_unchecked
124+
[] [] [φ self] (Ref.t Pointer.Kind.Ref Pubkey.t).
125+
Proof.
126+
constructor. admit.
127+
Admitted.
128+
End Impl_InstructionContext.
129+
130+
Module Impl_MaybeAccount.
131+
Definition Self : Set := MaybeAccount.t.
132+
133+
Instance run_assume_account
134+
(self : Self) :
135+
Run.Trait
136+
pinocchio.entrypoint.lazy.entrypoint.lazy.Impl_pinocchio_entrypoint_lazy_MaybeAccount.assume_account
137+
[] [] [φ self] AccountInfo.t.
138+
Proof.
139+
constructor. admit.
140+
Admitted.
141+
End Impl_MaybeAccount.

‎CoqOfRust/pinocchio/entrypoint/links/mod.v‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
Require Import CoqOfRust.CoqOfRust.
2+
Require Import CoqOfRust.links.M.
3+
Require Import core.links.array.
4+
Require Import pinocchio.links.account_info.
5+
Require Import pinocchio.entrypoint.mod.
6+
7+
Module entrypoint.
8+
Module deserialize.
9+
10+
Parameter MAX_ACCOUNTS : Usize.t.
11+
12+
Definition Self : Set := (Ref.t Pointer.Kind.Ref U8.t *
13+
Usize.t *
14+
Ref.t Pointer.Kind.Ref (list U8.t))%type.
15+
16+
Instance run_deserialize
17+
(input : Ref.t Pointer.Kind.Raw U8.t)
18+
(accounts : Ref.t Pointer.Kind.Ref (array.t AccountInfo.t MAX_ACCOUNTS)) :
19+
Run.Trait
20+
pinocchio.entrypoint.mod.entrypoint.deserialize
21+
[φ MAX_ACCOUNTS] []
22+
[ φ input; φ accounts ]
23+
Self.
24+
Proof.
25+
constructor.
26+
run_symbolic.
27+
- admit.
28+
- admit.
29+
- admit.
30+
Admitted.
31+
End deserialize.
32+
33+
Module parse.
34+
Parameter MAX_ACCOUNTS : Usize.t.
35+
36+
Definition Self : Set := (Ref.t Pointer.Kind.Raw U8.t *
37+
Usize.t *
38+
Ref.t Pointer.Kind.Ref (list U8.t))%type.
39+
40+
Instance run
41+
(input : Ref.t Pointer.Kind.Raw U8.t)
42+
(accounts : Ref.t Pointer.Kind.Ref (array.t AccountInfo.t MAX_ACCOUNTS)) :
43+
Run.Trait
44+
pinocchio.entrypoint.mod.entrypoint.parse
45+
[φ MAX_ACCOUNTS] []
46+
[ φ input; φ accounts ]
47+
Self.
48+
Proof.
49+
constructor.
50+
run_symbolic.
51+
- admit.
52+
- admit.
53+
- admit.
54+
Admitted.
55+
End parse.
56+
End entrypoint.

‎CoqOfRust/pinocchio/links/account_info.v‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Require Import core.links.cmp.
44
Require Import pinocchio.links.pubkey.
55
Require Import pinocchio.account_info.
66
Require Import core.links.array.
7+
Require Import core.links.marker.
78

89
Import core.links.cmp.PartialEq.
910
Import core.links.cmp.
@@ -83,6 +84,9 @@ Module Account.
8384
];
8485
}.
8586

87+
Global Instance PointeeSized_Run : PointeeSized.Run t :=
88+
{ dummy_empty_class := tt }.
89+
8690
Definition of_ty : OfTy.t (Ty.path "pinocchio::account_info::Account").
8791
Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
8892
Smpl Add apply of_ty : of_ty.
@@ -261,6 +265,9 @@ Module AccountInfo.
261265
];
262266
}.
263267

268+
Global Instance PointeeSized_Run : PointeeSized.Run t :=
269+
{ dummy_empty_class := tt }.
270+
264271
Definition of_ty : OfTy.t (Ty.path "pinocchio::account_info::AccountInfo").
265272
Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
266273
Smpl Add apply of_ty : of_ty.

0 commit comments

Comments
 (0)