Skip to content

Instantly share code, notes, and snippets.

View JasonGross's full-sized avatar

Jason Gross JasonGross

186 followers · 11 following
View GitHub Profile
@JasonGross
JasonGross / p434_sqr_64.c
Created October 9, 2019 00:49
Fiat-crypto generated field arithmetic via `./src/ExtractionOCaml/word_by_word_montgomery --static p434_sqr_64 '(2^216 * 3^137 - 1)^2' 64 | tee p434_sqr_64.c` (takes about 18m)
/* Autogenerated */
/* curve description: p434_sqr_64 */
/* requested operations: (all) */
/* m = 0x4db194809d18b920f2ecf68816ae3d3d0063244f01221708ab42abe1b46445ab96af6359a5732ca2221c664b96c55f373d2cdca41254497c1b1d1197726074052fc75bf530873470f9d4ea2b8047d130a3a000000000000000000000000000000000000000000000000000001 (from "(2^216 * 3^137 - 1)^2") */
/* machine_wordsize = 64 (from "64") */
/* */
/* NOTE: In addition to the bounds specified above each function, all */
/* functions synthesized for this Montgomery arithmetic require the */
/* input to be strictly less than the prime modulus (m), and also */
/* require the input to be in the unique saturated representation. */
@JasonGross
JasonGross / fast_fin.v
Created May 23, 2019 02:42
Fast boolean equality proofs on finite types
Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Import ListNotations.
Lemma negb_existsb_nth_error {A} (ls : list A) (f : A -> bool) (H : existsb f ls = false) n v (H' : nth_error ls n = Some v)
: f v = false.
Proof.
revert dependent n; induction ls, n; cbn in *; intros; try congruence.
all: repeat first [ progress subst
| rewrite orb_false_iff in *
@JasonGross
JasonGross / bls12_381_q_64.c
Last active May 16, 2019 18:47
Fiat-Crypto (https://github.com/mit-plv/fiat-crypto) generated word-by-word montgomery reduction C code for 64-bit modular arithmetic for BLS12-381 based on info at https://z.cash/blog/new-snark-curve/
/* Autogenerated */
/* curve description: bls12_381_q */
/* requested operations: (all) */
/* m = 0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab (from "0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab") */
/* machine_wordsize = 64 (from "64") */
/* */
/* NOTE: In addition to the bounds specified above each function, all */
/* functions synthesized for this Montgomery arithmetic require the */
/* input to be strictly less than the prime modulus (m), and also */
/* require the input to be in the unique saturated representation. */
@JasonGross
JasonGross / named_intros.v
Created February 23, 2019 00:28
Require Import Coq.Strings.String.
Open Scope string_scope.
Definition with_name (n : string) {T} (v : T) := v.
(* ensures that the name [H] is free by renaming existing hypotheses *)
Ltac ensure_free H :=
try (* not sure how many [fresh]es I need, probably not more than 3 *)
let H' := fresh H in
let H' := fresh H' in
@JasonGross
JasonGross / update_record.v
Created November 29, 2018 20:40
Record updating notations
Definition marker {T} (v : T) := v.
Ltac apply_with_underscores f x :=
match constr:(Set) with
| _ => constr:(f x)
| _ => apply_with_underscores uconstr:(f _) x
@JasonGross
JasonGross / funext_from_interval.v
Created November 1, 2018 18:56
A derivation of function extensionality from the interval in Coq using private inductives
Module Import Interval.
Unset Elimination Schemes.
(** An [interval] is the quotient of [bool] under the trivial
relation, that [true = false]. Based on the real interval, we
call the left endpoint [zero], the right endpoint [one], and the
proof of equality [seg : zero = one]. *)
Private Inductive interval := zero | one.
Axiom seg : zero = one.
(** The eliminator for the interval says that if you send [zero]
@JasonGross
JasonGross / replace-notations.py
Last active May 6, 2020 13:37
Python script for dealing with deprecated notations in Coq
#!/usr/bin/env python3
import sys, re, os
from collections import defaultdict
# Authors: Jason Gross and Jean-Christophe Léchenet
#
# Usage: ./replace-notations.py logfile
# Uses the warnings in logfile to locate compatibility notation warnings,
# then search and replace to use the correct notations.
#
@JasonGross
JasonGross / fix.py
Last active May 20, 2020 05:16
Python script taking a log of `make` on stdin, which adds imports to fix numeral notations
#!/usr/bin/env python2
from __future__ import with_statement
import sys, re
MODULES = {'string': 'Coq.Strings.String',
'ascii': 'Coq.Strings.Ascii',
'Z': 'Coq.ZArith.BinIntDef',
'positive': 'Coq.PArith.BinPosDef',
'N': 'Coq.NArith.BinNatDef',
'R': 'Coq.Reals.Rdefinitions',
@JasonGross
JasonGross / has_syntax.v
Last active August 13, 2018 14:28
inductive of dependently typed syntax
Inductive has_syntax : forall {T}, T -> Type :=
| App {A} {B : A -> Type} (f : forall a : A, B a) (x : A)
: has_syntax f -> has_syntax x -> has_syntax (f x)
| Abs {A} {B : A -> Type} (f : forall a : A, B a)
: (forall a : A, has_syntax (f a)) -> has_syntax f
| Forall A (B : A -> Type)
: has_syntax A -> has_syntax B -> has_syntax (forall a : A, B a)
| O : has_syntax Datatypes.O
| S : has_syntax Datatypes.S
| tt : has_syntax Datatypes.tt
@JasonGross
JasonGross / ltac2app.v
Last active August 10, 2018 00:24
Require Import Coq.Init.Prelude.
Fixpoint fnd (n : nat) : Prop :=
match n with
| O => True
| S n => True /\ fnd n
end.
Fixpoint big_and (xs : list Prop) : Prop :=
match xs with