Sequential Proofs

[satnam6502]

The purpose of this issue is to track work on the development of sequential proofs for Cava circuits.

The first proof we consider is for a synthetic example of a circuit made with a counter which counts-by the current input values:

        _______
    ---| delay |------------
   |   |_______|            |
   |   ___                  |
    --| + ---------------------- out
 in --|___|   

The countBy circuit takes the current 8-bit input (in) and the current state value represented by the register (delay) which is output in the current cycle as the output of the circuit, and this value is also the next state value for the delay. The adder is an 8-bit adder with no bit-growth i.e. it computes (a + b) mod 256.

Currently this circuit description is in the PR #367 in the file tests/Delay.v.

The implementation makes use of the loop combinator which implicitly places a register on the feedback path:

Section WithCava.
  Context {signal} `{Cava signal} `{Monad cava}.

  Definition countFork (i : signal (Vec Bit 8) * signal (Vec Bit 8))
                       : cava (signal (Vec Bit 8) * signal (Vec Bit 8)) :=
    newCount <- addN (fst i) (snd i) ;;
    ret (newCount, newCount).

  Definition countBy : signal (Vec Bit 8) -> cava (signal (Vec Bit 8))
    := loop countFork.

End WithCava.

We can test the circuit with some concrete values to confirm that it seems to work as intended:

Example countBy_ex1: sequential (countBy [b14; b7; b3; b250]) = [b14; b21; b24; b18].
Proof. reflexivity. Qed.

We can write a specification for the intended behaviour:

Fixpoint countBySpec' (state: N) (i : list (Bvector 8)) 
                      : list (Bvector 8) :=
  match i with
  | [] => []
  | x::xs => let newState := (Bv2N x + state) mod 256 in
             N2Bv_sized 8 newState :: countBySpec' newState xs 
  end.

Definition countBySpec := countBySpec' 0.

Now the challenge is to prove that the implementation countBy has equivalent behaviour to the specification countBySpec:

Lemma countByCorrect: forall (i : list (Bvector 8)),
                      sequential (countBy i) = countBySpec i.

To make the proof work out it is fine to write the specification in a different way, or to change how the underlying semantics are expressed (e.g. computing the circuit "backwards" has been suggested) or making any other change that helps with the proof. Also, feel free to change the spec (e.g. to make it simpler): it's currently written in a mechanistic manner to mirror how the hardware is constructed.

[jadephilipoom]

Just to record some experimenting:

Following the pattern from #374, I tried defining a loop using a function from nat to simulate an infinite list. I wasn't able to get it working, though, because of trouble with interleaving the timestep argument and the monad. The timestep argument, with this type, has to be underneath the ident. However, the timestep needs to be exposed to any recursive definition because it's the decreasing argument. But because the subcircuit returns something wrapped in ident, it's necessary to have the ident in the single-step case, and these constraints aren't compatible as far as I can tell. Of course, I could use unIdent, but I think that violates the circuit graph principle, no?

Here's the definition without ident:

Definition seqFType t := nat -> combType t.

Fixpoint loopSeqF' {A B C : SignalType}
         (f : combType A * combType C -> combType B * combType C)
         (a : seqFType A) (t : nat) : combType B * combType C :=
  match t with
  | 0 => (defaultCombValue B, defaultCombValue C)
  | S t' =>
    let '(_, ct') := loopSeqF' f a t' in
    f (a t', ct')
  end.

Definition loopSeqF {A B C : SignalType}
         (f : combType A * combType C -> combType B * combType C)
         (a : seqFType A) : seqFType B * seqFType C :=
  let bc := loopSeqF' f a in
  (fun t => fst (bc t), fun t => snd (bc t)).

And here's as far as I got with ident included:

Fixpoint loopSeqF' {A B C : SignalType}
         (f : combType A * combType C -> ident (combType B * combType C))
         (a : seqFType A) (t : nat) : ident (combType B * combType C) :=
  match t with
  | 0 => ret (defaultCombValue B, defaultCombValue C)
  | S t' =>
    '(_, ct') <- loopSeqF' f a t' ;;
    f (a t', ct')
  end.

The version above typechecks but I can't make loopSeqF by calling it.

[blaxill]

Great progress, I think we should continue to add examples with increasing sequential complexity #376

[jadephilipoom]

(For archival purposes / to remind myself later) In the meeting, we said it would be fine to use unIdent inside the loop.

[satnam6502]

Although it is possible to express a loop circuit who's output comes directly from the output of the register, this involves in internal combinational circuit using the enable input to control a multiplexor. However, I don't want the enable signal to be accessible to the internal logic (the f function): I only want it wired up under the hood to the clock enable input of registers (for the netlist interpretation, to yield good circuits).

I think we should have a variant of loopDelay as the primitive loop element which exposed both the output of f and the current state:

  loopDelayS : forall {A B C: SignalType},
               (signal A * signal C -> cava (signal B * signal C)) ->
               signal A ->
               cava (signal B * signal C);

i.e.

    ---------------------------- current state
   |
   |     _______
    ---| delay |-------------
   |   |_______|            |
   |   ___                  |
    --| + ---------------------- out
 in --|___|  

Now loopDelay becomes a special case of loopDelayS and can be defined in Combinators.v. This then allows us to make a countBy with enable which counts from 0 as the initial argument and does not need to burn logic to implement a multiplexor driven by an enable signal. However, when giving the semantics of loopDelayS it is totally fine to use a multiplexor controlled by enable to model the clock-enable behaviour.

[jadephilipoom]

Closing this; we managed long ago in https://github.com/project-oak/silveroak/pull/561 to represent sequential circuits, and are now moving on to v2 with finer improvements, so I think there's no more need for a tracking issue.