Revision 7f5fe7453912332a9be00d1efc0f880d80f47a7c authored by François Dupressoir on 14 March 2022, 17:21:04 UTC, committed by François Dupressoir on 14 March 2022, 17:21:15 UTC
Some more work needs done to present a clean theory of prime order
groups, and use it properly.

We should also ensure that we can eventually support DH over cyclic
groups of composite order (operating over prime order subgroups)
1 parent 87ff7f8
History
File Mode Size
phl
system
dune -rw-r--r-- 449 bytes
ec.ml -rw-r--r-- 13.3 KB
ecAlgTactic.ml -rw-r--r-- 8.5 KB
ecAlgTactic.mli -rw-r--r-- 1.5 KB
ecAlgebra.ml -rw-r--r-- 13.7 KB
ecAlgebra.mli -rw-r--r-- 4.9 KB
ecBaseLogic.ml -rw-r--r-- 842 bytes
ecBigInt.ml -rw-r--r-- 5.0 KB
ecBigInt.mli -rw-r--r-- 390 bytes
ecBigIntCore.ml -rw-r--r-- 2.0 KB
ecCallbyValue.ml -rw-r--r-- 18.9 KB
ecCallbyValue.mli -rw-r--r-- 606 bytes
ecCommands.ml -rw-r--r-- 32.2 KB
ecCommands.mli -rw-r--r-- 2.0 KB
ecCoreFol.ml -rw-r--r-- 54.4 KB
ecCoreFol.mli -rw-r--r-- 14.5 KB
ecCoreGoal.ml -rw-r--r-- 36.3 KB
ecCoreGoal.mli -rw-r--r-- 16.6 KB
ecCoreHiPhl.ml -rw-r--r-- 2.6 KB
ecCoreHiPhl.mli -rw-r--r-- 985 bytes
ecCoreLib.ml -rw-r--r-- 6.9 KB
ecCoreLib.mli -rw-r--r-- 4.9 KB
ecDecl.ml -rw-r--r-- 9.2 KB
ecDecl.mli -rw-r--r-- 5.2 KB
ecEco.ml -rw-r--r-- 6.3 KB
ecEnv.ml -rw-r--r-- 112.6 KB
ecEnv.mli -rw-r--r-- 15.8 KB
ecField.ml -rw-r--r-- 6.3 KB
ecField.mli -rw-r--r-- 882 bytes
ecFol.ml -rw-r--r-- 29.0 KB
ecFol.mli -rw-r--r-- 6.5 KB
ecGState.ml -rw-r--r-- 4.1 KB
ecGState.mli -rw-r--r-- 1.8 KB
ecGenRegexp.ml -rw-r--r-- 10.5 KB
ecHiGoal.ml -rw-r--r-- 66.1 KB
ecHiGoal.mli -rw-r--r-- 4.4 KB
ecHiInductive.ml -rw-r--r-- 12.9 KB
ecHiInductive.mli -rw-r--r-- 2.1 KB
ecHiNotations.ml -rw-r--r-- 3.8 KB
ecHiNotations.mli -rw-r--r-- 1022 bytes
ecHiPredicates.ml -rw-r--r-- 3.3 KB
ecHiPredicates.mli -rw-r--r-- 924 bytes
ecHiTacticals.ml -rw-r--r-- 14.7 KB
ecHiTacticals.mli -rw-r--r-- 683 bytes
ecIdent.ml -rw-r--r-- 2.0 KB
ecIdent.mli -rw-r--r-- 1.5 KB
ecInductive.ml -rw-r--r-- 10.9 KB
ecInductive.mli -rw-r--r-- 3.0 KB
ecIo.ml -rw-r--r-- 7.2 KB
ecIo.mli -rw-r--r-- 1.3 KB
ecLexer.mll -rw-r--r-- 18.2 KB
ecLoader.ml -rw-r--r-- 5.3 KB
ecLoader.mli -rw-r--r-- 1.2 KB
ecLocation.ml -rw-r--r-- 3.1 KB
ecLocation.mli -rw-r--r-- 1.6 KB
ecLowGoal.ml -rw-r--r-- 82.9 KB
ecLowGoal.mli -rw-r--r-- 11.4 KB
ecLowPhlGoal.ml -rw-r--r-- 21.6 KB
ecMaps.ml -rw-r--r-- 4.3 KB
ecMatching.ml -rw-r--r-- 38.0 KB
ecMatching.mli -rw-r--r-- 6.4 KB
ecMemory.ml -rw-r--r-- 3.8 KB
ecMemory.mli -rw-r--r-- 2.7 KB
ecModules.ml -rw-r--r-- 21.3 KB
ecModules.mli -rw-r--r-- 7.1 KB
ecOptions.ml -rw-r--r-- 14.6 KB
ecOptions.mli -rw-r--r-- 1.8 KB
ecPException.ml -rw-r--r-- 1.7 KB
ecPException.mli -rw-r--r-- 583 bytes
ecPV.ml -rw-r--r-- 34.4 KB
ecPV.mli -rw-r--r-- 6.4 KB
ecParser.mly -rw-r--r-- 90.7 KB
ecParsetree.ml -rw-r--r-- 33.5 KB
ecPath.ml -rw-r--r-- 10.9 KB
ecPath.mli -rw-r--r-- 4.4 KB
ecPrinting.ml -rw-r--r-- 103.3 KB
ecPrinting.mli -rw-r--r-- 4.2 KB
ecProofTerm.ml -rw-r--r-- 31.0 KB
ecProofTerm.mli -rw-r--r-- 6.5 KB
ecProofTyping.ml -rw-r--r-- 7.5 KB
ecProofTyping.mli -rw-r--r-- 3.6 KB
ecProvers.ml -rw-r--r-- 15.0 KB
ecProvers.mli -rw-r--r-- 2.1 KB
ecReduction.ml -rw-r--r-- 58.4 KB
ecReduction.mli -rw-r--r-- 3.7 KB
ecRegexp.ml -rw-r--r-- 4.3 KB
ecRegexp.mli -rw-r--r-- 1.5 KB
ecRelocate.ml -rw-r--r-- 805 bytes
ecRelocate.mli -rw-r--r-- 84 bytes
ecRing.ml -rw-r--r-- 13.6 KB
ecRing.mli -rw-r--r-- 2.4 KB
ecScope.ml -rw-r--r-- 77.2 KB
ecScope.mli -rw-r--r-- 7.8 KB
ecSearch.ml -rw-r--r-- 3.5 KB
ecSearch.mli -rw-r--r-- 836 bytes
ecSection.ml -rw-r--r-- 47.8 KB
ecSection.mli -rw-r--r-- 1.7 KB
ecSmt.ml -rw-r--r-- 54.1 KB
ecSmt.mli -rw-r--r-- 1.2 KB
ecStrongRing.ml -rw-r--r-- 10.7 KB
ecSubst.ml -rw-r--r-- 20.3 KB
ecSubst.mli -rw-r--r-- 2.9 KB
ecSymbols.ml -rw-r--r-- 2.7 KB
ecSymbols.mli -rw-r--r-- 1.6 KB
ecTerminal.ml -rw-r--r-- 7.6 KB
ecTerminal.mli -rw-r--r-- 1.1 KB
ecThCloning.ml -rw-r--r-- 19.9 KB
ecThCloning.mli -rw-r--r-- 3.1 KB
ecTheory.ml -rw-r--r-- 3.1 KB
ecTheory.mli -rw-r--r-- 2.6 KB
ecTheoryReplay.ml -rw-r--r-- 38.0 KB
ecTheoryReplay.mli -rw-r--r-- 1.6 KB
ecTransMatching.ml -rw-r--r-- 4.1 KB
ecTransMatching.mli -rw-r--r-- 802 bytes
ecTypeClass.ml -rw-r--r-- 2.5 KB
ecTypeClass.mli -rw-r--r-- 841 bytes
ecTypes.ml -rw-r--r-- 31.8 KB
ecTypes.mli -rw-r--r-- 9.0 KB
ecTyping.ml -rw-r--r-- 101.8 KB
ecTyping.mli -rw-r--r-- 7.4 KB
ecUFind.ml -rw-r--r-- 5.5 KB
ecUFind.mli -rw-r--r-- 1.8 KB
ecUid.ml -rw-r--r-- 2.2 KB
ecUid.mli -rw-r--r-- 1.2 KB
ecUnify.ml -rw-r--r-- 14.1 KB
ecUnify.mli -rw-r--r-- 1.9 KB
ecUserMessages.ml -rw-r--r-- 26.6 KB
ecUserMessages.mli -rw-r--r-- 2.7 KB
ecUtils.ml -rw-r--r-- 20.6 KB
ecUtils.mli -rw-r--r-- 11.2 KB
ecVersion.ml -rw-r--r-- 951 bytes
ecVersion.mli -rw-r--r-- 598 bytes
ecWhy3Conv.ml -rw-r--r-- 6.4 KB
ecWhy3Conv.mli -rw-r--r-- 645 bytes

back to top