From 76403b49f74340e7fb7687bc4effa53c8845390e Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Tue, 10 Dec 2024 18:31:16 +0100 Subject: [PATCH] proof: simplify the proof thanks to autorewrite --- CoqOfNoir/base64/simulation.v | 120 +++---------------------------- CoqOfNoir/simulation/CoqOfNoir.v | 58 +++++++-------- scripts/coq_of_noir.py | 2 +- 3 files changed, 38 insertions(+), 142 deletions(-) diff --git a/CoqOfNoir/base64/simulation.v b/CoqOfNoir/base64/simulation.v index e1565fc044f..5eb8fbf5038 100644 --- a/CoqOfNoir/base64/simulation.v +++ b/CoqOfNoir/base64/simulation.v @@ -240,7 +240,8 @@ Definition base64_encode_elements_for_body (p : Z) {InputElements : U32.t} letS! result := return!toS! (Array.write result i new_result_i) in writeS! result. -Definition base64_encode_elements (p : Z) {InputElements : U32.t} (input : Array.t U8.t InputElements) : +Definition base64_encode_elements (p : Z) {InputElements : U32.t} + (input : Array.t U8.t InputElements) : M! (Array.t U8.t InputElements) * Array.t U8.t InputElements := let Base64Encoder := Base64EncodeBE.new in @@ -255,20 +256,14 @@ Definition base64_encode_elements (p : Z) {InputElements : U32.t} (input : Array returnS! result ) (base64_encode_elements_for_init input). -Ltac cbn_goal := - match goal with - | |- Run.t _ ?result _ _ ?e => - let result' := eval cbn in result in - change result with result'; - let e' := eval cbn in e in - change e with e' - end. - Lemma map_listUpdate_eq {A B : Type} (f : A -> B) (l : list A) (i : nat) (x : A) (y : B) (H_y : y = f x) : List.listUpdate (List.map f l) i y = List.map f (List.listUpdate l i x). Proof. -Admitted. + unfold List.listUpdate. + rewrite List.firstn_map, List.skipn_map, List.map_app. + sfirstorder. +Qed. Lemma map_listUpdate_error_eq {A B : Type} (f : A -> B) (l : list A) (i : nat) (x : A) (y : B) (H_y : y = f x) : @@ -356,7 +351,6 @@ Proof. unfold cast_to_field; cbn. destruct (_ && _); cbn; [|apply Run.Pure]. eapply Run.CallClosure. { - repeat rewrite Array.rewrite_to_value by (intros; now autorewrite with to_value). autorewrite with to_value. match goal with | |- context[Value.Integer IntegerKind.Field ?i] => @@ -385,105 +379,11 @@ Proof. } } fold @LowM.let_. - (* destruct fst; cbn; [|apply Run.Pure]. *) + unfold StatePanic.bind. destruct (foldS! _ _ _) as [status result]. - destruct status; cbn. - { - - } - { exfalso. - set (Z.to_nat i) in *. - - lia. - } - [lia|]. - Search List.listUpdate_error. - { - (* pose proof (List.nth_error_None accumulator_in.(Array.value) (Z.to_nat i)). - best. *) - - } - epose proof (List.nth_error_None _ _). H_nth_error). - } - set (length := Z.of_nat (List.length accumulator_in.(Array.value))). - destruct (i - state <| State.base64_encode_elements := - state.(State.base64_encode_elements) <| - base64_encode_elements.State.result := Some accumulator - |> - |> - ) - ). - apply H. - eapply (Run.For (State := State.t)). - } - - apply Run.LetUnfold. - fold @LowM.let_. - apply Run.LetUnfold. - unfold M.for_, M.for_Z. - cbn_goal. - unfold Integer.to_nat, Integer.to_Z. - repeat match goal with - | |- context[Z.to_nat ?x] => - let n' := eval cbn in (Z.to_nat x) in - change (Z.to_nat x) with n' - end. - match goal with - | |- context[?x - 0] => - replace (x - 0) with x by lia - end. - unfold Array.Valid.t in H_input. - cbn in H_input. - unfold base64_encode_elements, Array.repeat in H_base64_encode_elements. - cbn in H_base64_encode_elements. - induction (Z.to_nat _); cbn_goal. - { eapply Run.CallPrimitiveStateRead; [reflexivity|]. - cbn in H_base64_encode_elements. - inversion_clear H_base64_encode_elements. - apply Run.Pure. - } - { eapply Run.CallPrimitiveStateRead; [reflexivity|]. - fold @LowM.let_. - Transparent M.index. - unfold M.index. - cbn_goal. - } - set (n := Z.to_nat _). - - simpl. - cbn. - (* Entering the loop *) - destruct input as [input]. - simpl. + destruct status; cbn; [|apply Run.Pure]. + eapply Run.CallPrimitiveStateRead; [reflexivity|]. + apply Run.Pure. Qed. (* Lemma run_eq₂ {State Address : Set} `{State.Trait State Address} diff --git a/CoqOfNoir/simulation/CoqOfNoir.v b/CoqOfNoir/simulation/CoqOfNoir.v index 28f1e6f74fa..ff9ed759581 100644 --- a/CoqOfNoir/simulation/CoqOfNoir.v +++ b/CoqOfNoir/simulation/CoqOfNoir.v @@ -1,5 +1,4 @@ Require Import CoqOfNoir.CoqOfNoir. -Require Import Coq.Logic.FunctionalExtensionality. Module ToValue. Class Trait (Self : Set) : Set := { @@ -141,8 +140,8 @@ Global Instance Impl_ToValue_for_bool : ToValue.Trait bool := { Value.Bool b; }. -Lemma rewrite_to_value_bool (b : bool) : - Value.Bool b = to_value b. +Lemma rewrite_to_value_bool : + Value.Bool = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value_bool : to_value. @@ -156,8 +155,8 @@ Module Field. Value.Integer IntegerKind.Field i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.Field i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.Field i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End Field. @@ -172,8 +171,8 @@ Module U1. Value.Integer IntegerKind.U1 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.U1 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.U1 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End U1. @@ -188,8 +187,8 @@ Module U8. Value.Integer IntegerKind.U8 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.U8 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.U8 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End U8. @@ -204,8 +203,8 @@ Module U16. Value.Integer IntegerKind.U16 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.U16 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.U16 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End U16. @@ -220,8 +219,8 @@ Module U32. Value.Integer IntegerKind.U32 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.U32 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.U32 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End U32. @@ -236,8 +235,8 @@ Module U64. Value.Integer IntegerKind.U64 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.U64 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.U64 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End U64. @@ -252,8 +251,8 @@ Module I1. Value.Integer IntegerKind.I1 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.I1 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.I1 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End I1. @@ -268,8 +267,8 @@ Module I8. Value.Integer IntegerKind.I8 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.I8 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.I8 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End I8. @@ -284,8 +283,8 @@ Module I16. Value.Integer IntegerKind.I16 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.I16 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.I16 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End I16. @@ -300,8 +299,8 @@ Module I32. Value.Integer IntegerKind.I32 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.I32 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.I32 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End I32. @@ -316,8 +315,8 @@ Module I64. Value.Integer IntegerKind.I64 i.(value); }. - Lemma rewrite_to_value (i : t) : - Value.Integer IntegerKind.I64 i.(value) = to_value i. + Lemma rewrite_to_value : + (fun i => Value.Integer IntegerKind.I64 i.(value)) = to_value. Proof. reflexivity. Qed. Global Hint Rewrite rewrite_to_value : to_value. End I64. @@ -472,12 +471,9 @@ Module Array. Value.Array (List.map to_value array.(value)); }. - Lemma rewrite_to_value {A : Set} `{ToValue.Trait A} {size : U32.t} (array : t A size) f : - (forall (x : A), f x = to_value x) -> - Value.Array (List.map f array.(value)) = to_value array. - Proof. - hauto lq: on use: functional_extensionality. - Qed. + Lemma rewrite_to_value {A : Set} `{ToValue.Trait A} {size : U32.t} (array : t A size) : + Value.Array (List.map to_value array.(value)) = to_value array. + Proof. reflexivity. Qed. Global Hint Rewrite @rewrite_to_value : to_value. Definition repeat {A : Set} (size : U32.t) (value : A) : t A size := diff --git a/scripts/coq_of_noir.py b/scripts/coq_of_noir.py index b0cffb0ea8f..b5929a55e68 100644 --- a/scripts/coq_of_noir.py +++ b/scripts/coq_of_noir.py @@ -416,7 +416,7 @@ def lvalue_to_coq(node) -> str: ''' def assign_to_coq(node) -> str: return alloc( - "M.assign (|\n" + + "M.write (|\n" + indent( read(lvalue_to_coq(node["lvalue"])) + ",\n" + read(expression_to_coq(node["expression"]))