Fifo spec

[blaxill]

@jadephilipoom let me know if i'm on the right track. It's currently missing any state invariant which we would likely want to say something about the correctness of the fifo vector.

[blaxill]

I've pushed a new version, I think this is closer to what you are saying. I've linked the ghost contents to the real fifo in step_fifo_invariant. There is one admit in step_fifo_invariant that should be true. new_contents is currently existential but I can just move it into the lemma signature- I wasn't sure what was preferred (I think I have to do one of the two though).

Im unsure if I'm capturing properties correctly because the proof is quite fiddly.

[jadephilipoom]

Hmm, it's a bit tricky to formulate. Thinking about it from the perspective of a proof that needs to use this lemma, I have a few thoughts:

• The existential means that rewrite won't work; I'd have to pose proof, fill in all preconditions, and then destruct to get the existential, even if all I care about is the other half of the tuple. This would be a really awkward process.
• Circuits that use a fifo probably don't only step it when it's non-empty, so in those proofs you'd have to rewrite in the "invalid" case somehow.

One deep change that could fix the issue here and in future places is to encode optional types in our type system. In netlists, they could be implemented as a bit and a value, but in the semantics they'd get interpreted as option. Then, in this lemma, it would be completely fine to just write None for the invalid case. We could define operations on options in the style of option_bind; it's fine to do a computation on an optional value, but your result will also be optional (in circuitry, it would just be wiring through the valid bit).

Alternatively, it's possible to write the step_fifo lemma with multiple clauses so that it specifies only the other parts of the result, without mentioning the stale data at all in the invalid case. Something like:

Lemma step_fifo :
  ...
  (fst (snd (step fifo input state)) = fst (fifo_spec ...)
   /\ if fst (fifo_spec ...) then fst (snd (snd (step fifo input state)) = fst (snd (fifo spec ...)) else True
   /\ snd (snd (snd (step fifo input state)))) = snd (snd (fifo_spec ...)))).

However, this is not very readable and the strategy might not scale well if there are many optional outputs.

[blaxill]

• Circuits that use a fifo probably don't only step it when it's non-empty, so in those proofs you'd have to rewrite in the "invalid" case somehow.

Although, the invalid value should never be used so when valid=false the existential should also disappear. I agree its awkward though.

One deep change that could fix the issue here and in future places is to encode optional types in our type system. In netlists, they could be implemented as a bit and a value, but in the semantics they'd get interpreted as option. Then, in this lemma, it would be completely fine to just write None for the invalid case. We could define operations on options in the style of option_bind; it's fine to do a computation on an optional value, but your result will also be optional (in circuitry, it would just be wiring through the valid bit).

Yeah I've been thinking about this but held off in the interest of time, perhaps it would require less work than I've been thinking...

I've just realised I can of course change the circuit to just always zero when invalid, I think in the interest of time I might just do this consistently.

[jadephilipoom]

• Circuits that use a fifo probably don't only step it when it's non-empty, so in those proofs you'd have to rewrite in the "invalid" case somehow.

Although, the invalid value should never be used so when valid=false the existential should also disappear.

The problem is that even if the existential is unused and will disappear after the lemma is used, the tactic rewrite itself won't work. Concrete example:

Definition foo (x : N) := (x, 1).
Lemma foo_eq x : exists y, foo x = (y, 1).
Proof. exists x. reflexivity. Qed.
Lemma foo2_eq x : snd (foo x) = 1.
Proof.
  Fail rewrite foo_eq.
  (* Error: Cannot find an homogeneous relation to rewrite. *)

You can work around it, e.g.:

  destruct (foo_eq x) as [? H].
  rewrite H. reflexivity.

But plugging in all of the arguments for your lemma is going to get really annoying when the lemmas are complex and have many arguments, and when those arguments might be big expressions you have to hunt for in your goal.

I've just realised I can of course change the circuit to just always zero when invalid, I think in the interest of time I might just do this consistently.

For the sake of short term progress, I think that sounds like a good way to go!

[blaxill]

Ok should be good to go... The proofs are a bit ugly but I'm not sure it matters.