search

maxhaslbeck / ProvingForFun-July2019

1 stars 1 forks source link

XOR #1

Open maxhaslbeck opened 5 years ago

maxhaslbeck commented 5 years ago

Task Authors and Translators

Task was stated by @maxhaslbeck in Isabelle, and translated to Coq by Armaël Guéneau.

The sample solution

For solving the task one has to notice that xor is commutative and associative. Similar to caching partial sums one thus can first calculate all partial XORs from index 0 to i and then get constant time access to XOR i j f by xor (XOR 0 i f) (XOR 0 j f).

The program to solve the task in three phases:

  1. Get the registers into a usable state: B should serve as accumulator in the next step and should be initialized to XOR 0 0 f = False.
  2. The second phase collects the "partial XORs" into the tmp memory by xoring one more element to the accumulator and storing the result at the right place. This takes a number of operations linear in n.
  3. In the final phase, all queries are served in constant time each by using the lookup table in tmp and the observation above. This results again in a number of operations linear in n.

In Isabelle

The sample solution due to @maxhaslbeck can be found here.

The definition of parts of the plan is: https://github.com/maxhaslbeck/ProvingForFun-July2019/blob/d6bb31e16caf9abf253f56d3bb50fe7466730b6d/xor/isabelle/haslbema/Submission.thy#L98-L102

https://github.com/maxhaslbeck/ProvingForFun-July2019/blob/d6bb31e16caf9abf253f56d3bb50fe7466730b6d/xor/isabelle/haslbema/Submission.thy#L144

https://github.com/maxhaslbeck/ProvingForFun-July2019/blob/d6bb31e16caf9abf253f56d3bb50fe7466730b6d/xor/isabelle/haslbema/Submission.thy#L170-L172

and the functional correctness theorem of the whole plan is:

https://github.com/maxhaslbeck/ProvingForFun-July2019/blob/d6bb31e16caf9abf253f56d3bb50fe7466730b6d/xor/isabelle/haslbema/Submission.thy#L298-L301

In Coq

The sample solution due to Armaël Guéneau can be found here.