Skip to content

Draft: add zkWasm / halo_proofs translation #546

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

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Draft: add zkWasm / halo_proofs translation #546

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f0eff77
proofs: add zkWasm translation
clarus May 17, 2024
bd16fa2
proof: add halo2_proofs translation
clarus May 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12,313 changes: 12,313 additions & 0 deletions CoqOfRust/halo2_proofs/arithmetic.v
View file
Open in desktop

Large diffs are not rendered by default.

3,465 changes: 3,465 additions & 0 deletions CoqOfRust/halo2_proofs/circuit.v
View file
Open in desktop

Large diffs are not rendered by default.

6,410 changes: 6,410 additions & 0 deletions CoqOfRust/halo2_proofs/circuit/floor_planner/flat.v
View file
Open in desktop

Large diffs are not rendered by default.

1,753 changes: 1,753 additions & 0 deletions CoqOfRust/halo2_proofs/circuit/floor_planner/flat/region.v
View file
Open in desktop

Large diffs are not rendered by default.

973 changes: 973 additions & 0 deletions CoqOfRust/halo2_proofs/circuit/floor_planner/single_pass.v
View file
Open in desktop

Large diffs are not rendered by default.

10,154 changes: 10,154 additions & 0 deletions CoqOfRust/halo2_proofs/circuit/floor_planner/v1.v
View file
Open in desktop

Large diffs are not rendered by default.

3,196 changes: 3,196 additions & 0 deletions CoqOfRust/halo2_proofs/circuit/floor_planner/v1/strategy.v
View file
Open in desktop

Large diffs are not rendered by default.

2,012 changes: 2,012 additions & 0 deletions CoqOfRust/halo2_proofs/circuit/layouter.v
View file
Open in desktop

Large diffs are not rendered by default.

25,066 changes: 25,066 additions & 0 deletions CoqOfRust/halo2_proofs/dev.v
View file
Open in desktop

Large diffs are not rendered by default.

5,388 changes: 5,388 additions & 0 deletions CoqOfRust/halo2_proofs/dev/cost.v
View file
Open in desktop

Large diffs are not rendered by default.

8,107 changes: 8,107 additions & 0 deletions CoqOfRust/halo2_proofs/dev/gates.v
View file
Open in desktop

Large diffs are not rendered by default.

2,444 changes: 2,444 additions & 0 deletions CoqOfRust/halo2_proofs/dev/metadata.v
View file
Open in desktop

Large diffs are not rendered by default.

1,275 changes: 1,275 additions & 0 deletions CoqOfRust/halo2_proofs/dev/util.v
View file
Open in desktop

Large diffs are not rendered by default.

22,659 changes: 22,659 additions & 0 deletions CoqOfRust/halo2_proofs/helpers.v
View file
Open in desktop

Large diffs are not rendered by default.

285 changes: 285 additions & 0 deletions CoqOfRust/halo2_proofs/parallel.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,285 @@
(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module parallel.
(* StructTuple
{
name := "Parallel";
ty_params := [ "T" ];
fields :=
[
Ty.apply
(Ty.path "alloc::sync::Arc")
[ Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ]; Ty.path "alloc::alloc::Global" ]
];
} *)

Module Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_fmt_Debug_T_for_halo2_proofs_parallel_Parallel_T.
Definition Self (T : Ty.t) : Ty.t :=
Ty.apply (Ty.path "halo2_proofs::parallel::Parallel") [ T ].

(* Debug *)
Definition fmt (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
let Self : Ty.t := Self T in
match τ, α with
| [], [ self; f ] =>
ltac:(M.monadic
(let self := M.alloc (| self |) in
let f := M.alloc (| f |) in
M.call_closure (|
M.get_associated_function (|
Ty.path "core::fmt::Formatter",
"debug_tuple_field1_finish",
[]
|),
[
M.read (| f |);
M.read (| Value.String "Parallel" |);
(* Unsize *)
M.pointer_coercion
(M.alloc (|
M.SubPointer.get_struct_tuple_field (|
M.read (| self |),
"halo2_proofs::parallel::Parallel",
0
|)
|))
]
|)))
| _, _ => M.impossible
end.

Axiom Implements :
forall (T : Ty.t),
M.IsTraitInstance
"core::fmt::Debug"
(Self T)
(* Trait polymorphic types *) []
(* Instance *) [ ("fmt", InstanceField.Method (fmt T)) ].
End Impl_core_fmt_Debug_where_core_fmt_Debug_T_where_core_fmt_Debug_T_for_halo2_proofs_parallel_Parallel_T.

Module Impl_core_clone_Clone_where_core_fmt_Debug_T_for_halo2_proofs_parallel_Parallel_T.
Definition Self (T : Ty.t) : Ty.t :=
Ty.apply (Ty.path "halo2_proofs::parallel::Parallel") [ T ].

(*
fn clone(&self) -> Self {
Self(self.0.clone())
}
*)
Definition clone (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
let Self : Ty.t := Self T in
match τ, α with
| [], [ self ] =>
ltac:(M.monadic
(let self := M.alloc (| self |) in
Value.StructTuple
"halo2_proofs::parallel::Parallel"
[
M.call_closure (|
M.get_trait_method (|
"core::clone::Clone",
Ty.apply
(Ty.path "alloc::sync::Arc")
[
Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ];
Ty.path "alloc::alloc::Global"
],
[],
"clone",
[]
|),
[
M.SubPointer.get_struct_tuple_field (|
M.read (| self |),
"halo2_proofs::parallel::Parallel",
0
|)
]
|)
]))
| _, _ => M.impossible
end.

Axiom Implements :
forall (T : Ty.t),
M.IsTraitInstance
"core::clone::Clone"
(Self T)
(* Trait polymorphic types *) []
(* Instance *) [ ("clone", InstanceField.Method (clone T)) ].
End Impl_core_clone_Clone_where_core_fmt_Debug_T_for_halo2_proofs_parallel_Parallel_T.

Module Impl_halo2_proofs_parallel_Parallel_T.
Definition Self (T : Ty.t) : Ty.t :=
Ty.apply (Ty.path "halo2_proofs::parallel::Parallel") [ T ].

(*
pub(crate) fn new(v: T) -> Self {
Parallel(Arc::new(Mutex::new(v)))
}
*)
Definition new (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
let Self : Ty.t := Self T in
match τ, α with
| [], [ v ] =>
ltac:(M.monadic
(let v := M.alloc (| v |) in
Value.StructTuple
"halo2_proofs::parallel::Parallel"
[
M.call_closure (|
M.get_associated_function (|
Ty.apply
(Ty.path "alloc::sync::Arc")
[
Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ];
Ty.path "alloc::alloc::Global"
],
"new",
[]
|),
[
M.call_closure (|
M.get_associated_function (|
Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ],
"new",
[]
|),
[ M.read (| v |) ]
|)
]
|)
]))
| _, _ => M.impossible
end.

Axiom AssociatedFunction_new : forall (T : Ty.t), M.IsAssociatedFunction (Self T) "new" (new T).

(*
pub(crate) fn into_inner(self) -> T {
Arc::try_unwrap(self.0).unwrap().into_inner().unwrap()
}
*)
Definition into_inner (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
let Self : Ty.t := Self T in
match τ, α with
| [], [ self ] =>
ltac:(M.monadic
(let self := M.alloc (| self |) in
M.call_closure (|
M.get_associated_function (|
Ty.apply
(Ty.path "core::result::Result")
[ T; Ty.apply (Ty.path "std::sync::poison::PoisonError") [ T ] ],
"unwrap",
[]
|),
[
M.call_closure (|
M.get_associated_function (|
Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ],
"into_inner",
[]
|),
[
M.call_closure (|
M.get_associated_function (|
Ty.apply
(Ty.path "core::result::Result")
[
Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ];
Ty.apply
(Ty.path "alloc::sync::Arc")
[
Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ];
Ty.path "alloc::alloc::Global"
]
],
"unwrap",
[]
|),
[
M.call_closure (|
M.get_associated_function (|
Ty.apply
(Ty.path "alloc::sync::Arc")
[
Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ];
Ty.path "alloc::alloc::Global"
],
"try_unwrap",
[]
|),
[
M.read (|
M.SubPointer.get_struct_tuple_field (|
self,
"halo2_proofs::parallel::Parallel",
0
|)
|)
]
|)
]
|)
]
|)
]
|)))
| _, _ => M.impossible
end.

Axiom AssociatedFunction_into_inner :
forall (T : Ty.t),
M.IsAssociatedFunction (Self T) "into_inner" (into_inner T).

(*
pub(crate) fn lock(&self) -> Result<MutexGuard<'_, T>, PoisonError<MutexGuard<'_, T>>> {
self.0.lock()
}
*)
Definition lock (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
let Self : Ty.t := Self T in
match τ, α with
| [], [ self ] =>
ltac:(M.monadic
(let self := M.alloc (| self |) in
M.call_closure (|
M.get_associated_function (|
Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ],
"lock",
[]
|),
[
M.call_closure (|
M.get_trait_method (|
"core::ops::deref::Deref",
Ty.apply
(Ty.path "alloc::sync::Arc")
[
Ty.apply (Ty.path "std::sync::mutex::Mutex") [ T ];
Ty.path "alloc::alloc::Global"
],
[],
"deref",
[]
|),
[
M.SubPointer.get_struct_tuple_field (|
M.read (| self |),
"halo2_proofs::parallel::Parallel",
0
|)
]
|)
]
|)))
| _, _ => M.impossible
end.

Axiom AssociatedFunction_lock :
forall (T : Ty.t),
M.IsAssociatedFunction (Self T) "lock" (lock T).
End Impl_halo2_proofs_parallel_Parallel_T.
End parallel.
Loading