search

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
716 stars 147 forks source link

Remove axioms #736

Open JasonGross opened 4 years ago

JasonGross commented 4 years ago

On Coq master, coqchk successfully runs on fiat-crypto and the parts of bedrock and the rewriter that fiat-crypto uses (I'm working on adding it to the CI in https://github.com/mit-plv/fiat-crypto/pull/724). However, it reports a number of axioms:

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.printf_float
    Crypto.Algebra.Field.isomorphism_to_subfield_field
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rquot2
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rquot1
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.R1_def
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.R0_def
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rmult_def
    Coq.ssr.ssrunder.Under_rel.Over_rel
    Coq.Reals.Rdefinitions.RinvImpl.Rinv_def
    Crypto.Bedrock.Tests.Proofs.X25519_64.mulmod_Wf
    Crypto.Curves.Edwards.AffineProofs.E.Kchar_ge_2
    Crypto.StandaloneOCamlMain.printf_char
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rrepr
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rplus
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rmult
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rabst
    Crypto.Bedrock.Tests.Proofs.X25519_64.mulmod_correct
    Crypto.StandaloneOCamlMain.string_init
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Ropp
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rlt
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.R1
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.R0
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.R
    Coq.ssr.ssrunder.Under_rel.Under_rel_from_rel
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.runtime_nth_default
    Coq.Reals.Rdefinitions.RinvImpl.Rinv
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.runtime_modulo
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.land
    Crypto.StandaloneHaskellMain._IO
    Crypto.Bedrock.Tests.Proofs.X25519_64.decimal_varname_gen_unique
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.float
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.fsub
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rlt_def
    Crypto.StandaloneHaskellMain._IO_return
    Crypto.StandaloneHaskellMain.getProgName
    Coq.Logic.ProofIrrelevance.proof_irrelevance
    Coq.ssr.ssrunder.Under_rel.over_rel
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.add_get_carry_full
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.Unix_gettimeofday
    Crypto.StandaloneHaskellMain.getArgs
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    Coq.Reals.ClassicalDedekindReals.sig_not_dec
    coqutil.Map.SortedList.TODO_andres
    Crypto.StandaloneOCamlMain.string_length
    Coq.ssr.ssrunder.Under_rel.over_rel_done
    Crypto.StandaloneHaskellMain.printf_string
    Coq.ssr.ssrunder.Under_rel.Under_rel
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.zselect
    Crypto.StandaloneHaskellMain.raise_failure
    Coq.Reals.ClassicalDedekindReals.sig_forall_dec
    Coq.Logic.PropExtensionality.propositional_extensionality
    Crypto.StandaloneOCamlMain.sys_argv
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.Let_In
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.Sys_time
    Coq.Logic.Classical_Prop.classic
    Crypto.StandaloneHaskellMain.cast_io
    Crypto.StandaloneOCamlMain.string
    Coq.ssr.ssrunder.Under_rel.Under_relE
    Crypto.StandaloneOCamlMain.raise_Failure
    Crypto.StandaloneHaskellMain._IO_bind
    Crypto.Algebra.Field.equivalent_operations_field
    Coq.Logic.JMeq.JMeq_eq
    Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.mul_split
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Ropp_def
    Coq.Compat.AdmitAxiom.proof_admitted
    coqutil.Map.SortedListString.TODO_andres
    Crypto.StandaloneHaskellMain.IO_unit
    Crypto.StandaloneOCamlMain.string_get
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.runtime_sub
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.runtime_opp
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.runtime_mul
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.runtime_div
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.runtime_add
    Coq.ssr.ssrunder.Under_rel.under_rel_done
    Crypto.StandaloneOCamlMain.flush
    Coq.Reals.Rdefinitions.RbaseSymbolsImpl.Rplus_def
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.add_with_get_carry_full

* Constants/Inductives relying on type-in-type: <none>

* Constants/Inductives relying on unsafe (co)fixpoints: <none>

* Inductives whose positivity is assumed: <none>

Some of these are a result of a 4-year-old bug in Coq (coq/coq#5030). Some of them are dead code, such as https://github.com/mit-plv/fiat-crypto/blob/b3bbb68c652e88ba4d55f3ab1e2b245b76452ff3/src/Algebra/Field.v#L79-L101 which is used nowhere. Some of them are axioms that exist only for extraction, which I can replace with dummy definitions, possibly locked behind a Qed or something, at least until coq/coq#5030 is fixed. We should probably figure out where we're using the reals, and stop using them. Similarly for JMeq_eq and classic and propext. Others seem to be todos from bedrock2 (cc @andres-erbsen @samuelgruetter ). We should try to remove as many as we can.

andres-erbsen commented 4 years ago

propext may be used in bedrock2 (though maybe just in the compiler?). My suspects for reals and classic are coqprime and tauto.

JasonGross commented 4 years ago

The coqprime file we depend on gives

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
    Coq.ssr.ssrunder.Under_rel.Over_rel
    Coq.ssr.ssrunder.Under_rel.Under_rel_from_rel
    Coq.ssr.ssrunder.Under_rel.over_rel
    Coq.ssr.ssrunder.Under_rel.over_rel_done
    Coq.ssr.ssrunder.Under_rel.Under_rel
    Coq.ssr.ssrunder.Under_rel.Under_relE
    Coq.ssr.ssrunder.Under_rel.under_rel_done

* Constants/Inductives relying on type-in-type: <none>

* Constants/Inductives relying on unsafe (co)fixpoints: <none>

* Inductives whose positivity is assumed: <none>
JasonGross commented 4 years ago

bedrock2 is also relatively tame:

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
    Coq.ssr.ssrunder.Under_rel.Over_rel
    bedrock2.StructNotations.TODO_structs_might_require_multiplication
    Coq.ssr.ssrunder.Under_rel.Under_rel_from_rel
    bedrock2.Map.FDSepLog.disjoint_putmany
    Coq.ssr.ssrunder.Under_rel.over_rel
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    coqutil.Map.SortedList.TODO_andres
    Coq.ssr.ssrunder.Under_rel.over_rel_done
    Coq.ssr.ssrunder.Under_rel.Under_rel
    Coq.Logic.PropExtensionality.propositional_extensionality
    Coq.ssr.ssrunder.Under_rel.Under_relE
    coqutil.Map.SortedListString.TODO_andres
    Coq.ssr.ssrunder.Under_rel.under_rel_done

* Constants/Inductives relying on type-in-type: <none>

* Constants/Inductives relying on unsafe (co)fixpoints: <none>

* Inductives whose positivity is assumed: <none>

You're right about propext, though. Where does bedrock2 use that? (and why?)

JasonGross commented 4 years ago

The reals and classic come from nsatz (https://github.com/coq/coq/issues/5445)

JasonGross commented 4 years ago

Interestingly, looking for JMeq_eq via

for i in $(git ls-files "*.v"); do echo "Require $(echo "$i" | sed 's,/,.,g; s/\.v//g; s/^src\./Crypto./g'). Check Coq.Logic.JMeq.JMeq_eq." > foo.v; COQPATH=/home/jgross/Documents/repos/fiat-crypto/coqprime/src:/home/jgross/Documents/repos/fiat-crypto/bedrock2/bedrock2/src:/home/jgross/Documents/repos/fiat-crypto/bedrock2/deps/coqutil/src:/home/jgross/Documents/repos/fiat-crypto/rewriter/src coqc -q -R src Crypto foo.v 2>/dev/null >/dev/null && echo $i; done

suggests that in 8.11, there is no file which loads JMeq_eq. Thus perhaps this is a regression of master over 8.11?

samuelgruetter commented 4 years ago

bedrock2 is also relatively tame

I just fixed bedrock2.StructNotations.TODO_structs_might_require_multiplication and bedrock2.Map.FDSepLog.disjoint_putmany

JasonGross commented 4 years ago

Now that coq/coq#5030 is fixed, our current axiom list is

* Axioms:
    Coq.Logic.Classical_Prop.classic
    Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    Coq.Logic.JMeq.JMeq_eq
    Coq.Logic.ProofIrrelevance.proof_irrelevance
    Coq.Logic.PropExtensionality.propositional_extensionality
    Coq.Reals.ClassicalDedekindReals.sig_forall_dec
    Coq.Reals.ClassicalDedekindReals.sig_not_dec
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.add_get_carry_full
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.add_with_get_carry_full
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.land
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.mul_split
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.zselect
    Crypto.Bedrock.Field.Common.Arrays.MakeAccessSizes.access_size_to_zrange_word_upper_bound
    Crypto.Bedrock.Field.Common.Arrays.MakeAccessSizes.zrange_to_access_size_ok
    Crypto.Bedrock.Field.Synthesis.Generic.Bignum.Bignum_of_bytes
    Crypto.Bedrock.Field.Synthesis.Generic.Bignum.Bignum_to_bytes
    Crypto.Curves.Edwards.AffineProofs.E.Kchar_ge_2
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.float
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.fsub
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.printf_float
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.Sys_time
    Crypto.Rewriter.PerfTesting.StandaloneOCamlMain.Unix_gettimeofday
    Crypto.Rewriter.TestRulesProofs.test_rewrite_rules_proofs
    Crypto.StandaloneHaskellMain.cast_io
    Crypto.StandaloneHaskellMain.getArgs
    Crypto.StandaloneHaskellMain.getProgName
    Crypto.StandaloneHaskellMain._IO
    Crypto.StandaloneHaskellMain._IO_bind
    Crypto.StandaloneHaskellMain._IO_return
    Crypto.StandaloneHaskellMain.IO_unit
    Crypto.StandaloneHaskellMain.printf_string
    Crypto.StandaloneHaskellMain.raise_failure
    Crypto.StandaloneOCamlMain.flush
    Crypto.StandaloneOCamlMain.printf_char
    Crypto.StandaloneOCamlMain.raise_Failure
    Crypto.StandaloneOCamlMain.string
    Crypto.StandaloneOCamlMain.string_get
    Crypto.StandaloneOCamlMain.string_init
    Crypto.StandaloneOCamlMain.string_length
    Crypto.StandaloneOCamlMain.sys_argv

@jadephilipoom are you aware of these Bedrock ones? What's the story on them?

jadephilipoom commented 4 years ago

@jadephilipoom are you aware of these Bedrock ones? What's the story on them?

All 4 are unused. I removed two and commented out the other two in #868

JasonGross commented 4 years ago

Thanks! As of https://github.com/mit-plv/rewriter/pull/20 and https://github.com/mit-plv/fiat-crypto/pull/871, we no longer depend on funext (at least the main pipeline does not).

JasonGross commented 4 years ago

I have just reported the RT_Z "axioms" as a bug in Coq: https://github.com/coq/coq/issues/12845

JasonGross commented 4 years ago

The classical axioms were coming from Psatz, which we don't actually need; I've removed them in 8e00fa7a06366cef04680fa7dde5022820913031

JasonGross commented 4 years ago

Current list of axioms:

* Axioms:
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.land
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.add_get_carry_full
    Coq.Logic.FunctionalExtensionality.functional_extensionality_dep
    Coq.Reals.ClassicalDedekindReals.sig_not_dec
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.zselect
    Coq.Reals.ClassicalDedekindReals.sig_forall_dec
    Coq.Logic.PropExtensionality.propositional_extensionality
    Coq.Logic.Classical_Prop.classic
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.mul_split
    Crypto.ArithmeticCPS.Core.RuntimeAxioms.RT_Z.add_with_get_carry_full

Idk where these are coming from.... note that things are worse on master because of https://github.com/coq/coq/issues/13324