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
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 |
Computing file changes ...