%
% General Pipeline Theory with Speculation
% N is the number of stages
%
% Copyright 2000 Daniel Kroening
%
 
spec_theory[N: { N:posint | N>=2 },
            last_spec_stage: { i:below(N) | i>=1 },
            (IMPORTING mathmtimet)
            ue:[below(N), mathmtimet->bool],
            full:[below(N), mathmtimet->bool],
            stall:[below(N), mathmtimet->bool],
            rollbackp:[below(N), mathmtimet->bool],
            stage_correct?:[below(N), mathmtimet->bool],
            stage_correctp?:[below(N), mathmtimet->bool],
            spec_correct?:[mathmtimet->bool],
            stage_spec_correct?:[below(N), mathmtimet->bool]]: THEORY
BEGIN

  % stage_correct: registers that are not speculative
  %
  % stage_correctp: registers that are speculative
  %
  % spec_correct: speculation registers

  ASSUMING
    T: VAR mathmtimet;
    k,l: VAR below(N);

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

    rollback_correct: ASSUMPTION
      (rollbackp(k, T) AND (k=N-1 OR NOT rollbackp(k+1, T))) IMPLIES
      (full(k, T) AND NOT stall(k, T));

    IMPORTING pipetheory_spec[N, ue, full, stall, rollbackp];
 
    prev_spec_correct?(k, T):bool=
      IF k=0 THEN
        spec_correct?(T)
      ELSE
        stage_spec_correct?(k-1, T)
      ENDIF;

    spec_initialization_premise: ASSUMPTION
      stage_correct?(k, 0) AND
      stage_correctp?(k, 0) AND
      stage_spec_correct?(k, 0);

    % non-speculative inputs
    stage_correct_inputs?(k, T):bool=
      (FORALL l: l>=k   => stage_correctp?(l, T)) AND
      (FORALL l: l>=k-1 => stage_correct?(l, T));

    % speculative inputs
    stage_correct_spec_inputs?(k, T):bool=
      IF k=0 THEN
        spec_correct?(T)
      ELSE
        stage_spec_correct?(k-1, T) AND
        stage_correctp?(k-1, T)
      ENDIF;

    spec_premise1: ASSUMPTION
      (k=N-1 OR NOT rollbackp(k+1, T)) AND
      stage_correct_inputs?(k, T) IMPLIES
      stage_correct?(k, T+1);

    spec_premise2: ASSUMPTION 
      (k=N-1 OR NOT rollbackp(k+1, T)) AND
      stage_correct_spec_inputs?(k, T) AND 
      stage_correct_inputs?(k, T) IMPLIES
      stage_correctp?(k, T+1);

    spec_premise3: ASSUMPTION
      (NOT ue(k, T) AND (k=N-1 OR NOT rollbackp(k+1, T))) IMPLIES
        (stage_correct?(k, T)=>stage_correct?(k, T+1)) AND
        (stage_correctp?(k, T)=>stage_correctp?(k, T+1)) AND
        (stage_spec_correct?(k, T)=>stage_spec_correct?(k, T+1));

    spec_premise4: ASSUMPTION
      ue(last_spec_stage, T) AND
      stage_correct_inputs?(last_spec_stage, T) IMPLIES
      stage_spec_correct?(last_spec_stage-1, T);

    spec_premise5: ASSUMPTION
      ue(k, T) AND
      stage_correct_inputs?(k, T) IMPLIES
      stage_spec_correct?(k, T+1)=prev_spec_correct?(k, T);

    spec_premise6: ASSUMPTION
        is_rollback_stage(k, T) AND
        (k>=1 => stage_correct?(k-1, T))
      IMPLIES
        FORALL l: l<k IMPLIES
         (stage_correct?(l, T+1) AND 
          stage_correctp?(l, T+1) AND
          stage_spec_correct?(l, T+1));

    spec_premise7: ASSUMPTION
      (NOT ue(k, T) AND (k=N-1 OR (NOT rollbackp(k+1, T)) AND 
         full(k+1, T) AND full(k+1, T+1))) IMPLIES
      stage_spec_correct?(k, T)=stage_spec_correct?(k, T+1);

    spec_premise8: ASSUMPTION
        is_rollback_stage(k, T) AND
        stage_correct_inputs?(k, T)
      IMPLIES
        (NOT prev_spec_correct?(k, T)) AND
        spec_correct?(T+1);

    spec_premise9: ASSUMPTION
      (NOT ue(0, T) AND NOT rollbackp(0, T) AND spec_correct?(T)) IMPLIES
      spec_correct?(T+1);

  ENDASSUMING

  rollback_stage_exists: LEMMA
    rollbackp(k, T) =>
    (EXISTS (j: below(N) | j>=k): is_rollback_stage(j, T));

  SPEC(T: mathmtimet): RECURSIVE below(N)=
    IF T=0 THEN
      0
    ELSIF ue(SPEC(T-1), T-1) THEN
      IF SPEC(T-1)=0 THEN
        IF spec_correct?(T-1) THEN 0 ELSE 1 ENDIF
      ELSIF SPEC(T-1)>=last_spec_stage THEN
        0
      ELSE
        SPEC(T-1)+1
      ENDIF
    ELSIF rollbackp(SPEC(T-1), T-1) THEN
      0
    ELSE
      SPEC(T-1)
    ENDIF
    MEASURE T;

  spec_full_lemma: LEMMA
    full(SPEC(T), T);

  spec_max_lemma: LEMMA
    SPEC(T)<=last_spec_stage;

  stage_spec_correct_lem: LEMMA
    (k=N-1 OR NOT rollbackp(k+1, T)) AND
    stage_correct_spec_inputs?(k, T) AND
    stage_correct_inputs?(k, T) AND
    stage_spec_correct?(k, T) IMPLIES
    stage_spec_correct?(k, T+1);
   
  spec_misspec_inv?(T):bool=
    (SPEC(T)>=1 => NOT stage_spec_correct?(SPEC(T)-1, T));

  spec_correct_inv?(T):bool=
    FORALL k:
    (k>=(SPEC(T)-1) => stage_correct?(k, T)) AND
    (k>=SPEC(T)     => stage_correctp?(k, T)) AND
    (k>=SPEC(T)     => stage_spec_correct?(k, T));

  spec_correct_inputs_lemma: LEMMA
    k>=SPEC(T) AND spec_correct_inv?(T) => stage_correct_inputs?(k, T);

  spec_correct_spec_inputs_lemma: LEMMA
    k>SPEC(T) AND spec_correct_inv?(T) => stage_correct_spec_inputs?(k, T);

  spec_inv?(T):bool=
    spec_misspec_inv?(T) AND
    spec_correct_inv?(T);

  spec_misspec_step: LEMMA
    spec_inv?(T) => spec_misspec_inv?(T+1);

  spec_data_consistency_lemma2: LEMMA
    (spec_inv?(T) AND NOT ue(k,T)) IMPLIES
    (k>=SPEC(T)-1 => stage_correct?(k, T+1)) AND
    (k>=SPEC(T)   => stage_correctp?(k, T+1)) AND
    (k>=SPEC(T)   => stage_spec_correct?(k, T+1));

  spec_data_consistency_lemma1: LEMMA
    spec_inv?(T) IMPLIES
    (k>=SPEC(T)   => stage_correct?(k, T+1)) AND
    (k>=SPEC(T)+1 => stage_correctp?(k, T+1)) AND
    (k>=SPEC(T)+1 => stage_spec_correct?(k, T+1));

  spec_data_consistency1: LEMMA
    spec_inv?(T) AND ue(SPEC(T), T) => spec_correct_inv?(T+1);

  spec_data_consistency2: LEMMA
    spec_inv?(T) AND (NOT ue(SPEC(T), T)) AND rollbackp(SPEC(T), T) => spec_correct_inv?(T+1);

  spec_data_consistency3: LEMMA
    spec_inv?(T) AND (NOT ue(SPEC(T), T)) AND (NOT rollbackp(SPEC(T), T)) => spec_correct_inv?(T+1);

  spec_inv_hold: LEMMA
    spec_inv?(T);

  spec_data_consistency: LEMMA
    (k>=(SPEC(T)-1) => stage_correct?(k, T)) AND
    (k>=SPEC(T)     => stage_correctp?(k, T)) AND
    (k>=SPEC(T)     => stage_spec_correct?(k, T));

  %
  % liveness
  %

  spec_le_M_lem: LEMMA
    SPEC(T)<=M(T);

  M_correct_inputs_lemma: LEMMA
    stage_correct_inputs?(M(T), T);

  mc_premise_spec: LEMMA
    Mc(T) => prev_spec_correct?(M(T), T);

  mc_premise_lem: LEMMA
    mc_premise;
 
END spec_theory