diff options
| -rw-r--r-- | Makefile | 13 | ||||
| -rw-r--r-- | _CoqProject | 8 | ||||
| -rw-r--r-- | src/Reflection/Z/CNotations.v | 163 | ||||
| -rw-r--r-- | src/Reflection/Z/JavaNotations.v | 151 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/AddDisplay.v | 4 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/AddJavaDisplay.v | 4 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/LadderStepDisplay.v | 4 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/LadderStepJavaDisplay.v | 4 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/MulDisplay.v | 4 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Reified/MulJavaDisplay.v | 4 |
10 files changed, 359 insertions, 0 deletions
@@ -12,6 +12,7 @@ HIDE := $(if $(VERBOSE),,@) .PHONY: coq clean update-_CoqProject cleanall install \ install-coqprime clean-coqprime coqprime \ + display \ specific non-specific \ small-specific-gen medium-specific-gen specific-gen \ extraction ghc @@ -54,12 +55,16 @@ SPECIFIC_GEN_VO := $(filter src/SpecificGen/%,$(VOFILES)) MEDIUM_SPECIFIC_GEN_VO := $(filter-out src/SpecificGen/GF5211_32%,$(SPECIFIC_GEN_VO)) SMALL_SPECIFIC_GEN_VO := $(filter-out src/SpecificGen/GF41417_32%,$(MEDIUM_SPECIFIC_GEN_VO)) NON_SPECIFIC_VO := $(filter-out $(SPECIFIC_VO),$(VO_FILES)) +DISPLAY_VO := $(filter src/Specific/%Display.vo src/SpecificGen/%Display.vo,$(VOFILES)) +DISPLAY_JAVA_VO := $(filter src/Specific/%JavaDisplay.vo src/SpecificGen/%JavaDisplay.vo,$(DISPLAY_VO)) +DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO)) specific: $(SPECIFIC_VO) coqprime specific-gen: $(SPECIFIC_GEN_VO) coqprime medium-specific-gen: $(MEDIUM_SPECIFIC_GEN_VO) coqprime small-specific-gen: $(SMALL_SPECIFIC_GEN_VO) coqprime non-specific: $(NON_SPECIFIC_VO) coqprime +display: $(DISPLAY_VO:.vo=.log) coqprime coq: $(COQ_VOFILES) coqprime ifneq ($(filter 8.4%,$(COQ_VERSION)),) # 8.4 @@ -92,6 +97,14 @@ Makefile.coq: Makefile _CoqProject $(SHOW)'COQ_MAKEFILE -f _CoqProject > $@' $(HIDE)$(COQBIN)coq_makefile -f _CoqProject | sed s'|^\(-include.*\)$$|ifneq ($$(filter-out $(FAST_TARGETS),$$(MAKECMDGOALS)),)~\1~else~ifeq ($$(MAKECMDGOALS),)~\1~endif~endif|g' | tr '~' '\n' | sed s'/^clean:$$/clean::/g' | sed s'/^Makefile: /Makefile-old: /g' | sed s'/^printenv:$$/printenv::/g' > $@ +$(DISPLAY_NON_JAVA_VO:.vo=.log) : %Display.log : %.vo %Display.v src/Reflection/Z/CNotations.vo + $(SHOW)"COQC $*Display > $@" + $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*Display.v > $@.tmp && mv -f $@.tmp $@ + +$(DISPLAY_JAVA_VO:.vo=.log) : %JavaDisplay.log : %.vo %JavaDisplay.v src/Reflection/Z/CNotations.vo + $(SHOW)"COQC $*JavaDisplay > $@" + $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*JavaDisplay.v > $@.tmp && mv -f $@.tmp $@ + src/Experiments/Ed25519_noimports.hs: src/Experiments/Ed25519Extraction.vo src/Experiments/Ed25519Extraction.v src/Experiments/Ed25519.hs: src/Experiments/Ed25519_noimports.hs src/Experiments/Ed25519_imports.hs diff --git a/_CoqProject b/_CoqProject index 81613d8aa..db28e36c1 100644 --- a/_CoqProject +++ b/_CoqProject @@ -153,10 +153,12 @@ src/Reflection/Named/NameUtil.v src/Reflection/Named/RegisterAssign.v src/Reflection/Named/Syntax.v src/Reflection/Z/BinaryNotationConstants.v +src/Reflection/Z/CNotations.v src/Reflection/Z/HexNotationConstants.v src/Reflection/Z/Interpretations128.v src/Reflection/Z/Interpretations64.v src/Reflection/Z/InterpretationsGen.v +src/Reflection/Z/JavaNotations.v src/Reflection/Z/OpInversion.v src/Reflection/Z/Reify.v src/Reflection/Z/Syntax.v @@ -197,12 +199,18 @@ src/Specific/GF25519Reflective/CommonUnOpWireToFE.v src/Specific/GF25519Reflective/Reified.v src/Specific/GF25519Reflective/Reified/Add.v src/Specific/GF25519Reflective/Reified/AddCoordinates.v +src/Specific/GF25519Reflective/Reified/AddDisplay.v +src/Specific/GF25519Reflective/Reified/AddJavaDisplay.v src/Specific/GF25519Reflective/Reified/CarryAdd.v src/Specific/GF25519Reflective/Reified/CarryOpp.v src/Specific/GF25519Reflective/Reified/CarrySub.v src/Specific/GF25519Reflective/Reified/GeModulus.v src/Specific/GF25519Reflective/Reified/LadderStep.v +src/Specific/GF25519Reflective/Reified/LadderStepDisplay.v +src/Specific/GF25519Reflective/Reified/LadderStepJavaDisplay.v src/Specific/GF25519Reflective/Reified/Mul.v +src/Specific/GF25519Reflective/Reified/MulDisplay.v +src/Specific/GF25519Reflective/Reified/MulJavaDisplay.v src/Specific/GF25519Reflective/Reified/Opp.v src/Specific/GF25519Reflective/Reified/Pack.v src/Specific/GF25519Reflective/Reified/PreFreeze.v diff --git a/src/Reflection/Z/CNotations.v b/src/Reflection/Z/CNotations.v new file mode 100644 index 000000000..764094c99 --- /dev/null +++ b/src/Reflection/Z/CNotations.v @@ -0,0 +1,163 @@ +Require Export Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Z.Syntax. +Require Export Crypto.Reflection.Z.HexNotationConstants. +Require Export Crypto.Util.Notations. + +Reserved Notation "T x = A ; b" (at level 200, b at level 200, format "T x = A ; '//' b"). +Reserved Notation "'(bool)' x" (at level 200, x at level 9). +Reserved Notation "'(uint8_t)' x" (at level 200, x at level 9). +Reserved Notation "'(uint16_t)' x" (at level 200, x at level 9). +Reserved Notation "'(uint32_t)' x" (at level 200, x at level 9). +Reserved Notation "'(uint64_t)' x" (at level 200, x at level 9). +Reserved Notation "'(uint128_t)' x" (at level 200, x at level 9). +Reserved Notation "x & y" (at level 40). + +Global Open Scope expr_scope. + +Notation "T x = A ; b" := (LetIn (tx:=T) A (fun x => b)) : expr_scope. +(*Notation uint32_t := (_ (TWord 5)). +Notation uint64_t := (_ (TWord 6)). +Notation uint128_t := (_ (TWord 7)).*) +(* +Notation bool := (Tbase (TWord 0)). +Notation "'uint8_t'" := (Tbase (TWord 1)). +Notation "'uint8_t'" := (Tbase (TWord 2)). +Notation "'uint8_t'" := (Tbase (TWord 3)). +Notation uint16_t := (Tbase (TWord 4)). +Notation uint32_t := (Tbase (TWord 5)). +Notation uint64_t := (Tbase (TWord 6)). +Notation uint128_t := (Tbase (TWord 7)). +Notation "'(bool)' x" := (Op (Cast _ (TWord 0)) x). +Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 1)) x). +Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 2)) x). +Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 3)) x). +Notation "'(uint16_t)' x" := (Op (Cast _ (TWord 4)) x). +Notation "'(uint32_t)' x" := (Op (Cast _ (TWord 5)) x). +Notation "'(uint64_t)' x" := (Op (Cast _ (TWord 6)) x). +Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) x). +Notation "'(bool)' x" := (Op (Cast _ (TWord 0)) (Var x)). +Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 1)) (Var x)). +Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 2)) (Var x)). +Notation "'(uint8_t)' x" := (Op (Cast _ (TWord 3)) (Var x)). +Notation "'(uint16_t)' x" := (Op (Cast _ (TWord 4)) (Var x)). +Notation "'(uint32_t)' x" := (Op (Cast _ (TWord 5)) (Var x)). +Notation "'(uint64_t)' x" := (Op (Cast _ (TWord 6)) (Var x)). +Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) (Var x)). +*) +Notation "x + y" := (Op (Add) (Pair x y)). +Notation "x + y" := (Op (Add) (Pair (Var x) y)). +Notation "x + y" := (Op (Add) (Pair x (Var y))). +Notation "x + y" := (Op (Add) (Pair (Var x) (Var y))). +Notation "x - y" := (Op (Sub) (Pair x y)). +Notation "x - y" := (Op (Sub) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub) (Pair x (Var y))). +Notation "x - y" := (Op (Sub) (Pair (Var x) (Var y))). +Notation "x * y" := (Op (Mul) (Pair x y)). +Notation "x * y" := (Op (Mul) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul) (Pair x (Var y))). +Notation "x * y" := (Op (Mul) (Pair (Var x) (Var y))). +(* python: +<< +for opn, op in (('*', 'Mul'), ('+', 'Add'), ('&', 'Land')): + for lgwordsz in (5, 6, 7): + for side in ('l', 'r'): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + lhs = (lhs if side != 'l' else '(Op (Cast _ (TWord %d)) %s)' % (lgwordsz, lhs)) + rhs = ('y' if not v2 else '(Var y)') + rhs = (rhs if side != 'r' else '(Op (Cast _ (TWord %d)) %s)' % (lgwordsz, rhs)) + print('Notation "x %s y" := (Op (%s (TWord %d)) (Pair %s %s)).' % (opn, op, lgwordsz, lhs, rhs)) +>> *) +(* +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). +*) +Notation "x >> y" := (Op (Shr) (Pair x y)). +Notation "x >> y" := (Op (Shr) (Pair (Var x) y)). +Notation "x >> y" := (Op (Shr) (Pair x (Var y))). +Notation "x >> y" := (Op (Shr) (Pair (Var x) (Var y))). +(* +Notation "x >> y" := (Op (Shr _) (Pair x (Op (Cast _ _) y))). +Notation "x >> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) y))). +Notation "x >> y" := (Op (Shr _) (Pair x (Op (Cast _ _) (Var y)))). +Notation "x >> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) (Var y)))). +*) +Notation "x & y" := (Op (Land) (Pair x y)). +Notation "x & y" := (Op (Land) (Pair (Var x) y)). +Notation "x & y" := (Op (Land) (Pair x (Var y))). +Notation "x & y" := (Op (Land) (Pair (Var x) (Var y))). +(* +Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). +Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). +Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). +Notation "x & y" := (Op (Land (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). +Notation "x & y" := (Op (Land (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). +Notation "x & y" := (Op (Land (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x & y" := (Op (Land (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). +Notation "x & y" := (Op (Land (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). +*) +Notation Return x := (Var x). +Notation C_like := (Expr base_type op _). diff --git a/src/Reflection/Z/JavaNotations.v b/src/Reflection/Z/JavaNotations.v new file mode 100644 index 000000000..4a33a6330 --- /dev/null +++ b/src/Reflection/Z/JavaNotations.v @@ -0,0 +1,151 @@ +Require Export Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Z.Syntax. +Require Export Crypto.Reflection.Z.HexNotationConstants. +Require Export Crypto.Util.Notations. + +Reserved Notation "T x = A ; b" (at level 200, b at level 200, format "T x = A ; '//' b"). +Reserved Notation "'(int)' x" (at level 200, x at level 9). +Reserved Notation "'(long)' x" (at level 200, x at level 9). +Reserved Notation "'(uint128_t)' x" (at level 200, x at level 9). +Reserved Notation "x & y" (at level 40). +(* N.B. M32 is 0xFFFFFFFFL, and is how to cast a 64-bit thing to a 32-bit thing in Java *) +Reserved Notation "'M32' & x" (at level 200, x at level 9). + +Global Open Scope expr_scope. + +Notation "T x = A ; b" := (LetIn (tx:=T) A (fun x => b)) : expr_scope. +(* +Notation "'int'" := (Tbase (TWord 0)). +Notation "'int'" := (Tbase (TWord 1)). +Notation "'int'" := (Tbase (TWord 2)). +Notation "'int'" := (Tbase (TWord 3)). +Notation "'int'" := (Tbase (TWord 4)). +Notation "'int'" := (Tbase (TWord 5)). +Notation long := (Tbase (TWord 6)). +Notation uint128_t := (Tbase (TWord 7)). +Notation "'(int)' x" := (Op (Cast _ (TWord 0)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 1)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 2)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 3)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 4)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 5)) x). +Notation "'M32' & x" := (Op (Cast _ (TWord 6)) x). +Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) x). +Notation "'(int)' x" := (Op (Cast _ (TWord 0)) (Var x)). +Notation "'(int)' x" := (Op (Cast _ (TWord 1)) (Var x)). +Notation "'(int)' x" := (Op (Cast _ (TWord 2)) (Var x)). +Notation "'(int)' x" := (Op (Cast _ (TWord 3)) (Var x)). +Notation "'(int)' x" := (Op (Cast _ (TWord 4)) (Var x)). +Notation "'(int)' x" := (Op (Cast _ (TWord 5)) (Var x)). +Notation "'M32' & x" := (Op (Cast _ (TWord 6)) (Var x)). +Notation "'(uint128_t)' x" := (Op (Cast _ (TWord 7)) (Var x)). +*) +Notation "x + y" := (Op (Add) (Pair x y)). +Notation "x + y" := (Op (Add) (Pair (Var x) y)). +Notation "x + y" := (Op (Add) (Pair x (Var y))). +Notation "x + y" := (Op (Add) (Pair (Var x) (Var y))). +Notation "x - y" := (Op (Sub) (Pair x y)). +Notation "x - y" := (Op (Sub) (Pair (Var x) y)). +Notation "x - y" := (Op (Sub) (Pair x (Var y))). +Notation "x - y" := (Op (Sub) (Pair (Var x) (Var y))). +Notation "x * y" := (Op (Mul) (Pair x y)). +Notation "x * y" := (Op (Mul) (Pair (Var x) y)). +Notation "x * y" := (Op (Mul) (Pair x (Var y))). +Notation "x * y" := (Op (Mul) (Pair (Var x) (Var y))). +(* python: +<< +for opn, op in (('*', 'Mul'), ('+', 'Add'), ('&', 'Land')): + for lgwordsz in (5, 6, 7): + for side in ('l', 'r'): + for v1 in (False, True): + for v2 in (False, True): + lhs = ('x' if not v1 else '(Var x)') + lhs = (lhs if side != 'l' else '(Op (Cast _ (TWord %d)) %s)' % (lgwordsz, lhs)) + rhs = ('y' if not v2 else '(Var y)') + rhs = (rhs if side != 'r' else '(Op (Cast _ (TWord %d)) %s)' % (lgwordsz, rhs)) + print('Notation "x %s y" := (Op (%s (TWord %d)) (Pair %s %s)).' % (opn, op, lgwordsz, lhs, rhs)) +>> *) +(* +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). +Notation "x * y" := (Op (Mul (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). +Notation "x * y" := (Op (Mul (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). +Notation "x * y" := (Op (Mul (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) y)). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) x) (Var y))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) y)). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Op (Cast _ (TWord 5)) (Var x)) (Var y))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) y))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair x (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) y))). +Notation "x + y" := (Op (Add (TWord 5)) (Pair (Var x) (Op (Cast _ (TWord 5)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). +Notation "x + y" := (Op (Add (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). +Notation "x + y" := (Op (Add (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). +*) +Notation "x >>> y" := (Op (Shr) (Pair x y)). +Notation "x >>> y" := (Op (Shr) (Pair (Var x) y)). +Notation "x >>> y" := (Op (Shr) (Pair x (Var y))). +Notation "x >>> y" := (Op (Shr) (Pair (Var x) (Var y))). +(* +Notation "x >>> y" := (Op (Shr _) (Pair x (Op (Cast _ _) y))). +Notation "x >>> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) y))). +Notation "x >>> y" := (Op (Shr _) (Pair x (Op (Cast _ _) (Var y)))). +Notation "x >>> y" := (Op (Shr _) (Pair (Var x) (Op (Cast _ _) (Var y)))). +*) +Notation "x & y" := (Op (Land) (Pair x y)). +Notation "x & y" := (Op (Land) (Pair (Var x) y)). +Notation "x & y" := (Op (Land) (Pair x (Var y))). +Notation "x & y" := (Op (Land) (Pair (Var x) (Var y))). +(* +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) y)). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) x) (Var y))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) y)). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Op (Cast _ (TWord 6)) (Var x)) (Var y))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) y))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair x (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) y))). +Notation "x & y" := (Op (Land (TWord 6)) (Pair (Var x) (Op (Cast _ (TWord 6)) (Var y)))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) y)). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) x) (Var y))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) y)). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Op (Cast _ (TWord 7)) (Var x)) (Var y))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) y))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair x (Op (Cast _ (TWord 7)) (Var y)))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) y))). +Notation "x & y" := (Op (Land (TWord 7)) (Pair (Var x) (Op (Cast _ (TWord 7)) (Var y)))). +*) +Notation Return x := (Var x). +Notation Java_like := (Expr base_type op _). diff --git a/src/Specific/GF25519Reflective/Reified/AddDisplay.v b/src/Specific/GF25519Reflective/Reified/AddDisplay.v new file mode 100644 index 000000000..27b5519a3 --- /dev/null +++ b/src/Specific/GF25519Reflective/Reified/AddDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.GF25519Reflective.Reified.Add. +Require Export Crypto.Reflection.Z.CNotations. + +Print raddW. diff --git a/src/Specific/GF25519Reflective/Reified/AddJavaDisplay.v b/src/Specific/GF25519Reflective/Reified/AddJavaDisplay.v new file mode 100644 index 000000000..3daefb168 --- /dev/null +++ b/src/Specific/GF25519Reflective/Reified/AddJavaDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.GF25519Reflective.Reified.Add. +Require Export Crypto.Reflection.Z.JavaNotations. + +Print raddW. diff --git a/src/Specific/GF25519Reflective/Reified/LadderStepDisplay.v b/src/Specific/GF25519Reflective/Reified/LadderStepDisplay.v new file mode 100644 index 000000000..9e395e4eb --- /dev/null +++ b/src/Specific/GF25519Reflective/Reified/LadderStepDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.GF25519Reflective.Reified.LadderStep. +Require Export Crypto.Reflection.Z.CNotations. + +Print rladderstepW. diff --git a/src/Specific/GF25519Reflective/Reified/LadderStepJavaDisplay.v b/src/Specific/GF25519Reflective/Reified/LadderStepJavaDisplay.v new file mode 100644 index 000000000..34afd08b6 --- /dev/null +++ b/src/Specific/GF25519Reflective/Reified/LadderStepJavaDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.GF25519Reflective.Reified.LadderStep. +Require Export Crypto.Reflection.Z.JavaNotations. + +Print rladderstepW. diff --git a/src/Specific/GF25519Reflective/Reified/MulDisplay.v b/src/Specific/GF25519Reflective/Reified/MulDisplay.v new file mode 100644 index 000000000..8ab2f65dc --- /dev/null +++ b/src/Specific/GF25519Reflective/Reified/MulDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.GF25519Reflective.Reified.Mul. +Require Export Crypto.Reflection.Z.CNotations. + +Print rmulW. diff --git a/src/Specific/GF25519Reflective/Reified/MulJavaDisplay.v b/src/Specific/GF25519Reflective/Reified/MulJavaDisplay.v new file mode 100644 index 000000000..ed82f9e6c --- /dev/null +++ b/src/Specific/GF25519Reflective/Reified/MulJavaDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.GF25519Reflective.Reified.Mul. +Require Export Crypto.Reflection.Z.JavaNotations. + +Print rmulW. |