Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

More work on base64 proofs #5

Merged
merged 2 commits into from
Dec 10, 2024
Merged

More work on base64 proofs #5

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2fbc29e
proof: more work on base64
clarus Dec 2, 2024
76403b4
proof: simplify the proof thanks to autorewrite
clarus Dec 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions CoqOfNoir/CoqOfNoir.v
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading