\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

This tutorial provides a very quick introduction to the main concepts of Squirrel. It can be used to ease its discovery and to get an intuitive grasp of the multiple concepts by going through a concrete example. The reference manual provides a more extensive presentation of all the concepts.

In many cases, the concepts introduced here are also direct clickable references to the more extensive presentation in the reference manual.

Protocol modelling

Squirrel allows performing proofs of security for communication protocols relying on cryptography. It works within a high-order logic, and a first step is to be able to model all the components of a protocol inside the logic.

First, let us load the standard library of Squirrel, Core, loaded in most examples, and which provides basic logical reasonings capabilities (the standard library can be found in the theories/ subfolder of Squirrel).

include Core. (* as a preliminary, we simply load the Core library, preload in all files. *)

op assoc [‘a] (f:’a -> ‘a -> ‘a) : bool = forall (x,y,z:’a), f (f x y) z = f x (f y z) axiom eq_iff {‘P:system} @system:(set:’P; equiv:None) : forall (x,y:bool), (x = y) = (x <=> y) axiom eq_not {‘P:system} @system:(set:’P; equiv:None) : forall (x,y:bool), (not x = not y) = (x = y) Goal eq_sym : (x = y) = (y = x) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a —————————————- (x = y) = (y = x) [goal> lemma eq_sym is proved lemma eq_sym {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), (x = y) = (y = x) Exiting proof mode. Goal neq_sym : (x <> y) = (y <> x) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a —————————————- (x <> y) = (y <> x) [goal> lemma neq_sym is proved lemma neq_sym {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), (x <> y) = (y <> x) Exiting proof mode. Goal eq_refl_e : (x = x) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x:’a —————————————- (x = x) = true [goal> lemma eq_refl_e is proved lemma eq_refl_e {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x:’a), (x = x) = true Exiting proof mode. Goal eq_refl : x = x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x:’a —————————————- x = x [goal> lemma eq_refl is proved lemma eq_refl {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x:’a), x = x Exiting proof mode. Goal neq_irrefl : x <> x <=> false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x:’a —————————————- x <> x <=> false [goal> lemma neq_irrefl is proved lemma neq_irrefl {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x:’a), x <> x <=> false Exiting proof mode. Goal eq_assoc : ((b0 = b1) = b2) = (b0 = (b1 = b2)) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1,b2:bool —————————————- ((b0 = b1) = b2) = (b0 = (b1 = b2)) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1,b2:bool[const] true_false: (true = false) = false —————————————- ((b0 = b1) = b2) = (b0 = (b1 = b2)) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1,b2:bool[const] false_true: (false = true) = false true_false: (true = false) = false —————————————- ((b0 = b1) = b2) = (b0 = (b1 = b2)) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1,b2:bool[const] false_true: (false = true) = false true_false: (true = false) = false —————————————- not b2 => not b1 => b0 => ((true = false) = false) = (true = (false = false)) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1,b2:bool[const] false_true: (false = true) = false true_false: (true = false) = false —————————————- b2 => not b1 => not b0 => ((false = false) = true) = (false = (false = true)) [goal> lemma eq_assoc is proved lemma eq_assoc {‘P:system} @system:(set:’P; equiv:None) : forall (b0,b1,b2:bool), ((b0 = b1) = b2) = (b0 = (b1 = b2)) Exiting proof mode. axiom fun_ext {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (f,g:’a -> ‘b), (forall (x:’a), f x = g x) => f = g Goal true_false : (true = false) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) —————————————- (true = false) = false [goal> lemma true_false is proved lemma true_false {‘P:system} @system:(set:’P; equiv:None) : (true = false) = false Exiting proof mode. Goal false_true : (false = true) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) —————————————- (false = true) = false [goal> lemma false_true is proved lemma false_true {‘P:system} @system:(set:’P; equiv:None) : (false = true) = false Exiting proof mode. Goal eq_true : (b = true) = b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (b = true) = b [goal> lemma eq_true is proved lemma eq_true {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (b = true) = b Exiting proof mode. Goal eq_true2 : (true = b) = b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (true = b) = b [goal> lemma eq_true2 is proved lemma eq_true2 {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (true = b) = b Exiting proof mode. axiom not_true {‘P:system} @system:(set:’P; equiv:None) : not true = false axiom not_false {‘P:system} @system:(set:’P; equiv:None) : not false = true Goal not_not : not (not b) = b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- not (not b) = b [goal> lemma not_not is proved lemma not_not {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), not (not b) = b Exiting proof mode. Goal not_eq : not (x = y) = (x <> y) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a —————————————- not (x = y) = (x <> y) [goal> lemma not_eq is proved lemma not_eq {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), not (x = y) = (x <> y) Exiting proof mode. Goal not_neq : not (x <> y) = (x = y) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a —————————————- not (x <> y) = (x = y) [goal> lemma not_neq is proved lemma not_neq {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), not (x <> y) = (x = y) Exiting proof mode. Goal not_eqfalse : (b = false) = not b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (b = false) = not b [goal> lemma not_eqfalse is proved lemma not_eqfalse {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (b = false) = not b Exiting proof mode. Goal not_impl : not (a => b) = (a && not b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool —————————————- not (a => b) = (a && not b) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] H: not (a => b) —————————————- a && not b [goal> Focused goal (1/3): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] H: not (a => b) —————————————- a [goal> Focused goal (1/3): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] H: not (a => b) —————————————- not (not a) [goal> Focused goal (1/3): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] H: not (a => b) Hna: not a —————————————- false [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] H: not (a => b) —————————————- not b [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] H: not (a => b) Hb: b —————————————- false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] H: a && not b —————————————- not (a => b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] H: a && not b Hi: a => b —————————————- false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] Ha: a Hi: a => b Hnb: not b —————————————- false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] Ha: a Hi: a => b Hnb: not b —————————————- b [goal> lemma not_impl is proved lemma not_impl {‘P:system} @system:(set:’P; equiv:None) : forall (a,b:bool), not (a => b) = (a && not b) Exiting proof mode. Goal eq_false : ((x = y) = false) = (x <> y) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a —————————————- ((x = y) = false) = (x <> y) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a —————————————- ((x = y) = false) = not (x = y) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a _: x = y —————————————- (true = false) = not true [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a _: x = y —————————————- true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a _: not (x = y) —————————————- (false = false) = not false [goal> lemma eq_false is proved lemma eq_false {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), ((x = y) = false) = (x <> y) Exiting proof mode. axiom and_comm {‘P:system} @system:(set:’P; equiv:None) : forall (b,b’:bool), (b && b’) = (b’ && b) Goal and_dist : ((b0 || b1) && b2) = (b0 && b2 || b1 && b2) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1,b2:bool —————————————- ((b0 || b1) && b2) = (b0 && b2 || b1 && b2) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1,b2:bool[const] —————————————- (b0 || b1) && b2 <=> b0 && b2 || b1 && b2 [goal> lemma and_dist is proved lemma and_dist {‘P:system} @system:(set:’P; equiv:None) : forall (b0,b1,b2:bool), ((b0 || b1) && b2) = (b0 && b2 || b1 && b2) Exiting proof mode. axiom and_true_l {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (true && b) = b Goal and_true_r : (b && true) = b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (b && true) = b [goal> lemma and_true_r is proved lemma and_true_r {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (b && true) = b Exiting proof mode. axiom and_false_l {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (false && b) = false Goal and_false_r : (b && false) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (b && false) = false [goal> lemma and_false_r is proved lemma and_false_r {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (b && false) = false Exiting proof mode. Goal and_double : (b && b) = b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (b && b) = b [goal> lemma and_double is proved lemma and_double {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (b && b) = b Exiting proof mode. axiom or_comm {‘P:system} @system:(set:’P; equiv:None) : forall (b,b’:bool), (b || b’) = (b’ || b) Goal or_dist : ((b0 || b2) && (b1 || b2)) = (b0 && b1 || b2) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1,b2:bool —————————————- ((b0 || b2) && (b1 || b2)) = (b0 && b1 || b2) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1,b2:bool[const] —————————————- (b0 || b2) && (b1 || b2) <=> b0 && b1 || b2 [goal> lemma or_dist is proved lemma or_dist {‘P:system} @system:(set:’P; equiv:None) : forall (b0,b1,b2:bool), ((b0 || b2) && (b1 || b2)) = (b0 && b1 || b2) Exiting proof mode. axiom or_false_l {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (false || b) = b Goal or_false_r : (b || false) = b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (b || false) = b [goal> lemma or_false_r is proved lemma or_false_r {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (b || false) = b Exiting proof mode. axiom or_true_l {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (true || b) = true Goal or_true_r : (b || true) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (b || true) = true [goal> lemma or_true_r is proved lemma or_true_r {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (b || true) = true Exiting proof mode. Goal or_double : (b || b) = b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (b || b) = b [goal> lemma or_double is proved lemma or_double {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (b || b) = b Exiting proof mode. Goal impl_charac : (b => b’) = (not b || b’) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b,b’:bool —————————————- (b => b’) = (not b || b’) [goal> lemma impl_charac is proved lemma impl_charac {‘P:system} @system:(set:’P; equiv:None) : forall (b,b’:bool), (b => b’) = (not b || b’) Exiting proof mode. Goal impl_false_l : (false => b) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (false => b) = true [goal> lemma impl_false_l is proved lemma impl_false_l {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (false => b) = true Exiting proof mode. Goal impl_true_r : (b => true) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (b => true) = true [goal> lemma impl_true_r is proved lemma impl_true_r {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (b => true) = true Exiting proof mode. Goal impl_true_l : (true => b) = b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool —————————————- (true => b) = b [goal> lemma impl_true_l is proved lemma impl_true_l {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool), (true => b) = b Exiting proof mode. Goal impl_contra : (b => c) = (not c => not b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b,c:bool —————————————- (b => c) = (not c => not b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b,c:bool[const] —————————————- (not b || c) = (c || not b) [goal> lemma impl_contra is proved lemma impl_contra {‘P:system} @system:(set:’P; equiv:None) : forall (b,c:bool), (b => c) = (not c => not b) Exiting proof mode. Goal absurd : not (not a) => a [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a:bool —————————————- not (not a) => a [goal> lemma absurd is proved lemma absurd {‘P:system} @system:(set:’P; equiv:None) : forall (a:bool), not (not a) => a Exiting proof mode. Goal not_and : not (a && b) = (not a || not b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool —————————————- not (a && b) = (not a || not b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] —————————————- not (a && b) <=> not a || not b [goal> lemma not_and is proved lemma not_and {‘P:system} @system:(set:’P; equiv:None) : forall (a,b:bool), not (a && b) = (not a || not b) Exiting proof mode. Goal not_or : not (a || b) = (not a && not b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool —————————————- not (a || b) = (not a && not b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: a,b:bool[const] —————————————- not (a || b) <=> not a && not b [goal> lemma not_or is proved lemma not_or {‘P:system} @system:(set:’P; equiv:None) : forall (a,b:bool), not (a || b) = (not a && not b) Exiting proof mode. Goal if_true : b => if b then x else y = x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool,x,y:’a —————————————- b => if b then x else y = x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool[const],x,y:’a H: b —————————————- if b then x else y = x [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool[const],x,y:’a H: b —————————————- b && if b then x else y = x => x = x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool[const],x,y:’a H: b —————————————- not b && if b then x else y = y => y = x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool[const],x,y:’a H: b HH: not b _: if b then x else y = y —————————————- y = x [goal> lemma if_true is proved lemma if_true {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b:bool,x,y:’a), b => if b then x else y = x Exiting proof mode. Goal if_true0 : if true then x else y = x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a —————————————- if true then x else y = x [goal> lemma if_true0 is proved lemma if_true0 {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), if true then x else y = x Exiting proof mode. Goal if_false : not b => if b then x else y = y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool,x,y:’a —————————————- not b => if b then x else y = y [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool[const],x,y:’a H: not b —————————————- b && if b then x else y = x => x = y [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool[const],x,y:’a H: not b H1: b H2: if b then x else y = x —————————————- x = y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool[const],x,y:’a H: not b —————————————- not b && if b then x else y = y => y = y [goal> lemma if_false is proved lemma if_false {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b:bool,x,y:’a), not b => if b then x else y = y Exiting proof mode. Goal if_false0 : if false then x else y = y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a —————————————- if false then x else y = y [goal> lemma if_false0 is proved lemma if_false0 {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), if false then x else y = y Exiting proof mode. Goal if_then_then : if b then (if b’ then x else y) else y = if (b && b’) then x else y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b,b’:bool,x,y:’a —————————————- if b then (if b’ then x else y) else y = if (b && b’) then x else y [goal> lemma if_then_then is proved lemma if_then_then {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b,b’:bool,x,y:’a), if b then (if b’ then x else y) else y = if (b && b’) then x else y Exiting proof mode. Goal if_then_or : if b0 then m0 else if b1 then m0 else m1 = if (b0 || b1) then m0 else m1 [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1:bool,m0,m1:message —————————————- if b0 then m0 else if b1 then m0 else m1 = if (b0 || b1) then m0 else m1 [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1:bool[const],m0,m1:message _: b0 —————————————- if b0 then m0 else if b1 then m0 else m1 = if (b0 || b1) then m0 else m1 [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1:bool[const],m0,m1:message _: b0 —————————————- m0 = if (b0 || b1) then m0 else m1 [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1:bool[const],m0,m1:message _: not b0 —————————————- if b0 then m0 else if b1 then m0 else m1 = if (b0 || b1) then m0 else m1 [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1:bool[const],m0,m1:message _: b1 _: not b0 —————————————- if b0 then m0 else if b1 then m0 else m1 = if (b0 || b1) then m0 else m1 [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1:bool[const],m0,m1:message _: b1 _: not b0 —————————————- if b1 then m0 else m1 = if (b0 || b1) then m0 else m1 [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b0,b1:bool[const],m0,m1:message _: not b1 _: not b0 —————————————- if b0 then m0 else if b1 then m0 else m1 = if (b0 || b1) then m0 else m1 [goal> lemma if_then_or is proved lemma if_then_or {‘P:system} @system:(set:’P; equiv:None) : forall (b0,b1:bool,m0,m1:message), if b0 then m0 else if b1 then m0 else m1 = if (b0 || b1) then m0 else m1 Exiting proof mode. Goal if_then_implies : if b then (if b’ then x else y) else z = if b then (if (b => b’) then x else y) else z [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b,b’:bool,x,y,z:’a —————————————- if b then (if b’ then x else y) else z = if b then (if (b => b’) then x else y) else z [goal> lemma if_then_implies is proved lemma if_then_implies {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b,b’:bool,x,y,z:’a), if b then (if b’ then x else y) else z = if b then (if (b => b’) then x else y) else z Exiting proof mode. Goal if_same : if b then x else x = x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool,x:’a —————————————- if b then x else x = x [goal> lemma if_same is proved lemma if_same {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b:bool,x:’a), if b then x else x = x Exiting proof mode. Goal if_same_under_cond : (b => x = y) => if b then x else y = y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool,x,y:’a —————————————- (b => x = y) => if b then x else y = y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b:bool[const],x,y:’a Eq: b => x = y —————————————- if b then x else y = y [goal> lemma if_same_under_cond is proved lemma if_same_under_cond {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b:bool,x,y:’a), (b => x = y) => if b then x else y = y Exiting proof mode. Goal if_then : b = b’ => if b then (if b’ then x else y) else z = if b then x else z [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b,b’:bool,x,y,z:’a —————————————- b = b’ => if b then (if b’ then x else y) else z = if b then x else z [goal> lemma if_then is proved lemma if_then {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b,b’:bool,x,y,z:’a), b = b’ => if b then (if b’ then x else y) else z = if b then x else z Exiting proof mode. Goal if_then_inv : if b then m0 else m1 = if b then (if b then m0) else m1 [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool,m0,m1:message —————————————- if b then m0 else m1 = if b then (if b then m0) else m1 [goal> lemma if_then_inv is proved lemma if_then_inv {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool,m0,m1:message), if b then m0 else m1 = if b then (if b then m0) else m1 Exiting proof mode. Goal if_else : b = b’ => if b then x else if b’ then y else z = if b then x else z [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b,b’:bool,x,y,z:’a —————————————- b = b’ => if b then x else if b’ then y else z = if b then x else z [goal> lemma if_else is proved lemma if_else {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b,b’:bool,x,y,z:’a), b = b’ => if b then x else if b’ then y else z = if b then x else z Exiting proof mode. Goal if_else_inv : if b then m0 else m1 = if b then m0 else if not b then m1 [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool,m0,m1:message —————————————- if b then m0 else m1 = if b then m0 else if not b then m1 [goal> lemma if_else_inv is proved lemma if_else_inv {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool,m0,m1:message), if b then m0 else m1 = if b then m0 else if not b then m1 Exiting proof mode. Goal if_push : if b then m0 else m1 = if b then (if b then m0) else if not b then m1 [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: b:bool,m0,m1:message —————————————- if b then m0 else m1 = if b then (if b then m0) else if not b then m1 [goal> lemma if_push is proved lemma if_push {‘P:system} @system:(set:’P; equiv:None) : forall (b:bool,m0,m1:message), if b then m0 else m1 = if b then (if b then m0) else if not b then m1 Exiting proof mode. Goal if_then_not : b = not b’ => if b then (if b’ then x else y) else z = if b then y else z [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b,b’:bool,x,y,z:’a —————————————- b = not b’ => if b then (if b’ then x else y) else z = if b then y else z [goal> lemma if_then_not is proved lemma if_then_not {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b,b’:bool,x,y,z:’a), b = not b’ => if b then (if b’ then x else y) else z = if b then y else z Exiting proof mode. Goal if_else_not : b = not b’ => if b then x else if b’ then y else z = if b then x else y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: b,b’:bool,x,y,z:’a —————————————- b = not b’ => if b then x else if b’ then y else z = if b then x else y [goal> lemma if_else_not is proved lemma if_else_not {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (b,b’:bool,x,y,z:’a), b = not b’ => if b then x else if b’ then y else z = if b then x else y Exiting proof mode. Goal if_app : f (if c then x else y) = if c then f x else f y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: c:bool,f:’a -> ‘b,x,y:’a —————————————- f (if c then x else y) = if c then f x else f y [goal> lemma if_app is proved lemma if_app {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (f:’a -> ‘b,c:bool,x,y:’a), f (if c then x else y) = if c then f x else f y Exiting proof mode. Goal fst_pair : fst <x,y> = x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: x,y:message —————————————- fst <x,y> = x [goal> lemma fst_pair is proved lemma fst_pair {‘P:system} @system:(set:’P; equiv:None) : forall (x,y:message), fst <x,y> = x Exiting proof mode. Goal snd_pair : snd <x,y> = y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: x,y:message —————————————- snd <x,y> = y [goal> lemma snd_pair is proved lemma snd_pair {‘P:system} @system:(set:’P; equiv:None) : forall (x,y:message), snd <x,y> = y Exiting proof mode. Goal iff_def : (x <=> y) = ((x => y) && (y => x)) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: x,y:bool —————————————- (x <=> y) = ((x => y) && (y => x)) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: x,y:bool[const] —————————————- x <=> y => (x => y) && (y => x) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: x,y:bool[const] —————————————- (x => y) && (y => x) => x <=> y [goal> lemma iff_def is proved lemma iff_def {‘P:system} @system:(set:’P; equiv:None) : forall (x,y:bool), (x <=> y) = ((x => y) && (y => x)) Exiting proof mode. Goal iff_refl : (x <=> x) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: x:bool —————————————- (x <=> x) = true [goal> lemma iff_refl is proved lemma iff_refl {‘P:system} @system:(set:’P; equiv:None) : forall (x:bool), (x <=> x) = true Exiting proof mode. Goal iff_sym : (x <=> y) = (y <=> x) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: x,y:bool —————————————- (x <=> y) = (y <=> x) [goal> lemma iff_sym is proved lemma iff_sym {‘P:system} @system:(set:’P; equiv:None) : forall (x,y:bool), (x <=> y) = (y <=> x) Exiting proof mode. Goal true_iff_false : (true <=> false) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) —————————————- (true <=> false) = false [goal> lemma true_iff_false is proved lemma true_iff_false {‘P:system} @system:(set:’P; equiv:None) : (true <=> false) = false Exiting proof mode. Goal false_iff_true : (false <=> true) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) —————————————- (false <=> true) = false [goal> lemma false_iff_true is proved lemma false_iff_true {‘P:system} @system:(set:’P; equiv:None) : (false <=> true) = false Exiting proof mode. Goal contra_iff : (not x <=> y) = (x <=> not y) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: x,y:bool —————————————- (not x <=> y) = (x <=> not y) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: x,y:bool[const] —————————————- (not x <=> y) <=> (x <=> not y) [goal> lemma contra_iff is proved lemma contra_iff {‘P:system} @system:(set:’P; equiv:None) : forall (x,y:bool), (not x <=> y) = (x <=> not y) Exiting proof mode. Goal exists_false1 : (exists (a:’a), false) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a —————————————- (exists (a:’a), false) = false [goal> lemma exists_false1 is proved lemma exists_false1 {‘P:system} @system:(set:’P; equiv:None) [‘a] : (exists (a:’a), false) = false Exiting proof mode. Goal exists_false2 : (exists (a:’a,b:’b), false) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b —————————————- (exists (a:’a,b:’b), false) = false [goal> lemma exists_false2 is proved lemma exists_false2 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : (exists (a:’a,b:’b), false) = false Exiting proof mode. Goal exists_false3 : (exists (a:’a,b:’b,c:’c), false) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b, ‘c —————————————- (exists (a:’a,b:’b,c:’c), false) = false [goal> lemma exists_false3 is proved lemma exists_false3 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c] : (exists (a:’a,b:’b,c:’c), false) = false Exiting proof mode. Goal exists_false4 : (exists (a:’a,b:’b,c:’c,d:’d), false) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b, ‘c, ‘d —————————————- (exists (a:’a,b:’b,c:’c,d:’d), false) = false [goal> lemma exists_false4 is proved lemma exists_false4 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c ‘d] : (exists (a:’a,b:’b,c:’c,d:’d), false) = false Exiting proof mode. Goal exists_false5 : (exists (a:’a,b:’b,c:’c,d:’d,e:’e), false) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b, ‘c, ‘d, ‘e —————————————- (exists (a:’a,b:’b,c:’c,d:’d,e:’e), false) = false [goal> lemma exists_false5 is proved lemma exists_false5 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c ‘d ‘e] : (exists (a:’a,b:’b,c:’c,d:’d,e:’e), false) = false Exiting proof mode. Goal exists_false6 : (exists (a:’a,b:’b,c:’c,d:’d,e:’e,f:’f), false) = false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b, ‘c, ‘d, ‘e, ‘f —————————————- (exists (a:’a,b:’b,c:’c,d:’d,e:’e,f:’f), false) = false [goal> lemma exists_false6 is proved lemma exists_false6 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c ‘d ‘e ‘f] : (exists (a:’a,b:’b,c:’c,d:’d,e:’e,f:’f), false) = false Exiting proof mode. Goal forall_true1 : (forall (a:’a), true) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a —————————————- (forall (a:’a), true) = true [goal> lemma forall_true1 is proved lemma forall_true1 {‘P:system} @system:(set:’P; equiv:None) [‘a] : (forall (a:’a), true) = true Exiting proof mode. Goal forall_true2 : (forall (a:’a,b:’b), true) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b —————————————- (forall (a:’a,b:’b), true) = true [goal> lemma forall_true2 is proved lemma forall_true2 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : (forall (a:’a,b:’b), true) = true Exiting proof mode. Goal forall_true3 : (forall (a:’a,b:’b,c:’c), true) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b, ‘c —————————————- (forall (a:’a,b:’b,c:’c), true) = true [goal> lemma forall_true3 is proved lemma forall_true3 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c] : (forall (a:’a,b:’b,c:’c), true) = true Exiting proof mode. Goal forall_true4 : (forall (a:’a,b:’b,c:’c,d:’d), true) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b, ‘c, ‘d —————————————- (forall (a:’a,b:’b,c:’c,d:’d), true) = true [goal> lemma forall_true4 is proved lemma forall_true4 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c ‘d] : (forall (a:’a,b:’b,c:’c,d:’d), true) = true Exiting proof mode. Goal forall_true5 : (forall (a:’a,b:’b,c:’c,d:’d,e:’e), true) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b, ‘c, ‘d, ‘e —————————————- (forall (a:’a,b:’b,c:’c,d:’d,e:’e), true) = true [goal> lemma forall_true5 is proved lemma forall_true5 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c ‘d ‘e] : (forall (a:’a,b:’b,c:’c,d:’d,e:’e), true) = true Exiting proof mode. Goal forall_true6 : (forall (a:’a,b:’b,c:’c,d:’d,e:’e,f:’f), true) = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b, ‘c, ‘d, ‘e, ‘f —————————————- (forall (a:’a,b:’b,c:’c,d:’d,e:’e,f:’f), true) = true [goal> lemma forall_true6 is proved lemma forall_true6 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c ‘d ‘e ‘f] : (forall (a:’a,b:’b,c:’c,d:’d,e:’e,f:’f), true) = true Exiting proof mode. axiom len_zeroes {‘P:system} @system:(set:’P; equiv:None) : forall (x:message), len (zeroes x) = len x axiom tuple2_surj {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (x:’a * ‘b), x = (x#1, x#2) axiom tuple3_surj {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c] : forall (x:’a * ‘b * ‘c), x = (x#1, x#2, x#3) axiom tuple4_surj {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c ‘d] : forall (x:’a * ‘b * ‘c * ‘d), x = (x#1, x#2, x#3, x#4) axiom tuple5_surj {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b ‘c ‘d ‘e] : forall (x:’a * ‘b * ‘c * ‘d * ‘e), x = (x#1, x#2, x#3, x#4, x#5) Goal f_apply : x = y => f x = f y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: f:’a -> ‘b,x,y:’a —————————————- x = y => f x = f y [goal> lemma f_apply is proved lemma f_apply {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (f:’a -> ‘b,x,y:’a), x = y => f x = f y Exiting proof mode. Goal not_exists_1 : not exists (a:’a), phi a = forall (a:’a), not (phi a) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool —————————————- not exists (a:’a), phi a = forall (a:’a), not (phi a) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool —————————————- not exists (a:’a), phi a <=> forall (a:’a), not (phi a) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool —————————————- not exists (a:’a), phi a => forall (a:’a), not (phi a) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: a:’a,phi:’a -> bool H: not exists (a:’a), phi a Hp: phi a —————————————- false [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: a:’a,phi:’a -> bool H: not exists (a:’a), phi a Hp: phi a —————————————- exists (a:’a), phi a [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool —————————————- (forall (a:’a), not (phi a)) => not exists (a:’a), phi a [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: a:’a,phi:’a -> bool H: forall (a:’a), not (phi a) Hp: phi a —————————————- false [goal> lemma not_exists_1 is proved lemma not_exists_1 {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (phi:’a -> bool), not exists (a:’a), phi a = forall (a:’a), not (phi a) Exiting proof mode. Goal not_exists_2 : not exists (a:’a,b:’b), phi a b = forall (a:’a,b:’b), not (phi a b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool —————————————- not exists (a:’a,b:’b), phi a b = forall (a:’a,b:’b), not (phi a b) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool —————————————- not exists (a:’a,b:’b), phi a b <=> forall (a:’a,b:’b), not (phi a b) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool —————————————- not exists (a:’a,b:’b), phi a b => forall (a:’a,b:’b), not (phi a b) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: a:’a,b:’b,phi:’a -> ‘b -> bool H: not exists (a:’a,b:’b), phi a b Hp: phi a b —————————————- false [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: a:’a,b:’b,phi:’a -> ‘b -> bool H: not exists (a:’a,b:’b), phi a b Hp: phi a b —————————————- exists (a:’a,b:’b), phi a b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool —————————————- (forall (a:’a,b:’b), not (phi a b)) => not exists (a:’a,b:’b), phi a b [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: a:’a,b:’b,phi:’a -> ‘b -> bool H: forall (a:’a,b:’b), not (phi a b) Hp: phi a b —————————————- false [goal> lemma not_exists_2 is proved lemma not_exists_2 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (phi:’a -> ‘b -> bool), not exists (a:’a,b:’b), phi a b = forall (a:’a,b:’b), not (phi a b) Exiting proof mode. axiom not_forall_1 {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (phi:’a -> bool), not forall (a:’a), phi a = exists (a:’a), not (phi a) axiom not_forall_2 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (phi:’a -> ‘b -> bool), not forall (a:’a,b:’b), phi a b = exists (a:’a,b:’b), not (phi a b) axiom try_carac_1 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (phi:’a -> bool,f:’a -> ‘b,g:’b), try find x:’a such that phi x in f x else g = if (exists (x:’a), phi x) then f (choose phi) else g axiom try_carac_2 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘aa ‘b] : forall (phi:’a -> ‘aa -> bool,f:’a -> ‘aa -> ‘b,g:’b), try find x:’a,y:’aa such that phi x y in f x y else g = if (exists (xy:’a * ‘aa), phi (xy#1) (xy#2)) then f (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#1) (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#2) else g axiom try_carac_3 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘aa ‘aaa ‘b] : forall (phi:’a -> ‘aa -> ‘aaa -> bool,f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b), try find x:’a,y:’aa,z:’aaa such that phi x y z in f x y z else g = if (exists (xyz:’a * ‘aa * ‘aaa), phi (xyz#1) (xyz#2) (xyz#3)) then f (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#1) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#2) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#3) else g Goal choose_spec : phi x => phi (choose phi) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a —————————————- phi x => phi (choose phi) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a H: phi x —————————————- phi (choose phi) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a H: phi x —————————————- phi (choose phi) = if (exists (x:’a), phi x) then phi (choose phi) else false [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a H: phi x —————————————- phi (choose phi) = if (exists (x:’a), phi x) then phi (choose phi) else false [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a H: phi x —————————————- exists (x:’a), phi x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a H: phi x —————————————- if (exists (x:’a), phi x) then phi (choose phi) else false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a H: phi x —————————————- if (exists (x:’a), phi x) then phi (choose phi) else false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a H: phi x —————————————- try find x:’a such that phi x in phi x else false [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a H: phi x —————————————- (exists (x:’a), phi x && try find x:’a such that phi x in phi x else false = phi x) => try find x:’a such that phi x in phi x else false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:’a -> bool,x:’a H: phi x —————————————- (forall (x:’a), not (phi x)) && try find x:’a such that phi x in phi x else false = false => try find x:’a such that phi x in phi x else false [goal> lemma choose_spec is proved lemma choose_spec {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (phi:’a -> bool,x:’a), phi x => phi (choose phi) Exiting proof mode. Goal try_true_1 : forall (phi:’a -> bool,f:’a -> ‘b,g:’b), (exists (x:’a), phi x) => try find x:’a such that phi x in f x else g = f (choose phi) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b —————————————- forall (phi:’a -> bool,f:’a -> ‘b,g:’b), (exists (x:’a), phi x) => try find x:’a such that phi x in f x else g = f (choose phi) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: f:’a -> ‘b,g:’b,phi:’a -> bool H: exists (x:’a), phi x —————————————- try find x:’a such that phi x in f x else g = f (choose phi) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: f:’a -> ‘b,g:’b,phi:’a -> bool H: exists (x:’a), phi x —————————————- if (exists (x:’a), phi x) then f (choose phi) else g = f (choose phi) [goal> lemma try_true_1 is proved lemma try_true_1 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (phi:’a -> bool,f:’a -> ‘b,g:’b), (exists (x:’a), phi x) => try find x:’a such that phi x in f x else g = f (choose phi) Exiting proof mode. Goal try_true_2 : forall (phi:’a -> ‘aa -> bool,f:’a -> ‘aa -> ‘b,g:’b), (exists (x:’a,y:’aa), phi x y) => try find x:’a,y:’aa such that phi x y in f x y else g = f (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#1) (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#2) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b —————————————- forall (phi:’a -> ‘aa -> bool,f:’a -> ‘aa -> ‘b,g:’b), (exists (x:’a,y:’aa), phi x y) => try find x:’a,y:’aa such that phi x y in f x y else g = f (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#1) (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#2) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b Variables: f:’a -> ‘aa -> ‘b,g:’b,phi:’a -> ‘aa -> bool,x:’a,y:’aa H: phi x y —————————————- try find x:’a,y:’aa such that phi x y in f x y else g = f (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#1) (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#2) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b Variables: f:’a -> ‘aa -> ‘b,g:’b,phi:’a -> ‘aa -> bool,x:’a,y:’aa H: phi x y —————————————- if (exists (xy:’a * ‘aa), phi (xy#1) (xy#2)) then f (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#1) (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#2) else g = f (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#1) (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#2) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b Variables: f:’a -> ‘aa -> ‘b,g:’b,phi:’a -> ‘aa -> bool,x:’a,y:’aa H: phi x y —————————————- exists (xy:’a * ‘aa), phi (xy#1) (xy#2) [goal> lemma try_true_2 is proved lemma try_true_2 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘aa ‘b] : forall (phi:’a -> ‘aa -> bool,f:’a -> ‘aa -> ‘b,g:’b), (exists (x:’a,y:’aa), phi x y) => try find x:’a,y:’aa such that phi x y in f x y else g = f (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#1) (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#2) Exiting proof mode. Goal try_true_3 : forall (phi:’a -> ‘aa -> ‘aaa -> bool,f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b), (exists (x:’a,y:’aa,z:’aaa), phi x y z) => try find x:’a,y:’aa,z:’aaa such that phi x y z in f x y z else g = f (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#1) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#2) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#3) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b —————————————- forall (phi:’a -> ‘aa -> ‘aaa -> bool,f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b), (exists (x:’a,y:’aa,z:’aaa), phi x y z) => try find x:’a,y:’aa,z:’aaa such that phi x y z in f x y z else g = f (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#1) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#2) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#3) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b Variables: f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b,phi:’a -> ‘aa -> ‘aaa -> bool,x:’a,y:’aa, z:’aaa H: phi x y z —————————————- try find x:’a,y:’aa,z:’aaa such that phi x y z in f x y z else g = f (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#1) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#2) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#3) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b Variables: f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b,phi:’a -> ‘aa -> ‘aaa -> bool,x:’a,y:’aa, z:’aaa H: phi x y z —————————————- if (exists (xyz:’a * ‘aa * ‘aaa), phi (xyz#1) (xyz#2) (xyz#3)) then f (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#1) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#2) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#3) else g = f (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#1) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#2) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#3) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b Variables: f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b,phi:’a -> ‘aa -> ‘aaa -> bool,x:’a,y:’aa, z:’aaa H: phi x y z —————————————- exists (xyz:’a * ‘aa * ‘aaa), phi (xyz#1) (xyz#2) (xyz#3) [goal> lemma try_true_3 is proved lemma try_true_3 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘aa ‘aaa ‘b] : forall (phi:’a -> ‘aa -> ‘aaa -> bool,f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b), (exists (x:’a,y:’aa,z:’aaa), phi x y z) => try find x:’a,y:’aa,z:’aaa such that phi x y z in f x y z else g = f (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#1) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#2) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#3) Exiting proof mode. Goal try_false_1 : forall (phi:’a -> bool,f:’a -> ‘b,g:’b), (forall (x:’a), phi x => false) => try find x:’a such that phi x in f x else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b —————————————- forall (phi:’a -> bool,f:’a -> ‘b,g:’b), (forall (x:’a), phi x => false) => try find x:’a such that phi x in f x else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: f:’a -> ‘b,g:’b,phi:’a -> bool H: forall (x:’a), phi x => false —————————————- try find x:’a such that phi x in f x else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: f:’a -> ‘b,g:’b,phi:’a -> bool H: forall (x:’a), phi x => false —————————————- if (exists (x:’a), phi x) then f (choose phi) else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: f:’a -> ‘b,g:’b,phi:’a -> bool H: forall (x:’a), phi x => false —————————————- not exists (x:’a), phi x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: f:’a -> ‘b,g:’b,phi:’a -> bool H: forall (x:’a), phi x => false —————————————- forall (a:’a), not (phi a) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: f:’a -> ‘b,g:’b,phi:’a -> bool,x:’a H: forall (x:’a), phi x => false H’: phi x —————————————- false [goal> lemma try_false_1 is proved lemma try_false_1 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (phi:’a -> bool,f:’a -> ‘b,g:’b), (forall (x:’a), phi x => false) => try find x:’a such that phi x in f x else g = g Exiting proof mode. Goal try_false_2 : forall (phi:’a -> ‘aa -> bool,f:’a -> ‘aa -> ‘b,g:’b), (forall (x:’a,y:’aa), phi x y => false) => try find x:’a,y:’aa such that phi x y in f x y else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b —————————————- forall (phi:’a -> ‘aa -> bool,f:’a -> ‘aa -> ‘b,g:’b), (forall (x:’a,y:’aa), phi x y => false) => try find x:’a,y:’aa such that phi x y in f x y else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b Variables: f:’a -> ‘aa -> ‘b,g:’b,phi:’a -> ‘aa -> bool H: forall (x:’a,y:’aa), phi x y => false —————————————- try find x:’a,y:’aa such that phi x y in f x y else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b Variables: f:’a -> ‘aa -> ‘b,g:’b,phi:’a -> ‘aa -> bool H: forall (x:’a,y:’aa), phi x y => false —————————————- if (exists (xy:’a * ‘aa), phi (xy#1) (xy#2)) then f (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#1) (choose (fun (xy:’a * ‘aa) => phi (xy#1) (xy#2))#2) else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b Variables: f:’a -> ‘aa -> ‘b,g:’b,phi:’a -> ‘aa -> bool H: forall (x:’a,y:’aa), phi x y => false —————————————- not exists (xy:’a * ‘aa), phi (xy#1) (xy#2) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b Variables: f:’a -> ‘aa -> ‘b,g:’b,phi:’a -> ‘aa -> bool H: forall (x:’a,y:’aa), phi x y => false —————————————- forall (a:’a * ‘aa), not ((fun (y:’a * ‘aa) => phi (y#1) (y#2)) a) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘b Variables: f:’a -> ‘aa -> ‘b,g:’b,phi:’a -> ‘aa -> bool,xy:’a * ‘aa H: forall (x:’a,y:’aa), phi x y => false H’: (fun (y:’a * ‘aa) => phi (y#1) (y#2)) xy —————————————- false [goal> lemma try_false_2 is proved lemma try_false_2 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘aa ‘b] : forall (phi:’a -> ‘aa -> bool,f:’a -> ‘aa -> ‘b,g:’b), (forall (x:’a,y:’aa), phi x y => false) => try find x:’a,y:’aa such that phi x y in f x y else g = g Exiting proof mode. Goal try_false_3 : forall (phi:’a -> ‘aa -> ‘aaa -> bool,f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b), (forall (x:’a,y:’aa,z:’aaa), phi x y z => false) => try find x:’a,y:’aa,z:’aaa such that phi x y z in f x y z else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b —————————————- forall (phi:’a -> ‘aa -> ‘aaa -> bool,f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b), (forall (x:’a,y:’aa,z:’aaa), phi x y z => false) => try find x:’a,y:’aa,z:’aaa such that phi x y z in f x y z else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b Variables: f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b,phi:’a -> ‘aa -> ‘aaa -> bool H: forall (x:’a,y:’aa,z:’aaa), phi x y z => false —————————————- try find x:’a,y:’aa,z:’aaa such that phi x y z in f x y z else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b Variables: f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b,phi:’a -> ‘aa -> ‘aaa -> bool H: forall (x:’a,y:’aa,z:’aaa), phi x y z => false —————————————- if (exists (xyz:’a * ‘aa * ‘aaa), phi (xyz#1) (xyz#2) (xyz#3)) then f (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#1) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#2) (choose (fun (xyz:’a * ‘aa * ‘aaa) => phi (xyz#1) (xyz#2) (xyz#3))#3) else g = g [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b Variables: f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b,phi:’a -> ‘aa -> ‘aaa -> bool H: forall (x:’a,y:’aa,z:’aaa), phi x y z => false —————————————- not exists (xyz:’a * ‘aa * ‘aaa), phi (xyz#1) (xyz#2) (xyz#3) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b Variables: f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b,phi:’a -> ‘aa -> ‘aaa -> bool H: forall (x:’a,y:’aa,z:’aaa), phi x y z => false —————————————- forall (a:’a * ‘aa * ‘aaa), not ((fun (y:’a * ‘aa * ‘aaa) => phi (y#1) (y#2) (y#3)) a) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘aa, ‘aaa, ‘b Variables: f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b,phi:’a -> ‘aa -> ‘aaa -> bool, xyz:’a * ‘aa * ‘aaa H: forall (x:’a,y:’aa,z:’aaa), phi x y z => false H’: (fun (y:’a * ‘aa * ‘aaa) => phi (y#1) (y#2) (y#3)) xyz —————————————- false [goal> lemma try_false_3 is proved lemma try_false_3 {‘P:system} @system:(set:’P; equiv:None) [‘a ‘aa ‘aaa ‘b] : forall (phi:’a -> ‘aa -> ‘aaa -> bool,f:’a -> ‘aa -> ‘aaa -> ‘b,g:’b), (forall (x:’a,y:’aa,z:’aaa), phi x y z => false) => try find x:’a,y:’aa,z:’aaa such that phi x y z in f x y z else g = g Exiting proof mode. Goal forall_exists : (forall (x:’a), exists (y:’b), phi x y) = exists (y’:’a -> ‘b), forall (x:’a), phi x (y’ x) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool —————————————- (forall (x:’a), exists (y:’b), phi x y) = exists (y’:’a -> ‘b), forall (x:’a), phi x (y’ x) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool —————————————- (forall (x:’a), exists (y:’b), phi x y) => exists (y’:’a -> ‘b), forall (x:’a), phi x (y’ x) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool H: forall (x:’a), exists (y:’b), phi x y —————————————- exists (y’:’a -> ‘b), forall (x:’a), phi x (y’ x) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool H: forall (x:’a), exists (y:’b), phi x y —————————————- forall (x:’a), phi x ((fun (x:’a) => choose (fun (y:’b) => phi x y)) x) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool,x:’a H: forall (x:’a), exists (y:’b), phi x y —————————————- phi x (choose (fun (y:’b) => phi x y)) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool,x:’a,y:’b H: forall (x:’a), exists (y:’b), phi x y Hy: phi x y —————————————- phi x (choose (fun (y:’b) => phi x y)) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool,x:’a,y:’b H: forall (x:’a), exists (y:’b), phi x y Hy: phi x y —————————————- (fun (y:’b) => phi x y) (choose (fun (y:’b) => phi x y)) [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool,x:’a,y:’b H: forall (x:’a), exists (y:’b), phi x y Hy: phi x y —————————————- (fun (y:’b) => phi x y) y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool —————————————- (exists (y’:’a -> ‘b), forall (x:’a), phi x (y’ x)) => forall (x:’a), exists (y:’b), phi x y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool,x:’a,y’:’a -> ‘b H: forall (x:’a), phi x (y’ x) —————————————- exists (y:’b), phi x y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a, ‘b Variables: phi:’a -> ‘b -> bool,x:’a,y’:’a -> ‘b H: forall (x:’a), phi x (y’ x) —————————————- phi x (y’ x) [goal> lemma forall_exists is proved lemma forall_exists {‘P:system} @system:(set:’P; equiv:None) [‘a ‘b] : forall (phi:’a -> ‘b -> bool), (forall (x:’a), exists (y:’b), phi x y) = exists (y’:’a -> ‘b), forall (x:’a), phi x (y’ x) Exiting proof mode. Goal implies_exists : (phi => exists (j:’a), psi j) = exists (x:’a), phi => psi x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool,psi:’a -> bool —————————————- (phi => exists (j:’a), psi j) = exists (x:’a), phi => psi x [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool[const],psi:’a -> bool —————————————- (phi => exists (j:’a), psi j) => exists (x:’a), phi => psi x [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool[const],psi:’a -> bool H: phi => exists (j:’a), psi j —————————————- exists (x:’a), phi => psi x [goal> Focused goal (1/3): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool[const],psi:’a -> bool H: phi => exists (j:’a), psi j —————————————- phi => exists (x:’a), true => psi x [goal> Focused goal (1/3): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool[const],psi:’a -> bool H: phi => exists (j:’a), psi j phi: phi —————————————- exists (x:’a), true => psi x [goal> Focused goal (1/3): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool[const],psi:’a -> bool,x:’a H: phi => exists (j:’a), psi j _: psi x phi: phi —————————————- exists (x:’a), true => psi x [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool[const],psi:’a -> bool H: phi => exists (j:’a), psi j —————————————- not phi => exists (x:’a), false => psi x [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool[const],psi:’a -> bool H: phi => exists (j:’a), psi j _: not phi —————————————- exists (x:’a), false => psi x [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool[const],psi:’a -> bool —————————————- (exists (x:’a), phi => psi x) => phi => exists (j:’a), psi j [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: phi:bool[const],psi:’a -> bool,x:’a H: phi => psi x H’: phi —————————————- exists (j:’a), psi j [goal> lemma implies_exists is proved lemma implies_exists {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (phi:bool,psi:’a -> bool), (phi => exists (j:’a), psi j) = exists (x:’a), phi => psi x Exiting proof mode. op well_founded [‘a] (ord:’a -> ‘a -> bool) : bool = forall (S:’a -> bool), (exists (x:’a), S x) => exists (min:’a), S min && forall (x:’a), S x => not (ord x min) axiom lt_wf {‘P:system} @system:(set:’P; equiv:None) [‘a] : well_founded (fun (x,y:’a) => x < y) axiom le_trans {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y,z:’a), x <= y => y <= z => x <= z axiom lt_trans {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y,z:’a), x < y => y < z => x < z axiom lt_le_trans {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y,z:’a), x < y => y <= z => x < z axiom le_lt_trans {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y,z:’a), x <= y => y < z => x < z axiom lt_charac {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), x < y <=> x <> y && x <= y axiom le_not_lt_impl_eq {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), x <= y => not (x < y) => x = y Goal lt_impl_le : x < y => x <= y [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x,y:’a —————————————- x < y => x <= y [goal> lemma lt_impl_le is proved lemma lt_impl_le {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), x < y => x <= y Exiting proof mode. Goal not_lt_refl : not (x < x) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x:’a —————————————- not (x < x) [goal> lemma not_lt_refl is proved lemma not_lt_refl {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x:’a), not (x < x) Exiting proof mode. Goal lt_irrefl : x < x <=> false [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Type variables: ‘a Variables: x:’a —————————————- x < x <=> false [goal> lemma lt_irrefl is proved lemma lt_irrefl {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x:’a), x < x <=> false Exiting proof mode. axiom le_impl_eq_lt {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,y:’a), x <= y => x = y || x < y axiom le_refl_index {‘P:system} @system:(set:’P; equiv:None) : forall (x:index), x <= x Goal le_refl_index_eq : x <= x = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: x:index —————————————- x <= x = true [goal> lemma le_refl_index_eq is proved lemma le_refl_index_eq {‘P:system} @system:(set:’P; equiv:None) : forall (x:index), x <= x = true Exiting proof mode. Goal le_pred_lt : t <= pred t’ = t < t’ [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: t,t’:timestamp —————————————- t <= pred t’ = t < t’ [goal> lemma le_pred_lt is proved lemma le_pred_lt {‘P:system} @system:(set:’P; equiv:None) : forall (t,t’:timestamp), t <= pred t’ = t < t’ Exiting proof mode. Goal neq_le_pred_le : t <> t’ => t <= t’ = t <= pred t’ [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: t,t’:timestamp —————————————- t <> t’ => t <= t’ = t <= pred t’ [goal> lemma neq_le_pred_le is proved lemma neq_le_pred_le {‘P:system} @system:(set:’P; equiv:None) : forall (t,t’:timestamp), t <> t’ => t <= t’ = t <= pred t’ Exiting proof mode. axiom le_lt {‘P:system} @system:(set:’P; equiv:None) [‘a] : forall (x,x’:’a), x <> x’ => x <= x’ = x < x’ [warning>Loaded “Logic.sp”. <]op singleton (m:message) : mset = add m empty_set op union (s1,s2:mset) : mset = fold (fun (t:message,s:mset) => add t s) s1 s2 op subseteq (s1,s2:mset) : bool = fold (fun (t:message,b:bool) => b && mem t s2) true s1 axiom empty_set_is_empty {‘P:system} @system:(set:’P; equiv:None) : forall (x:message), not (mem x empty_set) [warning>Loaded “Set.sp”. <]new predicate: predicate (|>) {set:system} [‘a ‘b] {set: u:’a,m:’b} = Exists (f:’a -> ‘b[adv, glob]), [f u = m] new predicate: predicate (|1>) {set:system} [‘a ‘b ‘c] {set: u:’a -> ‘b,m:’a -> ‘c} = Exists (f:’b -> ‘c[adv, glob]), [forall (x:’a), f (u x) = m x] [warning>Loaded “DeductionSyntax.sp”. <]Goal unnamed1 : forall u:’b[glob],v:’a -> ‘c[glob], Let u0 = fun (_x:’a) => u in $(u0 |1>{Empty} fun (x:’a) => v x) -> $(u |>{Empty} fun (x:’a) => v x) [goal> Focused goal (1/1): Systems: Empty Type variables: ‘a, ‘b, ‘c Variables: u:’b[glob],v:’a -> ‘c[glob] —————————————- Let u0 = fun (_x:’a) => u in $(u0 |1> fun (x:’a) => v x) -> $(u |> fun (x:’a) => v x) [goal> Focused goal (1/1): Systems: Empty Type variables: ‘a, ‘b, ‘c Variables: u:’b[glob],v:’a -> ‘c[glob] H: $(u0 |1> fun (x:’a) => v x) u0 := fun (_x:’a) => u —————————————- $(u |> fun (x:’a) => v x) [goal> Focused goal (1/1): Systems: Empty Type variables: ‘a, ‘b, ‘c Variables: u:’b[glob],v:’a -> ‘c[glob] H: $(u0 |1> fun (x:’a) => v x) u0 := fun (_x:’a) => u —————————————- Exists (f:’b -> ‘a -> ‘c[adv, glob]), [f u = (fun (x:’a) => v x)] [goal> Focused goal (1/1): Systems: Empty Type variables: ‘a, ‘b, ‘c Variables: u:’b[glob],v:’a -> ‘c[glob] H: Exists (f:’b -> ‘c[adv, glob]), [forall (x:’a), f (u0 x) = (fun (x:’a) => v x) x] u0 := fun (_x:’a) => u —————————————- Exists (f:’b -> ‘a -> ‘c[adv, glob]), [f u = (fun (x:’a) => v x)] [goal> Focused goal (1/1): Systems: Empty Type variables: ‘a, ‘b, ‘c Variables: f:’b -> ‘c[adv, glob],u:’b[glob],v:’a -> ‘c[glob] H: [forall (x:’a), f (u0 x) = (fun (x:’a) => v x) x] u0 := fun (_x:’a) => u —————————————- Exists (f:’b -> ‘a -> ‘c[adv, glob]), [f u = (fun (x:’a) => v x)] [goal> Focused goal (1/1): System: Empty Type variables: ‘a, ‘b, ‘c Variables: f:’b -> ‘c[adv, glob],u:’b[glob],v:’a -> ‘c[glob] H: [forall (x:’a), f (u0 x) = v x] u0 := fun (_x:’a) => u —————————————- (fun (x:’a) => f u) = (fun (x:’a) => v x) [goal> Focused goal (1/1): System: Empty Type variables: ‘a, ‘b, ‘c Variables: f:’b -> ‘c[adv, glob],u:’b[glob],v:’a -> ‘c[glob],x:’a H: [forall (x:’a), f (u0 x) = v x] u0 := fun (_x:’a) => u —————————————- f u = v x [goal> Focused goal (1/1): System: Empty Type variables: ‘a, ‘b, ‘c Variables: f:’b -> ‘c[adv, glob],u:’b[glob],v:’a -> ‘c[glob],x:’a H: [forall (x:’a), f u = v x] u0 := fun (_x:’a) => u —————————————- f u = v x [goal> lemma unnamed1 is proved global lemma unnamed1 @system:Empty [‘a ‘b ‘c] : Forall (u:’b[glob],v:’a -> ‘c[glob]), Let u0 = fun (_x:’a) => u in $(u0 |1>{Empty} fun (x:’a) => v x) -> $(u |>{Empty} fun (x:’a) => v x) Exiting proof mode. global axiom frame_from_frame {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => frame@t |1>{P} fun (t,t’:timestamp) => if (t’ <= t) then frame@t’) New deduction hint frame_from_frame : ∀{P:system} , @system:(P), ∀ x ⊢ frame@x ▷ λ t’ ⇒ (frame@t’ | t’ <= x) global axiom exec_from_frame {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => frame@t |1>{P} fun (t,t’:timestamp) => if (t’ <= t) then exec@t’ else witness) New deduction hint exec_from_frame : ∀{P:system} , @system:(P), ∀ x ⊢ frame@x ▷ λ t’ ⇒ (exec@t’ | t’ <= x) global axiom output_from_frame {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => frame@t |1>{P} fun (t,t’:timestamp) => if (t’ <= t && exec@t’) then output@t’) New deduction hint output_from_frame : ∀{P:system} , @system:(P), ∀ x ⊢ frame@x ▷ λ t’ ⇒ (output@t’ | t’ <= x && exec@t’) global axiom input_from_frame {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => frame@t |1>{P} fun (t,t’:timestamp) => if (pred t’ <= t) then input@t’) New deduction hint input_from_frame : ∀{P:system} , @system:(P), ∀ x ⊢ frame@x ▷ λ t’ ⇒ (input@t’ | pred t’ <= x) global axiom exec_from_frame {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => frame@t |1>{P} fun (t,t’:timestamp) => if (t’ <= t) then exec@t’ else witness) New deduction hint exec_from_frame : ∀{P:system} , @system:(P), ∀ x ⊢ frame@x ▷ λ t’ ⇒ (exec@t’ | t’ <= x) global axiom output_from_frame {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => frame@t |1>{P} fun (t,t’:timestamp) => if (t’ <= t && exec@t’) then output@t’) New deduction hint output_from_frame : ∀{P:system} , @system:(P), ∀ x ⊢ frame@x ▷ λ t’ ⇒ (output@t’ | t’ <= x && exec@t’) global axiom input_from_frame {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => frame@t |1>{P} fun (t,t’:timestamp) => if (pred t’ <= t) then input@t’) New deduction hint input_from_frame : ∀{P:system} , @system:(P), ∀ x ⊢ frame@x ▷ λ t’ ⇒ (input@t’ | pred t’ <= x) global axiom transcript_from_frame {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => frame@t |1>{P} fun (t,t’:timestamp) => if (t’ <= t) then transcript@t’) New deduction hint transcript_from_frame : ∀{P:system} , @system:(P), ∀ x ⊢ frame@x ▷ λ t’ ⇒ (transcript@t’ | t’ <= x) global axiom transcript_from_transcript {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => transcript@t |1>{P} fun (t,t’:timestamp) => if (t’ <= t) then transcript@t’) New deduction hint transcript_from_transcript : ∀{P:system} , @system:(P), ∀ x ⊢ transcript@x ▷ λ t’ ⇒ ( transcript@t’ | t’ <= x) global axiom exec_from_transcript {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => transcript@t |1>{P} fun (t,t’:timestamp) => if (t’ <= t) then exec@t’ else witness) New deduction hint exec_from_transcript : ∀{P:system} , @system:(P), ∀ x ⊢ transcript@x ▷ λ t’ ⇒ ( exec@t’ | t’ <= x) global axiom output_from_transcript {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => transcript@t |1>{P} fun (t,t’:timestamp) => if (t’ <= t && exec@t’) then output@t’) New deduction hint output_from_transcript : ∀{P:system} , @system:(P), ∀ x ⊢ transcript@x ▷ λ t’ ⇒ ( output@t’ | t’ <= x && exec@t’) global axiom input_from_transcript {P:system} @system:(set:P; equiv:None) : $(fun (t:timestamp) => transcript@t |1>{P} fun (t,t’:timestamp) => if (pred t’ <= t) then input@t’) New deduction hint input_from_transcript : ∀{P:system} , @system:(P), ∀ x ⊢ transcript@x ▷ λ t’ ⇒ ( input@t’ | pred t’ <= x) [warning>Loaded “Deduction.sp”. <]Goal exec_not_init : init < tau => exec@tau = (exec@pred tau && cond@tau) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp —————————————- init < tau => exec@tau = (exec@pred tau && cond@tau) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp[const] Ord: init < tau —————————————- exec@tau = (exec@pred tau && cond@tau) [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp[const] Ord: init < tau —————————————- if not happens(tau) then false else if (tau = init) then true else if (tau <> init && happens(tau)) then (exec@pred tau && cond@tau) else witness = (exec@pred tau && cond@tau) [goal> lemma exec_not_init is proved lemma exec_not_init {‘P:system} @system:(set:’P; equiv:None) : forall (tau:timestamp), init < tau => exec@tau = (exec@pred tau && cond@tau) Exiting proof mode. Goal exec_init : tau = init => exec@tau = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp —————————————- tau = init => exec@tau = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp[const] Eq: tau = init —————————————- exec@tau = true [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp[const] Eq: tau = init —————————————- if not happens(init) then false else true = true [goal> lemma exec_init is proved lemma exec_init {‘P:system} @system:(set:’P; equiv:None) : forall (tau:timestamp), tau = init => exec@tau = true Exiting proof mode. axiom cond_init {‘P:system} @system:(set:’P; equiv:None) : forall (tau:timestamp), tau = init => cond@tau = true Goal exec_le : tau’ <= tau => exec@tau => exec@tau’ [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau,tau’:timestamp —————————————- tau’ <= tau => exec@tau => exec@tau’ [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau,tau’:timestamp[const] Hexec: exec@tau Hle: tau’ <= tau IH: forall (tau0:timestamp), tau0 < tau => tau’ <= tau0 => exec@tau0 => exec@tau’ —————————————- exec@tau’ [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: tau,tau’:timestamp[const] Hexec: exec@tau Hle: tau’ <= tau IH: forall (tau0:timestamp), tau0 < tau => tau’ <= tau0 => exec@tau0 => exec@tau’ —————————————- tau = tau’ => exec@tau’ [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau,tau’:timestamp[const] Hexec: exec@tau Hle: tau’ <= tau IH: forall (tau0:timestamp), tau0 < tau => tau’ <= tau0 => exec@tau0 => exec@tau’ —————————————- not (tau = tau’) => exec@tau’ [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau,tau’:timestamp[const] Hexec: exec@tau Hle: tau’ <= tau Hneq: not (tau = tau’) IH: forall (tau0:timestamp), tau0 < tau => tau’ <= tau0 => exec@tau0 => exec@tau’ —————————————- exec@tau’ [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau,tau’:timestamp[const] Hexec: exec@pred tau && cond@tau Hle: tau’ <= tau Hneq: not (tau = tau’) IH: forall (tau0:timestamp), tau0 < tau => tau’ <= tau0 => exec@tau0 => exec@tau’ —————————————- exec@tau’ [goal> lemma exec_le is proved lemma exec_le {‘P:system} @system:(set:’P; equiv:None) : forall (tau,tau’:timestamp), tau’ <= tau => exec@tau => exec@tau’ Exiting proof mode. Goal exec_cond : happens(tau) => exec@tau => cond@tau [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp —————————————- happens(tau) => exec@tau => cond@tau [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp[const] Hap: happens(tau) Hexec: exec@tau —————————————- cond@tau [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp[const] Hap: happens(tau) Hexec: exec@tau _: init < tau —————————————- cond@tau [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp[const] Hap: happens(tau) Hexec: exec@tau _: not (init < tau) —————————————- cond@tau [goal> lemma exec_cond is proved lemma exec_cond {‘P:system} @system:(set:’P; equiv:None) : forall (tau:timestamp), happens(tau) => exec@tau => cond@tau Exiting proof mode. Goal executability : happens(t) => exec@t => forall (t0:timestamp), t0 <= t => exec@t0 [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: t:timestamp —————————————- happens(t) => exec@t => forall (t0:timestamp), t0 <= t => exec@t0 [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) —————————————- forall (t:timestamp), (forall (t0:timestamp), t0 < t => happens(t0) => exec@t0 => forall (t1:timestamp), t1 <= t0 => exec@t1) => happens(t) => exec@t => forall (t0:timestamp), t0 <= t => exec@t0 [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: t,t’:timestamp[const] Hap: happens(t) Hex: exec@t Hle: t’ <= t IH: forall (t0:timestamp), t0 < t => happens(t0) => exec@t0 => forall (t1:timestamp), t1 <= t0 => exec@t1 —————————————- exec@t’ [goal> Focused goal (1/2): System variables: ‘P System: (set:’P; equiv:None) Variables: t,t’:timestamp[const] Hap: happens(t) Hex: exec@t Hle: t’ <= t IH: forall (t0:timestamp), t0 < t => happens(t0) => exec@t0 => forall (t1:timestamp), t1 <= t0 => exec@t1 _: t’ = t —————————————- exec@t’ [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: t,t’:timestamp[const] Hap: happens(t) Hex: exec@t Hle: t’ <= t IH: forall (t0:timestamp), t0 < t => happens(t0) => exec@t0 => forall (t1:timestamp), t1 <= t0 => exec@t1 _: t’ < t —————————————- exec@t’ [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: t,t’:timestamp[const] Hap: happens(t) Hex: exec@t Hle: t’ <= t IH: forall (t0:timestamp), t0 < t => happens(t0) => exec@t0 => forall (t1:timestamp), t1 <= t0 => exec@t1 _: t’ < t —————————————- exec@pred t [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: t,t’:timestamp[const] H: init < t => exec@t = (exec@pred t && cond@t) Hap: happens(t) Hex: exec@t Hle: t’ <= t IH: forall (t0:timestamp), t0 < t => happens(t0) => exec@t0 => forall (t1:timestamp), t1 <= t0 => exec@t1 _: t’ < t —————————————- exec@pred t [goal> lemma executability is proved lemma executability {‘P:system} @system:(set:’P; equiv:None) : forall (t:timestamp), happens(t) => exec@t => forall (t0:timestamp), t0 <= t => exec@t0 Exiting proof mode. Goal frame_not_init : init < tau => frame@tau = <frame@pred tau,<of_bool (exec@tau),if exec@tau then output@tau>> [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp —————————————- init < tau => frame@tau = <frame@pred tau,<of_bool (exec@tau),if exec@tau then output@tau>> [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp[const] Neq: init < tau —————————————- frame@tau = <frame@pred tau,<of_bool (exec@tau),if exec@tau then output@tau>> [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) Variables: tau:timestamp[const] Neq: init < tau —————————————- if not happens(tau) then empty else if (tau = init) then zero else if (tau <> init && happens(tau)) then <frame@pred tau,<of_bool (exec@tau),if exec@tau then output@tau>> else witness = <frame@pred tau,<of_bool (exec@tau),if exec@tau then output@tau>> [goal> lemma frame_not_init is proved lemma frame_not_init {‘P:system} @system:(set:’P; equiv:None) : forall (tau:timestamp), init < tau => frame@tau = <frame@pred tau,<of_bool (exec@tau),if exec@tau then output@tau>> Exiting proof mode. Goal frame_init : frame@init = zero [goal> Focused goal (1/1): System variables: ‘P System: (set:’P; equiv:None) —————————————- frame@init = zero [goal> lemma frame_init is proved lemma frame_init {‘P:system} @system:(set:’P; equiv:None) : frame@init = zero Exiting proof mode. [warning>Loaded “Classic.sp”. <][warning>Loaded “Core.sp”. <]

Messages

Messages computed by a protocol and sent over the network are modelled using terms.

Concretely, a term is built from

• names n used to model random sampling;

• application of functions f(m_1,...,m_k).

This allows effectively modelling any computation, as one can have function symbols modelling any sort of computations, from equality testing to conditional branching or encryption functions.

In Squirrel, a function symbol without any assumption can be defined with:

abstract ok : message abstract ko : message abstract f1 : message -> message abstract f2 : message * message -> message.

When using such function symbols inside a protocol, we are effectively saying that those function symbol may be in practice instantiated by any function of the correct type. And a proof in such a model holds for any possible implementation of those functions. This is notably useful to model a constant ok, without giving any specific concrete value to this constant.

ok and ko are constants, and f1 is a function that expects a message, and returns a message. f2 is then a function symbol of arity two. Function symbols of any arity can be defined similarly.

A name n typically allows to model secret keys or nonces. As we wish to be able to refer to an unbounded number of sessions, we allow names to be indexed, each value of the index yielding a fresh independent random value. An indexed name is denoted by n(i), with variable i as an index. Names can be indexed by any number of indices.

In the tool, one can declare names and indexed names as follows.

name n : message name n1 : index -> message name n2 : index * index -> message.

global axiom namelength_n {‘P:system} @system:(set:’P; equiv:None) : [len n = namelength_message] global axiom namelength_n1 {‘P:system} @system:(set:’P; equiv:None) : [forall (i:index), len (n1 i) = namelength_message] global axiom namelength_n2 {‘P:system} @system:(set:’P; equiv:None) : [forall (i:index * index), len (n2 i) = namelength_message]

Compared to usual game based cryptography, one can think about names as sampling at the beginning of the protocol execution all possible random values that will ever be needed, and store them within indexed cells, which are our names.

To model a setting where multiple people each have their own secret key, one could declare an indexed name as follows.

name kT : index -> message.

global axiom namelength_kT {‘P:system} @system:(set:’P; equiv:None) : [forall (i:index), len (kT i) = namelength_message]

Basic assumption

We can declare axioms over our abstract function symbols, for instance to state that the two abstract constant ok and ko are not equal.

axiom [any] ok_not_ko: ok <> ko.

axiom ok_not_ko {‘P:system} @system:(set:’P; equiv:None) : ok <> ko

A proof made in such a model would then apply to any concrete implementation in which ok and ko are given two distinct concrete values.

Axioms are formulas in a high-order logic, for instance allowing free variables, universal and existential quantification, implications, etc. Here, we define the axiom as true over any protocol.

Another axiom that could be useful to prove the security of a protocol is for instance that ko can never be equal to any pair <x,y>.

axiom [any] ok_not_pair (x,y:message): <x,y> <> ko.

axiom ok_not_pair {‘P:system} @system:(set:’P; equiv:None) : forall (x,y:message), <x,y> <> ko

Going back to the name declaration, if we now display the Squirrel output after a declaration, we see the following:

name skey : index -> message.

global axiom namelength_skey {‘P:system} @system:(set:’P; equiv:None) : [forall (i:index), len (skey i) = namelength_message]

This means that whenever a new name is declared, we also create a dedicated axiom stating that the length of the name (which is a random bitstring) is equal to some constant. In other words, all names have the same length.

Cryptographic assumptions

Function symbols can be defined as being encryption functions, hash functions, signature functions, etc. The tool will then assume that such functions satisfy some classical cryptographic assumptions.

Some possible primitives, and the corresponding assumptions, are:

• symmetric and asymmetric encryption, CCA1 & INT-CTXT (only in the symmetric case)

• signature, EUF-CMA

• hash function, PRF, and thus EUF-CMA, CR

Each is declared in the following way.

signature sign,checksign,pk hash h senc enc,dec aenc asenc,asdec,aspk.

Libraries

Libraries can be included, most Squirrel file typically include (at the begining), the core library, with:

Protocols

Protocols are described in a variant of the pi-calculus as processes. They are defined by the following constructs:

• new n is used to declare a fresh name (this is optional, and equivalent to the style of name declarations described earlier);

• out(c,m) is used to send term m over channel c;

• in(c,x) is used to receive some value from channel c, bound to the variable x;

• act; P correspond to the sequential composition of action act with process P;

• process name(vars) = ... allows to give a name to a process: using name(vars) inside another process then unfold the process definition;

• P | Q is the parallel composition of two processes;

• if phi then P else Q is conditional branching;

• try find vars such that phi in P else Q is a global lookup over indices, it can be seen as a lookup in a database.

As an example, we use a small RFID-based protocol, with a tag and a reader, called the basic hash protocol [BCDH10].

Example: Basic Hash

T –> R : <nT, h(nT,kT)>

R –> T : ok

Here, a tag T sends to the reader R a fresh challenge nT, authenticated via a MAC using the tag’s key kT. Each tag has a distinct kT, and the reader has a database containing all of them.

We first declare the channels used by the protocol. Remark that channels are mostly byproducts of the theory, and do not play a big role.

channel cT channel cR.

We then define the first process for the tags, which may correspond to multiple identities, and thus depends on some index variable i.

process tag(i:index) = new nT; T : out(cT, <nT, h(nT,kT(i))>).

process tag (i:index) = new nT : message; T: out(cT,<nT,h (nT, kT i)>); null

We now declare the process for the reader.

process reader = in(cT,x); try find i such that snd(x) = h(fst(x),kT(i)) in R : out(cR,ok) else R1 : out(cR,ko).

process reader = in(cT,x); find (i) such that snd x = h (fst x, kT i) in R: out(cR,ok); null else R1: out(cR,ko); null

Finally, we declare the complete system. We instantiate multiple copies of the reader process, and for each value i, we also instantiate multiple copies of tag(i) with the replication over k.

system ((!_j reader) | (!_i !_k tag(i))).

[warning>Type-checked process: ( !_j( reader ) ) | !_i( !_k( tag i)) <]global axiom namelength_nT {‘P:system} @system:(set:’P; equiv:None) : [forall (i:index * index), len (nT i) = namelength_message] [warning>Pre-processed system: 0 - parallel/left 1 - !_j 2 - in(cT,x) 3 - try find i such that snd x = h (fst x, kT i) 4 - out(cR,ok) 5 - null 3 - else 6 - out(cR,ko) 7 - null 0 - parallel/right 8 - !_i 9 - !_k 10 - out(cT,<nT (i, k),h (nT (i, k), kT i)>) 11 - null <][warning>System can be used to prove diff-equivalences and diff-inclusions. <][warning>No conflict found. <][warning>Pre-processed system with end of blocks marked: 0 - parallel/left 1 - !_j 2 - in(cT,x) 3 - try find i such that snd x = h (fst x, kT i) * 4 - out(cR,ok) 5 - null 3 - else * 6 - out(cR,ko) 7 - null 0 - parallel/right 8 - !_i 9 - !_k *10 - out(cT,<nT (i, k),h (nT (i, k), kT i)>) 11 - null <]Added action dependencies lemmas: axiom mutex_R1_R {‘P:system[like default]} @system:(set:’P; equiv:None) : forall (j,i:index), not happens(R1(j)) || not happens(R(j, i)) axiom mutex_R_R1 {‘P:system[like default]} @system:(set:’P; equiv:None) : forall (j,i:index), not happens(R(j, i)) || not happens(R1(j)) axiom depends_init_T {‘P:system[like default]} @system:(set:’P; equiv:None) : forall (i,k:index), happens(T(i, k)) => init < T(i, k) axiom depends_init_R1 {‘P:system[like default]} @system:(set:’P; equiv:None) : forall (j:index), happens(R1(j)) => init < R1(j) axiom depends_init_R {‘P:system[like default]} @system:(set:’P; equiv:None) : forall (j,i:index), happens(R(j, i)) => init < R(j, i) System default registered with actions (init,R,R1,T).

We see that with this declaration, in the resulting system after processing, all outputs have been given a name, and each output corresponds to a possible action that can be triggered by the attacker. Here, the possible actions are (init,R,R1,T). Many axioms are created, expressing the fact that for instance actions R1 and R are mutually exclusive, as they are exclusive branches; this is the mutex_default_R1_R axiom, stating that for any possible execution, the two actions cannot both happen in the trace.

A system declared this way is given the name default. Other systems can be defined and given an explicit name. For instance, the following declares the system simple, where each tag can only be executed once for each identity.

system simple = ((!_j reader) | (!_i tag(i))).

[warning>Type-checked process: ( !_j( reader ) ) | !_i( tag i) <]global axiom namelength_nT1 {‘P:system} @system:(set:’P; equiv:None) : [forall (i:index), len (nT1 i) = namelength_message] [warning>Pre-processed system: 0 - parallel/left 1 - !_j 2 - in(cT,x) 3 - try find i such that snd x = h (fst x, kT i) 4 - out(cR,ok) 5 - null 3 - else 6 - out(cR,ko) 7 - null 0 - parallel/right 8 - !_i 9 - out(cT,<nT1 i,h (nT1 i, kT i)>) 10 - null <][warning>System can be used to prove diff-equivalences and diff-inclusions. <][warning>No conflict found. <][warning>Pre-processed system with end of blocks marked: 0 - parallel/left 1 - !_j 2 - in(cT,x) 3 - try find i such that snd x = h (fst x, kT i) * 4 - out(cR,ok) 5 - null 3 - else * 6 - out(cR,ko) 7 - null 0 - parallel/right 8 - !_i * 9 - out(cT,<nT1 i,h (nT1 i, kT i)>) 10 - null <]Added action dependencies lemmas: axiom depends_init_T1 {‘P:system[like simple]} @system:(set:’P; equiv:None) : forall (i:index), happens(T1(i)) => init < T1(i) System simple registered with actions (init,R,R1,T1).

Reachability properties

We consider reachability formulas, that is, properties that talk about what is possible or not for all traces. In Squirrel, we express such formulas in a first order logic, and call them local formulas.

In this logic, terms can be of type message, boolean, index and timestamp. The logic lets us prove that formulas are true for all possible traces of the protocol, and for all possible values of the variables given a trace.

For instance, a timestamp variable t allows to talk about a given point inside a trace. t will intuitively have to take the value of some concrete action, e.g., T(i) or R(j) in our case.

Macros

To discuss about the value of the output performed at some timestamp, we use macros:

• input@t is the value given as input by the attacker to the action at t;

• output@t is the output performed by the action at t;

• cond@t is the executability condition of the action at t;

• frame@t is the sequence of all previous outputs up to t;

• exec@t is the conjunction of all executability conditions up to t.

Formulas

It is then possible to write formulas that capture properties satisfied by all executions of the protocol. For instance, the following formula describes that the executability execution of the reader in fact implies some authentication property. More precisely, there must exist an action T(i,k) that was executed before the reader, and such the input of the reader corresponds to the name of T(i,k).

lemma wa : forall (i:index, j:index), happens(R(j,i)) => cond@R(j,i) => exists (k:index), T(i,k) <= R(j,i) && fst(input@R(j,i)) = nT(i,k).

Goal wa : forall (i,j:index), happens(R(j, i)) => cond@R(j, i) => exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)

We write below the simple proof of this statement. The high-level idea of the proof is to use the EUF cryptographic axiom: only the tag T(i,k) can compute h(nT(i,k),kT(i)) because the secret key is not known by the attacker. Therefore, any message accepted by the reader must come from a tag that has played before. The converse implication is trivial, because any honest tag output is accepted by the reader.

Once inside a proof context, delimited by Proof. and Qed., it is possible to display the list of available tactics by typing help., and details about any tactic with help tacticname.

We now start the proof.

Proof.

[goal> Focused goal (1/1): System: (set:default; equiv:None) —————————————- forall (i,j:index), happens(R(j, i)) => cond@R(j, i) => exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)

After the Proof command, Squirrel displays the current judgement. It contains the number of goals that remain to be proved (one at first, but additional subgoals may be created by tactics), the system we are working in, and the formula to be proved.

intro i j Hh Hc.

[goal> Focused goal (1/1): System: (set:default; equiv:None) Variables: i,j:index[const] Hc: cond@R(j, i) Hh: happens(R(j, i)) —————————————- exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)

We have performed an introduction with the intro tactic. This pushes universal quantification inside the judgment context, where the universally quantified variables become free variables. This allows us to then push the left-hand side of the implications as hypotheses of the judgment, that we can then reason on. The free variables and assumptions are named according to the identifiers given as parameters to intro.

expand cond.

[goal> Focused goal (1/1): System: (set:default; equiv:None) Variables: i,j:index[const] Hc: snd (input@R(j, i)) = h (fst (input@R(j, i)), kT i) Hh: happens(R(j, i)) —————————————- exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)

After introducing the hypotheses and expanding the executability condition of R, we get an equality between a hash and some other term snd (input@R(j, i)). We then use the unforgeability of the hash function, the EUF assumption, to get that the hashed value fst (input@R(j, i)) must be equal to some honestly hashed value in snd (input@R(j, i)), since the key kT is secret. All honestly hashes are produced by the tag, which will then conclude our proof. This cryptographic axiom is applied thanks to the euf tactic.

euf Hc.

Indirect bad occurrences of key kT(i), and messages authenticated by it in other actions: nT (i, k) auth. by kT(i) (collision with fst (input@R(j, i)) auth. by kT(i)) in action T(i, k) in term (happens(T(i, k)), <nT (i, k),h (nT (i, k), kT i)>) Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining [goal> Focused goal (1/1): System: (set:default; equiv:None) Variables: i,j:index[const] Hc: snd (input@R(j, i)) = h (fst (input@R(j, i)), kT i) Hh: happens(R(j, i)) —————————————- (exists (k:index), T(i, k) < R(j, i) && fst (input@R(j, i)) = nT (i, k)) => exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)

To conclude, we just have to use the k introduced by the euf tactic as a witness for the existential k we have to find.

intro [k _].

[goal> Focused goal (1/1): System: (set:default; equiv:None) Variables: i,j,k:index[const] Hc: snd (input@R(j, i)) = h (fst (input@R(j, i)), kT i) Hh: happens(R(j, i)) _: T(i, k) < R(j, i) && fst (input@R(j, i)) = nT (i, k) —————————————- exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k)

by exists k.

[goal> lemma wa is proved

Qed.

lemma wa @system:(set:default; equiv:None) : forall (i,j:index), happens(R(j, i)) => cond@R(j, i) => exists (k:index), T(i, k) <= R(j, i) && fst (input@R(j, i)) = nT (i, k) Exiting proof mode.

Equivalence properties

More complex properties based on equivalence can be expressed. Intuitively, two processes are equivalent if the attacker cannot know whether it is interacting with one or the other. This is a generic security property used in the computational model to prove many distinct flavours of security.

We can declare in Squirrel two variants of a protocol at once using the diff(t1,t2) operator. A process containing diff-terms is called a bi-process, as it can lead to two distinct processes when projecting on the left or the right of the diff. This allows to easily model some security properties.

For instance, we can declare a bi-process tagD, where on one side each tag may be called many times and always use there own key, while on the right side, we in fact use a new fresh independent key every time a tag is called. The left-hand side of the process can be seen as the real world, while the right-hand side is an idealised world where a new tag is used each time. Proving that these two worlds are equivalent will establish that tags cannot be tracked.

name kT’: index * index -> message process tagD(i:index,k:index) = new nT; out(cT, <nT, h(nT,diff(kT(i),kT’(i,k)))>).

global axiom namelength_kT’ {‘P:system} @system:(set:’P; equiv:None) : [forall (i:index * index), len (kT’ i) = namelength_message] process tagD (i,k:index) = new nT : message; out(cT,<nT,h (nT, diff(kT i, kT’ (i, k)))>); null

process readerD(j:index) = in(cT,x); if exists (i,k:index), snd(x) = h(fst(x),diff(kT(i),kT’(i,k))) then out(cR,ok) else out(cR,ko) system BasicHash = ((!_j R: readerD(j)) | (!_i !_k T: tagD(i,k))).

process readerD (j:index) = in(cT,x); if exists (i,k:index), snd x = h (fst x, diff(kT i, kT’ (i, k))) then out(cR,ok); null else out(cR,ko); null [warning>Type-checked process: ( !_j( R: readerD j) ) | !_i( !_k( T: tagD i k)) <]global axiom namelength_nT2 {‘P:system} @system:(set:’P; equiv:None) : [forall (i:index * index), len (nT2 i) = namelength_message] [warning>Pre-processed system: 0 - parallel/left 1 - !_j 2 - in(cT,x) 3 - if exists (i,k:index), snd x = h (fst x, diff(kT i, kT’ (i, k))) 4 - out(cR,ok) 5 - null 3 - else 6 - out(cR,ko) 7 - null 0 - parallel/right 8 - !_i 9 - !_k 10 - out(cT,<nT2 (i, k),h (nT2 (i, k), diff(kT i, kT’ (i, k)))>) 11 - null <][warning>System can be used to prove diff-equivalences and diff-inclusions. <][warning>No conflict found. <][warning>Pre-processed system with end of blocks marked: 0 - parallel/left 1 - !_j 2 - in(cT,x) 3 - if exists (i,k:index), snd x = h (fst x, diff(kT i, kT’ (i, k))) * 4 - out(cR,ok) 5 - null 3 - else * 6 - out(cR,ko) 7 - null 0 - parallel/right 8 - !_i 9 - !_k *10 - out(cT,<nT2 (i, k),h (nT2 (i, k), diff(kT i, kT’ (i, k)))>) 11 - null <]Added action dependencies lemmas: axiom mutex_R1_R2 {‘P:system[like BasicHash]} @system:(set:’P; equiv:None) : forall (j:index), not happens(R1(j)) || not happens(R2(j)) axiom mutex_R2_R1 {‘P:system[like BasicHash]} @system:(set:’P; equiv:None) : forall (j:index), not happens(R2(j)) || not happens(R1(j)) axiom depends_init_R2 {‘P:system[like BasicHash]} @system:(set:’P; equiv:None) : forall (j:index), happens(R2(j)) => init < R2(j) System BasicHash registered with actions (init,R2,R1,T).

Importantly, reachability formulas can be expressed and proved directly on bi-systems. We can for instance write a variant of the previous proof directly on the bi-system:

lemma [BasicHash] wa_R : forall (tau:timestamp), happens(tau) => ((exists (i,k:index), snd(input@tau) = h(fst(input@tau),diff(kT(i),kT’(i,k)))) <=> (exists (i,k:index), T(i,k) < tau && fst(output@T(i,k)) = fst(input@tau) && snd(output@T(i,k)) = snd(input@tau))).

Goal wa_R : forall (tau:timestamp), happens(tau) => (exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))) <=> exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

The idea of the proof is similar, except that we prove here a logical equivalence instead of an implication.

Proof.

[goal> Focused goal (1/1): System: (set:BasicHash; equiv:None) —————————————- forall (tau:timestamp), happens(tau) => (exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))) <=> exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

intro tau Hap.

[goal> Focused goal (1/1): System: (set:BasicHash; equiv:None) Variables: tau:timestamp[const] Hap: happens(tau) —————————————- (exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))) <=> exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

We have to prove two implications (<=>): we thus split the proof in two parts. We now have two different goals to prove.

split; intro [i k Meq].

[goal> Focused goal (1/2): System: (set:BasicHash; equiv:None) Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k))) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

For the first implication (=>), we actually consider separately the real system (left) and the ideal system (right).

project.

[goal> Focused goal (1/3): System: (set:left:BasicHash/left; equiv:None) Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT i) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

The proof is very similar on both sides, and relies on the euf tactic. Applying the euf tactic on the Meq hypothesis generates a new hypothesis stating that fst(input@R(j)) must be equal to some message that has already been hashed before. The only possibility is that this hash comes from the output of a tag that has played before (thus the new hypothesis on timestamps).

euf Meq.

Indirect bad occurrences of key kT(i), and messages authenticated by it in other actions: nT2 (i, k) auth. by kT(i) (collision with fst (input@tau) auth. by kT(i)) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT i)>) Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining [goal> Focused goal (1/3): System: (set:left:BasicHash/left; equiv:None) Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT i) —————————————- (exists (k:index), T(i, k) < tau && fst (input@tau) = nT2 (i, k)) => exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

intro [k0 _].

[goal> Focused goal (1/3): System: (set:left:BasicHash/left; equiv:None) Variables: i,k,k0:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT i) _: T(i, k0) < tau && fst (input@tau) = nT2 (i, k0) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

by exists i,k0.

[goal> Focused goal (1/2): System: (set:right:BasicHash/right; equiv:None) Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT’ (i, k)) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

The right side of the proof is very similar.

euf Meq => *.

Indirect bad occurrences of key kT’((i, k)), and messages authenticated by it in other actions: nT2 (i, k) auth. by kT’((i, k)) (collision with fst (input@tau) auth. by kT’((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))>) Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining [goal> Focused goal (1/2): System: (set:right:BasicHash/right; equiv:None) Variables: i,k:index[const],tau:timestamp[const] H: T(i, k) < tau && fst (input@tau) = nT2 (i, k) Hap: happens(tau) Meq: snd (input@tau) = h (fst (input@tau), kT’ (i, k)) —————————————- exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau)

by exists i,k.

[goal> Focused goal (1/1): System: (set:BasicHash; equiv:None) Variables: i,k:index[const],tau:timestamp[const] Hap: happens(tau) Meq: T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau) —————————————- exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))

We use here the notation euf Meq => *, which is a shortcut for euf Meq; intro *, the * performing as many introductions as possible, with automatic naming of variables and hypotheses.

For the second implication (<=), the conclusion of the goal can directly be obtained from the hypotheses.

by exists i,k.

[goal> lemma wa_R is proved

Qed.

lemma wa_R @system:(set:BasicHash; equiv:None) : forall (tau:timestamp), happens(tau) => (exists (i,k:index), snd (input@tau) = h (fst (input@tau), diff(kT i, kT’ (i, k)))) <=> exists (i,k:index), T(i, k) < tau && fst (output@T(i, k)) = fst (input@tau) && snd (output@T(i, k)) = snd (input@tau) Exiting proof mode.

We now prove an equivalence property expressing the unlinkability of the protocol. This property is expressed by the logical formula forall t:timestamp, [happens(t)] -> equiv(frame@t) where frame@t is actually a bi-frame. It states that for any trace (the quantification is implicit over all traces), at any point that happens in the trace, the two frames (derived by projecting the diff operator) are equivalent. Square brackets contain local formulas, and such a formula mixing both local formulas and equivalences is called a global formula.

Here, we will have to prove that the left projection of frame@t (i.e. the real system) is indistinguishable from the right projection of frame@t (i.e. the ideal system).

As this goal is a frequent one, a shortcut allows declaring this goal without writing the full formula, using the keyword equiv.

equiv [BasicHash] unlinkability.

Goal unlinkability : forall t:timestamp[const, glob], equiv(frame@t)

Proof.

[goal> Focused goal (1/1): Systems: BasicHash Variables: t:timestamp[const, glob] H: [happens(t)] —————————————- 0: frame@t

An equivalence judgment contains the list of hypotheses, as before. The conclusion is however different to the reachability case. Now, we have a numbered list of diff-terms, and we must prove that the left projection and the right projection of this list are indistinguishable. We refer to this sequence of diff terms as the biframe of the goal.

The high-level idea of the proof is as follows:

• if t corresponds to a reader’s action, we show that the outcome of the conditional is the same on both sides and that this outcome only depends on information already available to the attacker;

• if t corresponds to a tag’s action, we show that the new message added in the frame (i.e. the tag’s output) does not give any information that helps the attacker distinguish the real system from the ideal one. Indeed, hashes can intuitively be seen as fresh names thanks to the PRF cryptographic axiom.

The proof is done by induction over the timestamp t. The induction tactic also automatically introduces a case analysis over all possible values for t. The first case, where t = init corresponds to the initial point of the execution trace, before any protocol action has happened. That case is trivial, we directly close it with auto. The other cases correspond to the 3 different actions of the protocol.

induction t.

[goal> Focused goal (1/4): Systems: BasicHash H: [happens(init)] —————————————- 0: frame@init

auto.

[goal> Focused goal (1/3): Systems: BasicHash Variables: j:index[const, glob] H: [happens(R2(j))] IH: equiv(frame@pred (R2(j))) —————————————- 0: frame@R2(j)

For the case where t = R2(j), we start by expanding the macros and splitting the pairs. Splitting the pairs is done by using the fa tactic, which when applied to all pairs thanks to the pattern !<_,_> splits a bi-frame element containing a pair into two biframe elements, containing the the two components.

expand frame, exec, output.

[goal> Focused goal (1/3): Systems: BasicHash Variables: j:index[const, glob] H: [happens(R2(j))] IH: equiv(frame@pred (R2(j))) —————————————- 0: <frame@pred (R2(j)), <of_bool (exec@pred (R2(j)) && cond@R2(j)), if (exec@pred (R2(j)) && cond@R2(j)) then ok>>

fa !<_,_>.

[goal> Focused goal (1/3): Systems: BasicHash Variables: j:index[const, glob] H: [happens(R2(j))] IH: equiv(frame@pred (R2(j))) —————————————- 0: frame@pred (R2(j)) 1: exec@pred (R2(j)) && cond@R2(j)

Using the previously proved authentication goal wa_R, we replace the formula cond@R2(j) with an equivalent formula, which states that a tag T(i,k) has played before and that the output of this tag is equal to the message input by the reader. This is one of the strength of Squirrel: we can finely reuse previously proved goals to simplify a current goal. Here, we can see the wa_R lemma as a rewriting rule over boolean formulas, and so we use the rewrite tactic.

rewrite /cond (wa_R (R2 j)) //.

[goal> Focused goal (1/3): Systems: BasicHash Variables: j:index[const, glob] H: [happens(R2(j))] IH: equiv(frame@pred (R2(j))) —————————————- 0: frame@pred (R2(j)) 1: exec@pred (R2(j)) && exists (i,k:index), T(i, k) < R2(j) && fst (output@T(i, k)) = fst (input@R2(j)) && snd (output@T(i, k)) = snd (input@R2(j))

We are now able to remove this formula from the frame because the attacker is able to compute it using information obtained in the past. Indeed, each of its elements is already available in frame@pred(R2(j)). This is done by the deduce tactic.

by deduce 1.

[goal> Focused goal (1/2): Systems: BasicHash Variables: j:index[const, glob] H: [happens(R1(j))] IH: equiv(frame@pred (R1(j))) —————————————- 0: frame@R1(j)

The case where t = R1(j) is similar to the previous one.

expand frame, exec, output.

[goal> Focused goal (1/2): Systems: BasicHash Variables: j:index[const, glob] H: [happens(R1(j))] IH: equiv(frame@pred (R1(j))) —————————————- 0: <frame@pred (R1(j)), <of_bool (exec@pred (R1(j)) && cond@R1(j)), if (exec@pred (R1(j)) && cond@R1(j)) then ko>>

fa !<_,_>.

[goal> Focused goal (1/2): Systems: BasicHash Variables: j:index[const, glob] H: [happens(R1(j))] IH: equiv(frame@pred (R1(j))) —————————————- 0: frame@pred (R1(j)) 1: exec@pred (R1(j)) && cond@R1(j)

rewrite /cond (wa_R (R1 j)) //.

[goal> Focused goal (1/2): Systems: BasicHash Variables: j:index[const, glob] H: [happens(R1(j))] IH: equiv(frame@pred (R1(j))) —————————————- 0: frame@pred (R1(j)) 1: exec@pred (R1(j)) && not exists (i,k:index), T(i, k) < R1(j) && fst (output@T(i, k)) = fst (input@R1(j)) && snd (output@T(i, k)) = snd (input@R1(j))

by deduce 1.

[goal> Focused goal (1/1): Systems: BasicHash Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: frame@T(i, k)

Finally, for the case where t = T(i,k), we similarly start by expanding the macros and splitting the pairs.

expand frame, exec, cond, output.

[goal> Focused goal (1/1): Systems: BasicHash Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: <frame@pred (T(i, k)), <of_bool (exec@pred (T(i, k)) && true), if (exec@pred (T(i, k)) && true) then <nT2 (i, k),h (nT2 (i, k), diff(kT i, kT’ (i, k)))>>>

fa !<_,_>, if _ then _, <_,_>.

[goal> Focused goal (1/1): Systems: BasicHash Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: frame@pred (T(i, k)) 1: nT2 (i, k) 2: h (nT2 (i, k), diff(kT i, kT’ (i, k)))

We now apply the prf tactic, in order to replace the hash with a fresh name. This creates a new subgoal, asking to prove that the hashed value has never been hased before.

prf 2.

global axiom namelength_n_PRF {‘P:system} @system:(set:’P; equiv:None) : [len n_PRF = namelength_message] Applying PRF to h (nT2 (i, k), diff(kT i, kT’ (i, k))) Checking for occurrences on the left Indirect bad occurrences of key kT(i), and messages hashed by it in other actions: nT2 (i, k) hashed by kT(i) (collision with nT2 (i, k) hashed by kT(i)) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT i)>) fst (input@R2(j)) hashed by kT(i) (collision with nT2 (i, k) hashed by kT(i)) in action R2(j) in term snd (input@R2(j)) = h (fst (input@R2(j)), kT i) fst (input@R1(j)) hashed by kT(i) (collision with nT2 (i, k) hashed by kT(i)) in action R1(j) in term snd (input@R1(j)) = h (fst (input@R1(j)), kT i) Total: 3 occurrences 0 of them are subsumed by another 3 occurrences remaining Checking for occurrences on the right Indirect bad occurrences of key kT’((i, k)), and messages hashed by it in other actions: nT2 (i, k) hashed by kT’((i, k)) (collision with nT2 (i, k) hashed by kT’((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))>) fst (input@R2(j)) hashed by kT’((i, k)) (collision with nT2 (i, k) hashed by kT’((i, k))) in action R2(j) in term snd (input@R2(j)) = h (fst (input@R2(j)), kT’ (i, k)) fst (input@R1(j)) hashed by kT’((i, k)) (collision with nT2 (i, k) hashed by kT’((i, k))) in action R1(j) in term snd (input@R1(j)) = h (fst (input@R1(j)), kT’ (i, k)) Total: 3 occurrences 0 of them are subsumed by another 3 occurrences remaining [goal> Focused goal (1/3): System: (set:left:BasicHash/left; equiv:BasicHash) Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- (forall (i0,k0:index), T(i0, k0) < T(i, k) => i = i0 => nT2 (i, k) <> nT2 (i0, k0)) && (forall (i0,j:index), R2(j) < T(i, k) => i = i0 => nT2 (i, k) <> fst (input@R2(j))) && forall (i0,j:index), R1(j) < T(i, k) => i = i0 => nT2 (i, k) <> fst (input@R1(j))

Several conjuncts must now be proved, the same tactic can be used on all of them. Here are a few representative cases:

• In one case, nT(i,k) cannot occur in input@R2(j) because R2(j) < T(i,k).

• In another case, nT(i,k) = nT(i0,k0) implies that i=i0 and k=k0, contradicting T(i0,k0)<T(i,k).

In both cases, the reasoning is performed by the fresh tactic on the message equality hypothesis Meq, whose negation was initially to be proved. To be able to use (split and) fresh, we first project the goal onto on the left projection and one goal for the right projection of the initial bi-system.

repeat split; intro *; by fresh Meq.

Freshness of nT2 (i, k): Direct occurrences of nT2((i, k)) in nT2 (i0, k0): nT2((i0, k0)) (collision with nT2((i, k))) in term nT2 (i0, k0) Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining Freshness of nT2 (i, k): Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT i)>) nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT i)>) Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining Freshness of nT2 (i, k): Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT i)>) nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT i)>) Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining [goal> Focused goal (1/2): System: (set:right:BasicHash/right; equiv:BasicHash) Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- (forall (i0,k0:index), T(i0, k0) < T(i, k) => i = i0 && k = k0 => nT2 (i, k) <> nT2 (i0, k0)) && (forall (k0,i0,j:index), R2(j) < T(i, k) => i = i0 && k = k0 => nT2 (i, k) <> fst (input@R2(j))) && forall (k0,i0,j:index), R1(j) < T(i, k) => i = i0 && k = k0 => nT2 (i, k) <> fst (input@R1(j))

repeat split; intro *; by fresh Meq.

Freshness of nT2 (i, k): Direct occurrences of nT2((i, k)) in nT2 (i0, k0): nT2((i0, k0)) (collision with nT2((i, k))) in term nT2 (i0, k0) Total: 1 occurrence 0 of them are subsumed by another 1 occurrence remaining Freshness of nT2 (i, k): Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))>) nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))>) Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining Freshness of nT2 (i, k): Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))>) nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))>) Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining [goal> Focused goal (1/1): Systems: BasicHash Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: frame@pred (T(i, k)) 1: nT2 (i, k) 2: n_PRF

We have now replaced the hash by a fresh name occurring nowhere else, so we can remove it using the fresh tactic.

fresh 2; 1:auto.

Freshness on the left side: Freshness on the right side: [goal> Focused goal (1/1): Systems: BasicHash Variables: i,k:index[const, glob] H: [happens(T(i, k))] IH: equiv(frame@pred (T(i, k))) —————————————- 0: frame@pred (T(i, k)) 1: nT2 (i, k)

We can also remove the name nT(i,k), and conclude (automatically) by the induction hypothesis.

by fresh 1.

Freshness on the left side: Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT i)>) nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT i)>) Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining Freshness on the right side: Indirect occurrences of nT2((i, k)) in other actions: nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))>) nT2((i, k)) (collision with nT2((i, k))) in action T(i, k) in term (happens(T(i, k)), <nT2 (i, k),h (nT2 (i, k), kT’ (i, k))>) Total: 2 occurrences 1 of them is subsumed by another 1 occurrence remaining [goal> lemma unlinkability is proved

Qed.

global lemma unlinkability @system:BasicHash : Forall (t:timestamp[const, glob]), [happens(t)] -> equiv(frame@t) Exiting proof mode.