Skip to content

Commit

Permalink
Merge pull request #5 from formal-land/guillaume-claret@more-progress…
Browse files Browse the repository at this point in the history 
…-on-the-proofs

More work on base64 proofs
  • Loading branch information
@clarus
clarus authored Dec 10, 2024
2 parents 0d3043f + 76403b4 commit 404cd2a
Show file tree
Hide file tree
Showing 7 changed files with 553 additions and 309 deletions.
9 changes: 4 additions & 5 deletions CoqOfNoir/CoqOfNoir.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ Require Export Coq.Strings.Ascii.
Require Coq.Strings.HexString.
Require Export Coq.Strings.String.
Require Export Coq.ZArith.ZArith.
Require Coq.micromega.ZifyBool.
Require coqutil.Datatypes.List.
Require Export RecordUpdate.

Expand Down Expand Up @@ -122,7 +123,7 @@ Module Value.
match value with
| Tuple values =>
match List.listUpdate_error values (Z.to_nat i) update with
| Some new_values => Some (Tuple values)
| Some new_values => Some (Tuple new_values)
| None => None
end
| _ => None
Expand All @@ -131,7 +132,7 @@ Module Value.
match value with
| Array values =>
match List.listUpdate_error values (Z.to_nat i) update with
| Some new_values => Some (Array values)
| Some new_values => Some (Array new_values)
| None => None
end
| _ => None
Expand Down Expand Up @@ -454,8 +455,6 @@ Module M.
| _ => impossible "index: expected a pointer"
end.

Parameter assign : Value.t -> Value.t -> M.t.

Definition extract_tuple_field (tuple : Value.t) (field : Z) : M.t :=
match tuple with
| Value.Pointer tuple_pointer =>
Expand Down Expand Up @@ -487,7 +486,7 @@ Module M.

Fixpoint for_nat (end_ : Z) (fuel : nat) (body : Z -> M.t) {struct fuel} : M.t :=
match fuel with
| O => pure (Value.Tuple [])
| O => pure (alloc (Value.Tuple []))
| S fuel' =>
let* _ := body (end_ - Z.of_nat fuel) in
for_nat end_ fuel' body
Expand Down
40 changes: 20 additions & 20 deletions CoqOfNoir/base64/monomorphic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -295,7 +295,7 @@ Definition base64_encode₁ (α : list Value.t) : M.t :=
M.read (| BYTES_PER_CHUNK |),
fun (j : Value.t) =>
do~ [[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.multiply (|
M.read (| slice |),
Expand All @@ -304,7 +304,7 @@ Definition base64_encode₁ (α : list Value.t) : M.t :=
|))
]] in
[[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.add (|
M.read (| slice |),
Expand Down Expand Up @@ -341,7 +341,7 @@ Definition base64_encode₁ (α : list Value.t) : M.t :=
M.read (| BASE64_ELEMENTS_PER_CHUNK |),
fun (j : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
M.index (|
result,
Binary.add (|
Expand Down Expand Up @@ -383,7 +383,7 @@ Definition base64_encode₁ (α : list Value.t) : M.t :=
M.read (| bytes_in_final_chunk |),
fun (j : Value.t) =>
do~ [[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.multiply (|
M.read (| slice |),
Expand All @@ -392,7 +392,7 @@ Definition base64_encode₁ (α : list Value.t) : M.t :=
|))
]] in
[[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.add (|
M.read (| slice |),
Expand Down Expand Up @@ -423,7 +423,7 @@ Definition base64_encode₁ (α : list Value.t) : M.t :=
M.read (| BYTES_PER_CHUNK |),
fun (_ : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.multiply (|
M.read (| slice |),
Expand Down Expand Up @@ -460,7 +460,7 @@ Definition base64_encode₁ (α : list Value.t) : M.t :=
M.read (| num_elements_in_final_chunk |),
fun (i : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
M.index (|
result,
Binary.add (|
Expand All @@ -483,7 +483,7 @@ Definition base64_encode₁ (α : list Value.t) : M.t :=
|)
]] in
[[
M.alloc (M.assign (|
M.alloc (M.write (|
result,
M.call_closure (|
get_function "base64_encode_elements" 6,
Expand Down Expand Up @@ -537,7 +537,7 @@ Definition eq₂ (α : list Value.t) : M.t :=
|),
fun (i : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
result,
Binary.and_ (|
M.read (| result |),
Expand Down Expand Up @@ -760,7 +760,7 @@ Definition base64_decode₃ (α : list Value.t) : M.t :=
M.read (| BASE64_ELEMENTS_PER_CHUNK |),
fun (j : Value.t) =>
do~ [[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.multiply (|
M.read (| slice |),
Expand All @@ -769,7 +769,7 @@ Definition base64_decode₃ (α : list Value.t) : M.t :=
|))
]] in
[[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.add (|
M.read (| slice |),
Expand Down Expand Up @@ -805,7 +805,7 @@ Definition base64_decode₃ (α : list Value.t) : M.t :=
M.read (| BYTES_PER_CHUNK |),
fun (j : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
M.index (|
result,
Binary.add (|
Expand Down Expand Up @@ -847,7 +847,7 @@ Definition base64_decode₃ (α : list Value.t) : M.t :=
M.read (| base64_elements_in_final_chunk |),
fun (j : Value.t) =>
do~ [[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.multiply (|
M.read (| slice |),
Expand All @@ -856,7 +856,7 @@ Definition base64_decode₃ (α : list Value.t) : M.t :=
|))
]] in
[[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.add (|
M.read (| slice |),
Expand Down Expand Up @@ -887,7 +887,7 @@ Definition base64_decode₃ (α : list Value.t) : M.t :=
M.read (| BASE64_ELEMENTS_PER_CHUNK |),
fun (_ : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.multiply (|
M.read (| slice |),
Expand Down Expand Up @@ -923,7 +923,7 @@ Definition base64_decode₃ (α : list Value.t) : M.t :=
M.read (| num_bytes_in_final_chunk |),
fun (i : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
M.index (|
result,
Binary.add (|
Expand Down Expand Up @@ -989,7 +989,7 @@ Definition eq₄ (α : list Value.t) : M.t :=
|),
fun (i : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
result,
Binary.and_ (|
M.read (| result |),
Expand Down Expand Up @@ -1210,7 +1210,7 @@ Definition base64_encode_elements₆ (α : list Value.t) : M.t :=
Value.Integer IntegerKind.U32 118,
fun (i : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
M.index (|
result,
M.read (| i |)
Expand Down Expand Up @@ -1427,7 +1427,7 @@ Definition base64_decode_elements₈ (α : list Value.t) : M.t :=
|)
|) ]] in
do~ [[
M.alloc (M.assign (|
M.alloc (M.write (|
M.index (|
result,
M.read (| i |)
Expand Down Expand Up @@ -1621,7 +1621,7 @@ Definition to_be_bytes₉ (α : list Value.t) : M.t :=
|))
]] in
[[
M.alloc (M.assign (|
M.alloc (M.write (|
ok,
Value.Bool true
|))
Expand Down
22 changes: 11 additions & 11 deletions CoqOfNoir/base64/polymorphic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,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) (Integer.to_nat InputElements)
List.repeat (Value.Integer IntegerKind.U8 0) (Z.to_nat (Integer.to_Z InputElements))
))
|) ]] in
do~ [[
Expand All @@ -240,7 +240,7 @@ Definition base64_encode_elements (InputElements : U32.t) (α : list Value.t) :
to_value InputElements,
fun (i : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
M.index (|
result,
M.read (| i |)
Expand Down Expand Up @@ -288,7 +288,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)
(Integer.to_nat OutputElements)
(Z.to_nat (Integer.to_Z OutputElements))
))
|) ]] in
let~ BASE64_ELEMENTS_PER_CHUNK := [[ M.copy (|
Expand Down Expand Up @@ -338,7 +338,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
M.read (| BYTES_PER_CHUNK |),
fun (j : Value.t) =>
do~ [[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.multiply (|
M.read (| slice |),
Expand All @@ -347,7 +347,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
|))
]] in
[[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.add (|
M.read (| slice |),
Expand Down Expand Up @@ -384,7 +384,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
M.read (| BASE64_ELEMENTS_PER_CHUNK |),
fun (j : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
M.index (|
result,
Binary.add (|
Expand Down Expand Up @@ -426,7 +426,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
M.read (| bytes_in_final_chunk |),
fun (j : Value.t) =>
do~ [[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.multiply (|
M.read (| slice |),
Expand All @@ -435,7 +435,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
|))
]] in
[[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.add (|
M.read (| slice |),
Expand Down Expand Up @@ -466,7 +466,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
M.read (| BYTES_PER_CHUNK |),
fun (_ : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
slice,
Binary.multiply (|
M.read (| slice |),
Expand Down Expand Up @@ -503,7 +503,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
M.read (| num_elements_in_final_chunk |),
fun (i : Value.t) =>
[[
M.alloc (M.assign (|
M.alloc (M.write (|
M.index (|
result,
Binary.add (|
Expand All @@ -526,7 +526,7 @@ Definition base64_encode (InputBytes OutputElements : U32.t) (α : list Value.t)
|)
]] in
[[
M.alloc (M.assign (|
M.alloc (M.write (|
result,
M.call_closure (|
closure (base64_encode_elements (U32.Build_t 118)),
Expand Down
Loading

0 comments on commit 404cd2a

Please sign in to comment.