adampetcher / fcf Goto Github PK
View Code? Open in Web Editor NEWFoundational Cryptography Framework for machine-checked proofs of cryptography.
License: Other
Foundational Cryptography Framework for machine-checked proofs of cryptography.
License: Other
In various tactics such as fcf_skip, the use of "intuition" leads to this warning in Coq 8.17:
Warning:
"auto with *" was used through the default "intuition_solver" tactic.
This will be replaced by just "auto" in the future.
The quick-and-dirty way to fix this is to replace intuition
with intuition auto with *
. The cleaner way to fix it is intuition auto with XXX
where XXX is the set of hint databases you really need.
If you like, you can remove the entire ESPADA directory. I don't plan to maintain this proof. If you do this, create a ticket (assigned to me) reminding me to look through this proof and see if there is any useful theory that should be extracted.
@adampetcher
COQC Rat.v
File "./Rat.v", line 188, characters 2-26:
Error: Found no subterm matching "(x * n1)%nat" in the current goal.
We need to fix the following copyright and license issues:
As described in PrincetonUniversity/VST#290, the use of Qed
when creating typeclass instances makes it so that you can't evaluate expressions using the typeclass:
Compute 1 ?= 1.
= (let (eqb, _) := nat_EqDec in eqb) 1 1
The instances in EqDec.v
that currently end in Qed
and shoulde be changed to Defined
are:
Vector_EqDec
unit_EqDec
bool_EqDec
nat_EqDec
option_EqDec
list_EqDec
Hello,
I am considering using this library in a project, and I noticed that this repository does not seem to contain any information about copyright/patent licensing. https://github.com/PrincetonUniversity/VST/blob/master/LICENSE says that its imported copy of fcf is released under the 2-clause BSD license. If this is also true for this repository, please
Add a corresponding license file into the root directory of the project (e.g., from https://github.com/IQAndreas/markdown-licenses/blob/master/bsd-2.md)
Add a short license header to each file (possibly using the 10-line shell script from https://stackoverflow.com/questions/151677/tool-for-adding-license-headers-to-source-files), for example
(* Copyright 2010 <AUTHOR>. All rights reserved.
* Use of this source code is governed by a BSD-style
* license that can be found in the LICENSE file. *)
(patents) if something similar to https://golang.org/PATENTS is true about this project as well, add a corresponding statement to a corresponding file. This is not implied by the BSD-2 license, and some may be comfortable using this code without it, but IMHO it is easier to add the statement (if it is true) than to convince somebody's employer that they don't need it to use the code.
The options I outlined here are almost straight from http://choosealicense.com/, you can see there for more information and alternatives.
Thanks,
Andres
Since FCF is useful and seems to have at least one maintainer (for example, @andres-erbsen), I suggest that FCF should be released via opam in the coq-released archive, and then added to the Coq Platform.
Does anyone else think this is a good idea, and is anybody willing to be a "maintainer" for the purposes of this process? If so, there's at least one member of the Coq Platform board who will advocate for it.
There are a lot of deprecation warnings when compiling FCF with Coq 8.16. It might be worth fixing these, to save trouble in the future.
Currently, a project using FCF as a module gets all FCF filenames in the root namespace, e.g.
"Require Import Asymptotic" refers to FCF-s notion of asymptotic, and effectively prevents use of any library of the same name. I think it would make sense to change FCF _Coqproject to -R . FCF
. In that case importers would need to type "Require Import FCF.Asymptotic". Should I go do it and make a PR?
Since omega
is now deprecated, it would be a good idea to use lia
everywhere instead.
`I would prefer to keep the non-building files in the repo for the following reasons:
They still can be useful illustrations (especially the examples).
There may be some argument in there that is needed in the future, and it would be easier to fix the file than to develop it from scratch. A person probably wouldn't think to look in the history for "almost working" theory.
That being said, some of the non-building files are definitely old junk that needs to be removed. So I suggest:
Leave these files in and exclude them from the build. If you like, you can move the non-building files to a separate directory to simplify the build.
Create a ticket (assigned to me) reminding me to go through and clean up these broken files. Useless ones should be removed, valuable ones should be fixed.` @adampetcher
The files are now under src/FCF/Broken
, with non-building bits commented out.
I'm working on a class project to use FCF to prove some things about the Luby-Rackoff construction (basically section 6 from the following paper http://www.shoup.net/papers/games.pdf).
I'm not sure about the purpose of getSupport but I see that it is used in a lot of places. Can you provide a description?
Thanks!
Erik
I was trying to use IND_CPA_SecretKey_equiv
from Encryption_2W.v
, but building Encryption_2W.v
seems to fail on the line:
Context
{EncryptionScheme_SecretKey}`.
I couldn't find EncryptionScheme_SecretKey
in the file directory or the Git commit history. Looks like it was never committed? What would need to be done to get this file to compile?
Since Coq 8.13 (plus or minus), the Instance and Hint Resolve require a locality annotation, such as Global
or Local
or #[export]
. Without the annotation, one gets a deprecation warning message. Here's an example from compiling FCF in Coq 8.15.1:
File ".\fcf/src/FCF/EqDec.v", line 387, characters 0-62:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
For strict compatibility with previous FCF behavior, you would add Global before each such Instance or Hint. But I would suggest instead using #[export]
. For clients that do Require Import, there will be no difference. Clients that do Require without Import will be affected. Anyway, one way or another I would like to stop seeing these deprecation messages.
@adampetcher What's the current status of FCF? I see recent additions by @JasonGross, @andres-erbsen and @natelaunchbury.
Are there other projects using FCF?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.