Skip to content

Instantly share code, notes, and snippets.

Jason Gross JasonGross

Block or report user

Report or block JasonGross

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@JasonGross
JasonGross / p434_sqr_64.c
Created Oct 9, 2019
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)
View p434_sqr_64.c
/* 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
Fast boolean equality proofs on finite types
View fast_fin.v
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
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/
View bls12_381_q_64.c
/* 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. */
View named_intros.v
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 Nov 29, 2018
Record updating notations
View update_record.v
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 Nov 1, 2018
A derivation of function extensionality from the interval in Coq using private inductives
View funext_from_interval.v
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 Oct 10, 2018
Python script for dealing with deprecated notations in Coq
View replace-notations.py
#!/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 Aug 24, 2018
Python script taking a log of `make` on stdin, which adds imports to fix numeral notations
View fix.py
#!/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 Aug 13, 2018
inductive of dependently typed syntax
View has_syntax.v
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
View ltac2app.v
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
You can’t perform that action at this time.