%
% General Pipeline Theory
% N is the number of stages
%
% Copyright 2000 Daniel Kroening
%

pipetheory[N:posint, 
           (IMPORTING mathmtimet)
           ue:[below(N), mathmtimet->bool],
           full:[below(N), mathmtimet->bool],
           stall:[below(N), mathmtimet->bool],
           sequential:bool]: THEORY
BEGIN
  ASSUMING
    k, l: VAR below(N);
    i, T, Tp, Tpp: VAR mathmtimet;

    pipe_ue_def: ASSUMPTION
      ue(k, T)=(full(k, T) AND NOT stall(k, T));

    pipe_full_def: ASSUMPTION
      k>=1 IMPLIES (full(k, T+1)=(ue(k-1, T) OR stall(k, T)));

    pipe_stall_correct: ASSUMPTION
      ((NOT full(k, T)) IMPLIES NOT stall(k, T)) AND
      ((k>=1 AND full(k-1, T) AND stall(k, T)) IMPLIES stall(k-1, T));
    
    pipe_full_init: ASSUMPTION 
      full(k, 0) IFF k=0;

    pipe_full0_def: ASSUMPTION
      (NOT sequential IMPLIES full(0, T)) AND
      (sequential IMPLIES full(0, T+1)=(ue(N-1, T) OR stall(0, T)));

  ENDASSUMING

  old_full_correct: LEMMA
    k>=1 IMPLIES
      (IF (NOT stall(k-1, T) AND full(k-1, T)) OR ue(k, T) THEN ue(k-1, T) ELSE full(k, T) ENDIF)=
      (ue(k-1, T) OR stall(k, T));

  sched_overwrite: LEMMA % nichts ueberschreiben
      k>=1 AND full(k, T) AND ue(k-1, T) IMPLIES ue(k, T);

  sched_full_bits_save: LEMMA % kein full bit geht verloren 
    (k>=1 AND full(k, T) AND NOT ue(k, T)) IMPLIES full(k, T+1);

  sched_clear_full_bits: LEMMA % nichts verdoppeln 
    (k>=1 AND full(k, T) AND ue(k, T) AND NOT ue(k-1, T)) IMPLIES NOT full(k, T+1);
 
  Imeas(k, T):nat =
    T*N+k;    

  sI(k, T):RECURSIVE mathmtimet=
    IF T=0 THEN
      0
    ELSIF NOT ue(k, T-1) THEN
      sI(k, T-1)
    ELSIF k=0 THEN
      sI(0, T-1)+1
    ELSE
      sI(k-1, T-1)
    ENDIF
    MEASURE Imeas;

  sched_pipe_start: LEMMA
    full(k, T) IMPLIES T>=k;

  sched_lemma1?(T):bool=
    FORALL (k:below(N)): T>0 IMPLIES
      sI(k, T)=sI(k, T-1)+IF ue(k, T-1) THEN 1 ELSE 0 ENDIF;

  sched_lemma2?(T):bool=
    FORALL (k: below(N)): k>=1 IMPLIES
      ((sI(k-1, T)=sI(k, T)+1) XOR (sI(k-1, T)=sI(k, T)));

  sched_lemma3?(T):bool=
    FORALL (k: below(N)): k>=1 IMPLIES
      (full(k, T) IFF sI(k-1, T)=sI(k, T)+1);

  sched_lemma1_step: LEMMA
    (T>0 AND sched_lemma3?(T-1)) IMPLIES
    sched_lemma1?(T);

  sched_lemma2_step: LEMMA
    (T>0 AND sched_lemma1?(T) AND sched_lemma2?(T-1) AND sched_lemma3?(T-1)) IMPLIES
    sched_lemma2?(T);

  sched_lemma3_step: LEMMA
    (T>0 AND sched_lemma1?(T) AND sched_lemma2?(T-1) AND sched_lemma3?(T-1)) IMPLIES
    sched_lemma3?(T);

  sched_lemmas: LEMMA
    sched_lemma1?(T) AND sched_lemma2?(T) AND sched_lemma3?(T);

  sched_lemma1: LEMMA
    T>0 IMPLIES sI(k, T)=sI(k, T-1)+IF ue(k, T-1) THEN 1 ELSE 0 ENDIF;

  sched_lemma2: LEMMA
    k>=1 IMPLIES ((sI(k-1, T)=sI(k, T)+1) XOR (sI(k-1, T)=sI(k, T)));

  sched_lemma3: LEMMA
    k>=1 IMPLIES (full(k, T) IFF sI(k-1, T)=sI(k, T)+1);

  sched_prev_stage: LEMMA
    k>=1 AND T>0 AND ue(k, T-1) IMPLIES sI(k, T)=sI(k-1, T-1);

  sched_initialization: LEMMA
    sI(k, T+1)=0 IMPLIES (sI(k, T)=0 AND NOT ue(k, T));

  full_bit_lemma: LEMMA
    FORALL k:
    FORALL (l:below(N) | l>k):
    ((FORALL (m:integer | m>k AND m<=l): (full(m, T)=FALSE)) IMPLIES
      sI(k, T)=sI(l, T));

  sched_min_lemma: LEMMA
    T >= sI(k, T);

  prev(k):below(N)=IF k=0 THEN N-1 ELSE k-1 ENDIF;
  next(k):below(N)=IF k=N-1 THEN 0 ELSE k+1 ENDIF;

  %
  % sequential machine
  %

  pipe_sequential_full: LEMMA
    sequential IMPLIES (full(k, T+1)=(ue(prev(k), T) OR stall(k, T)));

  sched_sequential_lemma1: LEMMA
    (sequential AND full(k, T+1)) IMPLIES
    (full(k, T) OR full(prev(k), T));

  sched_sequential_lemma2: LEMMA
    (sequential AND full(k, T)) IMPLIES (full(k, T+1) OR full(next(k), T+1));

  sched_sequential_lemma3: LEMMA
    (sequential AND (NOT full(k, T)) AND full(k, T+1)) IMPLIES
    (full(prev(k), T) AND ue(prev(k), T));

  sched_sequential_lemma4: LEMMA
    sequential IMPLIES (exists1! k: full(k, T));

  sched_sequential_lemma: LEMMA
    (sequential AND full(k, T)) IMPLIES sI(l, T)=
      IF l<k THEN
        sI(k, T)+1
      ELSE
        sI(k, T)
      ENDIF;

  %
  % liveness
  %

  IMPORTING live_calculus;

  conf_is_calc(k, i):timepred=
    LAMBDA T: sI(k, T)=i;

  ue_sI_lemma: LEMMA
    (Tp>=T AND
    (FORALL (Tpp: mathmtimet | Tpp>=T AND Tpp<Tp): (ue(k, Tpp)=FALSE)))
    IMPLIES sI(k, T)=sI(k, Tp)    ;

  ue_is_live_IS_lem: LEMMA
    (full(k, T) AND finite_true(LAMBDA T: stall(k, T))) IMPLIES 
    strongEafter(LAMBDA T: ue(k, T), T);

  ue_is_live_IS_lem2: LEMMA % unbenutzt
    (k<(N-1) AND NOT full(k+1, T) AND Tp>=T AND 
     (FORALL (Tpp: timet | Tpp>=T AND Tpp<Tp): NOT ue(k, Tpp))) IMPLIES 
     NOT full(k+1, Tp);

  ue_is_live_IS: LEMMA
    (k<(N-1) AND
      (FORALL l: finite_true(LAMBDA T: stall(l, T))) AND
      finite_false(LAMBDA T: ue(k, T))) IMPLIES
      finite_false(LAMBDA T: ue(k+1, T));

  ue_is_live_IS2: LEMMA
    ((FORALL l: finite_true(LAMBDA T: stall(l, T))) AND
     strongEafter(LAMBDA T: (ue(0, T)), T)) IMPLIES
     strongEafter(LAMBDA T: (ue(k, T)), T);

  ue_is_live_seq: LEMMA
    (sequential AND FORALL l: finite_true(LAMBDA T: stall(l, T))) IMPLIES
    finite_false(LAMBDA T: ue(k, T));

  ue_is_live_pipe: LEMMA
   (NOT sequential AND FORALL l: finite_true(LAMBDA T: stall(l, T))) IMPLIES
    finite_false(LAMBDA T: ue(k, T));

  Machine_is_live_IS: LEMMA
    (sI(k, T)=i AND finite_false(LAMBDA T: ue(k, T))) IMPLIES
    E(conf_is_calc(k, i+1));

  Machine_is_live: LEMMA
    (FORALL l: finite_true(LAMBDA T: stall(l, T))) IMPLIES
    E(conf_is_calc(k, i));

  IMPORTING live_calculus2;

  below_empty(k, T):bool=
    FORALL (j: below(N) | j>k): NOT full(j, T);

  pipe_live_premise:bool=
    EXISTS (dhaz:[below(N), mathmtimet->bool],
            ext_stall:[below(N), mathmtimet->bool]):
      FORALL k: (FORALL T: stall(k, T)=(full(k, T) AND (ext_stall(k, T) OR dhaz(k, T) OR
                     IF k=N-1 THEN
                       FALSE
                     ELSE
                       stall(k+1, T)
                     ENDIF))) AND
                  finite_true(LAMBDA T: ext_stall(k, T)) AND
                  FORALL T: below_empty(k, T) IMPLIES NOT dhaz(k, T);

  pipe_drain_lem: LEMMA
    (FORALL (j: below(N) | j>k): finite_true(LAMBDA T: stall(j, T))) IMPLIES
    EXISTS (Tp | Tp>=T):
      (FORALL (Tpp | Tpp >= T AND Tpp<Tp): NOT ue(k, Tpp)) IMPLIES
      below_empty(k, Tp);

  below_empty_lem: LEMMA
    below_empty(k, T) IMPLIES
    stays_until(LAMBDA T: below_empty(k, T), T, LAMBDA T: ue(k, T));

  pipe_stall_is_finite_true: LEMMA
    pipe_live_premise IMPLIES
    FORALL k: finite_true(LAMBDA T: stall(k, T));

END pipetheory