(* Full model of LAK with pairs and tags, for authentication only. *)
(* R --> T: nr *)
(* T --> R: nT, h(<nR, nT, tag1>, k) *)
(* R --> T: h(<h(<nR, nT, tag1>, k), nr, tag2>, k)*)
set postQuantumSound = true.
hash h
abstract ok:message
abstract ko:message
abstract tag1:message
abstract tag2:message
name key : index->message
channel cT
channel cR
process tag(i:index) =
new nT;
in(cR,nR);
out(cT,<nT,h(<<nR,nT>,tag1>,key(i))>);
in(cR,m3);
if m3 = h(<<h(<<nR,nT>,tag1>,key(i)),nR>,tag2>,key(i)) then
out(cT,ok)
else
out(cT,ko)
process reader =
new nR;
out(cR,nR);
in(cT,x);
try find i such that snd(x) = h(<<nR,fst(x)>,tag1>,key(i)) in
out(cR,h(<<snd(x),nR>,tag2>,key(i)))
else
out(cR,ko)
system ((!_k R: reader) | (!_i !_j T: tag(i))).
System before processing:
(!_k R: reader ) | (!_i !_j T: tag i)
System after processing:
(!_k
R:
out(cR,nR(k));
in(cT,x);
find (i) such that (snd(x) = h(pair(pair(nR(k),fst(x)),tag1),key(i))) in
R1: out(cR,h(pair(pair(snd(x),nR(k)),tag2),key(i))); null else
R2: out(cR,ko); null) |
(!_i
!_j
in(cR,nR);
T:
out(cT,pair(nT(i,j),h(pair(pair(nR,nT(i,j)),tag1),key(i))));
in(cR,m3);
if (m3 =
h(pair(pair(h(pair(pair(nR,nT(i,j)),tag1),key(i)),nR),tag2),key(i))) then
T1: out(cT,ok); null else T2: out(cT,ko); null)
System default registered with actions (init,R,R1,R2,T,T1,T2).
axiom tags_neq : tag1 <> tag2.
goal wa_R:
forall (k:index, i:index),
happens(R1(k,i)) =>
cond@R1(k,i) =>
exists (j:index),
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) &&
output@R(k) = input@T(i,j).
Goal wa_R :
forall (k,i:index),
happens(R1(k,i)) =>
cond@R1(k,i) =>
exists (j:index),
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
Proof.
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
----------------------------------------
forall (k,i:index),
happens(R1(k,i)) =>
cond@R1(k,i) =>
exists (j:index),
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
intro k i _ Hc.
[> Line 56: (intro k i _ Hc)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,k:index
Hc: cond@R1(k,i)
_: happens(R1(k,i))
----------------------------------------
exists (j:index),
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
rewrite /cond in Hc.
[> Line 57: (rewrite ... in Hc)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,k:index
Hc: snd(input@R1(k,i)) = h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i))
_: happens(R1(k,i))
----------------------------------------
exists (j:index),
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
euf Hc => // _ _ _.
[> Line 57: ((euf Hc);(intro // _ _ _))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,k,k0:index
Hc: snd(input@R1(k,i)) = h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i))
_: <<snd(input@R1(k0,i)),nR(k0)>,tag2> = <<nR(k),fst(input@R1(k,i))>,tag1>
_: R1(k0,i) < R1(k,i)
_: happens(R1(k,i))
----------------------------------------
exists (j:index),
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
+ by use tags_neq.
[> Line 58: by (have ... as )
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,k:index
Hc: snd(input@R1(k,i)) = h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i))
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k,i))>,tag1>
_: T(i,j) < R1(k,i)
_: happens(R1(k,i))
----------------------------------------
exists (j:index),
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
+ exists j.
[> Line 59: (exists j)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,k:index
Hc: snd(input@R1(k,i)) = h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i))
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k,i))>,tag1>
_: T(i,j) < R1(k,i)
_: happens(R1(k,i))
----------------------------------------
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
assert (nR(k) = input@T(i,j)) as Mfresh by auto.
[> Line 60: ((have (nR(k) = input@T(i,j)), Mfresh); 1: by auto)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,k:index
Hc: snd(input@R1(k,i)) = h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i))
Mfresh: nR(k) = input@T(i,j)
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k,i))>,tag1>
_: T(i,j) < R1(k,i)
_: happens(R1(k,i))
----------------------------------------
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
fresh Mfresh => [Hfresh | Hfresh | [i' Hfresh]] //.
[> Line 61: ((fresh Mfresh);(intro [Hfresh|Hfresh|[i' Hfresh]] //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,k:index
Hc: snd(input@R1(k,i)) = h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i))
Hfresh: R2(k) < T(i,j)
Mfresh: nR(k) = input@T(i,j)
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k,i))>,tag1>
_: T(i,j) < R1(k,i)
_: happens(R1(k,i))
----------------------------------------
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
- by depends R(k), R2(k).
[> Line 62: by (depends R(k), R2(k))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i',j,k:index
Hc: snd(input@R1(k,i)) = h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i))
Hfresh: R1(k,i') < T(i,j)
Mfresh: nR(k) = input@T(i,j)
_: <<input@T(i,j),nT(i,j)>,tag1> = <<nR(k),fst(input@R1(k,i))>,tag1>
_: T(i,j) < R1(k,i)
_: happens(R1(k,i))
----------------------------------------
T(i,j) < R1(k,i) &&
fst(input@R1(k,i)) = fst(output@T(i,j)) &&
snd(input@R1(k,i)) = snd(output@T(i,j)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
- by depends R(k), R1(k,i').
[> Line 63: by (depends R(k), R1(k,i'))
[goal> Goal wa_R is proved
Qed.
Exiting proof mode.
goal executable_R1 (t:timestamp) (k,i:index) :
happens(t) => exec@t => R1(k,i)<=t => exec@R1(k,i) && cond@R1(k,i).
Goal executable_R1 :
happens(t) => exec@t => R1(k,i) <= t => exec@R1(k,i) && cond@R1(k,i)
Proof.
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,k:index,t:timestamp
----------------------------------------
happens(t) => exec@t => R1(k,i) <= t => exec@R1(k,i) && cond@R1(k,i)
intro _ _ _.
[> Line 69: (intro _ _ _)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,k:index,t:timestamp
_: R1(k,i) <= t
_: exec@t
_: happens(t)
----------------------------------------
exec@R1(k,i) && cond@R1(k,i)
executable t => // He.
[> Line 70: ((executable t);(intro // He))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,k:index,t:timestamp
He: forall (t0:timestamp), t0 <= t => exec@t0
_: R1(k,i) <= t
_: exec@t
_: happens(t)
----------------------------------------
exec@R1(k,i) && cond@R1(k,i)
by use He with R1(k,i).
[> Line 71: by (have ... as )
[goal> Goal executable_R1 is proved
Qed.
Exiting proof mode.
goal wa_T:
forall (i:index, j:index),
happens(T1(i,j)) =>
exec@T1(i,j) =>
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) &&
output@R(k) = input@T(i,j).
Goal wa_T :
forall (i,j:index),
happens(T1(i,j)) =>
exec@T1(i,j) =>
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
Proof.
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
----------------------------------------
forall (i,j:index),
happens(T1(i,j)) =>
exec@T1(i,j) =>
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
intro i j Hh He.
[> Line 90: (intro i j Hh He)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index
He: exec@T1(i,j)
Hh: happens(T1(i,j))
----------------------------------------
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
assert cond@T1(i,j) as Hc by auto.
[> Line 91: ((have cond@T1(i,j), Hc); 1: by auto)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index
Hc: cond@T1(i,j)
He: exec@T1(i,j)
Hh: happens(T1(i,j))
----------------------------------------
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
use tags_neq as _.
[> Line 92: (have ... as _)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j:index
Hc: cond@T1(i,j)
He: exec@T1(i,j)
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
rewrite /cond in Hc; euf Hc => // H1t H1m _.
[> Line 93: (((rewrite ... in Hc);(euf Hc));(intro // H1t H1m _))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j) || R1(k,i) < T(i,j)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
He: exec@T1(i,j)
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
assert (snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)))
as Heuf by auto.
[> Line 95: ((have
(snd(input@R1(k,i)) =
h(pair(pair(input@T(i,j),nT(i,j)),tag1),key(i))),
Heuf);
1: by auto)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j) || R1(k,i) < T(i,j)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
He: exec@T1(i,j)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
euf Heuf => // H2t H2m _.
[> Line 96: ((euf Heuf);(intro // H2t H2m _))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,j0,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j) || R1(k,i) < T(i,j)
H2m: <<input@T(i,j0),nT(i,j0)>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
H2t: T(i,j0) < T(i,j) || T(i,j0) < R1(k,i)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
He: exec@T1(i,j)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
case H1t; case H2t; try auto.
[> Line 97: ((case H1t);((case H2t);(try auto)))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,j0,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j)
H2m: <<input@T(i,j0),nT(i,j0)>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
H2t: T(i,j0) < R1(k,i)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
He: exec@T1(i,j)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
exists (k:index),
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
exists k.
[> Line 98: (exists k)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,j0,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j)
H2m: <<input@T(i,j0),nT(i,j0)>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
H2t: T(i,j0) < R1(k,i)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
He: exec@T1(i,j)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
use executable_R1 with T1(i,j),k,i as [He' Hc'] => //.
[> Line 99: ((have ... as [He' Hc']);(intro //))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,j0,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j)
H2m: <<input@T(i,j0),nT(i,j0)>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
H2t: T(i,j0) < R1(k,i)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
Hc': cond@R1(k,i)
He: exec@T1(i,j)
He': exec@R1(k,i)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
assert h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i)) =
h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
as Hcoll by auto.
[> Line 102: ((have
(h(pair(pair(nR(k),fst(input@R1(k,i))),tag1),key(i)) =
h(pair(pair(input@T(i,j),nT(i,j)),tag1),key(i))),
Hcoll);
1: by auto)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,j0,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j)
H2m: <<input@T(i,j0),nT(i,j0)>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
H2t: T(i,j0) < R1(k,i)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
Hc': cond@R1(k,i)
Hcoll: h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i)) =
h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
He: exec@T1(i,j)
He': exec@R1(k,i)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
collision Hcoll => Hcoll'.
[> Line 103: ((collision Hcoll);(intro Hcoll'))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,j0,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j)
H2m: <<input@T(i,j0),nT(i,j0)>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
H2t: T(i,j0) < R1(k,i)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
Hc': cond@R1(k,i)
Hcoll: h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i)) =
h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hcoll': <<nR(k),fst(input@R1(k,i))>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
He: exec@T1(i,j)
He': exec@R1(k,i)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
assert (input@T(i,j) = nR(k)) as Hfresh by auto.
[> Line 104: ((have (input@T(i,j) = nR(k)), Hfresh); 1: by auto)
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,j,j0,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j)
H2m: <<input@T(i,j0),nT(i,j0)>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
H2t: T(i,j0) < R1(k,i)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
Hc': cond@R1(k,i)
Hcoll: h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i)) =
h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hcoll': <<nR(k),fst(input@R1(k,i))>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
He: exec@T1(i,j)
He': exec@R1(k,i)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hfresh: input@T(i,j) = nR(k)
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
fresh Hfresh => [Hfresh' | Hfresh' | [i0 Hfresh']] //.
[> Line 105: ((fresh Hfresh);(intro [Hfresh'|Hfresh'|[i0 Hfresh']] //))
[goal> Focused goal (1/2):
System: left:default/left, right:default/right
Variables: i,j,j0,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j)
H2m: <<input@T(i,j0),nT(i,j0)>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
H2t: T(i,j0) < R1(k,i)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
Hc': cond@R1(k,i)
Hcoll: h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i)) =
h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hcoll': <<nR(k),fst(input@R1(k,i))>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
He: exec@T1(i,j)
He': exec@R1(k,i)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hfresh: input@T(i,j) = nR(k)
Hfresh': R2(k) < T(i,j)
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
+ by depends R(k), R2(k).
[> Line 106: by (depends R(k), R2(k))
[goal> Focused goal (1/1):
System: left:default/left, right:default/right
Variables: i,i0,j,j0,k:index
H1m: <<snd(input@R1(k,i)),nR(k)>,tag2> =
<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>
H1t: R1(k,i) < T1(i,j)
H2m: <<input@T(i,j0),nT(i,j0)>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
H2t: T(i,j0) < R1(k,i)
Hc: input@T1(i,j) =
h(<<h(<<input@T(i,j),nT(i,j)>,tag1>,key(i)),input@T(i,j)>,tag2>,key(i))
Hc': cond@R1(k,i)
Hcoll: h(<<nR(k),fst(input@R1(k,i))>,tag1>,key(i)) =
h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hcoll': <<nR(k),fst(input@R1(k,i))>,tag1> = <<input@T(i,j),nT(i,j)>,tag1>
He: exec@T1(i,j)
He': exec@R1(k,i)
Heuf: snd(input@R1(k,i)) = h(<<input@T(i,j),nT(i,j)>,tag1>,key(i))
Hfresh: input@T(i,j) = nR(k)
Hfresh': R1(k,i0) < T(i,j)
Hh: happens(T1(i,j))
_: tag1 <> tag2
----------------------------------------
R1(k,i) < T1(i,j) &&
output@R1(k,i) = input@T1(i,j) &&
T(i,j) < R1(k,i) &&
fst(output@T(i,j)) = fst(input@R1(k,i)) &&
snd(output@T(i,j)) = snd(input@R1(k,i)) &&
R(k) < T(i,j) && output@R(k) = input@T(i,j)
+ by depends R(k), R1(k,i0).
[> Line 107: by (depends R(k), R1(k,i0))
[goal> Goal wa_T is proved
Qed.
Exiting proof mode.
Press the left and right arrows to do and undo an instruction.
Alternatively, you can double-click on an instruction.
This zone shows a Squirrel file. You can double-click on a comment to collapse it for better readabilility.
This zone shows the output given by Squirrel.
This zone shows the output of the previous instruction, to help identifying the change caused by the instruction.
