https://github.com/EasyCrypt/easycrypt
Revision d809ef878b302f324c3d94eb1344b7e0e19e2a87 authored by François Dupressoir on 13 April 2021, 15:50:46 UTC, committed by François Dupressoir on 13 April 2021, 15:50:46 UTC
This instantiates BigOp for Booleans (with xor, or, and and) and gets rid of the old Monoid library, which Hybrid arguments relied upon. Some proof cleaning left to do in Hybrid, Indist, and PKE_Hybrid.
1 parent 1b25ed4
Tip revision: d809ef878b302f324c3d94eb1344b7e0e19e2a87 authored by François Dupressoir on 13 April 2021, 15:50:46 UTC
StdLib: use bigops in generic Hybrid
StdLib: use bigops in generic Hybrid
Tip revision: d809ef8
| File | Mode | Size |
|---|---|---|
| phl | ||
| system | ||
| ec.ml | -rw-r--r-- | 13.4 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.0 KB |
| ecCallbyValue.mli | -rw-r--r-- | 250 bytes |
| ecCommands.ml | -rw-r--r-- | 32.6 KB |
| ecCommands.mli | -rw-r--r-- | 2.0 KB |
| ecCoreFol.ml | -rw-r--r-- | 53.8 KB |
| ecCoreFol.mli | -rw-r--r-- | 14.3 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.5 KB |
| ecCoreLib.mli | -rw-r--r-- | 4.7 KB |
| ecDecl.ml | -rw-r--r-- | 8.7 KB |
| ecDecl.mli | -rw-r--r-- | 4.9 KB |
| ecEco.ml | -rw-r--r-- | 5.0 KB |
| ecEnv.ml | -rw-r--r-- | 108.2 KB |
| ecEnv.mli | -rw-r--r-- | 15.0 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 |
| ecFortune.ml | -rw-r--r-- | 1.8 KB |
| ecFortune.mli | -rw-r--r-- | 488 bytes |
| 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-- | 62.7 KB |
| ecHiGoal.mli | -rw-r--r-- | 4.2 KB |
| ecHiInductive.ml | -rw-r--r-- | 13.0 KB |
| ecHiInductive.mli | -rw-r--r-- | 2.3 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-- | 9.5 KB |
| ecInductive.mli | -rw-r--r-- | 2.7 KB |
| ecIo.ml | -rw-r--r-- | 7.1 KB |
| ecIo.mli | -rw-r--r-- | 1.3 KB |
| ecLexer.mll | -rw-r--r-- | 17.9 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.2 KB |
| ecMaps.ml | -rw-r--r-- | 4.1 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-- | 18.9 KB |
| ecModules.mli | -rw-r--r-- | 6.6 KB |
| ecOptions.ml | -rw-r--r-- | 14.4 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-- | 32.8 KB |
| ecPV.mli | -rw-r--r-- | 6.2 KB |
| ecParser.mly | -rw-r--r-- | 88.3 KB |
| ecParsetree.ml | -rw-r--r-- | 31.9 KB |
| ecPath.ml | -rw-r--r-- | 10.9 KB |
| ecPath.mli | -rw-r--r-- | 4.4 KB |
| ecPrinting.ml | -rw-r--r-- | 98.5 KB |
| ecPrinting.mli | -rw-r--r-- | 4.1 KB |
| ecProofTerm.ml | -rw-r--r-- | 30.0 KB |
| ecProofTerm.mli | -rw-r--r-- | 6.3 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-- | 45.2 KB |
| ecReduction.mli | -rw-r--r-- | 3.4 KB |
| ecRegexp.ml | -rw-r--r-- | 4.3 KB |
| ecRegexp.mli | -rw-r--r-- | 1.5 KB |
| ecRing.ml | -rw-r--r-- | 13.6 KB |
| ecRing.mli | -rw-r--r-- | 2.4 KB |
| ecScope.ml | -rw-r--r-- | 82.6 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-- | 14.8 KB |
| ecSection.mli | -rw-r--r-- | 1.8 KB |
| ecSmt.ml | -rw-r--r-- | 53.0 KB |
| ecSmt.mli | -rw-r--r-- | 1.2 KB |
| ecStrongRing.ml | -rw-r--r-- | 10.7 KB |
| ecSubst.ml | -rw-r--r-- | 20.7 KB |
| ecSubst.mli | -rw-r--r-- | 2.5 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-- | 17.7 KB |
| ecThCloning.mli | -rw-r--r-- | 2.6 KB |
| ecTheory.ml | -rw-r--r-- | 3.5 KB |
| ecTheory.mli | -rw-r--r-- | 3.0 KB |
| ecTheoryReplay.ml | -rw-r--r-- | 22.1 KB |
| ecTheoryReplay.mli | -rw-r--r-- | 2.1 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-- | 30.8 KB |
| ecTypes.mli | -rw-r--r-- | 8.6 KB |
| ecTyping.ml | -rw-r--r-- | 93.1 KB |
| ecTyping.mli | -rw-r--r-- | 7.0 KB |
| ecUFind.ml | -rw-r--r-- | 5.6 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.0 KB |
| ecUnify.mli | -rw-r--r-- | 1.9 KB |
| ecUserMessages.ml | -rw-r--r-- | 25.8 KB |
| ecUserMessages.mli | -rw-r--r-- | 2.7 KB |
| ecUtils.ml | -rw-r--r-- | 20.4 KB |
| ecUtils.mli | -rw-r--r-- | 11.0 KB |
| ecVersion.ml.in | -rw-r--r-- | 801 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 ...
