From ec685957cdd5e8d959dc4464f2d7889a8297d986 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 19 May 2025 18:37:53 +0800
Subject: [PATCH 01/19] minor: update `blake_air::air`

---
 CoqOfRust/plonky3/blake3_air/links/air.v | 186 ++++++++++++++++++++---
 1 file changed, 165 insertions(+), 21 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/air.v b/CoqOfRust/plonky3/blake3_air/links/air.v
index d150a9a05..1567ef4d9 100644
--- a/CoqOfRust/plonky3/blake3_air/links/air.v
+++ b/CoqOfRust/plonky3/blake3_air/links/air.v
@@ -1,41 +1,185 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import plonky3.blake3_air.air.
+Require Import plonky3.field.links.field.
+Require Import plonky3.blake3_air.links.columns.
+Require Import plonky3.air.links.air.
+Require Import plonky3.matrix.links.dense.
+
+(* 
+TODO:
+- Move all files under `src` to their parent files for consistency
+- In future, refer to `gas` to deal with different impls
+- In future, for all dependencies, fix their type path to actual path that starts with `p_3`
+- Check if AirBuilder needs `AB_types`
+*)
 
 (* pub struct Blake3Air {} *)
 Module Blake3Air.
-  Inductive t : Set :=
-  | Make.
+  Record t : Set := {}.
+
+  Parameter to_value : t -> Value.t.
 
   Global Instance IsLink : Link t := {
-    Φ := Ty.path "plonky3::blake3-air::Blake3Air";
-    φ _ := Value.StructRecord "p3_blake3_air::air::Blake3Air" [] [] [];
+  (* TODO: fix path here *)
+    Φ := Ty.path "plonky3::blake3_air::air::Blake3Air";
+    φ := to_value;
   }.
 
-  Definition of_ty : OfTy.t (Ty.path "plonky3::blake3-air::Blake3Air").
+  Definition of_ty : OfTy.t (Ty.path "plonky3::blake3_air::air::Blake3Air").
   Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
-  Smpl Add apply of_ty : of_ty.
+  Smpl Add apply of_ty : of_ty. 
 End Blake3Air.
 
 Module Impl_Blake3Air.
-(* TODO: figure out what is this `PrimeField64` *)
-(* 
-impl Blake3Air {
-    pub fn generate_trace_rows<F: PrimeField64>(
-        &self,
-        num_hashes: usize,
-        extra_capacity_bits: usize,
-    ) -> RowMajorMatrix<F> {
-*)
+  Definition Self := Blake3Air.t.
+  (* 
+  impl Blake3Air {
+      pub fn generate_trace_rows<F: PrimeField64>(
+          &self,
+          num_hashes: usize,
+          extra_capacity_bits: usize,
+      ) -> RowMajorMatrix<F>
+  *)
+  Instance run_generate_trace_rows
+    {F : Set} `{Link F} 
+    {run_PrimeField64_for_F : PrimeField64.Run F}
+    (self : Ref.t Pointer.Kind.Ref Self) (num_hashes : Usize.t) (extra_capacity_bits : Usize.t) :
+    Run.Trait
+      blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.generate_trace_rows [] [ Φ F ] [ φ num_hashes; φ extra_capacity_bits ]
+      (RowMajorMatrix.t F).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
 
-(* 
-  Instance run_STOP :
+  (* 
+  fn quarter_round_function<AB: AirBuilder>(
+          &self,
+          builder: &mut AB,
+          trace: &QuarterRound<<AB as AirBuilder>::Var, <AB as AirBuilder>::Expr>,
+      )
+  *)
+  Instance run_quarter_round_function
+    {AB : Set} `{Link AB} 
+    {run_AirBuilder_for_AB : AirBuilder.Run AB}
+    (* TODO: check if AirBuilder needs `AB_types` *)
+    (self : Ref.t Pointer.Kind.Ref Self) 
+    (builder : Ref.t Pointer.Kind.MutRef AB) 
+    (* TODO: translate `trace: &QuarterRound<<AB as AirBuilder>::Var, <AB as AirBuilder>::Expr>` *)
+    (trace : Set)
+    :
     Run.Trait
-      opcode.Impl_revm_bytecode_opcode_OpCode.value_STOP [] [] []
-      (Ref.t Pointer.Kind.Raw OpCode.t).
+      blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.quarter_round_function [] [ Φ AB ] [ φ builder (* ; φ trace *) ]
+      unit.
   Proof.
     constructor.
     run_symbolic.
-  Defined.
-*)
+  Admitted.
+
+  (* 
+  const fn full_round_to_column_quarter_round<'a, T: Copy, U>(
+      &self,
+      input: &'a Blake3State<T>,
+      round_data: &'a FullRound<T>,
+      m_vector: &'a [[U; 2]; 16],
+      index: usize,
+  ) -> QuarterRound<'a, T, U>
+  *)
+  Instance run_full_round_to_column_quarter_round
+  (* NOTE: seems like there are some issues with T and U being defined here *)
+    {T U : Set} `{Link T}  `{Link U}
+    (self : Ref.t Pointer.Kind.Ref Self) 
+    (input : Ref.t Pointer.Kind.Ref (Blake3State.t T))
+    (round_data : Ref.t Pointer.Kind.Ref (FullRound.t T))
+    (m_vector : list (list U))
+    (index : Usize.t)
+    :
+    Run.Trait
+      blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.full_round_to_column_quarter_round [] [ Φ T; Φ U ] 
+      [ (* φ input; φ round_data; φ m_vector; φ index *) ]
+      (QuarterRound.t T U).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* 
+  const fn full_round_to_diagonal_quarter_round<'a, T: Copy, U>(
+      &self,
+      round_data: &'a FullRound<T>,
+      m_vector: &'a [[U; 2]; 16],
+      index: usize,
+  ) -> QuarterRound<'a, T, U> 
+  *)
+  Instance run_full_round_to_diagonal_quarter_round
+    {T U : Set} `{Link T}  `{Link U}
+    (self : Ref.t Pointer.Kind.Ref Self) 
+    (round_data : Ref.t Pointer.Kind.Ref (FullRound.t T))
+    (m_vector : list (list U))
+    (index : Usize.t)
+    :
+    Run.Trait
+      blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.full_round_to_diagonal_quarter_round [] [ Φ T; Φ U ] 
+      [ (* φ input; φ round_data; φ m_vector; φ index *) ]
+      (QuarterRound.t T U).
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
+
+  (* 
+  fn verify_round<AB: AirBuilder>(
+      &self,
+      builder: &mut AB,
+      input: &Blake3State<AB::Var>,
+      round_data: &FullRound<AB::Var>,
+      m_vector: &[[AB::Expr; 2]; 16],
+  )
+  *)
+  Instance run_verify_round
+    {AB : Set} `{Link AB} 
+    {run_AirBuilder_for_AB : AirBuilder.Run AB}
+    (self : Ref.t Pointer.Kind.Ref Self) 
+    (builder : Ref.t Pointer.Kind.MutRef AB) 
+    (* TODO: translate correctly the following variables *)
+    (* (input : Ref.t Pointer.Kind.Ref Blake3State.t (AB.Var)) *)
+    (* (round_data : Ref.t Pointer.Kind.Ref FullRound (AB.Var)) *)
+    (* (m_vector : list (list Set)) *)
+    :
+    Run.Trait
+      blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.verify_round [] [ Φ AB ] 
+        [ φ builder (* ; φ input; φ round_data; φ m_vector *) ]
+      unit.
+  Proof.
+    constructor.
+    run_symbolic.
+  Admitted.
 End Impl_Blake3Air.
+
+(* 
+impl<F> BaseAir<F> for Blake3Air {
+    fn width(&self) -> usize {
+        NUM_BLAKE3_COLS
+    }
+}
+*)
+Module Impl_BaseAir_for_Blake3Air.
+  Definition Self : Set :=
+    Blake3Air.t.
+
+  (* Instance run : BaseAir.Run Self. *)
+  (* Admitted. *)
+End Impl_BaseAir_for_Blake3Air.
+
+(* 
+impl<AB: AirBuilder> Air<AB> for Blake3Air {
+    fn eval(&self, builder: &mut AB)
+*)
+Module Impl_Air_for_Blake3Air.
+  Definition Self : Set :=
+    Blake3Air.t.
+
+  (* Instance run : Air.Run Self. *)
+  (* Admitted. *)
+End Impl_Air_for_Blake3Air.

From 4af6c9ca4d39ea57eb9dee3035a0995e038cf3da Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 19 May 2025 18:39:30 +0800
Subject: [PATCH 02/19] minor: update `columns`

---
 CoqOfRust/plonky3/blake3_air/links/columns.v | 42 +++++++++++++-------
 1 file changed, 28 insertions(+), 14 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index 38bde645a..774302ac5 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -2,10 +2,6 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import plonky3.blake3_air.columns.
 
-(* TODO:
-- fill in `of_ty` for structs
-*)
-
 (* 
 pub(crate) struct QuarterRound<'a, T, U> {
     pub a: &'a [T; U32_LIMBS],
@@ -49,10 +45,16 @@ Module QuarterRound.
 
   Parameter to_value : forall {T U : Set}, t T U -> Value.t.
 
-  (* Global Instance IsLink (T U : Set) : Link (t T U) := {
-    Φ := Ty.path "plonky3::blake3_air::columns::QuarterRound";
+  Global Instance IsLink (T U : Set) `{Link T} `{Link U} : Link (t T U) := {
+    Φ := Ty.apply (Ty.path "plonky3::blake3_air::columns::QuarterRound") [] [ Φ T; Φ U ];
     φ := to_value;
-  }. *)
+  }.
+
+  Definition of_ty (T_ty U_ty : Ty.t) :
+    OfTy.t T_ty -> OfTy.t U_ty ->
+    OfTy.t (Ty.apply (Ty.path "plonky3::blake3_air::columns::QuarterRound") [] [ T_ty ; U_ty ]).
+  Proof. intros [T] [U]. eapply OfTy.Make with (A := t T U). now subst. Defined.
+  Smpl Add eapply of_ty : of_ty.
 End QuarterRound.
 
 (* 
@@ -74,10 +76,16 @@ Module Blake3State.
 
   Parameter to_value : forall {T : Set}, t T -> Value.t.
 
-  (* Global Instance IsLink (T : Set) : Link (t T) := {
-    Φ := Ty.path "plonky3::blake3_air::columns::Blake3State";
+  Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
+    Φ := Ty.apply (Ty.path "plonky3::blake3_air::columns::Blake3State") [] [ Φ T ];
     φ := to_value;
-  }. *)
+  }.
+
+  Definition of_ty (T_ty : Ty.t) :
+    OfTy.t T_ty -> 
+    OfTy.t (Ty.apply (Ty.path "plonky3::blake3_air::columns::Blake3State") [] [ T_ty ]).
+  Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
+  Smpl Add eapply of_ty : of_ty.
 End Blake3State.
 
 (* 
@@ -99,8 +107,14 @@ Module FullRound.
 
   Parameter to_value : forall {T : Set}, t T -> Value.t.
 
-  (* Global Instance IsLink (T : Set) : Link (t T) := {
-    Φ := Ty.path "plonky3::blake3_air::columns::FullRound";
+  Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
+    Φ := Ty.apply (Ty.path "plonky3::blake3_air::columns::FullRound") [] [ Φ T ];
     φ := to_value;
-  }. *)
-End FullRound.
+  }.
+
+  Definition of_ty (T_ty : Ty.t) :
+    OfTy.t T_ty -> 
+    OfTy.t (Ty.apply (Ty.path "plonky3::blake3_air::columns::FullRound") [] [ T_ty ]).
+  Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
+  Smpl Add eapply of_ty : of_ty.
+End FullRound.
\ No newline at end of file

From 20b8ab39d39db28e8ed75c66a47d4ac2df745b76 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 19 May 2025 18:43:25 +0800
Subject: [PATCH 03/19] minor: update `air` and `dense`

---
 CoqOfRust/plonky3/blake3_air/links/air.v |  2 ++
 CoqOfRust/plonky3/matrix/links/dense.v   | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/CoqOfRust/plonky3/blake3_air/links/air.v b/CoqOfRust/plonky3/blake3_air/links/air.v
index 1567ef4d9..ec28fcfcc 100644
--- a/CoqOfRust/plonky3/blake3_air/links/air.v
+++ b/CoqOfRust/plonky3/blake3_air/links/air.v
@@ -12,6 +12,8 @@ TODO:
 - In future, refer to `gas` to deal with different impls
 - In future, for all dependencies, fix their type path to actual path that starts with `p_3`
 - Check if AirBuilder needs `AB_types`
+- Check occurences for `Vec` as in `dense`
+- Check occurences for `of_ty` as in `dense`
 *)
 
 (* pub struct Blake3Air {} *)
diff --git a/CoqOfRust/plonky3/matrix/links/dense.v b/CoqOfRust/plonky3/matrix/links/dense.v
index b168f4fb8..0072fcdcf 100644
--- a/CoqOfRust/plonky3/matrix/links/dense.v
+++ b/CoqOfRust/plonky3/matrix/links/dense.v
@@ -4,6 +4,10 @@ Require Import alloc.links.alloc.
 Require Import alloc.vec.links.mod.
 Require Import plonky3.matrix.dense.
 
+(* TODO:
+  - in the future, check the detail of the proof
+*)
+
 (* 
 pub struct DenseMatrix<T, V = Vec<T>> {
     pub values: V,
@@ -30,6 +34,7 @@ Module DenseMatrix.
     OfTy.t T' ->
     OfTy.t V' ->
     OfTy.t (Ty.apply (Ty.path "p3_matrix::dense::DenseMatrix") [] [ T'; V']).
+  (* TODO: check the proof in the future *)
   Proof. intros [T] [V]. eapply OfTy.Make with (A := t T V). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 End DenseMatrix.
@@ -39,4 +44,17 @@ pub type RowMajorMatrix<T> = DenseMatrix<T, Vec<T>>;
 *)
 Module RowMajorMatrix.
   Definition t (T : Set) := DenseMatrix.t T (Vec.t Global.t T).
+
+  Parameter to_value : forall {T : Set}, t T -> Value.t.
+
+  Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
+    Φ := Ty.apply (Ty.path "p3_matrix::dense::RowMajorMatrix") [] [ Φ T ];
+    φ := to_value;
+  }.
+
+  Definition of_ty (T_ty : Ty.t) :
+    OfTy.t T_ty -> 
+    OfTy.t (Ty.apply (Ty.path "p3_matrix::dense::RowMajorMatrix") [] [ T_ty ]).
+  Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
+  Smpl Add eapply of_ty : of_ty.
 End RowMajorMatrix.

From 6b22e2bd9abc8e56c857c97b0433cc8c7b43ae67 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 19 May 2025 18:44:18 +0800
Subject: [PATCH 04/19] minor: update `air` comment

---
 CoqOfRust/plonky3/blake3_air/links/air.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/air.v b/CoqOfRust/plonky3/blake3_air/links/air.v
index ec28fcfcc..38353e074 100644
--- a/CoqOfRust/plonky3/blake3_air/links/air.v
+++ b/CoqOfRust/plonky3/blake3_air/links/air.v
@@ -8,9 +8,8 @@ Require Import plonky3.matrix.links.dense.
 
 (* 
 TODO:
-- Move all files under `src` to their parent files for consistency
-- In future, refer to `gas` to deal with different impls
-- In future, for all dependencies, fix their type path to actual path that starts with `p_3`
+- Refer to `gas` to deal with different impls
+- For all dependencies, fix their type path to actual path that starts with `p_3`
 - Check if AirBuilder needs `AB_types`
 - Check occurences for `Vec` as in `dense`
 - Check occurences for `of_ty` as in `dense`

From b432bb00510b8323a42c2588a05226b98017e9ee Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 19 May 2025 21:00:47 +0800
Subject: [PATCH 05/19] minor: update wrt comments

---
 CoqOfRust/plonky3/blake3_air/links/columns.v | 38 ++++++++++----------
 CoqOfRust/plonky3/matrix/links/dense.v       | 13 -------
 2 files changed, 20 insertions(+), 31 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index 774302ac5..69a44517c 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -2,6 +2,8 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import plonky3.blake3_air.columns.
 
+(* TODO: check where is U32_LIMBS *)
+
 (* 
 pub(crate) struct QuarterRound<'a, T, U> {
     pub a: &'a [T; U32_LIMBS],
@@ -26,20 +28,20 @@ pub(crate) struct QuarterRound<'a, T, U> {
 *)
 Module QuarterRound.
   Record t (T U : Set) : Set := {
-    a : list T; 
-    b : list T; 
-    c : list T; 
-    d : list T;
-    m_two_i : list U;
-    a_prime : list T;
-    b_prime : list T;
-    c_prime : list T;
-    d_prime : list T;
-    m_two_i_plus_one : list U;
-    a_output : list T;
-    b_output : list T;
-    c_output : list T;
-    d_output : list T;
+    a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
+    b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
+    c : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
+    d : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
+    m_two_i : Ref.t Pointer.Kind.Ref (array.t U {| Integer.value := 32 |});
+    a_prime : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
+    b_prime : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
+    c_prime : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
+    d_prime : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
+    m_two_i_plus_one : Ref.t Pointer.Kind.Ref (array.t U {| Integer.value := 32 |});
+    a_output : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
+    b_output : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
+    c_output : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
+    d_output : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
   }.
   Arguments t : clear implicits.
 
@@ -67,10 +69,10 @@ pub struct Blake3State<T> {
 *)
 Module Blake3State.
   Record t (T : Set) : Set := {
-    row0 : list (list T);
-    row1 : list (list T);
-    row2 : list (list T);
-    row3 : list (list T);
+    row0 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |};
+    row1 : array.t (array.t T {| Integer.value := 32 |}) {| Integer.value := 4 |};
+    row2 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |};
+    row3 : array.t (array.t T {| Integer.value := 32 |}) {| Integer.value := 4 |};
   }.
   Arguments t : clear implicits.
 
diff --git a/CoqOfRust/plonky3/matrix/links/dense.v b/CoqOfRust/plonky3/matrix/links/dense.v
index 0072fcdcf..dac418da6 100644
--- a/CoqOfRust/plonky3/matrix/links/dense.v
+++ b/CoqOfRust/plonky3/matrix/links/dense.v
@@ -44,17 +44,4 @@ pub type RowMajorMatrix<T> = DenseMatrix<T, Vec<T>>;
 *)
 Module RowMajorMatrix.
   Definition t (T : Set) := DenseMatrix.t T (Vec.t Global.t T).
-
-  Parameter to_value : forall {T : Set}, t T -> Value.t.
-
-  Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
-    Φ := Ty.apply (Ty.path "p3_matrix::dense::RowMajorMatrix") [] [ Φ T ];
-    φ := to_value;
-  }.
-
-  Definition of_ty (T_ty : Ty.t) :
-    OfTy.t T_ty -> 
-    OfTy.t (Ty.apply (Ty.path "p3_matrix::dense::RowMajorMatrix") [] [ T_ty ]).
-  Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
-  Smpl Add eapply of_ty : of_ty.
 End RowMajorMatrix.

From 27c9ed00e1a773459142c4416b2fc55182a85031 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 19 May 2025 21:03:25 +0800
Subject: [PATCH 06/19] minor: more updates to eliminate warnings

---
 CoqOfRust/plonky3/blake3_air/links/air.v | 8 ++++----
 CoqOfRust/plonky3/field/links/field.v    | 3 ++-
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/air.v b/CoqOfRust/plonky3/blake3_air/links/air.v
index 38353e074..44e2a880f 100644
--- a/CoqOfRust/plonky3/blake3_air/links/air.v
+++ b/CoqOfRust/plonky3/blake3_air/links/air.v
@@ -11,13 +11,13 @@ TODO:
 - Refer to `gas` to deal with different impls
 - For all dependencies, fix their type path to actual path that starts with `p_3`
 - Check if AirBuilder needs `AB_types`
-- Check occurences for `Vec` as in `dense`
 - Check occurences for `of_ty` as in `dense`
 *)
 
 (* pub struct Blake3Air {} *)
 Module Blake3Air.
-  Record t : Set := {}.
+  Inductive t : Set :=
+  | Make.
 
   Parameter to_value : t -> Value.t.
 
@@ -93,7 +93,7 @@ Module Impl_Blake3Air.
     (self : Ref.t Pointer.Kind.Ref Self) 
     (input : Ref.t Pointer.Kind.Ref (Blake3State.t T))
     (round_data : Ref.t Pointer.Kind.Ref (FullRound.t T))
-    (m_vector : list (list U))
+    (m_vector : Ref.t Pointer.Kind.Ref (array.t (array.t U {| Integer.value := 2 |}) {| Integer.value := 16 |})
     (index : Usize.t)
     :
     Run.Trait
@@ -117,7 +117,7 @@ Module Impl_Blake3Air.
     {T U : Set} `{Link T}  `{Link U}
     (self : Ref.t Pointer.Kind.Ref Self) 
     (round_data : Ref.t Pointer.Kind.Ref (FullRound.t T))
-    (m_vector : list (list U))
+    (m_vector : Ref.t Pointer.Kind.Ref (array.t (array.t U {| Integer.value := 2 |}) {| Integer.value := 16 |})
     (index : Usize.t)
     :
     Run.Trait
diff --git a/CoqOfRust/plonky3/field/links/field.v b/CoqOfRust/plonky3/field/links/field.v
index 35dca16c3..44f6db4ff 100644
--- a/CoqOfRust/plonky3/field/links/field.v
+++ b/CoqOfRust/plonky3/field/links/field.v
@@ -126,7 +126,8 @@ pub trait PrimeField64: PrimeField {
 }
 *)
 Module PrimeField64.
-  Parameter t : Set.
+  Inductive t : Set :=
+  | Make.
 
   Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
     ("plonky3::field::field::PrimeField64", [], [], Φ Self).

From ec6f890f9069457aefd74a36e50bb5ff9df9a256 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 19 May 2025 21:11:02 +0800
Subject: [PATCH 07/19] minor: fix type paths

---
 CoqOfRust/plonky3/blake3_air/links/air.v     |  8 +++-----
 CoqOfRust/plonky3/blake3_air/links/columns.v | 17 ++++++++++-------
 CoqOfRust/plonky3/field/links/field.v        |  6 +++---
 3 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/air.v b/CoqOfRust/plonky3/blake3_air/links/air.v
index 44e2a880f..f2c6203d5 100644
--- a/CoqOfRust/plonky3/blake3_air/links/air.v
+++ b/CoqOfRust/plonky3/blake3_air/links/air.v
@@ -19,15 +19,13 @@ Module Blake3Air.
   Inductive t : Set :=
   | Make.
 
-  Parameter to_value : t -> Value.t.
-
   Global Instance IsLink : Link t := {
   (* TODO: fix path here *)
-    Φ := Ty.path "plonky3::blake3_air::air::Blake3Air";
-    φ := to_value;
+    Φ := Ty.path "p3_blake3_air::air::Blake3Air";
+    φ _ := Value.StructRecord "p3_blake3_air::air::Blake3Air" [] [] [];
   }.
 
-  Definition of_ty : OfTy.t (Ty.path "plonky3::blake3_air::air::Blake3Air").
+  Definition of_ty : OfTy.t (Ty.path "p3_blake3_air::air::Blake3Air").
   Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
   Smpl Add apply of_ty : of_ty. 
 End Blake3Air.
diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index 69a44517c..b0b8ac0c4 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -2,7 +2,10 @@ Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
 Require Import plonky3.blake3_air.columns.
 
-(* TODO: check where is U32_LIMBS *)
+(* TODO: 
+- check where is U32_LIMBS 
+- change `to_value` into concrete definition(?)
+*)
 
 (* 
 pub(crate) struct QuarterRound<'a, T, U> {
@@ -48,13 +51,13 @@ Module QuarterRound.
   Parameter to_value : forall {T U : Set}, t T U -> Value.t.
 
   Global Instance IsLink (T U : Set) `{Link T} `{Link U} : Link (t T U) := {
-    Φ := Ty.apply (Ty.path "plonky3::blake3_air::columns::QuarterRound") [] [ Φ T; Φ U ];
+    Φ := Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ Φ T; Φ U ];
     φ := to_value;
   }.
 
   Definition of_ty (T_ty U_ty : Ty.t) :
     OfTy.t T_ty -> OfTy.t U_ty ->
-    OfTy.t (Ty.apply (Ty.path "plonky3::blake3_air::columns::QuarterRound") [] [ T_ty ; U_ty ]).
+    OfTy.t (Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ T_ty ; U_ty ]).
   Proof. intros [T] [U]. eapply OfTy.Make with (A := t T U). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 End QuarterRound.
@@ -79,13 +82,13 @@ Module Blake3State.
   Parameter to_value : forall {T : Set}, t T -> Value.t.
 
   Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
-    Φ := Ty.apply (Ty.path "plonky3::blake3_air::columns::Blake3State") [] [ Φ T ];
+    Φ := Ty.apply (Ty.path "p3_blake3_air::columns::Blake3State") [] [ Φ T ];
     φ := to_value;
   }.
 
   Definition of_ty (T_ty : Ty.t) :
     OfTy.t T_ty -> 
-    OfTy.t (Ty.apply (Ty.path "plonky3::blake3_air::columns::Blake3State") [] [ T_ty ]).
+    OfTy.t (Ty.apply (Ty.path "p3_blake3_air::columns::Blake3State") [] [ T_ty ]).
   Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 End Blake3State.
@@ -110,13 +113,13 @@ Module FullRound.
   Parameter to_value : forall {T : Set}, t T -> Value.t.
 
   Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
-    Φ := Ty.apply (Ty.path "plonky3::blake3_air::columns::FullRound") [] [ Φ T ];
+    Φ := Ty.apply (Ty.path "p3_blake3_air::columns::FullRound") [] [ Φ T ];
     φ := to_value;
   }.
 
   Definition of_ty (T_ty : Ty.t) :
     OfTy.t T_ty -> 
-    OfTy.t (Ty.apply (Ty.path "plonky3::blake3_air::columns::FullRound") [] [ T_ty ]).
+    OfTy.t (Ty.apply (Ty.path "p3_blake3_air::columns::FullRound") [] [ T_ty ]).
   Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 End FullRound.
\ No newline at end of file
diff --git a/CoqOfRust/plonky3/field/links/field.v b/CoqOfRust/plonky3/field/links/field.v
index 44f6db4ff..a5897c4c4 100644
--- a/CoqOfRust/plonky3/field/links/field.v
+++ b/CoqOfRust/plonky3/field/links/field.v
@@ -81,7 +81,7 @@ pub trait Field:
 *)
 Module Field.
   Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
-    ("plonky3::field::field::Field", [], [], Φ Self).
+    ("p3_field::field::Field", [], [], Φ Self).
 
   Class Run (Self : Set) `{Link Self} : Set := {
   }.
@@ -106,7 +106,7 @@ pub trait PrimeField:
 *)
 Module PrimeField.
   Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
-    ("plonky3::field::field::PrimeField", [], [], Φ Self).
+    ("p3_field::field::PrimeField", [], [], Φ Self).
 
   Class Run (Self : Set) `{Link Self} : Set := {
     run_Field_for_PrimeField : Field.Run Self;
@@ -130,7 +130,7 @@ Module PrimeField64.
   | Make.
 
   Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
-    ("plonky3::field::field::PrimeField64", [], [], Φ Self).
+    ("p3_field::field::PrimeField64", [], [], Φ Self).
 
   (* const ORDER_U64: u64; *)
   Definition run_ORDER_U64 (Self : Set) `{Link Self} : Set :=

From 4b36cad851cd756cc4749cbe0b73562fae13bb17 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 19 May 2025 21:13:28 +0800
Subject: [PATCH 08/19] minor: comments

---
 CoqOfRust/plonky3/blake3_air/links/air.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/air.v b/CoqOfRust/plonky3/blake3_air/links/air.v
index f2c6203d5..5622caa13 100644
--- a/CoqOfRust/plonky3/blake3_air/links/air.v
+++ b/CoqOfRust/plonky3/blake3_air/links/air.v
@@ -9,9 +9,7 @@ Require Import plonky3.matrix.links.dense.
 (* 
 TODO:
 - Refer to `gas` to deal with different impls
-- For all dependencies, fix their type path to actual path that starts with `p_3`
 - Check if AirBuilder needs `AB_types`
-- Check occurences for `of_ty` as in `dense`
 *)
 
 (* pub struct Blake3Air {} *)
@@ -20,7 +18,6 @@ Module Blake3Air.
   | Make.
 
   Global Instance IsLink : Link t := {
-  (* TODO: fix path here *)
     Φ := Ty.path "p3_blake3_air::air::Blake3Air";
     φ _ := Value.StructRecord "p3_blake3_air::air::Blake3Air" [] [] [];
   }.

From 4a13161f0bb3100b0ed2ec85c0b4b91ff6f49f30 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 21 May 2025 09:04:13 +0800
Subject: [PATCH 09/19] draft: save progress

---
 CoqOfRust/plonky3/blake3_air/links/columns.v  | 230 ++++++++++++++++--
 .../plonky3/blake3_air/links/constants.v      |  17 ++
 2 files changed, 232 insertions(+), 15 deletions(-)
 create mode 100644 CoqOfRust/plonky3/blake3_air/links/constants.v

diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index b0b8ac0c4..a483ee8ac 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -1,10 +1,13 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import core.links.array.
+Require Import plonky3.blake3_air.links.constants.
 Require Import plonky3.blake3_air.columns.
 
+Definition U32_LIMBS := links.constants.U32_LIMBS.
+
 (* TODO: 
 - check where is U32_LIMBS 
-- change `to_value` into concrete definition(?)
 *)
 
 (* 
@@ -29,8 +32,22 @@ pub(crate) struct QuarterRound<'a, T, U> {
     pub d_output: &'a [T; 32],
 }
 *)
+Module test.
+  Record t {T U : Set} `{Link T} `{Link U} : Set := {
+    a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
+  }.
+
+  Lemma of_value_with {T U : Set} `{Link T} `{Link U}
+    a a' :
+    a' = φ a -> Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
+    ("a", a')
+    ] = φ (Build_t a).
+  Admitted.
+End test.
 Module QuarterRound.
-  Record t (T U : Set) : Set := {
+  (* NOTE: here we provide link instance for T and U or otherwise Coq cannot recognize
+  instances for arrays of them *)
+  Record t {T U : Set} `{Link T} `{Link U} : Set := {
     a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
     b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
     c : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
@@ -48,20 +65,153 @@ Module QuarterRound.
   }.
   Arguments t : clear implicits.
 
-  Parameter to_value : forall {T U : Set}, t T U -> Value.t.
-
-  Global Instance IsLink (T U : Set) `{Link T} `{Link U} : Link (t T U) := {
+  (* NOTE: the result from definition above is that it needs two extra Link instance for T and U here(???) *)
+  Global Instance IsLink (T U : Set) `{Link T} `{Link U} : Link (t T U _ _)
+  := {
     Φ := Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ Φ T; Φ U ];
-    φ := to_value;
+    φ x :=
+      Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
+        ("a", φ x.(a));
+        ("b", φ x.(b));
+        ("c", φ x.(c));
+        ("d", φ x.(d));
+        ("m_two_i", φ x.(m_two_i));
+        ("a_prime", φ x.(a_prime));
+        ("b_prime", φ x.(b_prime));
+        ("c_prime", φ x.(c_prime));
+        ("d_prime", φ x.(d_prime));
+        ("m_two_i_plus_one", φ x.(m_two_i_plus_one));
+        ("a_output", φ x.(a_output));
+        ("b_output", φ x.(b_output));
+        ("c_output", φ x.(c_output));
+        ("d_output", φ x.(d_output))
+      ];
   }.
 
   Definition of_ty (T_ty U_ty : Ty.t) :
     OfTy.t T_ty -> OfTy.t U_ty ->
     OfTy.t (Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ T_ty ; U_ty ]).
-  Proof. intros [T] [U]. eapply OfTy.Make with (A := t T U). now subst. Defined.
+  Proof. intros [T] [U]. eapply OfTy.Make with (A := t T U _ _). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
-End QuarterRound.
 
+  (* 
+    Lemma of_value_with limit limit' remaining remaining' refunded refunded' memory memory' :
+    limit' = φ limit ->
+    remaining' = φ remaining ->
+    refunded' = φ refunded ->
+    memory' = φ memory ->
+    Value.StructRecord "revm_interpreter::gas::Gas" [] [] [
+      ("limit", limit');
+      ("remaining", remaining');
+      ("refunded", refunded');
+      ("memory", memory')
+    ] = φ (Build_t limit remaining refunded memory).
+  Proof. now intros; subst. Qed.
+  Smpl Add apply of_value_with : of_value.
+  *)
+
+  Lemma of_value_with {T U : Set} `{Link T} `{Link U}
+    a a'
+    b b'
+    c c'
+    d d'
+    m_two_i m_two_i'
+    a_prime a_prime'
+    b_prime b_prime'
+    c_prime c_prime'
+    d_prime d_prime'
+    m_two_i_plus_one m_two_i_plus_one'
+    a_output a_output'
+    b_output b_output'
+    c_output c_output'
+    d_output d_output' :
+      a' = φ a ->
+      b' = φ b ->
+      c' = φ c ->
+      d' = φ d ->
+      m_two_i' = φ m_two_i ->
+      a_prime' = φ a_prime ->
+      b_prime' = φ b_prime ->
+      c_prime' = φ c_prime ->
+      d_prime' = φ d_prime ->
+      m_two_i_plus_one' = φ m_two_i_plus_one ->
+      a_output' = φ a_output ->
+      b_output' = φ b_output ->
+      c_output' = φ c_output ->
+      d_output' = φ d_output ->
+    Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
+      ("a", a');
+      ("b", b');
+      ("c", c');
+      ("d", d');
+      ("m_two_i", m_two_i');
+      ("a_prime", a_prime');
+      ("b_prime", b_prime');
+      ("c_prime", c_prime');
+      ("d_prime", d_prime');
+      ("m_two_i_plus_one", m_two_i_plus_one');
+      ("a_output", a_output');
+      ("b_output", b_output');
+      ("c_output", c_output');
+      ("d_output", d_output');
+    ] = φ (Build_t a b c d m_two_i a_prime b_prime c_prime d_prime 
+      m_two_i_plus_one a_output b_output c_output d_output).
+  Proof. now intros; subst. Qed.
+  Smpl Add apply of_value_with : of_value.
+
+  (* NOTE: for future reference, deleting link instances will report errors about undefined evars *)
+  Definition of_value {T U : Set} `{Link T} `{Link U}
+    (a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) (a' : Value.t)
+    (b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32|}))  (b' : Value.t)
+    (c : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS))  (c' : Value.t)
+    (d : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32|}))  (d' : Value.t)
+    (m_two_i : Ref.t Pointer.Kind.Ref (array.t U {| Integer.value := 32 |})) (m_two_i' : Value.t)
+    (a_prime : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) (a_prime' : Value.t)
+    (b_prime : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |})) (b_prime' : Value.t)
+    (c_prime : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) (c_prime' : Value.t)
+    (d_prime : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |})) (d_prime' : Value.t)
+    (m_two_i_plus_one : Ref.t Pointer.Kind.Ref (array.t U {| Integer.value := 32 |})) (m_two_i_plus_one' : Value.t)
+    (a_output : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) (a_output' : Value.t)
+    (b_output : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |})) (b_output' : Value.t)
+    (c_output : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) (c_output' : Value.t)
+    (d_output : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |})) (d_output' : Value.t)
+    :
+      a' = φ a ->
+      b' = φ b ->
+      c' = φ c ->
+      d' = φ d ->
+      m_two_i' = φ m_two_i ->
+      a_prime' = φ a_prime ->
+      b_prime' = φ b_prime ->
+      c_prime' = φ c_prime ->
+      d_prime' = φ d_prime ->
+      m_two_i_plus_one' = φ m_two_i_plus_one ->
+      a_output' = φ a_output ->
+      b_output' = φ b_output ->
+      c_output' = φ c_output ->
+      d_output' = φ d_output ->
+    OfValue.t (
+      Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
+        ("a", a');
+        ("b", b');
+        ("c", c');
+        ("d", d');
+        ("m_two_i", m_two_i');
+        ("a_prime", a_prime');
+        ("b_prime", b_prime');
+        ("c_prime", c_prime');
+        ("d_prime", d_prime');
+        ("m_two_i_plus_one", m_two_i_plus_one');
+        ("a_output", a_output');
+        ("b_output", b_output');
+        ("c_output", c_output');
+        ("d_output", d_output')
+      ]
+    ).
+  Proof. econstructor; apply of_value_with; eassumption. Defined.
+  Smpl Add apply of_value : of_value.
+End QuarterRound.
+ 
 (* 
 pub struct Blake3State<T> {
     pub row0: [[T; U32_LIMBS]; 4],
@@ -79,11 +229,15 @@ Module Blake3State.
   }.
   Arguments t : clear implicits.
 
-  Parameter to_value : forall {T : Set}, t T -> Value.t.
-
-  Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
+  Global Instance IsLink (T U : Set) `{Link T} : Link (t T) := {
     Φ := Ty.apply (Ty.path "p3_blake3_air::columns::Blake3State") [] [ Φ T ];
-    φ := to_value;
+    φ x :=
+      Value.StructRecord "p3_blake3_air::columns::Blake3State" [] [] [
+        ("row0", φ x.(row0));
+        ("row1", φ x.(row1));
+        ("row2", φ x.(row2));
+        ("row3", φ x.(row3));
+      ];
   }.
 
   Definition of_ty (T_ty : Ty.t) :
@@ -91,6 +245,27 @@ Module Blake3State.
     OfTy.t (Ty.apply (Ty.path "p3_blake3_air::columns::Blake3State") [] [ T_ty ]).
   Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
+
+  Definition of_value {T : Set}
+    (row0 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |}) row0'
+    (row1 : array.t (array.t T {| Integer.value := 32 |}) {| Integer.value := 4 |}) row1'
+    (row2 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |}) row2'
+    (row3 : array.t (array.t T {| Integer.value := 32 |}) {| Integer.value := 4 |}) row3'
+    :
+    row0' = φ row0 ->
+    row1' = φ row1 ->
+    row2' = φ row2 ->
+    row3' = φ row3 ->
+    OfValue.t (
+      Value.StructRecord "p3_blake3_air::columns::Blake3State" [] [] [
+        ("row0", row0');
+        ("row1", row1');
+        ("row2", row2');
+        ("row3", row3');
+      ]
+    ).
+  Proof. econstructor; apply of_value_with; eassumption. Defined.
+  Smpl Add apply of_value : of_value.
 End Blake3State.
 
 (* 
@@ -110,11 +285,15 @@ Module FullRound.
   }.
   Arguments t : clear implicits.
 
-  Parameter to_value : forall {T : Set}, t T -> Value.t.
-
   Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
     Φ := Ty.apply (Ty.path "p3_blake3_air::columns::FullRound") [] [ Φ T ];
-    φ := to_value;
+    φ x :=
+      Value.StructRecord "p3_blake3_air::columns::FullRound" [] [] [
+        ("state_prime", φ x.(state_prime));
+        ("state_middle", φ x.(state_middle));
+        ("state_middle_prime", φ x.(state_middle_prime));
+        ("state_output", φ x.(state_output));
+      ];
   }.
 
   Definition of_ty (T_ty : Ty.t) :
@@ -122,4 +301,25 @@ Module FullRound.
     OfTy.t (Ty.apply (Ty.path "p3_blake3_air::columns::FullRound") [] [ T_ty ]).
   Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
+
+  Definition of_value {T : Set}
+    (state_prime : Blake3State.t T) state_prime'
+    (state_middle : Blake3State.t T) state_middle'
+    (state_middle_prime : Blake3State.t T) state_middle_prime'
+    (state_output : Blake3State.t T) state_output'
+  :
+    state_prime' = φ state_prime ->
+    state_middle' = φ state_middle ->
+    state_middle_prime' = φ state_middle_prime ->
+    state_output' = φ state_output ->
+    OfValue.t (
+      Value.StructRecord "p3_blake3_air::columns::FullRound"" [] [] [
+        ("state_prime", state_prime');
+        ("state_middle", state_middle');
+        ("state_middle_prime", state_middle_prime');
+        ("state_output", state_output');
+      ]
+    ).
+  Proof. econstructor; apply of_value_with; eassumption. Defined.
+  Smpl Add apply of_value : of_value.
 End FullRound.
\ No newline at end of file
diff --git a/CoqOfRust/plonky3/blake3_air/links/constants.v b/CoqOfRust/plonky3/blake3_air/links/constants.v
new file mode 100644
index 000000000..92b0ce8bf
--- /dev/null
+++ b/CoqOfRust/plonky3/blake3_air/links/constants.v
@@ -0,0 +1,17 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import plonky3.blake3_air.constants.
+
+(* 
+pub const BITS_PER_LIMB: usize = 16;
+pub const U32_LIMBS: usize = 32 / BITS_PER_LIMB;
+*)
+Definition BITS_PER_LIMB : Usize.t := {|
+  Integer.value := 16;
+|}.
+Definition U32_LIMBS : Usize.t := {|
+  Integer.value := 2;
+|}.
+
+Module test. 
+End test.
\ No newline at end of file

From eb971fa78d508a60f3c683b7220364e420322582 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 21 May 2025 19:45:54 +0800
Subject: [PATCH 10/19] minor: progress on `columns`

---
 CoqOfRust/plonky3/blake3_air/links/columns.v | 36 +++++++++-----------
 1 file changed, 16 insertions(+), 20 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index a483ee8ac..d83d40851 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -32,18 +32,29 @@ pub(crate) struct QuarterRound<'a, T, U> {
     pub d_output: &'a [T; 32],
 }
 *)
-Module test.
+(* NOTE: this is an example to explain what error happened in the actual code *)
+Module test_error.
+  (* First of all, we have to provide link instances for T U otherwise Coq cannot find an 
+    instance for `Ref (array.t T _)` *)
   Record t {T U : Set} `{Link T} `{Link U} : Set := {
     a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
   }.
 
+  (* When defining `of_value_with`, comparing to definitions in `gas` where entry types 
+    are being auto deducted, here we also need to provide instances for link T and U. *)
   Lemma of_value_with {T U : Set} `{Link T} `{Link U}
     a a' :
     a' = φ a -> Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
     ("a", a')
-    ] = φ (Build_t a).
-  Admitted.
-End test.
+    ] = 
+    (* The actual issue here is parameters for `Build_t`. Seems like it has 5 parameter:
+    Build_t (T U : Set) `{Link T} `{Link U} (a : Ref.t (...))
+    And I don't know how to correctly provide the Link T and U instances.
+    *)
+    φ (Build_t T U _ _ a).
+  Proof. Admitted.
+End test_error.
+
 Module QuarterRound.
   (* NOTE: here we provide link instance for T and U or otherwise Coq cannot recognize
   instances for arrays of them *)
@@ -94,22 +105,7 @@ Module QuarterRound.
   Proof. intros [T] [U]. eapply OfTy.Make with (A := t T U _ _). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 
-  (* 
-    Lemma of_value_with limit limit' remaining remaining' refunded refunded' memory memory' :
-    limit' = φ limit ->
-    remaining' = φ remaining ->
-    refunded' = φ refunded ->
-    memory' = φ memory ->
-    Value.StructRecord "revm_interpreter::gas::Gas" [] [] [
-      ("limit", limit');
-      ("remaining", remaining');
-      ("refunded", refunded');
-      ("memory", memory')
-    ] = φ (Build_t limit remaining refunded memory).
-  Proof. now intros; subst. Qed.
-  Smpl Add apply of_value_with : of_value.
-  *)
-
+  (* NOTE: stuck *)
   Lemma of_value_with {T U : Set} `{Link T} `{Link U}
     a a'
     b b'

From b3fb8ef0445aaed26b5a8af68e561ab1532b5142 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 21 May 2025 23:55:32 +0800
Subject: [PATCH 11/19] minor: progress

---
 CoqOfRust/plonky3/blake3_air/links/columns.v | 86 +++++++++++++++-----
 1 file changed, 64 insertions(+), 22 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index d83d40851..e9c5644f4 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -32,27 +32,69 @@ pub(crate) struct QuarterRound<'a, T, U> {
     pub d_output: &'a [T; 32],
 }
 *)
-(* NOTE: this is an example to explain what error happened in the actual code *)
 Module test_error.
-  (* First of all, we have to provide link instances for T U otherwise Coq cannot find an 
-    instance for `Ref (array.t T _)` *)
   Record t {T U : Set} `{Link T} `{Link U} : Set := {
     a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
+    b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
   }.
 
-  (* When defining `of_value_with`, comparing to definitions in `gas` where entry types 
-    are being auto deducted, here we also need to provide instances for link T and U. *)
-  Lemma of_value_with {T U : Set} `{Link T} `{Link U}
-    a a' :
-    a' = φ a -> Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
-    ("a", a')
-    ] = 
-    (* The actual issue here is parameters for `Build_t`. Seems like it has 5 parameter:
-    Build_t (T U : Set) `{Link T} `{Link U} (a : Ref.t (...))
-    And I don't know how to correctly provide the Link T and U instances.
-    *)
-    φ (Build_t T U _ _ a).
+  Global Instance IsLink (T U : Set) `{T_Link : Link T} `{U_Link : Link U} : Link (@t T U T_Link U_Link)
+  := {
+    Φ := Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ Φ T; Φ U ];
+    φ x :=
+      Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
+        ("a", φ x.(a));
+        ("b", φ x.(b))
+      ];
+  }.
+
+  Lemma of_value_with {T U : Set} `{T_Link : Link T} `{U_Link : Link U} 
+    a a' b b' :
+    a' = φ a ->
+    b' = φ b -> 
+    Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
+      ("a", a');
+      ("b", b')
+      ] 
+    = @φ (@t T U T_Link U_Link) (IsLink T U) (Build_t T U T_Link U_Link a b).
   Proof. Admitted.
+
+  Definition of_value {T U : Set} `{Link T} `{Link U}
+  (a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) a' 
+  (b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |})) b' :
+  a' = φ a ->
+  b' = φ b ->
+  OfValue.t (
+    Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
+      ("a", a');
+      ("b", b')
+    ]).
+  Proof. 
+  Set Typeclasses Debug.
+  intros Ha Hb.
+  (* econstructor. *)
+  (* 
+  Unable to unify
+  "Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] []
+      [("a", ?M1555); ("b", ?M1557)] =
+    (IsLink ?T ?U).(φ) {| a := ?M1554; b := ?M1556 |}"
+  with
+  "Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] []
+      [("a", a'); ("b", b')] = H0.(φ) ?value".
+  *)
+  (* 
+  Unable to unify
+   "Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] []
+      [("a", a'); ("b", b')] = (IsLink T U).(φ) {| a := a; b := b |}"
+  with
+   "Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] []
+      [("a", a'); ("b", b')] = H0.(φ) ?value".coqtop
+  *)
+  eapply (@of_value_with T U _ _ _ _ _ _ Ha Hb).
+  
+  econstructor;
+  Print of_value_with.
+  eapply (@of_value_with T U H H0 a a' b b' _ _); eassumption. Defined.
 End test_error.
 
 Module QuarterRound.
@@ -76,8 +118,7 @@ Module QuarterRound.
   }.
   Arguments t : clear implicits.
 
-  (* NOTE: the result from definition above is that it needs two extra Link instance for T and U here(???) *)
-  Global Instance IsLink (T U : Set) `{Link T} `{Link U} : Link (t T U _ _)
+  Global Instance IsLink (T U : Set) `{T_Link : Link T} `{U_Link : Link U} : Link (@t T U T_Link U_Link)
   := {
     Φ := Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ Φ T; Φ U ];
     φ x :=
@@ -105,8 +146,7 @@ Module QuarterRound.
   Proof. intros [T] [U]. eapply OfTy.Make with (A := t T U _ _). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 
-  (* NOTE: stuck *)
-  Lemma of_value_with {T U : Set} `{Link T} `{Link U}
+  Lemma of_value_with {T U : Set} `{T_Link : Link T} `{U_Link : Link U} 
     a a'
     b b'
     c c'
@@ -149,8 +189,10 @@ Module QuarterRound.
       ("a_output", a_output');
       ("b_output", b_output');
       ("c_output", c_output');
-      ("d_output", d_output');
-    ] = φ (Build_t a b c d m_two_i a_prime b_prime c_prime d_prime 
+      ("d_output", d_output')
+    ] = 
+    @φ (t T U T_Link U_Link) (IsLink T U) (Build_t T U T_Link U_Link
+    a b c d m_two_i a_prime b_prime c_prime d_prime 
       m_two_i_plus_one a_output b_output c_output d_output).
   Proof. now intros; subst. Qed.
   Smpl Add apply of_value_with : of_value.
@@ -204,7 +246,7 @@ Module QuarterRound.
         ("d_output", d_output')
       ]
     ).
-  Proof. econstructor; apply of_value_with; eassumption. Defined.
+  Proof. econstructor. apply (@of_value_with T U H H0). eassumption. Defined.
   Smpl Add apply of_value : of_value.
 End QuarterRound.
  

From e395c05326243f6bca232c28f8f444a7eab3e7a7 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 22 May 2025 19:53:10 +0800
Subject: [PATCH 12/19] feat : Add value instances for `columns`

---
 CoqOfRust/plonky3/blake3_air/links/columns.v | 139 ++++++++++++-------
 1 file changed, 89 insertions(+), 50 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index e9c5644f4..6437198ce 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -32,7 +32,7 @@ pub(crate) struct QuarterRound<'a, T, U> {
     pub d_output: &'a [T; 32],
 }
 *)
-Module test_error.
+Module test_case.
   Record t {T U : Set} `{Link T} `{Link U} : Set := {
     a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
     b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
@@ -59,7 +59,7 @@ Module test_error.
     = @φ (@t T U T_Link U_Link) (IsLink T U) (Build_t T U T_Link U_Link a b).
   Proof. Admitted.
 
-  Definition of_value {T U : Set} `{Link T} `{Link U}
+  Definition of_value {T U : Set} `{T_Link : Link T} `{U_Link : Link U}
   (a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) a' 
   (b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |})) b' :
   a' = φ a ->
@@ -69,37 +69,19 @@ Module test_error.
       ("a", a');
       ("b", b')
     ]).
-  Proof. 
-  Set Typeclasses Debug.
-  intros Ha Hb.
-  (* econstructor. *)
-  (* 
-  Unable to unify
-  "Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] []
-      [("a", ?M1555); ("b", ?M1557)] =
-    (IsLink ?T ?U).(φ) {| a := ?M1554; b := ?M1556 |}"
-  with
-  "Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] []
-      [("a", a'); ("b", b')] = H0.(φ) ?value".
-  *)
-  (* 
-  Unable to unify
-   "Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] []
-      [("a", a'); ("b", b')] = (IsLink T U).(φ) {| a := a; b := b |}"
-  with
-   "Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] []
-      [("a", a'); ("b", b')] = H0.(φ) ?value".coqtop
-  *)
-  eapply (@of_value_with T U _ _ _ _ _ _ Ha Hb).
-  
-  econstructor;
-  Print of_value_with.
-  eapply (@of_value_with T U H H0 a a' b b' _ _); eassumption. Defined.
-End test_error.
+  Proof.
+    (* Set Typeclasses Debug. *)
+    econstructor 1 with t (IsLink T U) _. 
+    apply (@of_value_with T U T_Link U_Link a a' b b' H H0). 
+  Defined.
+  Smpl Add apply of_value : of_value.
+End test_case.
 
 Module QuarterRound.
   (* NOTE: here we provide link instance for T and U or otherwise Coq cannot recognize
-  instances for arrays of them *)
+  instances for arrays of them(?)
+  Is there some way to avoid this, since this will cause much inconvenience when other
+  types are calling this? *)
   Record t {T U : Set} `{Link T} `{Link U} : Set := {
     a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
     b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
@@ -198,7 +180,7 @@ Module QuarterRound.
   Smpl Add apply of_value_with : of_value.
 
   (* NOTE: for future reference, deleting link instances will report errors about undefined evars *)
-  Definition of_value {T U : Set} `{Link T} `{Link U}
+  Definition of_value {T U : Set} `{T_Link : Link T} `{U_Link : Link U}
     (a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) (a' : Value.t)
     (b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32|}))  (b' : Value.t)
     (c : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS))  (c' : Value.t)
@@ -246,7 +228,10 @@ Module QuarterRound.
         ("d_output", d_output')
       ]
     ).
-  Proof. econstructor. apply (@of_value_with T U H H0). eassumption. Defined.
+  Proof. 
+  econstructor 1 with (t T U T_Link U_Link) (IsLink T U) _.
+  eapply (@of_value_with T U T_Link U_Link a a' b b' _ _).
+  all: eassumption. Defined.
   Smpl Add apply of_value : of_value.
 End QuarterRound.
  
@@ -259,7 +244,7 @@ pub struct Blake3State<T> {
 }
 *)
 Module Blake3State.
-  Record t (T : Set) : Set := {
+  Record t {T : Set} : Set := {
     row0 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |};
     row1 : array.t (array.t T {| Integer.value := 32 |}) {| Integer.value := 4 |};
     row2 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |};
@@ -267,14 +252,14 @@ Module Blake3State.
   }.
   Arguments t : clear implicits.
 
-  Global Instance IsLink (T U : Set) `{Link T} : Link (t T) := {
+  Global Instance IsLink (T : Set) `{T_Link : Link T} : Link (t T) := {
     Φ := Ty.apply (Ty.path "p3_blake3_air::columns::Blake3State") [] [ Φ T ];
     φ x :=
       Value.StructRecord "p3_blake3_air::columns::Blake3State" [] [] [
         ("row0", φ x.(row0));
         ("row1", φ x.(row1));
         ("row2", φ x.(row2));
-        ("row3", φ x.(row3));
+        ("row3", φ x.(row3))
       ];
   }.
 
@@ -284,7 +269,21 @@ Module Blake3State.
   Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 
-  Definition of_value {T : Set}
+  Lemma of_value_with {T : Set} `{T_Link : Link T} 
+    row0 row0' row1 row1' row2 row2' row3 row3' :
+    row0' = φ row0 ->
+    row1' = φ row1 ->
+    row2' = φ row2 ->
+    row3' = φ row3 ->
+    Value.StructRecord "p3_blake3_air::columns::Blake3State" [] [] [
+      ("row0", row0');
+      ("row1", row1');
+      ("row2", row2');
+      ("row3", row3')]
+    = φ (Build_t T row0 row1 row2 row3).
+  Proof. Admitted.
+
+  Definition of_value {T : Set} `{T_Link : Link T}
     (row0 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |}) row0'
     (row1 : array.t (array.t T {| Integer.value := 32 |}) {| Integer.value := 4 |}) row1'
     (row2 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |}) row2'
@@ -299,10 +298,13 @@ Module Blake3State.
         ("row0", row0');
         ("row1", row1');
         ("row2", row2');
-        ("row3", row3');
+        ("row3", row3')
       ]
     ).
-  Proof. econstructor; apply of_value_with; eassumption. Defined.
+  Proof. 
+  econstructor 1 with (t T) (IsLink T) _. 
+  eapply (@of_value_with T T_Link row0 row0' row1 row1' row2 row2' row3 row3').
+  all: eassumption. Defined.
   Smpl Add apply of_value : of_value.
 End Blake3State.
 
@@ -327,10 +329,10 @@ Module FullRound.
     Φ := Ty.apply (Ty.path "p3_blake3_air::columns::FullRound") [] [ Φ T ];
     φ x :=
       Value.StructRecord "p3_blake3_air::columns::FullRound" [] [] [
-        ("state_prime", φ x.(state_prime));
-        ("state_middle", φ x.(state_middle));
-        ("state_middle_prime", φ x.(state_middle_prime));
-        ("state_output", φ x.(state_output));
+        ("state_prime", φ x.(state_prime T));
+        ("state_middle", φ x.(state_middle T));
+        ("state_middle_prime", φ x.(state_middle_prime T));
+        ("state_output", φ x.(state_output T))
       ];
   }.
 
@@ -340,24 +342,61 @@ Module FullRound.
   Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 
-  Definition of_value {T : Set}
+  Lemma of_value_with {T : Set} `{T_Link : Link T} 
+    state_prime state_prime'
+    state_middle state_middle'
+    state_middle_prime state_middle_prime'
+    state_output state_output' :
+    state_prime' = φ state_prime ->
+    state_middle' = φ state_middle ->
+    state_middle_prime' = φ state_middle_prime ->
+    state_output' = φ state_output ->
+    Value.StructRecord "p3_blake3_air::columns::FullRound" [] [] [
+      ("state_prime", state_prime');
+      ("state_middle", state_middle');
+      ("state_middle_prime", state_middle_prime');
+      ("state_output", state_output')]
+    = φ (Build_t T state_prime state_middle state_middle_prime state_output).
+    Proof. Admitted.
+
+  (* Definition of_value {T U : Set} `{T_Link : Link T} `{U_Link : Link U}
+  (a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) a' 
+  (b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |})) b' :
+  a' = φ a ->
+  b' = φ b ->
+  OfValue.t (
+    Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
+      ("a", a');
+      ("b", b')
+    ]).
+  Proof.
+  (* Set Typeclasses Debug. *)
+  econstructor 1 with t (IsLink T U) _;
+  eapply (@of_value_with T U T_Link U_Link a a' b b' _ _). Unshelve.
+  all: eassumption. Defined.
+  Smpl Add apply of_value : of_value. *)
+
+  Definition of_value {T : Set} `{T_Link : Link T}
     (state_prime : Blake3State.t T) state_prime'
     (state_middle : Blake3State.t T) state_middle'
     (state_middle_prime : Blake3State.t T) state_middle_prime'
-    (state_output : Blake3State.t T) state_output'
-  :
+    (state_output : Blake3State.t T) state_output' :
     state_prime' = φ state_prime ->
     state_middle' = φ state_middle ->
     state_middle_prime' = φ state_middle_prime ->
     state_output' = φ state_output ->
     OfValue.t (
-      Value.StructRecord "p3_blake3_air::columns::FullRound"" [] [] [
+      Value.StructRecord "p3_blake3_air::columns::FullRound" [] [] [
         ("state_prime", state_prime');
         ("state_middle", state_middle');
         ("state_middle_prime", state_middle_prime');
-        ("state_output", state_output');
-      ]
-    ).
-  Proof. econstructor; apply of_value_with; eassumption. Defined.
+        ("state_output", state_output')
+      ]).
+  Proof. 
+    econstructor 1 with (t T) (IsLink T) _.
+    eapply (@of_value_with T T_Link state_prime state_prime' state_middle 
+      state_middle' state_middle_prime state_middle_prime' 
+      state_output state_output').
+    all: eassumption. Defined.
   Smpl Add apply of_value : of_value.
 End FullRound.
\ No newline at end of file

From 49e7918618ff5711c6a2320583e9016f56aecf99 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 22 May 2025 19:53:46 +0800
Subject: [PATCH 13/19] minor: delete test case in `columns`

---
 CoqOfRust/plonky3/blake3_air/links/columns.v | 45 --------------------
 1 file changed, 45 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index 6437198ce..d43e85ba5 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -32,51 +32,6 @@ pub(crate) struct QuarterRound<'a, T, U> {
     pub d_output: &'a [T; 32],
 }
 *)
-Module test_case.
-  Record t {T U : Set} `{Link T} `{Link U} : Set := {
-    a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
-    b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
-  }.
-
-  Global Instance IsLink (T U : Set) `{T_Link : Link T} `{U_Link : Link U} : Link (@t T U T_Link U_Link)
-  := {
-    Φ := Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ Φ T; Φ U ];
-    φ x :=
-      Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
-        ("a", φ x.(a));
-        ("b", φ x.(b))
-      ];
-  }.
-
-  Lemma of_value_with {T U : Set} `{T_Link : Link T} `{U_Link : Link U} 
-    a a' b b' :
-    a' = φ a ->
-    b' = φ b -> 
-    Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
-      ("a", a');
-      ("b", b')
-      ] 
-    = @φ (@t T U T_Link U_Link) (IsLink T U) (Build_t T U T_Link U_Link a b).
-  Proof. Admitted.
-
-  Definition of_value {T U : Set} `{T_Link : Link T} `{U_Link : Link U}
-  (a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) a' 
-  (b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |})) b' :
-  a' = φ a ->
-  b' = φ b ->
-  OfValue.t (
-    Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
-      ("a", a');
-      ("b", b')
-    ]).
-  Proof.
-    (* Set Typeclasses Debug. *)
-    econstructor 1 with t (IsLink T U) _. 
-    apply (@of_value_with T U T_Link U_Link a a' b b' H H0). 
-  Defined.
-  Smpl Add apply of_value : of_value.
-End test_case.
-
 Module QuarterRound.
   (* NOTE: here we provide link instance for T and U or otherwise Coq cannot recognize
   instances for arrays of them(?)

From 6f09a78cb62a809a7f1d4d63282de6f4ebe107e3 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 22 May 2025 19:54:29 +0800
Subject: [PATCH 14/19] minor: delete comment

---
 CoqOfRust/plonky3/blake3_air/links/columns.v | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index d43e85ba5..381abc051 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -314,23 +314,6 @@ Module FullRound.
     = φ (Build_t T state_prime state_middle state_middle_prime state_output).
     Proof. Admitted.
 
-  (* Definition of_value {T U : Set} `{T_Link : Link T} `{U_Link : Link U}
-  (a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) a' 
-  (b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |})) b' :
-  a' = φ a ->
-  b' = φ b ->
-  OfValue.t (
-    Value.StructRecord "p3_blake3_air::columns::QuarterRound" [] [] [
-      ("a", a');
-      ("b", b')
-    ]).
-  Proof.
-  (* Set Typeclasses Debug. *)
-  econstructor 1 with t (IsLink T U) _;
-  eapply (@of_value_with T U T_Link U_Link a a' b b' _ _). Unshelve.
-  all: eassumption. Defined.
-  Smpl Add apply of_value : of_value. *)
-
   Definition of_value {T : Set} `{T_Link : Link T}
     (state_prime : Blake3State.t T) state_prime'
     (state_middle : Blake3State.t T) state_middle'

From 31a99d225ed0e79f38dbb8d8eff7217a80d8e5f4 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 22 May 2025 21:15:43 +0800
Subject: [PATCH 15/19] feat: Compile `air`

---
 CoqOfRust/plonky3/blake3_air/links/air.v | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/air.v b/CoqOfRust/plonky3/blake3_air/links/air.v
index 5622caa13..ea03ea828 100644
--- a/CoqOfRust/plonky3/blake3_air/links/air.v
+++ b/CoqOfRust/plonky3/blake3_air/links/air.v
@@ -62,6 +62,7 @@ Module Impl_Blake3Air.
     (* TODO: check if AirBuilder needs `AB_types` *)
     (self : Ref.t Pointer.Kind.Ref Self) 
     (builder : Ref.t Pointer.Kind.MutRef AB) 
+    (* TODO: in the future, refer to revm to see if its possible to change ab into airbuilder *)
     (* TODO: translate `trace: &QuarterRound<<AB as AirBuilder>::Var, <AB as AirBuilder>::Expr>` *)
     (trace : Set)
     :
@@ -84,17 +85,17 @@ Module Impl_Blake3Air.
   *)
   Instance run_full_round_to_column_quarter_round
   (* NOTE: seems like there are some issues with T and U being defined here *)
-    {T U : Set} `{Link T}  `{Link U}
+    {T U : Set} `{T_Link : Link T}  `{U_Link : Link U}
     (self : Ref.t Pointer.Kind.Ref Self) 
     (input : Ref.t Pointer.Kind.Ref (Blake3State.t T))
     (round_data : Ref.t Pointer.Kind.Ref (FullRound.t T))
-    (m_vector : Ref.t Pointer.Kind.Ref (array.t (array.t U {| Integer.value := 2 |}) {| Integer.value := 16 |})
+    (m_vector : Ref.t Pointer.Kind.Ref (array.t (array.t U {| Integer.value := 2 |}) {| Integer.value := 16 |}))
     (index : Usize.t)
     :
     Run.Trait
       blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.full_round_to_column_quarter_round [] [ Φ T; Φ U ] 
       [ (* φ input; φ round_data; φ m_vector; φ index *) ]
-      (QuarterRound.t T U).
+      (QuarterRound.t T U T_Link U_Link).
   Proof.
     constructor.
     run_symbolic.
@@ -109,16 +110,16 @@ Module Impl_Blake3Air.
   ) -> QuarterRound<'a, T, U> 
   *)
   Instance run_full_round_to_diagonal_quarter_round
-    {T U : Set} `{Link T}  `{Link U}
+    {T U : Set} `{T_Link : Link T}  `{U_Link : Link U}
     (self : Ref.t Pointer.Kind.Ref Self) 
     (round_data : Ref.t Pointer.Kind.Ref (FullRound.t T))
-    (m_vector : Ref.t Pointer.Kind.Ref (array.t (array.t U {| Integer.value := 2 |}) {| Integer.value := 16 |})
+    (m_vector : Ref.t Pointer.Kind.Ref (array.t (array.t U {| Integer.value := 2 |}) {| Integer.value := 16 |}))
     (index : Usize.t)
     :
     Run.Trait
       blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.full_round_to_diagonal_quarter_round [] [ Φ T; Φ U ] 
       [ (* φ input; φ round_data; φ m_vector; φ index *) ]
-      (QuarterRound.t T U).
+      (QuarterRound.t T U T_Link U_Link).
   Proof.
     constructor.
     run_symbolic.

From 4fa1b359c60bcf84f12844a0d35339b613d6d019 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sat, 24 May 2025 08:40:53 +0800
Subject: [PATCH 16/19] minor: update `constants`

---
 CoqOfRust/plonky3/blake3_air/links/constants.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/constants.v b/CoqOfRust/plonky3/blake3_air/links/constants.v
index 92b0ce8bf..e2510f9cb 100644
--- a/CoqOfRust/plonky3/blake3_air/links/constants.v
+++ b/CoqOfRust/plonky3/blake3_air/links/constants.v
@@ -11,7 +11,4 @@ Definition BITS_PER_LIMB : Usize.t := {|
 |}.
 Definition U32_LIMBS : Usize.t := {|
   Integer.value := 2;
-|}.
-
-Module test. 
-End test.
\ No newline at end of file
+|}.
\ No newline at end of file

From 6c4582edfce7f70d8a14a457ef2e3e21be117e8c Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sat, 24 May 2025 08:41:08 +0800
Subject: [PATCH 17/19] minor: comments

---
 CoqOfRust/plonky3/blake3_air/links/columns.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index 381abc051..1847cd11f 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -6,10 +6,6 @@ Require Import plonky3.blake3_air.columns.
 
 Definition U32_LIMBS := links.constants.U32_LIMBS.
 
-(* TODO: 
-- check where is U32_LIMBS 
-*)
-
 (* 
 pub(crate) struct QuarterRound<'a, T, U> {
     pub a: &'a [T; U32_LIMBS],

From 2a927230de75de58898a402551255050fec000ec Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sat, 24 May 2025 08:51:34 +0800
Subject: [PATCH 18/19] minor: delete link namings wrt comments

---
 CoqOfRust/plonky3/blake3_air/links/air.v     | 14 +++++------
 CoqOfRust/plonky3/blake3_air/links/columns.v | 26 ++++++++++----------
 2 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/air.v b/CoqOfRust/plonky3/blake3_air/links/air.v
index ea03ea828..76ff8c5d1 100644
--- a/CoqOfRust/plonky3/blake3_air/links/air.v
+++ b/CoqOfRust/plonky3/blake3_air/links/air.v
@@ -1,9 +1,9 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.links.M.
+Require Import plonky3.air.links.air.
 Require Import plonky3.blake3_air.air.
-Require Import plonky3.field.links.field.
 Require Import plonky3.blake3_air.links.columns.
-Require Import plonky3.air.links.air.
+Require Import plonky3.field.links.field.
 Require Import plonky3.matrix.links.dense.
 
 (* 
@@ -24,7 +24,7 @@ Module Blake3Air.
 
   Definition of_ty : OfTy.t (Ty.path "p3_blake3_air::air::Blake3Air").
   Proof. eapply OfTy.Make with (A := t); reflexivity. Defined.
-  Smpl Add apply of_ty : of_ty. 
+  Smpl Add apply of_ty : of_ty.
 End Blake3Air.
 
 Module Impl_Blake3Air.
@@ -85,7 +85,7 @@ Module Impl_Blake3Air.
   *)
   Instance run_full_round_to_column_quarter_round
   (* NOTE: seems like there are some issues with T and U being defined here *)
-    {T U : Set} `{T_Link : Link T}  `{U_Link : Link U}
+    {T U : Set} `{Link T} `{Link U}
     (self : Ref.t Pointer.Kind.Ref Self) 
     (input : Ref.t Pointer.Kind.Ref (Blake3State.t T))
     (round_data : Ref.t Pointer.Kind.Ref (FullRound.t T))
@@ -95,7 +95,7 @@ Module Impl_Blake3Air.
     Run.Trait
       blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.full_round_to_column_quarter_round [] [ Φ T; Φ U ] 
       [ (* φ input; φ round_data; φ m_vector; φ index *) ]
-      (QuarterRound.t T U T_Link U_Link).
+      (QuarterRound.t T U _ _).
   Proof.
     constructor.
     run_symbolic.
@@ -110,7 +110,7 @@ Module Impl_Blake3Air.
   ) -> QuarterRound<'a, T, U> 
   *)
   Instance run_full_round_to_diagonal_quarter_round
-    {T U : Set} `{T_Link : Link T}  `{U_Link : Link U}
+    {T U : Set} `{Link T}  `{Link U}
     (self : Ref.t Pointer.Kind.Ref Self) 
     (round_data : Ref.t Pointer.Kind.Ref (FullRound.t T))
     (m_vector : Ref.t Pointer.Kind.Ref (array.t (array.t U {| Integer.value := 2 |}) {| Integer.value := 16 |}))
@@ -119,7 +119,7 @@ Module Impl_Blake3Air.
     Run.Trait
       blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.full_round_to_diagonal_quarter_round [] [ Φ T; Φ U ] 
       [ (* φ input; φ round_data; φ m_vector; φ index *) ]
-      (QuarterRound.t T U T_Link U_Link).
+      (QuarterRound.t T U _ _).
   Proof.
     constructor.
     run_symbolic.
diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index 1847cd11f..c7c99fb48 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -51,7 +51,7 @@ Module QuarterRound.
   }.
   Arguments t : clear implicits.
 
-  Global Instance IsLink (T U : Set) `{T_Link : Link T} `{U_Link : Link U} : Link (@t T U T_Link U_Link)
+  Global Instance IsLink (T U : Set) `{Link T} `{Link U} : Link (@t T U _ _)
   := {
     Φ := Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ Φ T; Φ U ];
     φ x :=
@@ -79,7 +79,7 @@ Module QuarterRound.
   Proof. intros [T] [U]. eapply OfTy.Make with (A := t T U _ _). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 
-  Lemma of_value_with {T U : Set} `{T_Link : Link T} `{U_Link : Link U} 
+  Lemma of_value_with {T U : Set} `{Link T} `{Link U} 
     a a'
     b b'
     c c'
@@ -124,14 +124,14 @@ Module QuarterRound.
       ("c_output", c_output');
       ("d_output", d_output')
     ] = 
-    @φ (t T U T_Link U_Link) (IsLink T U) (Build_t T U T_Link U_Link
+    @φ (t T U _ _) (IsLink T U) (Build_t T U _ _
     a b c d m_two_i a_prime b_prime c_prime d_prime 
       m_two_i_plus_one a_output b_output c_output d_output).
   Proof. now intros; subst. Qed.
   Smpl Add apply of_value_with : of_value.
 
   (* NOTE: for future reference, deleting link instances will report errors about undefined evars *)
-  Definition of_value {T U : Set} `{T_Link : Link T} `{U_Link : Link U}
+  Definition of_value {T U : Set} `{Link T} `{Link U}
     (a : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS)) (a' : Value.t)
     (b : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32|}))  (b' : Value.t)
     (c : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS))  (c' : Value.t)
@@ -180,8 +180,8 @@ Module QuarterRound.
       ]
     ).
   Proof. 
-  econstructor 1 with (t T U T_Link U_Link) (IsLink T U) _.
-  eapply (@of_value_with T U T_Link U_Link a a' b b' _ _).
+  econstructor 1 with (t T U _ _) (IsLink T U) _.
+  eapply (@of_value_with T U _ _ a a' b b' _ _).
   all: eassumption. Defined.
   Smpl Add apply of_value : of_value.
 End QuarterRound.
@@ -203,7 +203,7 @@ Module Blake3State.
   }.
   Arguments t : clear implicits.
 
-  Global Instance IsLink (T : Set) `{T_Link : Link T} : Link (t T) := {
+  Global Instance IsLink (T : Set) `{Link T} : Link (t T) := {
     Φ := Ty.apply (Ty.path "p3_blake3_air::columns::Blake3State") [] [ Φ T ];
     φ x :=
       Value.StructRecord "p3_blake3_air::columns::Blake3State" [] [] [
@@ -220,7 +220,7 @@ Module Blake3State.
   Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 
-  Lemma of_value_with {T : Set} `{T_Link : Link T} 
+  Lemma of_value_with {T : Set} `{Link T} 
     row0 row0' row1 row1' row2 row2' row3 row3' :
     row0' = φ row0 ->
     row1' = φ row1 ->
@@ -234,7 +234,7 @@ Module Blake3State.
     = φ (Build_t T row0 row1 row2 row3).
   Proof. Admitted.
 
-  Definition of_value {T : Set} `{T_Link : Link T}
+  Definition of_value {T : Set} `{Link T}
     (row0 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |}) row0'
     (row1 : array.t (array.t T {| Integer.value := 32 |}) {| Integer.value := 4 |}) row1'
     (row2 : array.t (array.t T U32_LIMBS) {| Integer.value := 4 |}) row2'
@@ -254,7 +254,7 @@ Module Blake3State.
     ).
   Proof. 
   econstructor 1 with (t T) (IsLink T) _. 
-  eapply (@of_value_with T T_Link row0 row0' row1 row1' row2 row2' row3 row3').
+  eapply (@of_value_with T _ row0 row0' row1 row1' row2 row2' row3 row3').
   all: eassumption. Defined.
   Smpl Add apply of_value : of_value.
 End Blake3State.
@@ -293,7 +293,7 @@ Module FullRound.
   Proof. intros [T]. eapply OfTy.Make with (A := t T). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 
-  Lemma of_value_with {T : Set} `{T_Link : Link T} 
+  Lemma of_value_with {T : Set} `{Link T} 
     state_prime state_prime'
     state_middle state_middle'
     state_middle_prime state_middle_prime'
@@ -310,7 +310,7 @@ Module FullRound.
     = φ (Build_t T state_prime state_middle state_middle_prime state_output).
     Proof. Admitted.
 
-  Definition of_value {T : Set} `{T_Link : Link T}
+  Definition of_value {T : Set} `{Link T}
     (state_prime : Blake3State.t T) state_prime'
     (state_middle : Blake3State.t T) state_middle'
     (state_middle_prime : Blake3State.t T) state_middle_prime'
@@ -328,7 +328,7 @@ Module FullRound.
       ]).
   Proof. 
     econstructor 1 with (t T) (IsLink T) _.
-    eapply (@of_value_with T T_Link state_prime state_prime' state_middle 
+    eapply (@of_value_with T _ state_prime state_prime' state_middle 
       state_middle' state_middle_prime state_middle_prime' 
       state_output state_output').
     all: eassumption. Defined.

From 2b0aaa99381c8b4d9ac2fca1342c2407ca35c14b Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sun, 25 May 2025 19:39:46 +0800
Subject: [PATCH 19/19] minor: redesign `QuarterRound`'s arguments

---
 CoqOfRust/plonky3/blake3_air/links/air.v     |  5 ++---
 CoqOfRust/plonky3/blake3_air/links/columns.v | 10 +++++-----
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/CoqOfRust/plonky3/blake3_air/links/air.v b/CoqOfRust/plonky3/blake3_air/links/air.v
index 76ff8c5d1..46f43a726 100644
--- a/CoqOfRust/plonky3/blake3_air/links/air.v
+++ b/CoqOfRust/plonky3/blake3_air/links/air.v
@@ -84,7 +84,6 @@ Module Impl_Blake3Air.
   ) -> QuarterRound<'a, T, U>
   *)
   Instance run_full_round_to_column_quarter_round
-  (* NOTE: seems like there are some issues with T and U being defined here *)
     {T U : Set} `{Link T} `{Link U}
     (self : Ref.t Pointer.Kind.Ref Self) 
     (input : Ref.t Pointer.Kind.Ref (Blake3State.t T))
@@ -95,7 +94,7 @@ Module Impl_Blake3Air.
     Run.Trait
       blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.full_round_to_column_quarter_round [] [ Φ T; Φ U ] 
       [ (* φ input; φ round_data; φ m_vector; φ index *) ]
-      (QuarterRound.t T U _ _).
+      (QuarterRound.t T U).
   Proof.
     constructor.
     run_symbolic.
@@ -119,7 +118,7 @@ Module Impl_Blake3Air.
     Run.Trait
       blake3_air.air.air.Impl_p3_blake3_air_air_Blake3Air.full_round_to_diagonal_quarter_round [] [ Φ T; Φ U ] 
       [ (* φ input; φ round_data; φ m_vector; φ index *) ]
-      (QuarterRound.t T U _ _).
+      (QuarterRound.t T U).
   Proof.
     constructor.
     run_symbolic.
diff --git a/CoqOfRust/plonky3/blake3_air/links/columns.v b/CoqOfRust/plonky3/blake3_air/links/columns.v
index c7c99fb48..bd9d4f80e 100644
--- a/CoqOfRust/plonky3/blake3_air/links/columns.v
+++ b/CoqOfRust/plonky3/blake3_air/links/columns.v
@@ -49,9 +49,9 @@ Module QuarterRound.
     c_output : Ref.t Pointer.Kind.Ref (array.t T U32_LIMBS); 
     d_output : Ref.t Pointer.Kind.Ref (array.t T {| Integer.value := 32 |});
   }.
-  Arguments t : clear implicits.
+  Arguments t T U {_} {_}.
 
-  Global Instance IsLink (T U : Set) `{Link T} `{Link U} : Link (@t T U _ _)
+  Global Instance IsLink (T U : Set) `{Link T} `{Link U} : Link (t T U)
   := {
     Φ := Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ Φ T; Φ U ];
     φ x :=
@@ -76,7 +76,7 @@ Module QuarterRound.
   Definition of_ty (T_ty U_ty : Ty.t) :
     OfTy.t T_ty -> OfTy.t U_ty ->
     OfTy.t (Ty.apply (Ty.path "p3_blake3_air::columns::QuarterRound") [] [ T_ty ; U_ty ]).
-  Proof. intros [T] [U]. eapply OfTy.Make with (A := t T U _ _). now subst. Defined.
+  Proof. intros [T] [U]. eapply OfTy.Make with (A := t T U). now subst. Defined.
   Smpl Add eapply of_ty : of_ty.
 
   Lemma of_value_with {T U : Set} `{Link T} `{Link U} 
@@ -124,7 +124,7 @@ Module QuarterRound.
       ("c_output", c_output');
       ("d_output", d_output')
     ] = 
-    @φ (t T U _ _) (IsLink T U) (Build_t T U _ _
+    @φ (t T U) (IsLink T U) (Build_t T U _ _
     a b c d m_two_i a_prime b_prime c_prime d_prime 
       m_two_i_plus_one a_output b_output c_output d_output).
   Proof. now intros; subst. Qed.
@@ -180,7 +180,7 @@ Module QuarterRound.
       ]
     ).
   Proof. 
-  econstructor 1 with (t T U _ _) (IsLink T U) _.
+  econstructor 1 with (t T U) (IsLink T U) _.
   eapply (@of_value_with T U _ _ a a' b b' _ _).
   all: eassumption. Defined.
   Smpl Add apply of_value : of_value.