From 4d76bd7f6a61259f476d9985bf4720d08880aa8c Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Mon, 5 May 2025 16:38:49 -0300
Subject: [PATCH 1/2] Adding air.v

---
 CoqOfRust/plonky3/air/links/air.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 CoqOfRust/plonky3/air/links/air.v

diff --git a/CoqOfRust/plonky3/air/links/air.v b/CoqOfRust/plonky3/air/links/air.v
new file mode 100644
index 000000000..e827c269a
--- /dev/null
+++ b/CoqOfRust/plonky3/air/links/air.v
@@ -0,0 +1,29 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+
+(*
+  pub trait BaseAir<F>: Sync {
+    /// The number of columns (a.k.a. registers) in this AIR.
+    fn width(&self) -> usize;
+
+    fn preprocessed_trace(&self) -> Option<RowMajorMatrix<F>> {
+        None
+    }
+}
+*)
+Module BaseAir.
+    Module Types.
+        Record t : Type := {
+            F : Set;
+        }.
+    End Types.
+    Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
+    ("BaseAir", [], [], Φ Self).
+
+    Definition Run_width (Self : Set) `{Link Self} : Set :=
+    TraitMethod.C (trait Self) "width" (fun method =>
+      forall (self : Ref.t Pointer.Kind.Ref Self),
+        Run.Trait method [] [] [ φ self ] Usize.t
+    ).
+
+End BaseAir.
\ No newline at end of file

From 1e8c36213834031193c8254f4bef23fcf7541ee3 Mon Sep 17 00:00:00 2001
From: romefeller <alexgrcol@hotmail.com>
Date: Tue, 6 May 2025 14:56:14 -0300
Subject: [PATCH 2/2] Include type parameter F

---
 CoqOfRust/plonky3/air/links/air.v | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/CoqOfRust/plonky3/air/links/air.v b/CoqOfRust/plonky3/air/links/air.v
index e827c269a..afacbc1a1 100644
--- a/CoqOfRust/plonky3/air/links/air.v
+++ b/CoqOfRust/plonky3/air/links/air.v
@@ -12,16 +12,11 @@ Require Import CoqOfRust.links.M.
 }
 *)
 Module BaseAir.
-    Module Types.
-        Record t : Type := {
-            F : Set;
-        }.
-    End Types.
-    Definition trait (Self : Set) `{Link Self} : TraitMethod.Header.t :=
-    ("BaseAir", [], [], Φ Self).
+    Definition trait (Self F : Set) (H_Self : Link Self) (H_F : Link F) : TraitMethod.Header.t :=
+  ("BaseAir", [], [Φ F], Φ Self).
 
-    Definition Run_width (Self : Set) `{Link Self} : Set :=
-    TraitMethod.C (trait Self) "width" (fun method =>
+    Definition Run_width (Self F : Set) {H_Self: Link Self} {H_F : Link F} : Set :=
+    TraitMethod.C (trait Self F H_Self H_F) "width" (fun method =>
       forall (self : Ref.t Pointer.Kind.Ref Self),
         Run.Trait method [] [] [ φ self ] Usize.t
     ).