Skip to content

Cyclic theorem prover for equalitional reasoning using egraphs

Notifications You must be signed in to change notification settings

nadia-polikarpova/cyclegg

Repository files navigation

cyclegg is a theorem prover for equational reasoning. It is based on the ideas from CycleQ but implements them on top of egraphs and equality saturation in order to avoid backtracking proof search.

To prove commutativity of addition, run:

cargo run -- examples/add.ceg

TODO

Organizational

  • Add flag for grounding
  • Create goals inside parser, do not expose RawGoal
  • Decouple proof generation from proof search (e.g. put Defs, Proof term somewhere else)
  • Make partial applications without $ work
  • Move from SymbolLang to a proper language.
  • Emit a proof data structure
    • Right now we just emit strings that are (mostly) valid LiquidHaskell.
    • Creating a proper equational proof data structure would allow us to emit to other backends.
    • It would also be cleaner.

Search

  • Canonical forms for termination checking:
    • Grounding for cyclic mode: extend the domain of grounding_instantiations to include new vars; instantiate sides of all lemmas
  • In cyclic mode: use multi-patterns instead of requiring that the premise has no extra vars?
  • Blocking variables analysis

Proofs

  • Conditional props proof generation
    • Add explanation for conditional unions (cannot just union_trusted).
    • Include the premise into the LH precondition
      • This can be accomplished by taking a witness of the precondition as an argument.
    • How to include the proof of the condition holding?
      • To use a conditional lemma you need a witness of the condition. We can take the e-graph from which we are getting the explanation and ask it to explain why the e-classes of the condition are equal and use those to build a proof. In LH this would look something like

        let conditionWitness =   condLHS 
                             ==. condLHS'
                             ? lemma lemmaArgs
                             ==. condRHS
                             *** QED
         in conditionalLemma conditionWitness args

Comparison to CycleQ

Results generated from a282086 using the command (prop52 removed because its proof was made easier by a bug)

cargo run --release -- examples/cycleq.ceg -t 10 --save-results

and compared to results from CycleQ.

All results come from runs on a Macbook Air M2.

N.B. We have cyclic proofs for prop_30 (49ms) and prop_73 (5364ms) but not with uncyclegg but these are believed unsound.

N.B. The cyclegg timing is a little suspect (e.g. I time prop_56 as taking 201ms instead of 5000 ms using cyclegg).

Name Cycleq result Uncyclegg result Cycleq time (ms) Cyclegg time (ms) Uncyclegg time (ms)
prop_01 Valid Valid 0.673 0.837… 0.589…
prop_02 Unknown Valid -1.000 7.748… 1.684…
prop_03 Unknown Valid -1.000 3.529… 2.117…
prop_04 Unknown Valid -1.000 3.090… 1.654…
prop_06 Valid Valid 0.134 0.202… 0.142…
prop_07 Valid Valid 0.210 0.191… 0.142…
prop_08 Valid Valid 1.270 0.237… 0.166…
prop_09 Valid Valid 0.641 0.783… 0.350…
prop_10 Valid Valid 0.079 0.141… 0.108…
prop_11 Valid Valid 0.014 0.029… 0.025…
prop_12 Valid Valid 1.007 0.504… 0.343…
prop_13 Valid Valid 0.047 0.034… 0.029…
prop_14 Unknown Valid -1.000 1.963… 0.400…
prop_15 Unknown Valid -1.000 2.072… 1.029…
prop_17 Valid Valid 0.051 0.151… 0.120…
prop_18 Valid Valid 0.163 0.170… 0.126…
prop_19 Valid Valid 0.847 0.480… 0.333…
prop_21 Valid Valid 0.143 0.170… 0.123…
prop_22 Valid Valid 1.591 1.110… 0.593…
prop_23 Valid Valid 1.104 0.422… 0.212…
prop_24 Valid Valid 1.445 1.146… 0.442…
prop_25 Valid Valid 0.640 0.716… 0.430…
prop_28 Unknown Valid -1.000 2.503… 0.995…
prop_29 Unknown Valid -1.000 4.213… 2.262…
prop_31 Valid Valid 1.352 1.210… 0.586…
prop_32 Valid Valid 1.071 0.452… 0.202…
prop_33 Valid Valid 0.427 0.417… 0.271…
prop_34 Valid Valid 0.709 0.524… 0.351…
prop_35 Valid Valid 0.059 0.319… 0.126…
prop_36 Valid Valid 0.188 0.332… 0.125…
prop_37 Unknown Valid -1.000 1.310… 1.402…
prop_38 Unknown Valid -1.000 6.999… 1.343…
prop_39 Unknown Valid -1.000 2.048… 0.250…
prop_40 Valid Valid 0.014 0.024… 0.020…
prop_41 Valid Valid 0.978 0.476… 0.280…
prop_42 Valid Valid 0.067 0.029… 0.025…
prop_43 Unknown Valid -1.000 0.593… 0.306…
prop_44 Valid Valid 0.193 0.552… 0.420…
prop_45 Valid Valid 0.101 0.032… 0.027…
prop_46 Valid Valid 0.020 0.021… 0.018…
prop_49 Valid Valid 231.569 2.492… 1.021…
prop_50 Valid Valid 21.207 0.796… 0.425…
prop_51 Valid Valid 1.855 0.453… 0.459…
prop_55 Valid Valid 1.516 0.631… 0.381…
prop_56 Valid Valid 1,615.585 5,194.048… 12.648…
prop_57 Valid Valid 35.090 3.122… 4.161…
prop_58 Valid Valid 3.633 0.910… 0.651…
prop_61 Valid Valid 163.463 2.073… 0.874…
prop_64 Valid Valid 0.660 0.413… 0.393…
prop_67 Valid Valid 1.045 0.653… 0.366…
prop_75 Unknown Valid -1.000 2,770.103… 17.077…
prop_79 Valid Valid 507.399 1.054… 0.284…
prop_80 Valid Valid 1.082 0.682… 0.415…
prop_82 Valid Valid 2.437 1.176… 0.726…
prop_83 Valid Valid 2.687 7.345… 1.645…
prop_84 Valid Valid 7.110 1.412… 0.847…
prop_86 Unknown Valid -1.000 0.768… 0.219…
prop_87 Unknown Valid -1.000 1.698… 0.398…
prop_88 Unknown Valid -1.000 1.157… 0.405…
prop_89 Unknown Valid -1.000 1.606… 0.360…
prop_90 Unknown Valid -1.000 0.630… 0.312…

About

Cyclic theorem prover for equalitional reasoning using egraphs

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published