Skip to content

Commit d9ddb74

Browse files
clarusclarus
committed
keccak: more wip
1 parent 44ccd09 commit d9ddb74

File tree

8 files changed

+485
-86
lines changed

8 files changed

+485
-86
lines changed

‎RocqOfNoir/RocqOfNoir.v‎

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,6 @@ End Pointer.
6363

6464
Module IntegerKind.
6565
Inductive t : Set :=
66-
| Field
6766
| U1
6867
| U8
6968
| U16
@@ -79,6 +78,7 @@ End IntegerKind.
7978
Module Value.
8079
Inductive t : Set :=
8180
| Bool (b : bool)
81+
| Field (integer : Z)
8282
| Integer (kind : IntegerKind.t) (integer : Z)
8383
| String (s : string)
8484
| FmtStr : string -> Z -> t -> t
@@ -366,19 +366,24 @@ Module M.
366366
| _ => LowM.Impossible "assert: expected a boolean"
367367
end.
368368

369+
Definition cast_to_field (value : Value.t) : M.t :=
370+
match value with
371+
| Value.Integer _ i =>
372+
LowM.CallPrimitive Primitive.GetFieldPrime (fun p =>
373+
if (0 <=? i) && (i <? p) then
374+
pure (Value.Field i)
375+
else
376+
panic ("cast_to_field: out of bounds", value))
377+
| _ => impossible "cast_to_field: expected a field"
378+
end.
379+
369380
(** We only consider cast between integer values. We consider that the cast succeed if we are
370381
in the bounds of the target type. For casts to fields we need to retrieve the current
371382
field prime, which could change depending on the backend. *)
372383
Definition cast (value : Value.t) (integer_kind : IntegerKind.t) : M.t :=
373384
match value with
374385
| Value.Integer _ i =>
375386
match integer_kind with
376-
| IntegerKind.Field =>
377-
LowM.CallPrimitive Primitive.GetFieldPrime (fun p =>
378-
if (0 <=? i) && (i <? p) then
379-
pure (Value.Integer integer_kind i)
380-
else
381-
panic ("cast: out of bounds", value, integer_kind))
382387
| IntegerKind.U1 =>
383388
if (0 <=? i) && (i <? 2) then
384389
pure (Value.Integer integer_kind i)
@@ -589,7 +594,13 @@ Module Binary.
589594

590595
Parameter greater : Value.t -> Value.t -> M.t.
591596

592-
Parameter greater_equal : Value.t -> Value.t -> M.t.
597+
Definition greater_equal (x y : Value.t) : M.t :=
598+
match x, y with
599+
| Value.Integer _ x, Value.Integer _ y =>
600+
M.pure (Value.Bool (x >=? y))
601+
| _, _ =>
602+
M.impossible "greater_equal: expected non-field integer values"
603+
end.
593604

594605
Parameter and_ : Value.t -> Value.t -> M.t.
595606

‎RocqOfNoir/base64/simulation.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -287,10 +287,10 @@ Lemma run_base64_encode_elements
287287
base64_encode_elements.State.result := Some (to_value (snd output));
288288
|}
289289
|> in
290-
{{ p, State.init ⏩
291-
polymorphic.base64_encode_elements InputElements [to_value input] 🔽
292-
Panic.to_result (fst output)
293-
⏩ state_end }}.
290+
{{ p, State.init ⏩
291+
polymorphic.base64_encode_elements InputElements [to_value input] 🔽
292+
Panic.to_result (fst output)
293+
⏩ state_end }}.
294294
Proof.
295295
unfold polymorphic.base64_encode_elements, base64_encode_elements.
296296
eapply Run.Let. {

‎RocqOfNoir/keccak/monomorphic.v‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -712,10 +712,10 @@ Definition keccak256₀ (α : list Value.t) : M.t :=
712712
|))
713713
|) ]] in
714714
let~ sliced := [[ M.copy_mutable (|
715-
M.alloc (Value.Integer IntegerKind.Field 0)
715+
M.alloc (Value.Field 0)
716716
|) ]] in
717717
let~ v := [[ M.copy_mutable (|
718-
M.alloc (Value.Integer IntegerKind.Field 1)
718+
M.alloc (Value.Field 1)
719719
|) ]] in
720720
do~ [[
721721
M.for_ (|
@@ -729,15 +729,14 @@ Definition keccak256₀ (α : list Value.t) : M.t :=
729729
M.read (| sliced |),
730730
Binary.multiply (|
731731
M.read (| v |),
732-
M.cast (|
732+
M.cast_to_field (|
733733
M.read (| M.index (|
734734
block_bytes,
735735
Binary.add (|
736736
M.read (| limb_start |),
737737
M.read (| k |)
738738
|)
739-
|) |),
740-
IntegerKind.Field
739+
|) |)
741740
|)
742741
|)
743742
|)
@@ -748,7 +747,7 @@ Definition keccak256₀ (α : list Value.t) : M.t :=
748747
v,
749748
Binary.multiply (|
750749
M.read (| v |),
751-
Value.Integer IntegerKind.Field 256
750+
Value.Field 256
752751
|)
753752
|))
754753
]]
@@ -1011,12 +1010,11 @@ Definition keccak256₀ (α : list Value.t) : M.t :=
10111010
Value.Integer IntegerKind.U32 4,
10121011
fun (i : Value.t) =>
10131012
let~ lane := [[ M.copy (|
1014-
M.alloc (M.cast (|
1013+
M.alloc (M.cast_to_field (|
10151014
M.read (| M.index (|
10161015
state,
10171016
M.read (| i |)
1018-
|) |),
1019-
IntegerKind.Field
1017+
|) |)
10201018
|))
10211019
|) ]] in
10221020
let~ lane_le := [[ M.copy (|

‎RocqOfNoir/keccak/polymorphic.v‎

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -358,10 +358,10 @@ Definition keccak256 (N : U32.t) (α : list Value.t) : M.t :=
358358
|))
359359
|) ]] in
360360
let~ sliced := [[ M.copy_mutable (|
361-
M.alloc (Value.Integer IntegerKind.Field 0)
361+
M.alloc (Value.Field 0)
362362
|) ]] in
363363
let~ v := [[ M.copy_mutable (|
364-
M.alloc (Value.Integer IntegerKind.Field 1)
364+
M.alloc (Value.Field 1)
365365
|) ]] in
366366
do~ [[
367367
M.for_ (|
@@ -375,15 +375,14 @@ Definition keccak256 (N : U32.t) (α : list Value.t) : M.t :=
375375
M.read (| sliced |),
376376
Binary.multiply (|
377377
M.read (| v |),
378-
M.cast (|
378+
M.cast_to_field (|
379379
M.read (| M.index (|
380380
block_bytes,
381381
Binary.add (|
382382
M.read (| limb_start |),
383383
M.read (| k |)
384384
|)
385-
|) |),
386-
IntegerKind.Field
385+
|) |)
387386
|)
388387
|)
389388
|)
@@ -394,7 +393,7 @@ Definition keccak256 (N : U32.t) (α : list Value.t) : M.t :=
394393
v,
395394
Binary.multiply (|
396395
M.read (| v |),
397-
Value.Integer IntegerKind.Field 256
396+
Value.Field 256
398397
|)
399398
|))
400399
]]
@@ -414,7 +413,11 @@ Definition keccak256 (N : U32.t) (α : list Value.t) : M.t :=
414413
]]
415414
|)
416415
]] in
417-
let~ state := [[ M.copy_mutable (|
416+
[[
417+
sliced_buffer
418+
]] in
419+
M.read result
420+
(* let~ state := [[ M.copy_mutable (|
418421
M.alloc (Value.Array [
419422
Value.Integer IntegerKind.U64 0;
420423
Value.Integer IntegerKind.U64 0;
@@ -657,12 +660,11 @@ Definition keccak256 (N : U32.t) (α : list Value.t) : M.t :=
657660
Value.Integer IntegerKind.U32 4,
658661
fun (i : Value.t) =>
659662
let~ lane := [[ M.copy (|
660-
M.alloc (M.cast (|
663+
M.alloc (M.cast_to_field (|
661664
M.read (| M.index (|
662665
state,
663666
M.read (| i |)
664-
|) |),
665-
IntegerKind.Field
667+
|) |)
666668
|))
667669
|) ]] in
668670
let~ lane_le := [[ M.copy (|
@@ -703,16 +705,16 @@ Definition keccak256 (N : U32.t) (α : list Value.t) : M.t :=
703705
[[
704706
result
705707
]] in
706-
M.read result
708+
M.read result *)
707709
| _ => M.impossible "wrong number of arguments"
708710
end.
709711

710-
Lemma eq_keccak256₀ :
712+
(* Lemma eq_keccak256₀ :
711713
get_function "keccak256" 0 = closure (keccak256 {| Integer.value := 1 |}).
712714
Proof.
713715
autorewrite with get_function; apply f_equal.
714716
apply functional_extensionality; intro α.
715717
unfold keccak256₀.
716718
reflexivity.
717719
Qed.
718-
Global Hint Rewrite eq_keccak256₀ : get_function_eq.
720+
Global Hint Rewrite eq_keccak256₀ : get_function_eq. *)

0 commit comments

Comments
 (0)