jadephilipoom
jadephilipoom
/ bedrockify_boringssl.patch
Created
July 10, 2020 14:31
Replace boringssl curve25519_64 function bodies with bedrock2 implementations
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| diff --git a/third_party/fiat/curve25519_64.h b/third_party/fiat/curve25519_64.h | |
| index 02679bbbd..a9bfe21e7 100644 | |
| --- a/third_party/fiat/curve25519_64.h | |
| +++ b/third_party/fiat/curve25519_64.h | |
| @@ -19,75 +19,6 @@ typedef unsigned __int128 fiat_25519_uint128; | |
| #endif | |
| -/* | |
| - * The function fiat_25519_addcarryx_u51 is an addition with carry. |
jadephilipoom
/ Crypto.Bedrock.Tests.X25519_64.mulmod_bedrock.out
Created
March 12, 2020 17:49
Fiat-crypto X25519 64-bit mulmod, in bedrock2
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| = ("mulmod_bedrock", | |
| (bedrock_call_lhs:("in0", "in1", "out0"), []%list, | |
| bedrock_func_body:((((("x0" = | |
| (load( constr:(expr.var "in0") + | |
| constr:(expr.literal 0)))); | |
| ("x1" = | |
| (load( constr:(expr.var "in0") + | |
| constr:(expr.literal 8)))); | |
| ("x2" = | |
| (load( constr:(expr.var "in0") + |
jadephilipoom
/ Combinators.v
Last active
October 7, 2019 17:07
Record of the "protocols" branch of fiat-crypto
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.Lists.List. | |
| Create HintDb trace_combinators discriminated. | |
| Fixpoint holds_of_messages_around_nth_messages_matching_aux | |
| (is_n : nat -> Prop) | |
| (if_none_found : Prop) | |
| {T} | |
| (matcher : T -> Prop) | |
| (property : list T -> T -> list T -> Prop) |
jadephilipoom
/ pdfdiff.bash
Last active
February 9, 2022 04:52
Pretty PDF diff using wdiff and MarkDown
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| wdiff -n -w $'~~' -x $'~~' -y $'\\textcolor{blue}{' -z '}' base.md new.md | pandoc -o diff.pdf |