# LoVe Project Introduction

I made this project as part of the LoVe 2020 course, so dropping it as a "project" subfolder in the course project should get it working.

## Module overview

Here I list all files and their abbreviated purpose.

### Major definitions and lemmas

- defs.lean
  - Contains all definitions needed for the rest of the project, such as the small step semantics, big step semantics,
    and definitions & aliases for the heap and boolean/numerical expressions.
- bs_ss.lean
  - Proves the correspondence between the big step and small step semantics.
- project.lean
  - Contains the proofs for the first two major lemmas from the Reynolds 2002 paper, and an incomplete attempt at a proof
    for the third major lemma.

### Supporting lemmas

- absurds.lean
  - Proves lemmas that formulate that the left hand side of a ⇒* can never be a terminal state.
- unfolds.lean
  - Proves various lemmas that manipulate ⇒*, such as unfolding an ite, or unfolding one iteration of a while.
- small_step_star.lean
  - Proves various properties of ⇒* and ↑ (a.k.a. "ridiculously strong divergence")
- small_step.lean
  - Proves some properties of the small step relation.
- heap.lean
  - Proves properties around heaps, such as maintaining finiteness of the heap while adding and removing elements.

### Basic lemmas

- star.lean
  - Mostly abstract properties about ⇒*, such as unfolding at the head.
- option.lean
  - General properties about the option datatype. Very messy.
- xor.lean
  - General properties about xor. Not as useful as I'd hoped.

### Irrelevant lemmas

- project-computing-elems-not-in-lists.lean
  - I ran into this but did not end up using it. Might be interesting if ideas for exercises are needed.

# Log

This is a log I kept to measure my working hours and findings over time. After the 8th of january I think
I worked on the project with a somewhat slower pace for about two weeks.

Saturday: 1.5 - Small step semantics
Sunday: 2.5 - First case of subheap_similar_0 (mainly skip_absurd_star)
Monday: 2.5 - Second case, beginning of third case (mainly stuck on seq_choice_abort)
Tuesday: 2 - Added "term" state for configs, still not getting through the third case (seq). I think the induction is not strong enough...
Wednesday: 2 - Proved the if-then-else case of the big lemma, and wasted an hour on the seq abort helper lemma again.
Thursday: 4 - I think there is an abort case missing for seq! Also a problem with alloc, in that the addresses might run out.
              Still have not solved the seq case.
Friday: 5 - Finally made some progress on the seq situation. Tried proving `cfg_small_step_possible`, but got stuck because of strict induction.
             By proving a simpler version first, proving `cfg_small_step_possible` became trivial.
Saturday: 3 - Made progress on abort -> ¬step ∧ ¬done lemma and variations
Sunday: 5 - Finished the xor variation of the abort -> ... lemmas. Refactored into separate files. Also got the nonterm_abort_step lemma.
              Tried the while case a bit of the "big" lemma but I'm also kind of running into a wall there... 
Tuesday 22-12-2020: 3hrs
  Got seq_step_star, so at least I now know how to use lift. Sadly the other way doesn't work so smoothly...
Wednesday 23-12-2020: 1.5hrs
  `seq_done_distrib` is also difficult to prove with induction. Somehow I get not very useful induction hypotheses?
Friday 25-12-2020: 2hrs
  Nice progress on `done_maintain_subheap_or_abort`, proved the alloc case. And some nice lemmas on heaps.
  Got lookup case too, and halfway mut.
Saturday 26-12-2020:
  Turns out the subheap relation (⊆) I defined must also say something about the values, I think. Currently it only reasons about the domain...
Saturday 02-01-2021:
  Proved equivalence of big step and small step! Hopefully I can finally prove those dreaded seq_unfold and other crutch lemmas for the paper lemmas.
  Also, I need to refactor the basic lemmas in this file to a separate file, the ss-bs equivalence stuff into a separate file.
  I also want to move the basic lemmas about cfg's being final and such in a "basic" file.
Sunday 03-01-2021:
  I found a nice way to refactor the while_unfold lemma, with proper use of ⇒* instead of ugly unfolds.
Tuesday 05-01-2021:
  Two lemmas proven! Now the only one left is the one about non-termination and subheaps.
Thursday 07-01-2021:
  Turns out the subheap_maintain_done lemma does not hold for alloc!
    ⟨c, (s, h₀)⟩ ⇒* ⟪s', h₀'⟫ → ∃h₁', ⟨c, (s, h₁)⟩ ⇒* ⟪s', h₁'⟫ ∧ h₀' ⊆ h₁'
  So I'll have to go back to the drawing board for the while case of the third lemma...
Friday 08-01-2021:
  Just realized that diverging is defined in the paper as "there exists an infinite trace starting at cfg",
  not as "cfg cannot go to done or abort"... Hmmm.

# TODO

- Refactor basic lemmas, ss-bs equivalence, basic lemmas about cfgs being final.
- Refactor multiple invocations of cases with rcases and rintro

# How to induct

```lean
generalize hC' : ⟨cmd.skip, (s, h)⟩ = C',
intro hh,
induction hh using LoVe.rtc.star.head_induction_on
    with _ D hD;
  cases hC'; clear hC' C',
```