feat: more work to have an example on Keccak

Author: clarus

.github/workflows/rocq.yml

@@ -23,7 +23,7 @@ jobs:
     - name: Run the Rocq tests
       uses: coq-community/docker-coq-action@v1
       with:
-        custom_image: coqorg/coq:8.17-ocaml-4.14-flambda
+        custom_image: coqorg/coq:8.20-ocaml-4.14-flambda
         custom_script: |
           startGroup "Install dependencies"
             curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
@@ -43,7 +43,7 @@ jobs:
             cd ..
           endGroup
           startGroup "Convert to Rocq"
-            python scripts/rocq_of_noir.py noir_stdlib/monomorphized_program.json >RocqOfNoir/keccak_monomorphic.v
+            python scripts/rocq_of_noir.py noir_stdlib/monomorphized_program.json >RocqOfNoir/keccak/monomorphic.v
             python scripts/rocq_of_noir.py RocqOfNoir/base64/monomorphized_program.json >RocqOfNoir/base64/monomorphic.v
           endGroup
           startGroup "Compile Rocq translations"

RocqOfNoir/RecordUpdate.v

@@ -15,7 +15,7 @@ Ltac2 rec strip_foralls (t : constr) :=
 
 Ltac2 app_arg_count (t : constr) :=
   match Constr.Unsafe.kind t with
-  | Constr.Unsafe.App f args => Array.length args
+  | Constr.Unsafe.App _ args => Array.length args
   | _ => 0
   end.
 
@@ -31,7 +31,7 @@ Ltac2 field_names (ctor_ref : Std.reference) :=
 
 Ltac2 constructor_of_record (t : constr) :=
   match Constr.Unsafe.kind t with
-  | Constr.Unsafe.Ind ind inst =>
+  | Constr.Unsafe.Ind ind _ =>
     Std.ConstructRef (Constr.Unsafe.constructor ind 0)
   | _ => Control.throw (Invalid_argument (Some (Message.of_constr t)))
   end.
@@ -44,7 +44,7 @@ Ltac2 record_with_set_val (ty : constr) (record : constr)
   let (h, args) :=
     match Constr.Unsafe.kind ty with
     | Constr.Unsafe.App h args => (h, args)
-    | _ => (ty, Array.empty ())
+    | _ => (ty, Array.empty)
     end in
   let ctor := constructor_of_record h in
   let getters := List.map (fun getterRef =>

RocqOfNoir/base64/polymorphic.v

@@ -5,63 +5,64 @@ Require Import base64.monomorphic.
 (** This module provides helpers to show the equality to debug [reflexivity] when it is too long or
     failing *)
 Module Eq.
-  Lemma LowLet {A : Set} (e e' : LowM.t A) k k'
+      Lemma LowLet {A : Set} (e e' : LowM.t A) k k'
       (H_e : e = e')
       (H_k : forall x, k x = k' x) :
-    LowM.Let e k = LowM.Let e' k'.
+      LowM.Let e k = LowM.Let e' k'.
   Proof.
     rewrite H_e.
     replace k with k' by now apply functional_extensionality.
     reflexivity.
   Qed.
 
-  Fixpoint LetMinus {A : Set} (e1 e1' : LowM.t A) (e2 e2' : A -> LowM.t A)
+  Lemma LetMinus {A : Set} (e1 e1' : LowM.t A) (e2 e2' : A -> LowM.t A)
       (H_e1 : e1 = e1')
-      (H_e2 : forall x, e2 x = e2' x)
-      {struct e1} :
-    LowM.let_ e1 e2 = LowM.let_ e1' e2'.
+      (H_e2 : forall x, e2 x = e2' x) :
+      LowM.let_ e1 e2 = LowM.let_ e1' e2'.
   Proof.
-    destruct e1; rewrite <- H_e1; simpl.
-    { apply H_e2. }
-    { f_equal.
-      apply functional_extensionality; intro x.
-      now rewrite LetMinus with (e1' := k x) (e2' := e2').
-    }
-    { f_equal.
-      apply functional_extensionality; intro x.
-      now rewrite LetMinus with (e1' := k x) (e2' := e2').
-    }
-    { f_equal.
-      apply functional_extensionality; intro x.
-      now rewrite LetMinus with (e1' := k x) (e2' := e2').
-    }
-    { reflexivity. }
+    rewrite H_e1.
+    replace e2 with e2' by now apply functional_extensionality.
+    reflexivity.
   Qed.
 
   Lemma LetStar e1 e1' e2 e2'
       (H_e1 : e1 = e1')
       (H_e2 : forall x, e2 x = e2' x) :
-    M.let_ e1 e2 = M.let_ e1' e2'.
+      M.let_ e1 e2 = M.let_ e1' e2'.
   Proof.
-    apply LetMinus; hauto lq: on.
+    rewrite H_e1.
+    replace e2 with e2' by now apply functional_extensionality.
+    reflexivity.
   Qed.
 
   Lemma LetTilde e1 e1' e2 e2'
       (H_e1 : e1 = e1')
       (H_e2 : forall x, e2 x = e2' x) :
-    M.let_strong e1 e2 = M.let_strong e1' e2'.
+      M.let_strong e1 e2 = M.let_strong e1' e2'.
   Proof.
-    apply LowLet; hauto lq: on.
+    rewrite H_e1.
+    replace e2 with e2' by now apply functional_extensionality.
+    reflexivity.
   Qed.
 
   Lemma If e e' t t' f f'
       (H_e : e = e')
       (H_t : t = t')
       (H_f : f = f') :
-    M.if_ e t f = M.if_ e' t' f'.
+      M.if_ e t f = M.if_ e' t' f'.
   Proof.
     f_equal; assumption.
   Qed.
+
+  Ltac tactic :=
+    repeat (
+      intro ||
+      apply LowLet ||
+      apply LetMinus ||
+      apply LetStar ||
+      apply LetTilde ||
+      apply If
+    ).
 End Eq.
 
 Module Field.
@@ -92,7 +93,7 @@ Module Field.
     | _ => M.impossible "wrong number of arguments"
     end.
 
-  Lemma eq_to_be_radix₁ : get_function "to_be_radix" 1 = closure (to_be_radix (U32.Build_t 40)).
+  Lemma eq_to_be_radix₁ : get_function "to_be_radix" 1 = closure (to_be_radix {| Integer.value := 40 |}).
   Proof.
     autorewrite with get_function; f_equal.
   Qed.
@@ -101,7 +102,7 @@ End Field.
 
 Module Base64EncodeBE.
   Record t : Set := {
-    table : Array.t U8.t (U32.Build_t 64);
+    table : Array.t U8.t {| Integer.value := 64 |};
   }.
 
   Definition new (α : list Value.t) : M.t :=
@@ -231,7 +232,7 @@ Definition base64_encode_elements (InputElements : U32.t) (α : list Value.t) :
       |) ]] in
       let~ result := [[ M.copy_mutable (|
         M.alloc (Value.Array (
-          List.repeat (Value.Integer IntegerKind.U8 0) (Z.to_nat (Integer.to_Z InputElements))
+          List.repeat (Value.Integer IntegerKind.U8 0) (Z.to_nat InputElements.(Integer.value))
         ))
       |) ]] in
       do~ [[
@@ -270,7 +271,7 @@ Definition base64_encode_elements (InputElements : U32.t) (α : list Value.t) :
   end.
 
 Lemma eq_base64_encode_elements₀ :
-  get_function "base64_encode_elements" 0 = closure (base64_encode_elements (U32.Build_t 118)).
+  get_function "base64_encode_elements" 0 = closure (base64_encode_elements {| Integer.value := 118 |}).
 Proof.
   autorewrite with get_function; apply f_equal.
   apply functional_extensionality; intro α.
@@ -288,7 +289,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
       let~ result := [[ M.copy_mutable (|
         M.alloc (Value.Array (List.repeat
           (Value.Integer IntegerKind.U8 0)
-          (Z.to_nat (Integer.to_Z OutputElements))
+          (Z.to_nat OutputElements.(Integer.value))
         ))
       |) ]] in
       let~ BASE64_ELEMENTS_PER_CHUNK := [[ M.copy (|
@@ -371,7 +372,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
               ]] in
               let~ slice_base64_chunks := [[ M.copy (|
                 M.alloc (M.call_closure (|
-                  closure (Field.to_be_radix (U32.Build_t 30)),
+                  closure (Field.to_be_radix {| Integer.value := 30 |}),
                   [
                     M.read (| slice |);
                     Value.Integer IntegerKind.U32 64
@@ -478,7 +479,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
           ]] in
           let~ slice_base64_chunks := [[ M.copy (|
             M.alloc (M.call_closure (|
-              closure (Field.to_be_radix (U32.Build_t 30)),
+              closure (Field.to_be_radix {| Integer.value := 30 |}),
               [
                 M.read (| slice |);
                 Value.Integer IntegerKind.U32 64
@@ -529,7 +530,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
             M.alloc (M.write (|
               result,
               M.call_closure (|
-                closure (base64_encode_elements (U32.Build_t 118)),
+                closure (base64_encode_elements {| Integer.value := 118 |}),
                 [
                   M.read (| result |)
                 ]
@@ -547,44 +548,14 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
   end.
 
 Lemma eq_base64_encode₀ :
-  get_function "base64_encode" 0 = closure (base64_encode (U32.Build_t 88) (U32.Build_t 118)).
+  get_function "base64_encode" 0 = closure (base64_encode {| Integer.value := 88 |} {| Integer.value := 118 |}).
 Proof.
   autorewrite with get_function; apply f_equal.
   apply functional_extensionality; intro α.
   unfold base64_encode₀.
   autorewrite with get_function_eq.
   destruct α as [|input α]; [reflexivity|].
   destruct α; [|reflexivity].
-  apply Eq.LetStar; [|reflexivity].
-  apply Eq.LetTilde; [reflexivity|intro result].
-  apply Eq.LetTilde; [reflexivity|intro BASE64_ELEMENTS_PER_CHUNK].
-  apply Eq.LetTilde; [reflexivity|intro BYTES_PER_CHUNK].
-  apply Eq.LetTilde; [reflexivity|intro num_chunks].
-  apply Eq.LetTilde. {
-    apply Eq.LetStar; [reflexivity|intro v].
-    apply Eq.If; [reflexivity | | reflexivity].
-    apply Eq.LetTilde. {
-      reflexivity.
-    }
-    intro.
-    apply Eq.LetTilde; [reflexivity|intro bytes_in_final_chunk].
-    apply Eq.LetTilde; [reflexivity|intro slice].
-    apply Eq.LetTilde. {
-      reflexivity.
-    }
-    intro.
-    apply Eq.LetTilde. {
-      reflexivity.
-    }
-    intro.
-    apply Eq.LetTilde; [reflexivity|intro slice_base64_chunks].
-    apply Eq.LetTilde; [reflexivity|intro num_elements_in_final_chunk].
-    apply Eq.LetTilde. {
-      reflexivity.
-    }
-    intro.
-    reflexivity.
-  }
-  intro.
+  apply Eq.LetStar; [reflexivity|intro result].
   reflexivity.
 Qed.

RocqOfNoir/base64/simulation.v

@@ -3,19 +3,17 @@ Require Import RocqOfNoir.proof.RocqOfNoir.
 Require Import RocqOfNoir.simulation.RocqOfNoir.
 Require RocqOfNoir.base64.polymorphic.
 
-Import Run.
-
 Module Base64EncodeBE.
   (*
   struct Base64EncodeBE {
       table: [u8; 64]
   }
   *)
   Record t : Set := {
-    table : Array.t U8.t (U32.Build_t 64);
+    table : Array.t U8.t {| Integer.value := 64 |};
   }.
 
-  Global Instance Impl_ToValue : ToValue.Trait t := {
+  Global Instance Impl_ToValue : ToValue t := {
     to_value (x : t) :=
       Value.Tuple [to_value x.(table)];
   }.
@@ -25,7 +23,7 @@ Module Base64EncodeBE.
   Proof. reflexivity. Qed.
   Global Hint Rewrite rewrite_to_value : to_value.
 
-  Definition ascii_codes : list U8.t := List.map U8.Build_t [
+  Definition ascii_codes : list U8.t := List.map (Integer.Build_t IntegerKind.U8) [
     65; 66; 67; 68; 69; 70; 71; 72; 73; 74; 75; 76; 77; 78; 79; 80; 81; 82; 83; 84; 85; 86; 87; 88; 89; 90;
     97; 98; 99; 100; 101; 102; 103; 104; 105; 106; 107; 108; 109; 110; 111; 112; 113; 114; 115; 116; 117; 118; 119; 120; 121; 122;
     48; 49; 50; 51; 52; 53; 54; 55; 56; 57;
@@ -226,12 +224,12 @@ pub fn base64_encode_elements<let InputElements: u32>(input: [u8; InputElements]
 Definition base64_encode_elements_for_init {InputElements : U32.t}
     (input : Array.t U8.t InputElements) :
     Array.t U8.t InputElements :=
-  Array.repeat InputElements (U8.Build_t 0).
+  Array.repeat InputElements {| Integer.value := 0 |}.
 
 Definition base64_encode_elements_for_body (p : Z) {InputElements : U32.t}
     (input : Array.t U8.t InputElements) (i : Z) :
     MS! (Array.t U8.t InputElements) unit :=
-  let i : U32.t := U32.Build_t i in
+  let i : U32.t := {| Integer.value := i |} in
   letS! input_i := return!toS! (Array.read input i) in
   letS! input_i := return!toS! (cast_to_field p input_i) in
   letS! new_result_i :=
@@ -249,7 +247,7 @@ Definition base64_encode_elements (p : Z) {InputElements : U32.t}
     doS! (
       foldS!
         tt
-        (List.map Z.of_nat (List.seq 0 (Z.to_nat (ToZ.to_Z InputElements))))
+        (List.map Z.of_nat (List.seq 0 (Z.to_nat InputElements.(Integer.value))))
         (fun result i => base64_encode_elements_for_body p input i)
     ) in
     letS! result := readS! in
@@ -270,7 +268,7 @@ Lemma map_listUpdate_error_eq {A B : Type} (f : A -> B) (l : list A) (i : nat) (
   List.listUpdate_error (List.map f l) i y = option_map (List.map f) (List.listUpdate_error l i x).
 Proof.
   unfold List.listUpdate_error.
-  rewrite List.map_length.
+  rewrite List.length_map.
   destruct (_ <? _)%nat; cbn; f_equal.
   now erewrite map_listUpdate_eq.
 Qed.
@@ -280,7 +278,7 @@ Lemma run_base64_encode_elements
     {InputElements : U32.t}
     (input : Array.t U8.t InputElements)
     (H_InputElements : Integer.Valid.t InputElements)
-    (H_input : Array.Valid.t input) :
+    (H_input : Array.Valid.t (fun _ => True) input) :
   let output := base64_encode_elements p input in
   let state_end : State.t :=
     State.init <|
@@ -324,7 +322,7 @@ Proof.
           |>
       )
       (accumulator_in := base64_encode_elements_for_init input)
-      (len := Z.to_nat InputElements.(U32.value))
+      (len := Z.to_nat InputElements.(Integer.value))
       (body_expression := base64_encode_elements_for_body p input).
     2: {
       unfold set.
@@ -354,7 +352,7 @@ Proof.
       autorewrite with to_value.
       match goal with
       | |- context[Value.Integer IntegerKind.Field ?i] =>
-        change (Value.Integer IntegerKind.Field i) with (to_value (Field.Build_t i))
+        change (Value.Integer IntegerKind.Field i) with (to_value (Self := Field.t) {| Integer.value := i |})
       end.
       apply Base64EncodeBE.run_get.
     }