Turned the files in src into a lib called Core. #397
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Merged
strub
approved these changes
Jun 15, 2023
added 2 commits
June 15, 2023 16:22
The file ecCoreHiPhl was removed as dead code, no need to exclude it in the dune file anymore.
Cameron-Low
pushed a commit
that referenced
this pull request
Jul 3, 2023
Exposing some lower level substitution mechanisms and other refactorings. Some simplifications to ty_subst and e_subst Removing modtydef from f_subst WIP: Attempting to use high-level subst in ecReduction Switched to maps for ty_subst. Still needs some cleanup. Simplified e_subst and f_subst to just use a single ty_subst. Memories cannot always be freshened as they are still hardcoded Further cleanup Track the argument variables as well. Also update ROM proof. [ci] update actions to avoid node deprecation Commit b2106aa suppressed additional parentheses around match ... end in all circumstances, even though on the left and right of applications the parser requires parentheses, the theory being this makes it easier for humans to scan. So this commit inserts parentheses around matches in applications, but not elsewhere (e.g., not in infix operators). See below for examples. [The pretty printer needs a major redesign, so this is another stopgap measure.] require import AllCore List. type t = [ A of int | B of bool]. (* the following formulas now parse and pretty-print the same *) lemma foo1 (f : int -> bool) : f (match A 3 with | A a => a | B b => if b then 1 else 2 end). proof. abort. lemma foo2 : (match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4. proof. abort. lemma foo3 (f : (int -> int) -> (int -> int)) : f (match A 3 with | A a => fun _ => a | B b => fun _ => 2 end) 3 = 4. proof. abort. lemma foo4 (f : int -> bool) : f (1 + match A 3 with | A a => a | B b => if b then 1 else 2 end). proof. abort. lemma foo5 (f : int -> bool) : f (match A 3 with | A a => a | B b => if b then 1 else 2 end + 1). proof. abort. lemma foo6 (f : int -> bool) : f (3 + match A 3 with | A a => a | B b => if b then 1 else 2 end + 1). proof. abort. New Subtype theory. Updated stdlib to match. Updated examples to match new Subtype. clean up SubType theory use polymorpic wrapper to enable theory cloning [theories] FunRO: RO for FinType using dfun for init New command: proc op. This command generates an operator that computes the output distribution of a stateless proc. The command is in beta-mode. It misses: - a support for a larger set of instructions, - better error messages, - a registry of generated proc ops, and - a hoare/phoare statement that links the operator to the procedure. Accept non-printed variable only abbreviations. fix #382 Fix datatype comparisons for theory replays We do not need to check the inductive schemas: - if the constructors are compatible, so are the schemas, - anyway, they are going to be checked right after, and - at that point, they are not convertible because they come from incomaptible enclosing theories. Fix #381 Forbid the usage of [declare] for concrete modules. Fix #328 Removed Smart constructors for types, expressions, formulae, paths, and statements. [theories]: p_max (maximum probability for atomic events) Co-authored-by: Ethan Lee <[email protected]> warn on `Invalid` SMT results properly fail early if one SMT returns `Invalid` This was seemingly intended, but racy New rewrite-pr lemma: Pr[muE] Transform a Pr[...] statement into its pointwise summation. [lib] List: remove all raw smt calls [lib] FSet: fcard_eq1 Co-authored-by: Christian Doczkal <[email protected]> Tighten the ROM bad call results restore name Take PolyReduce theory from Kyber project Add choice-based inverses and fix broken proofs from subtype changes Co-authored-by: Pierre-Yves Strub <[email protected]> Remove dead code (#398) The file ecCoreHiPhl.ml seems to be dead code because: - It contains an open EcLogic which was deleted in 2014 (commit 6fe0ea9) - The last time it was modified (apart from licence headers) was in 2013 (commit f2e05e2) Turned the files in src into a lib called Core. (#397) * Turned the files in src into a lib called core. * Removed reference to dead code in dune file The file ecCoreHiPhl was removed as dead code, no need to exclude it in the dune file anymore. --------- Co-authored-by: Romain Tetley <[email protected]> New inline tactic We realized that sometimes we want to inline everything besides one procedure and found that it is cumbersome to have to list everything that has to be inlined instead of listing what should remain as is. So we decided to add this to the current inline. We should have kept the previous use cases identical as supported by the fact that nothing broke while not touching any old ec files. In doing so, we also added the possibility to provide the name of a module leading to inlining all the procedure in this module. Finally, one can now provide the name of a procedure and it will inline all the procedures with that name regardless of the module in which they belong. As already mentioned, one can find examples at the following link. https://github.com/EasyCrypt/easycrypt/blob/deploy-inline/examples/tactics/inline.ec start with parsing pattern matching on inline add some examples fix Remove dead code relating to substitution; instead, the f_subst mechanism should be used. (And this is in fact done for simplification of let formulas in EcReduction.) Keep f_let_simp Prove Fermat's little theorem Refactor out Fermat's little theorem from ZModP to IntDiv [theories] additional elimination rules for finite sums (#401) Rename fs_sty to fs_ty removed testing code Remove dead code Replaced low level path substitution
Boutry
pushed a commit
that referenced
this pull request
Jul 19, 2023
* Turned the files in src into a lib called core. * Removed reference to dead code in dune file The file ecCoreHiPhl was removed as dead code, no need to exclude it in the dune file anymore. --------- Co-authored-by: Romain Tetley <[email protected]>
This pull request was closed.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
As part of an effort to create a language server for easycrypt, it would be handy to access the ocaml lib that is used to compile the easycrypt executable.
This is done in this branch.