The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Oh man, I'm sorry guys. I was trying to do that, but I didn't think the dependencies would be so big. I guess what I thought was that one could see what it was without my source, which was really a silly idea.

Actually, we depend on much of the RockSalt library in order to do our work, so if you download that, it comes with a Makefile. The only one of our files that you might need is now included on the github gist, it's PEFormat.v, but the script also depends on FastVerifier.v, and it's dependency chain is much greater. I think that if you just place the script in the RockSalt directory like so:

RockSalt/x86Model/proj/explanation.v

RockSalt/x86Model/proj/PEFormat.v

You can compile it after compiling the RockSalt/x86Model/Model and RockSalt/x86Model/RockSalt folders with

coqc -q -I ../Model PEFormat.v

and so on...

Here's RockSalt:

http://sos.cse.lehigh.edu/gonative/

Thank you so much, I appreciate it a lot. :)

On Sat, Dec 8, 2012 at 6:19 AM, AUGER Cédric <sedrikov AT gmail.com> wrote:

I am not sure it is required but the link you gave lack a lot of stuff.
Indicate at least what libraries you use (and try to interpret your
file, as the first non comment line cannot even be interpreted).


Le Sat,  8 Dec 2012 02:23:54 +0100 (CET),
<kennethadammiller AT gmail.com> a écrit :

> So, I've proved simple things before with Coq, which is like the
> boolean expressions and handling lists such as what are at the
> Software Foundations (up to the part on polymorphism on Lists).
>
> http://www.cis.upenn.edu/~bcpierce/sf/
>
> But I haven't yet done anything about proving a function, or at least
> maybe it's just that I'm having a hard time getting started. Anyway,
> I don't know if just proceeding to the part on functions will help me
> enough, because I need to get this done rather quickly, but the issue
> is explained at the gist link below.
>
> https://gist.github.com/1a09c8fc1cdd98bd40d4
>
> I talked on IRC, and I was told that I needed some sub-lemmas that
> related 1) lequ and <= 2) Int32Set.for_all xs P with forall x,
> Int32Set.In x xs -> P x 3) +32 with Word.add
>
> I agree that this should be a relatively trivial solve, but I guess
> its the first of this type that I've done before, and I need some
> help. One thing I should note is that
> by the time I get to "Proof. intros. split.", coqide is showing this:
>
> 2 subgoals
> addrs : Int32Set.t
> a : int32
> b : int32
> H : checkIATAddresses (iatbounds (a, b)) addrs = true
> addr : int32
> H0 : Int32Set.In addr addrs
> ______________________________________(1/2)
> (unsigned a <= unsigned addr)%Z
>
>
> ______________________________________(2/2)
> (unsigned addr <= unsigned (add a b))%Z
>
> So, I'm confused; I don't know where to start. Can anyone give me a
> pointer?