Skip to content

Commit

Permalink
proof: simplify the proof thanks to autorewrite
Browse files Browse the repository at this point in the history
  • Loading branch information
@clarus
clarus committed Dec 10, 2024
1 parent 2fbc29e commit 76403b4
Show file tree
Hide file tree
Showing 3 changed files with 38 additions and 142 deletions.
120 changes: 10 additions & 110 deletions CoqOfNoir/base64/simulation.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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) :
Expand Down Expand Up @@ -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] =>
Expand Down Expand Up @@ -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 <? length) eqn:H_i.
{ assert (i < length) by lia.
pose proof (List.nth_error_Some_bound_index _ _ _ H).
best use: List.nth_error_Some_bound_index.
destruct List.nth_error eqn:?.
2: {
assert (length <= i). {
best use: List.nth_error_nth'.
}

as [result|]; cbn; [|apply Run.Pure].
apply Run.Pure.
}
{ apply Run.Pure. }

}
Search List.nth_error.
Search List.listUpdate_error.
2: {
apply Run.Pure.
}
Search List.nth_error.
cbn.

eapply Run.Let.

epose proof (Run.For (State := State.t) _ _ _ _ _ _ _ _
(
fun state accumulator =>
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}
Expand Down
58 changes: 27 additions & 31 deletions CoqOfNoir/simulation/CoqOfNoir.v
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
Require Import CoqOfNoir.CoqOfNoir.
Require Import Coq.Logic.FunctionalExtensionality.

Module ToValue.
Class Trait (Self : Set) : Set := {
Expand Down Expand Up @@ -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.

Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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 :=
Expand Down
2 changes: 1 addition & 1 deletion scripts/coq_of_noir.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"]))
Expand Down

0 comments on commit 76403b4

Please sign in to comment.