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

pipetheory_spec[N:posint, 
           (IMPORTING mathmtimet)
           ue:[below(N), mathmtimet->bool],
           full:[below(N), mathmtimet->bool],
           stall:[below(N), mathmtimet->bool],
           rollbackp:[below(N), mathmtimet->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) AND NOT rollbackp(k, T));

    rollback_def: ASSUMPTION
      (rollbackp(k, T) AND l<k) IMPLIES
      rollbackp(l, T);

    pipe_full_def: ASSUMPTION
      k>=1 IMPLIES (full(k, T+1)=((ue(k-1, T) OR stall(k, T)) AND NOT rollbackp(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
      full(0, T);

    is_rollback_stage(k, T): bool=
      rollbackp(k, T) AND
      (k=N-1 OR NOT rollbackp(k+1, T));

    rollback_correct: ASSUMPTION
      is_rollback_stage(k, T) IMPLIES (full(k, T) AND NOT stall(k, T));

  ENDASSUMING

  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) AND NOT rollbackp(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+N-1-k;

  sI(k, T):RECURSIVE mathmtimet=
    IF T=0 THEN
      0
    ELSIF k<N-1 AND rollbackp(k+1, T-1) THEN
      sI(k+1, T)
    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_rollback_lem1: LEMMA
    (T>0 AND NOT ue(k, T-1) AND (k=N-1 OR NOT rollbackp(k+1, T-1))) IMPLIES
    sI(k, T)=sI(k, T-1);

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

  sched_lemma1?(T):bool=
    FORALL (k:below(N)): T>0 IMPLIES
      sI(k, T)=IF ue(k, T-1) THEN
                 sI(k, T-1)+1
               ELSIF k=N-1 OR NOT rollbackp(k+1, T-1) THEN
                 sI(k, T-1)
               ELSE
                 sI(k, T)
               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)=IF ue(k, T-1) THEN
                 sI(k, T-1)+1
               ELSIF k=N-1 OR NOT rollbackp(k+1, T-1) THEN
                 sI(k, T-1)
               ELSE
                 sI(k, T)
               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);

  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;

  %
  % rollback
  %

  sched_rollback_lem2: LEMMA
    (T>0 AND k>=1 AND full(k, T-1) AND 
     is_rollback_stage(k, T-1)) IMPLIES
    sI(k-1, T-1)=sI(k, T)+1;

  sched_rollback_lem3: LEMMA
    (T>0 AND k>=1 AND full(k, T-1) AND 
     is_rollback_stage(k, T-1)) IMPLIES
    sI(k-1, T-1)=sI(k-1, T)+1;

  sched_rollback_lem4: LEMMA
    (T>0 AND is_rollback_stage(k, T-1) AND l<=k) IMPLIES
    sI(l, T)=sI(k, T-1);

  %
  % liveness
  %

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

  IMPORTING live_calculus2;

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

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

  IMPORTING max_def[N];

  M_max_exists: LEMMA
    nonempty?(LAMBDA (k:below(N)): full(k, T));

  M(T):below(N)=max(LAMBDA (k:below(N)): full(k, T));

  live_M0_lem: LEMMA
    M(0)=0;

  g_M_not_full: LEMMA
    k>M(T) IMPLIES NOT full(k, T);

  M_rollback: LEMMA
    rollbackp(M(T), T) => is_rollback_stage(M(T), T);

  M_is_full: LEMMA
    full(M(T), T);

  M_implies_below_empty: LEMMA
    below_empty(M(T), T);

  M_lemma0: LEMMA
    M(T)=k IFF (full(k, T) AND below_empty(k, T));

  M_lemma1: LEMMA
    M(T+1)=
      IF ue(M(T), T) THEN
        IF M(T)=N-1 THEN
          M(T+1)
        ELSE
          M(T)+1
        ENDIF
      ELSIF rollbackp(M(T), T) THEN
        0
      ELSE
        M(T)
      ENDIF;

  Mc(T):RECURSIVE bool=
    IF T=0 THEN
      FALSE
    ELSIF rollbackp(M(T-1), T-1) THEN
      TRUE
    ELSIF ue(M(T-1), T-1) THEN
      IF M(T-1)=N-1 THEN
        FALSE
      ELSE
        Mc(T-1)
      ENDIF
    ELSE
      Mc(T-1)
    ENDIF
    MEASURE T;

  ue_M_lemma: LEMMA
    (Tp>=T AND
    (FORALL (Tpp: mathmtimet | Tpp>=T AND Tpp<Tp): 
      (ue(M(T), Tpp)=FALSE AND rollbackp(M(T), Tpp)=FALSE)))
    IMPLIES (M(T)=M(Tp) AND Mc(T)=Mc(Tp));

  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);

  M_stall_is_finite_true_lem: LEMMA
    pipe_live_premise IMPLIES
    strongEafter(LAMBDA Tp: NOT stall(M(T), Tp), T);

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

  stage_M_is_live_lem: LEMMA
    pipe_live_premise IMPLIES
    strongEafter(LAMBDA Tp: ue(M(T), Tp) OR rollbackp(M(T), Tp), T);

  mc_premise:bool=
    FORALL T: (Mc(T) IMPLIES NOT rollbackp(M(T), T));

  live_Mc_lem1: LEMMA
    (mc_premise AND pipe_live_premise AND Mc(T)) IMPLIES
    strongEafter(LAMBDA Tp: ue(M(T), Tp) AND 
                 (FORALL (Tpp | Tpp>=T AND Tpp<=Tp): NOT rollbackp(M(T), Tpp)), T);

  live_Mc_lem2: LEMMA
    (mc_premise AND pipe_live_premise AND Mc(T)) IMPLIES
    weakEafter(LAMBDA Tp: sI(M(T), Tp)=sI(M(T), T)+1, T);

  live_Mc_lem3: LEMMA
    (mc_premise AND pipe_live_premise AND Mc(T) AND M(T)<N-1) IMPLIES
    weakEafter(LAMBDA Tp: sI(M(T)+1, Tp)=sI(M(T), T) AND M(Tp)=M(T)+1 AND Mc(Tp), T);

  live_Mc_lem4: LEMMA
    (mc_premise AND pipe_live_premise AND Mc(T) AND k>=M(T)) IMPLIES
    weakEafter(LAMBDA Tp: sI(k, Tp)=sI(M(T), T) AND M(Tp)=k AND Mc(Tp), T);

  live_no_Mc_lem2: LEMMA
    (mc_premise AND pipe_live_premise) IMPLIES
    weakEafter(LAMBDA Tp: sI(M(T), Tp)=sI(M(T), T)+1, T);

  live_no_Mc_lem3: LEMMA
    (mc_premise AND pipe_live_premise AND M(T)<N-1) IMPLIES
    weakEafter(LAMBDA Tp: sI(M(T)+1, Tp)=sI(M(T), T) AND M(Tp)=M(T)+1, T);

  live_is_M_lem2_aux: LEMMA
    (mc_premise AND pipe_live_premise AND M(T)=N-k-1) IMPLIES
    EXISTS Tp: sI(N-1, Tp)=sI(N-k-1, T) AND M(Tp)=N-1;

  live_is_M_lem2: LEMMA
    (mc_premise AND pipe_live_premise) IMPLIES
    EXISTS Tp: sI(N-1, Tp)=sI(M(T), T) AND M(Tp)=N-1;

  live_sI_M_is_laststage_aux: LEMMA
    k<N-M(T) IMPLIES sI(N-1-k, T)=sI(N-1, T);

  live_sI_M_is_laststage_lem: LEMMA
    sI(M(T), T)=sI(N-1, T);

  live_is_M_lem1: LEMMA
    (mc_premise AND pipe_live_premise) IMPLIES
    EXISTS T: sI(N-1, T)=i;

  live_sI_exists_IS: LEMMA
    k>0 AND sI(k, T)=i IMPLIES
    EXISTS Tp: sI(k-1, Tp)=i;

  live_sI_exists_lem_aux: LEMMA
    sI(k, T)=i AND l<=k IMPLIES
    EXISTS Tp: sI(k-l, Tp)=i;

  live_sI_exists_lem: LEMMA
    sI(k, T)=i AND l<=k IMPLIES
    EXISTS Tp: sI(l, Tp)=i;

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

  Machine_is_live: LEMMA
    (mc_premise AND pipe_live_premise) IMPLIES
    E(conf_is_calc(k, i));

END pipetheory_spec