Fixpoint baseTermAtSamePosBaseTerms (btm:baseTerm) (bts1: list baseTerm) (bts2:list baseTerm) : Prop :=
  match bts1, bts2 with
    | bt1::btst1, bt2::btst2 => ( bt1=btm /\ bt2=btm ) \/ baseTermAtSamePosBaseTerms btm btst1 btst2
    | _, _ => False
  end.

Definition baseTermAtSamePosTerm (bt:baseTerm) (t1: term) (t2: term) : Prop :=
  match t1, t2 with
    | Bterm bt1, Bterm bt2 => bt1=bt /\ bt2=bt
    | Func n1 bts1, Func n2 bts2 => (n1=n2 /\ baseTermAtSamePosBaseTerms bt bts1 bts2)
    | _, _ => False
  end.

Fixpoint baseTermAtSamePosTerms (bt:baseTerm) (ts1: list term) (ts2:list term) : Prop :=
  match ts1, ts2 with
    | t1::ts1t, t2::ts2t => (baseTermAtSamePosTerm bt t1 t2) \/ (baseTermAtSamePosTerms bt ts1t ts2t)
    | _, _ => False
  end.

Definition variableInInputAndOutputOld (x:variable) (newRule:rule) (pastRules: list rule) : Prop :=
  match pastRules with
    | [] => False
    | prule::prules => exists ts1 ts2, member (IN ts1) (premiseFacts newRule)
                       /\ member (OUT ts2) (conclFacts (lastElement prule prules))
                       /\ baseTermAtSamePosTerms (Var x) ts1 ts2
end.

Fixpoint termPresentInFirstOutputFound (ts:terms) (pastRules:list rule) : Prop :=
  match pastRules with
    | [] => False
    | prule::prules => if (beq_facts (getOutFactConclusion (conclFacts (lastElement prule prules))) [])
                        then termPresentInFirstOutputFound ts prules
                          else (member (OUT ts) (conclFacts (lastElement prule prules)))
  end.

Definition variableInInputAndOutput (x:variable) (newRule:rule) (pastRules: list rule) : Prop :=
  match pastRules with
    | [] => False
    | prule::prules => exists ts1 ts2, (member (IN ts1) (premiseFacts newRule))
                       /\ termPresentInFirstOutputFound ts2 pastRules
                       /\ baseTermAtSamePosTerms (Var x) ts1 ts2
end.

Fixpoint NameDoesNotAppearInFacts (n:name) (fs:facts) : Prop :=
   match fs with
    | [] => True
    | fh::fst => match fh with
                   | STATE nm1 ts1 => n <> nm1 /\ (NameDoesNotAppearInFacts n fst)
                   | _ => (NameDoesNotAppearInFacts n fst)
                  end
   end.

Fixpoint stateFactNameDoesNotAppear (f:fact) (fs:facts) : Prop :=
   match f with
    | STATE n ts => NameDoesNotAppearInFacts n fs
    | _ => True
   end.

Fixpoint stateAppearsOnce (f:fact) (fs:facts) : Prop :=
  match fs, f with
    | fh::fst, STATE n1 ts1 => match fh with
                                 | STATE n2 ts2 => (n1=n2 /\ ts1=ts2 /\ NameDoesNotAppearInFacts n1 fst)
                                                   \/ (n1 <> n2 /\ stateAppearsOnce f fst)
                                 | _ => stateAppearsOnce f fst
                               end
    | _, _ => False
  end.

Fixpoint TermsInSamePosition (tm1:terms) (tm2:terms) (t1:term) (t2:term) : Prop :=
  match tm1, tm2 with
   | tm11::tm1s, tm21::tm2s => ((eq_term tm11 t1) /\ (eq_term tm21 t2)) \/ (TermsInSamePosition tm1s tm2s t1 t2)
   | [], [] => False
   | [], _::_ => False
   | _::_, [] => False
  end.

Fixpoint AllTermsEqualPositionWise (tm1:terms) (tm2:terms) : Prop :=
  match tm1, tm2 with
   | tm11::tm1s, tm21::tm2s => (eq_term tm11 tm21 ) /\ (AllTermsEqualPositionWise tm1s tm2s)
   | [], [] => True
   | [], _::_ => False
   | _::_, [] => False
  end.

Fixpoint AllSubTermsEqualPositionWise (bt1:list baseTerm) (bt2:list baseTerm) : Prop :=
  match bt1, bt2 with
   | bt11::bt1s, bt21::bt2s => (eq_baseTerm bt11 bt21 ) /\ (AllSubTermsEqualPositionWise bt1s bt2s)
   | [], [] => True
   | [], _::_ => False
   | _::_, [] => False
  end.

Fixpoint PresentInOutputInputConsecutiveRules (RL:list rule) (t1:term) (t2:term) : Prop :=
match RL with
  | r1::rs => match rs with
                    | rs1::rst => match getOutFactProtoRule r1, getInFactProtoRule rs1 with
                                          | [OUT lt1], [IN lt2] => TermsInSamePosition lt1 lt2 t1 t2
                                          | _,_ => False
                                  end
                    | [] => False
                end
  | [] => False
  end.

Fixpoint comparebaseTerms (t1: baseTerms) (t2: baseTerms) : list tpair :=
match t1, t2 with
      | t11::ts1, t21::ts2 =>
                         (match t11, t21 with
                              | Var v1, Var v2 => if (beq_var v1 v2)
                                                                  then (comparebaseTerms ts1 ts2)
                                                              else (pair (Bterm t11) (Bterm t21))::(comparebaseTerms ts1 ts2)
                              | Name nm1, Name nm2 => if (beq_name nm1 nm2)
                                                           then (comparebaseTerms ts1 ts2)
                                                              else (pair (Bterm t11) (Bterm t21))::(comparebaseTerms ts1 ts2)
                              | _, _ => (comparebaseTerms ts1 ts2)
                          end)
      | _,_ => []
  end.

Fixpoint compareTerms (t1: terms) (t2: terms) : list tpair :=
match t1, t2 with
      | t11::ts1, t21::ts2 =>
                        (match t11, t21 with
                        | Bterm bt1, Bterm bt2 => if (beq_baseTerm bt1 bt2)
                                                          then (compareTerms ts1 ts2)
                                                              else (pair t11 t21)::(compareTerms ts1 ts2)
                        | Func n1 bts1, Func n2 bts2 => if (beq_string n1 n2)
                                                           then (comparebaseTerms bts1 bts2)
                                                              else (pair t11 t21)::(compareTerms ts1 ts2)
                        | _, _ => (compareTerms ts1 ts2)
                        end)
      | _,_ => []
  end.

Fixpoint commonInPairs (p1:tpair) (p2:tpair) : bool :=
  match p1,p2 with
    | pair h1 t1, pair h2 t2 => orb (beq_term h1 h2) ( orb (beq_term h1 t2) (beq_term t1 t2))
    | _,_ => false
  end.

Fixpoint commonInList (ts1:terms) (ts2:terms) : bool :=
  match ts1 with
    | ts11::ts1s => orb (memberWith ts11 ts2 beq_term) (commonInList ts1s ts2)
    | [] => false
  end.

Fixpoint joinPairs (p1:tpair) (p2:tpair) : terms :=
  match p1,p2 with
    | pair h1 t1, pair h2 t2 => t2::(t1::(h2::(h1::[])))
    | _,_ => []
  end.

Fixpoint PairToList (p1:tpair) : terms :=
  match p1 with
    | pair h1 t1 => (t1::(h1::[]))
    | emptypair => []
  end.

Fixpoint uniqueTerms (tm: terms) : terms :=
  match tm with
    | t1::ts => if (memberWith t1 ts beq_term) then (uniqueTerms ts) else t1::(uniqueTerms ts)
    | [] => []
  end.

Fixpoint listIsASublist (t:terms) (lt:terms) : bool :=
  match t with
    | t1::ts => andb (memberWith t1 lt beq_term) (listIsASublist ts lt)
    | [] => true
  end.

Fixpoint listMembersAlreadyPresent (t:terms) (lt:list terms) : bool :=
  match lt with
    | lt1::lts => orb (listIsASublist t lt1) (listMembersAlreadyPresent t lts)
    | [] => false
  end.

Fixpoint finalListWithDuplicatesRemoved (t1:terms) (lt: list terms) : terms :=
match lt with
   | lt1::lts => if (commonInList lt1 t1)
                        then (t1)
                        else (uniqueTerms (appendAny t1 (finalListWithDuplicatesRemoved t1 lts )))
   | [] => []
  end.

Fixpoint finalListsWithDuplicatesRemoved (lt: list terms) : list terms :=
  match lt with
    | t1::ts => (finalListWithDuplicatesRemoved t1 ts) :: (finalListsWithDuplicatesRemoved ts )
    | [] => []
  end.

Fixpoint collectStateFacts (rlst:ruleList) : facts :=
  match rlst with
  | rl1::rls => appendAny (appendAny (getStateFacts (premiseFacts rl1 )) (getStateFacts (conclFacts rl1 ))) (collectStateFacts rls)
  | [] => []
  end.

Fixpoint eq_STATEname (f1:fact) (f2:fact) : Prop :=
  match f1,f2 with
   | STATE n1 ts1, STATE n2 ts2 => eq_name n1 n2
   | _, _ => False
  end.

Fixpoint CheckTermsUSF (f1:fact) (fs:list fact) (t1:term) (t2:term) : Prop :=
match fs with
  | fs1::fst => match f1, fs1 with
                   | STATE n1 tm1, STATE n2 tm2 => if (beq_name n1 n2) then (TermsInSamePosition tm1 tm2 t1 t2)
                                                    else (CheckTermsUSF f1 fst t1 t2)
                   | _,_ => False
                 end
  | [] => False
end.

Fixpoint CheckFactsInUSF (fls:facts) (usf:fact) (t1:term) (t2:term) : Prop :=
match fls with
  | f1::fs => (eq_STATEname f1 usf) /\ (CheckTermsUSF f1 fs t1 t2) \/ (CheckFactsInUSF fs usf t1 t2)
  | [] => False
end.

Fixpoint CheckTermsUAF (f1:fact) (fs:list fact) (t1:term) (t2:term) : Prop :=
match fs with
  | fs1::fst => match f1, fs1 with
                   | STATE n1 tm1, STATE n2 tm2 => if (beq_name n1 n2) then (TermsInSamePosition tm1 tm2 t1 t2)
                                                    else (CheckTermsUAF f1 fst t1 t2)
                   | _,_ => False
                 end
  | [] => False
end.

Fixpoint CheckFactsInUAF (fls:facts) (uaf:fact) (t1:term) (t2:term) : Prop :=
match fls with
  | f1::fs => (eq_STATEname f1 uaf) /\ (CheckTermsUAF f1 fs t1 t2) \/ (CheckFactsInUAF fs uaf t1 t2)
  | [] => False
end.

Fixpoint nameAndConstantDoNotAppear (n:name) (c:publicName) (fs:facts) : Prop :=
  match fs with
    | [] => True
    | fh::fst => match fh with
                  | STATE n2 ts => ((n=n2 /\ NotIn (Bterm (Name (Pub c))) ts) \/ n <> n2 )
                                  /\ (nameAndConstantDoNotAppear n c fst)
                  | _ => nameAndConstantDoNotAppear n c fst
                 end
  end.

Fixpoint termIsOnlyConstant (t:term) (n:name) (rs:(list rule)) : Prop :=
  match t with
    | Bterm (Name (Pub c)) => nameAndConstantDoNotAppear n c (allConclFacts rs)

    | _ => False
  end.

Fixpoint termIsFresh (t:term) (r:rule) : Prop :=
  match t with
    | Bterm (Var x) => member (FR_P (Var x)) (premiseFacts r)
    | _ => False
  end.

Fixpoint wellFormedSetupPremiseFact (f:fact) : Prop :=
  match f with
  | IN t => True
  | OUT t => False
  | K t => False
  | STATE n t => True
  | FR_P n => match n with
                  | Var v => True
                  | _ => False
                 end
  end.

Definition wellFormedSetupPremiseFacts : facts -> Prop := trueForAll wellFormedSetupPremiseFact.

Fixpoint wellFormedConclusionFact (f:fact) : Prop :=
  match f with
  | IN t => False
  | OUT t => True
  | K t => False
  | STATE n t => True
  | FR_P fp => False
  end.

Fixpoint wellFormedConclusionFacts (fs: facts) : Prop :=
  (match fs with
  | f1::fss => wellFormedConclusionFact f1 /\ wellFormedConclusionFacts fss
  | [] => True
  end)
  /\ (oneOrNoOutput fs).

Fixpoint wellFormedSetupLabel (l:label) :=
  match l with
    | BasicLabel l => True
    | LoggedLabel a l => False
    | LoggedSIDLabel t a l => False
  end.

Fixpoint wellFormedSetupRule (r:rule) : Prop :=
  match r with
    | RuleSetup fs1 l fs2 => ((wellFormedSetupPremiseFacts fs1) /\ (wellFormedSetupLabel l)) /\ (wellFormedConclusionFacts fs2)
    | _ => False
  end.

Definition wellFormedSetupRules : ruleList -> Prop := trueForAll wellFormedSetupRule.

Fixpoint wellFormedProtoPremiseFact (f:fact) : Prop :=
  match f with
  | IN t => True
  | OUT t => False
  | K t => False
  | STATE n t => True
  | FR_P n => match n with
                  | Var v => True
                  | _ => False
                 end
  end.

Fixpoint wellFormedProtoPremiseFacts (fs: facts) : Prop :=
(match fs with
  | f1::fss => wellFormedProtoPremiseFact f1 /\ wellFormedProtoPremiseFacts fss
  | [] => True
  end)
  /\ (oneOrNoInput fs).

Fixpoint wellFormedProtoRule (r:rule) : Prop :=
  match r with
    | RuleProto fs1 l fs2 => (wellFormedProtoPremiseFacts fs1) /\ (wellFormedConclusionFacts fs2)
    | _ => False
  end.

Fixpoint inputsOutputsFromRule (r : rule) : facts :=
  appendAny (getInFactProtoRule r) (getOutFactProtoRule r).

Fixpoint inputsOutputsFromRuleList (rl : ruleList) : facts :=
  match rl with
     | r1::rs => appendAny (inputsOutputsFromRule r1) (inputsOutputsFromRuleList rs)
     | [] => []
  end.

Fixpoint alternateInputsOutputs (fs : facts) : Prop :=
  match fs with
     | f1::fs => match fs with
                      | fs1:: fss => match f1,fs1 with
                                       | IN _, IN _ => False
                                       | OUT _, OUT _ => False
                                       | _, _ => alternateInputsOutputs fs
                                     end
                      | [] => True
                  end
    | [] => True
  end.

Fixpoint wellFormedProtoRules (rl: ruleList) : Prop :=
  (match rl with
  | r1::rs => wellFormedProtoRule r1 /\ wellFormedProtoRules rs
  | [] => True
  end)
  /\ (alternateInputsOutputs (inputsOutputsFromRuleList rl)).

Fixpoint wellFormedRule (r:rule) : Prop :=
  match r with
    | RuleSetup fs1 l fs2 => wellFormedSetupRule r
    | RuleProto fs1 l fs2 => wellFormedProtoRule r
  end.

Fixpoint wellFormedAllowedSequences (allowSeq:list ruleList) : Prop :=
  match allowSeq with
  | al1::als => (wellFormedProtoRules al1) /\ (wellFormedAllowedSequences als)
  | [] => True
  end.

Fixpoint wellFormedLoggedLabel (l:label) :=
  match l with
    | BasicLabel l => False
    | LoggedLabel a l => True
    | LoggedSIDLabel t a l => False
  end.

Fixpoint wellFormedLoggedSIDLabel (l:label) :=
  match l with
    | BasicLabel l => False
    | LoggedLabel a l => False
    | LoggedSIDLabel t a l => True
  end.

Lemma wellFormedTail : forall h ts, wellFormedSetupRules (h::ts) -> wellFormedSetupRules(ts).

Fixpoint InputToOutputProtocolRule (r:rule) : Prop :=
match r with
    | RuleProto fs1 l fs2 => (oneInput fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (oneOutput fs2)
    | _ => False
  end.

Fixpoint InputToStateProtocolRule (r:rule) : Prop :=
match r with
    | RuleProto fs1 l fs2 => (oneInput fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (noOutputs fs2)
    | _ => False
  end.

Fixpoint StateToOutputProtocolRule (r:rule) : Prop :=
match r with
    | RuleProto fs1 l fs2 => (noInputs fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (oneOutput fs2)
    | _ => False
  end.

Fixpoint StateToStateProtocolRule (r:rule) : Prop :=
match r with
    | RuleProto fs1 l fs2 => (noInputs fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (noOutputs fs2)
    | _ => False
  end.

Fixpoint wellFormedProtoRuleInOutState (r:rule) : Prop :=
(InputToOutputProtocolRule r ) \/ (InputToStateProtocolRule r)
    \/ (StateToOutputProtocolRule r) \/ (StateToStateProtocolRule r).

Fixpoint wellFormedProtoRuleNoInOut (rs:ruleList) : Prop :=
  match rs with
    | [] => True
    | r::rss => ((StateToOutputProtocolRule r) /\ (wellFormedProtoRuleFromInOut rss))
                  \/ ((StateToStateProtocolRule r) /\ (wellFormedProtoRuleNoInOut rss))
   end
with
  wellFormedProtoRuleFromInOut (rs:ruleList) : Prop :=
  match rs with
    | [] => True
    | r::rss => ((InputToStateProtocolRule r) /\ (wellFormedProtoRuleNoInOut rss))
                  \/ ((StateToStateProtocolRule r) /\ (wellFormedProtoRuleFromInOut rss))
                    \/ ((InputToOutputProtocolRule r) /\ (wellFormedProtoRuleFromInOut rss))
   end.

Definition Def6_2_wellformedRulesFromState (fs:facts) (rs:ruleList) : Prop :=
  (oneInputXorOutput fs /\ wellFormedProtoRuleFromInOut rs)
    \/ ( noInputOrOutput fs /\ wellFormedProtoRuleNoInOut rs).

Fixpoint InputToOutputSetupRule (r:rule) : Prop :=
match r with
    | RuleProto fs1 l fs2 => (oneInput fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (oneOutput fs2)
    | _ => False
  end.

Fixpoint InputToStateSetupRule (r:rule) : Prop :=
match r with
    | RuleProto fs1 l fs2 => (oneInput fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (noOutputs fs2)
    | _ => False
  end.

Fixpoint StateToOutputSetupRule (r:rule) : Prop :=
match r with
    | RuleProto fs1 l fs2 => (noInputs fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (oneOutput fs2)
    | _ => False
  end.

Fixpoint StateToStateSetupRule (r:rule) : Prop :=
match r with
    | RuleProto fs1 l fs2 => (noInputs fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (noOutputs fs2)
    | _ => False
  end.

Fixpoint wellFormedSetupRuleInOutState (r:rule) : Prop :=
(InputToOutputSetupRule r ) \/ (InputToStateSetupRule r)
    \/ (StateToOutputSetupRule r) \/ (StateToStateSetupRule r).

Fixpoint wellFormedSetupRuleNoInOut (rs:ruleList) : Prop :=
  match rs with
    | [] => True
    | r::rss => ((StateToOutputSetupRule r) /\ (wellFormedSetupRuleFromInOut rss))
                  \/ ((StateToStateSetupRule r) /\ (wellFormedSetupRuleNoInOut rss))
   end
with
  wellFormedSetupRuleFromInOut (rs:ruleList) : Prop :=
  match rs with
    | [] => True
    | r::rss => ((InputToStateSetupRule r) /\ (wellFormedSetupRuleNoInOut rss))
                  \/ ((StateToStateSetupRule r) /\ (wellFormedSetupRuleFromInOut rss))
                    \/ ((InputToOutputSetupRule r) /\ (wellFormedSetupRuleFromInOut rss))
   end.

Definition Def6_2_wellformedRulesFromStateSetup (fs:facts) (rs:ruleList) : Prop :=
  (oneInputXorOutput fs /\ wellFormedSetupRuleFromInOut rs)
    \/ ( noInputOrOutput fs /\ wellFormedSetupRuleNoInOut rs).

Fixpoint outputRule (r:rule) := StateToOutputProtocolRule r /\ InputToOutputProtocolRule r.
Fixpoint noOutputRule (r:rule) := StateToStateProtocolRule r /\ InputToStateProtocolRule r.
Fixpoint inputRule (r:rule) := InputToStateProtocolRule r /\ InputToOutputProtocolRule r.
Fixpoint noInputRule (r:rule) := StateToStateProtocolRule r /\ StateToOutputProtocolRule r.

Library Sec8_Chap6WellFormedRules

8C: Well formedness definitions

Global Index

S

Library Index

S