Unification.mlw 56.7 KB
Newer Older
1 2

module Types
3

4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
  use import Functions.Func
  (*use import Assoc.Types as AS
  use import Assoc.Logic as AS
  use import Assoc.Impl as AS*)
  use import BacktrackArray.Types as BA
  use import BacktrackArray.Logic as BA
  use import BacktrackArray.Impl as BA
  use import Firstorder_symbol_spec.Spec
  use import Firstorder_symbol_impl.Types
  use import Firstorder_symbol_impl.Logic
  use import Firstorder_symbol_impl.Impl
  use import Firstorder_term_spec.Spec
  use import Firstorder_term_impl.Types
  use import Firstorder_term_impl.Logic
  use import Firstorder_term_impl.Impl
19

20 21
  type sdata = PConflict nlimpl_fo_term_list nlimpl_fo_term_list
    | Assign nlimpl_fo_term
22

23 24
  type subst = BA.t sdata
  type timesubst = BA.timestamp sdata
25

26
  type unifier_subst = {
27 28
    ghost unifier_base_model : int -> (fo_term int int) ;
    ghost unifier : int -> (fo_term int int) ;
29
  }
30

31 32
  type unification_return = {
    ghost final_unifier : unifier_subst ;
33
    ghost unifier_factor : int -> (fo_term int int) ;
34
  }
35

36
  (*type unify_return = {
37
    ghost factor : int -> (fo_term int int);
38
  }*)
39

40 41 42
end

module Logic
43

44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
  use import int.Int
  use import Functions.Func
  use import option.Option
  use import BacktrackArray.Types as BA
  use import BacktrackArray.Logic as BA
  use import BacktrackArray.Impl as BA
  use import list.List
  use import Firstorder_symbol_spec.Spec
  use import Firstorder_symbol_impl.Types
  use import Firstorder_symbol_impl.Logic
  use import Firstorder_symbol_impl.Impl
  use import Firstorder_term_spec.Spec
  use import Firstorder_term_impl.Types
  use import Firstorder_term_impl.Logic
  use import Firstorder_term_impl.Impl
  use import Types
60

61
  constant sdata_inv : sdata -> bool
62 63 64 65 66 67 68 69 70 71 72 73
  axiom sdata_inv_def : forall x:sdata.
    sdata_inv x <-> match x with
      | PConflict l1 l2 -> nlimpl_fo_term_list_ok l1 /\
        nlimpl_fo_term_list_ok l2 /\ (forall x:int.
          is_fo_term_free_var_in_fo_term_list x
            l1.model_fo_term_list_field -> x >= 0) /\
          (forall x:int. is_fo_term_free_var_in_fo_term_list x
            l2.model_fo_term_list_field -> x >= 0)
      | Assign l -> nlimpl_fo_term_ok l /\
        (forall x:int. is_fo_term_free_var_in_fo_term x
          l.model_fo_term_field -> x >= 0)
    end
74

75
  function smodel (l:timesubst) : int -> (fo_term int int)
76 77 78 79 80 81
  axiom smodel_def : forall l:timesubst,x:int.
    smodel l x = match table l x with
      | Nil -> Var_fo_term x
      | Cons (PConflict _ _) _ -> Var_fo_term x
      | Cons (Assign u) _ -> u.model_fo_term_field
    end
82

83 84 85 86
  predicate unassigned (l:timesubst) (x:int) = match table l x with
    | Cons (Assign _) _ -> false
    | _ -> true
  end
87

88 89 90 91 92
  let lemma smodel_depend_only_model (l1 l2:timesubst) : unit
    requires { l1.table = l2.table }
    ensures { smodel l1 = smodel l2 }
  =
    assert { extensionalEqual (smodel l1) (smodel l2) }
93

94 95
  function sc (s1:'b -> (fo_term 'ls 'b)) (s2:'b -> (fo_term 'ls 'b)) :
    'b -> (fo_term 'ls 'b) =
96
    subst_compose_fo_term s1 subst_id_symbol s2
97

98
  function st (t:fo_term 'ls 'b) (s:'b -> (fo_term 'ls 'b)) : fo_term 'ls 'b =
99
    subst_fo_term t subst_id_symbol s
100

101
  function stl (t:fo_term_list 'ls 'b)
102
    (s:'b -> (fo_term 'ls 'b)) : fo_term_list 'ls 'b =
103
    subst_fo_term_list t subst_id_symbol s
104

105 106
  (*
  (* power relation. *)
107

108 109 110
  inductive power_rel (s:'b -> (fo_term 'ls 'b)) (n:int)
    (sr:'b -> (fo_term 'ls 'b)) =
    | Power0 : forall s:'b -> (fo_term 'ls 'b).
111
      power_rel s 0 subst_id_fo_term
112 113
    | Powern : forall s:'b -> (fo_term 'ls 'b),n:int,
      sr:'b -> (fo_term 'ls 'b).
114 115
      n >= 0 /\ power_rel s n sr ->
      power_rel s (n+1) (sc s sr)
116

117 118
  let rec lemma power_rel_det (s:'b -> (fo_term 'ls 'b)) (n:int) : unit
    ensures { forall sr1 sr2:'b -> (fo_term 'ls 'b).
119 120 121 122 123
      power_rel s n sr1 /\ power_rel s n sr2 -> sr1 = sr2 }
    variant { n }
  =
    if n > 0
    then power_rel_det s (n-1)
124

125 126 127
  let rec lemma power_rel_additive (s:'b -> (fo_term 'ls 'b)) (n m:int)
    (srm:'b -> (fo_term 'ls 'b)) : unit
    ensures { forall srn:'b -> (fo_term 'ls 'b).
128 129 130 131 132 133
      power_rel s n srn /\ power_rel s m srm ->
      power_rel s (n+m) (sc srn srm) }
    variant { n }
  =
    if n > 0
    then power_rel_additive s (n-1) m srm
134

135 136
  let rec ghost power (s:'b -> (fo_term 'ls 'b)) (n:int) :
    'b -> (fo_term 'ls 'b)
137 138 139 140 141 142 143
    requires { n >= 0 }
    ensures { power_rel s n result }
    variant { n }
  =
    if n = 0
    then subst_id_fo_term
    else sc s (power s (n-1))
144

145
  let rec lemma power_fixed_point (s:'b -> (fo_term 'ls 'b)) (n:int)
146 147
    (x:'b) : unit
    requires { s x = Var_fo_term x }
148
    ensures { forall srn:'b -> (fo_term 'ls 'b).
149 150 151 152 153 154
      power_rel s n srn -> srn x = Var_fo_term x }
    variant { n }
  =
    if n > 0
    then power_fixed_point s (n-1) x
  *)
155

156 157 158
  (* In other words : unifier is the idempotent limit reached by power
     iteration of the model of unifier_base, which is unifier_base_model,
     and iteration is an exponent reaching the fixed point. *)
159

160 161 162 163 164 165 166 167 168 169 170 171 172
  predicate unifier_subst_ok (rho:subst) (u:unifier_subst) =
    smodel (BA.current_timestamp rho) = u.unifier_base_model /\
    (forall x:int. eval u.unifier_base_model x = Var_fo_term x ->
      unassigned (BA.current_timestamp rho) x) /\
    (*power_rel u.unifier_base_model u.iteration u.unifier /\
    u.iteration > 0 /\*)
    (* Replace *) (forall x:int. eval u.unifier_base_model x = Var_fo_term x ->
      eval u.unifier x = Var_fo_term x) /\
    sc u.unifier_base_model u.unifier = u.unifier /\
    sc u.unifier u.unifier_base_model = u.unifier /\
    sc u.unifier u.unifier = u.unifier /\
    BA.correct rho /\
    rho.inv = sdata_inv
173

174
  (*let rec lemma size_term_increase (t:fo_term int int) (x:int)
175
    (s:int -> (fo_term int int)) : unit
176 177 178 179 180 181 182 183 184 185 186 187
    ensures { is_fo_term_free_var_in_fo_term x t ->
      size_fo_term (subst_fo_term t subst_id_symbol s)
      >= size_fo_term t + size_fo_term (s x) -
        size_fo_term (Var_fo_term x:fo_term int int) }
    ensures { size_fo_term (subst_fo_term t subst_id_symbol s) >=
      size_fo_term t }
    variant { size_fo_term t }
  =
    match t with
      | Var_fo_term _ -> ()
      | App _ l -> size_list_increase l x s
    end
188

189
  with lemma size_list_increase (t:fo_term_list int int) (x:int)
190
    (s:int -> (fo_term int int)) : unit
191 192 193 194 195 196 197 198 199 200 201 202 203
    ensures { is_fo_term_free_var_in_fo_term_list x t ->
      size_fo_term_list (subst_fo_term_list t subst_id_symbol s)
      >= size_fo_term_list t + size_fo_term (s x) -
        size_fo_term (Var_fo_term x:fo_term int int) }
    ensures { size_fo_term_list (subst_fo_term_list t subst_id_symbol s)
      >= size_fo_term_list t }
    variant { size_fo_term_list t }
  =
    match t with
      | FONil -> ()
      | FOCons u q -> size_term_increase u x s ;
        size_list_increase q x s
    end*)
204

205 206 207
end

module Impl
208

209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227
  use import int.Int
  use import Functions.Func
  use import option.Option
  use import BacktrackArray.Types as BA
  use import BacktrackArray.Logic as BA
  use import BacktrackArray.Impl as BA
  use import list.List
  use import Firstorder_symbol_spec.Spec
  use import Firstorder_symbol_impl.Types
  use import Firstorder_symbol_impl.Logic
  use import Firstorder_symbol_impl.Impl
  use import Firstorder_term_spec.Spec
  use import Firstorder_term_impl.Types
  use import Firstorder_term_impl.Logic
  use import Firstorder_term_impl.Impl
  use import Types
  use import Logic
  use import ref.Ref
  use import list.Mem
228

229
  exception UnificationFailure
230

231 232 233 234
  (* Utility for a frequent reasoning that
     allow to decrease variant. *)
  (*let ghost checkit (rhob:subst) (rho:unifier_subst) (x:int) (*(it:int)*) : unit
    (*requires { it >= 0 }
235
    requires { forall sp:int -> (fo_term int int).
236 237 238 239 240 241 242 243 244
      let tm = Var_fo_term x in
      power_rel rho.unifier_base_model it sp ->
      st tm sp = st tm rho.unifier }*)
    requires { unifier_subst_ok rhob rho }
    requires { match table (BA.current_timestamp rhob) x with
        | Cons (Assign _) _ -> true
        | _ -> false
      end }
    (*ensures { it >= 1 }*)
245
    ensures { forall sp:int -> (fo_term int int).
246 247 248 249 250 251 252 253 254 255 256 257 258 259
      let tm = eval rho.unifier_base_model x in
      power_rel rho.unifier_base_model (it-1) sp ->
      st tm sp = st tm rho.unifier }
  =
    let rho0 = rho.unifier in
    let tm = (Var_fo_term x:fo_term int int) in
    assert { (it = 0 -> tm = st tm subst_id_fo_term
      = st tm rho0 && tm = st tm (sc rho0 rho.unifier_base_model)
      = st tm rho.unifier_base_model &&
      eval rho.unifier_base_model x = Var_fo_term x &&
      match table (BA.current_timestamp rhob) x with
        | Cons (Assign _) _ -> false
        | _ -> true
      end) && it <> 0 } ;
260
    assert { forall sp:int -> (fo_term int int).
261 262 263 264 265 266 267 268
      let rho0 = rho.unifier_base_model in
      let rhoi = rho.unifier in
      let tm = rho0 x in
      let mx = Var_fo_term x in
      power_rel rho0 (it-1) sp ->
      power_rel rho0 it (sc rho0 sp) &&
      st tm sp = st mx (sc rho0 sp) = st mx rhoi =
      st mx (sc rho0 rhoi) = st tm rhoi && st tm sp = st tm rhoi }*)
269

270 271 272 273 274 275 276 277 278
  let ghost bottomvar (rhob:subst) (ghost rho:unifier_subst) (x:int) : unit
    requires { unifier_subst_ok rhob rho }
    requires { unassigned (BA.current_timestamp rhob) x }
    ensures { let tm = Var_fo_term x in
      tm = st tm rho.unifier_base_model /\
      tm = st tm rho.unifier }
  =
    assert { eval rho.unifier_base_model x = Var_fo_term x } ;
    assert { eval rho.unifier x = Var_fo_term x }
279

280 281 282 283 284 285 286
  (* Check presence of a variable inside the fully substituted term. *)
  let rec check_unified_free_var (x:int) (t:nlimpl_fo_term)
    (rhob:subst) (ghost rho:unifier_subst)
    (*(ghost it:int)*) : unit
    requires { unifier_subst_ok rhob rho }
    requires { nlimpl_fo_term_ok t }
    (* Variant requirement. *)
287
    (*requires { forall sp:int -> (fo_term int int).
288 289 290 291 292 293
      let tm = t.model_fo_term_field in
      power_rel rho.unifier_base_model it sp ->
      st tm sp = st tm rho.unifier }*)
    (*requires { it >= 0 }*)
    requires { forall y:int. is_fo_term_free_var_in_fo_term y
      t.model_fo_term_field -> y >= 0 }
294
    diverges (* variant { 0 } *)
MARCHE Claude's avatar
MARCHE Claude committed
295
    (* variant { it , size_fo_term t.model_fo_term_field } *)
296 297 298 299 300 301 302 303 304 305 306 307 308 309
    ensures { not(is_fo_term_free_var_in_fo_term x
      (st t.model_fo_term_field rho.unifier)) }
    raises { UnificationFailure (*->
      is_fo_term_free_var_in_fo_term x (st t.model_fo_term_field rho.unifier)*) }
  =
    let tm = t.model_fo_term_field in
    let rho0 = rho.unifier in
    match destruct_fo_term t with
      | NLCVar_fo_term y -> assert { tm = Var_fo_term y } ;
        assert { (y < 0 -> table (BA.current_timestamp rhob) y = Nil
          && eval rho.unifier_base_model y = Var_fo_term y
          && eval rho.unifier y = Var_fo_term y
          && st tm rho.unifier = Var_fo_term y
          && is_fo_term_free_var_in_fo_term y (st tm rho.unifier)) && y >= 0 } ;
310 311
        let by' = BA.get rhob y in
        match by' with
312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
          | Nil -> bottomvar rhob rho y ;
            if x = y
            then raise UnificationFailure
          | Cons (PConflict _ _) _ -> bottomvar rhob rho y ;
            if x = y
            then raise UnificationFailure
          | Cons (Assign t2) _ -> assert { sdata_inv (Assign t2) } ;
            let t2m = t2.model_fo_term_field in
            assert { st tm rho0 = eval rho0 y = st t2m rho0 } ;
            (*checkit rhob rho y it ;*)
            check_unified_free_var x t2 rhob rho (*(it-1)*)
        end
      | NLC_App f l -> let fm = f.model_symbol_field in
        let lm = l.model_fo_term_list_field in
        assert { tm = App fm lm } ;
327
        assert { forall s:int -> (fo_term int int).
328 329 330
          st tm s = App fm (stl lm s) } ;
        check_unified_free_var_list x l rhob rho (*it*)
    end
331

332 333 334 335 336
  with check_unified_free_var_list (x:int) (t:nlimpl_fo_term_list)
    (rhob:subst) (ghost rho:unifier_subst) (*(ghost it:int)*) : unit
    requires { nlimpl_fo_term_list_ok t }
    requires { unifier_subst_ok rhob rho }
    (* Variant requirement. *)
337
    (*requires { forall sp:int -> (fo_term int int).
338 339 340 341 342 343
      let tm = t.model_fo_term_list_field in
      power_rel rho.unifier_base_model it sp ->
      stl tm sp = stl tm rho.unifier }*)
    (*requires { it >= 0 }*)
    requires { forall y:int. is_fo_term_free_var_in_fo_term_list y
      t.model_fo_term_list_field -> y >= 0 }
344
    diverges (* variant { 0 } *)
345
    (*variant { it , size_fo_term_list t.model_fo_term_list_field }*)
346 347 348 349 350 351 352 353 354 355 356 357 358
    ensures { not(is_fo_term_free_var_in_fo_term_list x
        (stl t.model_fo_term_list_field rho.unifier)) }
    raises { UnificationFailure (*->
      is_fo_term_free_var_in_fo_term_list x
        (stl t.model_fo_term_list_field rho.unifier)*) }
  =
    let tm = t.model_fo_term_list_field in
    let rho0 = rho.unifier in
    match destruct_fo_term_list t with
      | NLC_FONil -> ()
      | NLC_FOCons u q -> let um = u.model_fo_term_field in
        let qm = q.model_fo_term_list_field in
        assert { tm = FOCons um qm } ;
359
        assert { forall s:int -> (fo_term int int).
360 361 362 363
          stl tm s = FOCons (st um s) (stl qm s) } ;
        check_unified_free_var x u rhob rho (*it*) ;
        check_unified_free_var_list x q rhob rho (*it*)
    end
364

365 366 367 368 369 370 371
  (*
  (* to prevent : 1) expanding of t0 as a record,
     2) inlining of nlimpl_fo_term *)
  predicate ugly_hack (rho:table int nlimpl_fo_term) =
    forall x:int, t0:nlimpl_fo_term.
      AS.model rho x = Some t0 -> nlimpl_fo_term_ok t0
  *)
372

373
  (* Unification core routine : set a variable to some equation. *)
374

375
  let assign (z:int) (t:nlimpl_fo_term) (lv:ref (list int)) (rhob:subst)
376
    (ghost rho:unifier_subst) (ghost lp:int -> bool)
377
    (*(ghost fv s:S.set int)*) : unification_return
378

379 380 381 382
    (* Invariant requirements. *)
    requires { z >= 0 }
    requires { nlimpl_fo_term_ok t }
    requires { unifier_subst_ok rhob rho }
383 384


385 386 387 388 389
    (* Essential requirement : the variable is not yet assigned. *)
    requires { unassigned (current_timestamp rhob) z }
    (* Essential requirement given the structure invariants :
       do not assign a variable to itself. *)
    requires { st t.model_fo_term_field rho.unifier <> Var_fo_term z }
390

391 392
    requires { forall y:int. is_fo_term_free_var_in_fo_term y
      t.model_fo_term_field -> y >= 0 }
393

394 395 396 397 398 399
    requires { forall x:int. mem x !lv ->
      lp x /\ x >= 0 }
    requires { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
    ensures { forall x:int. mem x !lv ->
      lp x /\ x >= 0 }
    ensures { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
400

401 402 403
    (* Invariant ensures. *)
    ensures { unifier_subst_ok rhob result.final_unifier }
    ensures { precede (old rhob) rhob }
404

405 406 407
    (* Unifier properties. *)
    ensures { sc rho.unifier result.unifier_factor =
      result.final_unifier.unifier }
408
    ensures { forall s:int -> (fo_term int int).
409 410 411 412 413 414 415 416 417 418 419
      let s' = sc rho.unifier s in
      s' z = st t.model_fo_term_field s' ->
      s' = sc result.final_unifier.unifier s }
    ensures { let s0 = result.final_unifier.unifier in
      s0 z = st t.model_fo_term_field s0 }
    ensures { let s0 = result.final_unifier.unifier in
      let s1 = rho.unifier_base_model in
      sc s0 s1 = s0 = sc s1 s0 }
    ensures { let s0 = result.final_unifier.unifier in
      let s1 = rho.unifier in
      sc s0 s1 = s0 = sc s1 s0 }
420

MARCHE Claude's avatar
MARCHE Claude committed
421
    diverges
422 423 424 425 426 427 428 429 430 431 432 433
    (* Variant post-conditions. *)
    (*ensures { cardinal result.unassigned_set < cardinal s }
    ensures { forall x:int.
      mem x fv /\ AS.model result.final_unifier.unifier_base x = None ->
      mem x result.unassigned_set }
    ensures { forall x y:int.
      mem x fv /\
      is_fo_term_free_var_in_fo_term y (
        eval result.final_unifier.unifier_base_model x)
        -> mem y fv }*)
    raises { UnificationFailure -> precede (old rhob) rhob /\
      correct rhob
434
    (*-> forall s:int -> (fo_term int int).
435 436 437
      let s' = sc rho.unifier s in
      s' z <> st t.model_fo_term_field s'*) }
  =
438 439
    label Init in
    assert { forall s1 s2 s3:int -> (fo_term int int).
440
      sc s1 (sc s2 s3) = sc (sc s1 s2) s3 } ;
441
    assert { forall t0:fo_term int int,s1 s2:int -> (fo_term int int).
442 443 444 445
      st (st t0 s1) s2 = st t0 (sc s1 s2) } ;
    let tm = t.model_fo_term_field in
    let rho0 = rho.unifier_base_model in
    let rhoi = rho.unifier in
446
    let ghost stm = st tm rhoi in
447
    (*let n0 = rho.iteration in*)
448
    bottomvar rhob rho z;
449 450
    assert { rho0 z = Var_fo_term z } ;
    assert { rhoi z = Var_fo_term z } ;
451
    (*assert { forall s:int -> (fo_term int int).
452 453 454 455 456 457 458
      is_fo_term_free_var_in_fo_term z stm ->
      match stm with
        | Var_fo_term _ -> false
        | _ -> size_fo_term (st stm s) > size_fo_term (s z) end &&
      size_fo_term (st tm (sc rhoi s)) > size_fo_term (s z) &&
      s z = sc rhoi s z && st tm (sc rhoi s) <> sc rhoi s z } ;*)
    check_unified_free_var z t rhob rho (*rho.iteration*) ;
459 460 461
    let ghost uf = subst_id_fo_term[z <- stm] in
    let ghost rhoi' = sc rhoi uf in
    let ghost rho0' = rho0[z <- tm] in
462 463 464
    BA.add z (Assign t) rhob ;
    lv := Cons z !lv;
    (*let n1 = 2 * n0 + 1 in*)
465
    assert { let rho' = current_timestamp (rhob at Init) in
466 467 468 469 470 471 472
      let rho'' = current_timestamp rhob in
      (forall x:int.
      (x <> z -> table rho'' x = table rho' x &&
        (smodel rho'' x = smodel rho' x = rho0 x = rho0' x)) /\
      (x = z -> (smodel rho'' x = t.model_fo_term_field = rho0' x))) &&
      extensionalEqual (smodel rho'') rho0' &&
      smodel rho'' = rho0' } ;
473
    let ghost rho0'' = rho0[z <- stm] in
474 475 476 477 478 479 480 481 482 483 484
    assert { (forall x:int.
      (x <> z -> uf x = Var_fo_term x && rho0'' x = rho0 x = sc uf rho0 x) /\
      (x = z -> rho0'' x = stm = st stm rho0 = sc uf rho0 x)) &&
      extensionalEqual rho0'' (sc uf rho0) && rho0'' = sc uf rho0 } ;
    free_var_equivalence_of_subst_fo_term stm subst_id_symbol
          subst_id_symbol rho0 rho0' ;
    assert { (forall x:int.
      (x <> z -> uf x = Var_fo_term x &&
        rho0'' x = rho0 x = rho0' x = sc uf rho0' x) /\
      (x = z -> rho0'' x = stm = st stm rho0 = st stm rho0' = sc uf rho0 x)) &&
      extensionalEqual rho0'' (sc uf rho0') && rho0'' = sc uf rho0' } ;
485
    (*assert { forall r:int -> (fo_term int int).
486 487
        power_rel r 0 subst_id_fo_term /\ sc r subst_id_fo_term = r &&
        power_rel r 1 r } ;*)
488
    (*let rec ghost aux0 (m:int) (sp1 sp2:int -> (fo_term int int)) : unit
489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521
      requires { m >= 0 }
      requires { power_rel rho0 m sp1 /\ power_rel rho0'' m sp2 }
      variant { m }
      ensures { sc sp2 uf = sc sp1 uf }
      ensures { sc rhoi sp1 = rhoi }
      ensures { sc sp1 rhoi = rhoi }
    =
      if m <> 0
      then ( let sp1' = power rho0 (m-1) in
        let sp2' = power rho0'' (m-1) in
        aux0 (m-1) sp1' sp2' ;
        free_var_equivalence_of_subst_fo_term stm subst_id_symbol
          subst_id_symbol subst_id_fo_term uf ;
        assert { power_rel rho0 1 rho0 &&
          power_rel rho0'' 1 rho0'' &&
          (power_rel rho0 m (sc rho0 sp1') /\
          power_rel rho0 m (sc sp1' rho0)) &&
          power_rel rho0'' m (sc rho0'' sp2') &&
          sc sp1' rho0 = sp1 = sc rho0 sp1' && sp2 = sc rho0'' sp2'} ;
        assert { sc rhoi sp1 = sc rhoi sp1' = rhoi = sc sp1' rhoi = sc sp1 rhoi
          && st stm sp1 = st tm (sc rhoi sp1) = st tm rhoi = stm } ;
        assert {
          sc sp2 uf = sc rho0'' (sc sp2' uf) = sc (sc uf rho0) (sc sp1' uf)
          = sc uf (sc sp1 uf) &&
          (forall x:int. x <> z ->
            sc uf (sc sp1 uf) x = sc sp1 uf x) &&
          (sc uf (sc sp1 uf) z = st stm (sc sp1 uf) = st stm uf = stm
            = uf z = sc sp1 uf z)
          && extensionalEqual (sc uf (sc sp1 uf)) (sc sp1 uf)
          && sc sp2 uf = sc sp1 uf })
      else assert { sp1 = subst_id_fo_term }
    in*)
    (*
522
    let rec ghost aux1 (m:int) (sp1 sp2:int -> (fo_term int int)) : unit
523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550
      requires { m >= 0 }
      requires { power_rel rho0 m sp1 }
      requires { power_rel rho0' m sp2 }
      variant { m }
      ensures { st tm sp1 = st tm sp2 }
    =
      if m <> 0
      then (
        let sp1' = power rho0 (m-1) in
        let sp2' = power rho0' (m-1) in
        assert { power_rel rho0 1 rho0 &&
          power_rel rho0 m (sc sp1' rho0) &&
          sp1 = sc sp1' rho0 } ;
        assert { power_rel rho0' 1 rho0' &&
          power_rel rho0' m (sc sp2' rho0') &&
          sc sp2' rho0' = sp2 } ;
        aux1 (m-1) sp1' sp2' ;
        aux0 (m-1) sp1' (power rho0'' (m-1)) ;
        assert { is_fo_term_free_var_in_fo_term z (rhoi z) &&
          (is_fo_term_free_var_in_fo_term z (st tm sp1') ->
          is_fo_term_free_var_in_fo_term z (st (st tm sp1') rhoi) &&
          is_fo_term_free_var_in_fo_term z stm) &&
          not(is_fo_term_free_var_in_fo_term z (st tm sp1')) } ;
        free_var_equivalence_of_subst_fo_term (st tm sp1') subst_id_symbol
          subst_id_symbol rho0 rho0'
      )
      else assert { sp1 = subst_id_fo_term = sp2 }
    in*)(*
551
    let rec ghost aux2 (m:int) (sp1 sp2 sp3:int -> (fo_term int int)) : unit
552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621
      requires { m >= 0 }
      requires { power_rel rho0 m sp2 /\
        power_rel rho0' n0 sp3 /\
        power_rel rho0' (m+n0+1) sp1 }
      variant { m }
      ensures { sp1 = sc sp2 (sc rho0'' sp3) }
    =
      let sp0 = sc rhoi rhoi in
      assert { power_rel rho0 (n0+n0) sp0 } ;
      aux0 n0 rhoi (power rho0'' n0) ; (*rho0^(2*n0) = rhoi *)
      aux1 n0 rhoi sp3 ; (* st t rho^n0 = st t rho'^n0 *)
      let sp3_ = sc sp3 sp3 in
      assert { power_rel rho0' (2*n0) sp3_ } ;
      aux1 (2*n0) sp0 sp3_ ; (* st t rho^(2*n0) = st t (rho'^(2*n0)) *)
      assert { st tm sp3 = st tm rhoi = st tm sp0 = st tm sp3_
        = st (st tm sp3) sp3 = st (st tm rhoi) sp3 = st stm sp3 } ;
      assert { extensionalEqual (sc rho0' sp3)
        (update (sc rho0 sp3) z (st tm sp3)) } ;
      assert { extensionalEqual (sc rho0'' sp3)
        (update (sc rho0 sp3) z (st stm sp3)) } ;
      assert { sc rho0' sp3 = sc rho0'' sp3 } ;
      assert { power_rel rho0' (1+n0) (sc rho0' sp3) &&
        power_rel rho0' (n0+1) (sc sp3 rho0') &&
        sc sp3 rho0' = sc rho0' sp3 } ;
      if m = 0
      then assert { sp2 = subst_id_fo_term /\
          sp1 = sc rho0' sp3 }
      else (
        let sp1' = power rho0' (m+n0) in
        assert { power_rel rho0' (m+n0+1) (sc sp1' rho0') &&
          sp1 = sc sp1' rho0' } ;
        let sp2' = power rho0 (m-1) in
        assert { power_rel rho0 1 rho0 &&
          power_rel rho0 ((m-1)+1) (sc sp2' rho0) &&
          sc sp2' rho0 = sp2 } ;
        aux2 (m-1) sp1' sp2' sp3 ;
        free_var_equivalence_of_subst_fo_term stm subst_id_symbol
          subst_id_symbol rho0'' rho0 ;
        assert { (forall x:int. x <> z ->
          sc rho0'' rho0'' x = sc rho0 rho0'' x) /\
          sc rho0'' rho0'' z = st stm rho0'' = st stm rho0
          = st tm (sc rhoi rho0) = stm = sc rho0 rho0'' z } ;
        assert { extensionalEqual (sc rho0'' rho0'') (sc rho0 rho0'') } ;
        assert { sp1 = sc sp2' (sc (sc rho0'' sp3) rho0')
          = sc sp2' (sc rho0'' (sc sp3 rho0'))
          = sc sp2' (sc rho0'' (sc rho0'' sp3))
          = sc (sc sp2' (sc rho0'' rho0'')) sp3
          = sc (sc (sc sp2' rho0) rho0'') sp3
          = sc (sc sp2' rho0) (sc rho0'' sp3)
          = sc sp2 (sc rho0'' sp3) }
      )
    in*)
    (*let sp3 = power rho0' n0 in
    let rhoi_ = power rho0' n1 in
    aux2 n0 rhoi_ rhoi sp3 ;
    assert { power_rel rho0' 1 rho0' &&
      power_rel rho0' (1+n1) (sc rho0' rhoi_) &&
      power_rel rho0' (n1+1) (sc rhoi_ rho0') } ;
    assert { power_rel rho0 1 rho0 &&
      power_rel rho0 (1+n0) (sc rho0 rhoi) } ;
    aux2 (1+n0) (sc rho0' rhoi_) (sc rho0 rhoi) sp3 ;
    assert { sc rhoi' (sc rho0 sp3)
      = sc rhoi (sc uf (sc rho0 sp3)) = rhoi_
      = sc rho0' rhoi_
      = sc (sc rho0 rhoi) (sc rho0'' sp3)
      = sc rho0 (sc rhoi (sc rho0'' sp3))
      = sc rho0 rhoi_ } ;
    assert { rhoi_ = sc rhoi_ rho0' } ;
    assert { rhoi_ = sc (sc rhoi' rho0) sp3
      = sc (sc rhoi' rho0') sp3 = sc rhoi' (sc rho0' sp3) } ;*)
622
    (*let rec ghost aux3 (m:int) (sp:int -> (fo_term int int)) : unit
623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659
      requires { m >= 0 }
      requires { power_rel rho0' m sp }
      variant { m }
      ensures { sc rhoi' sp = rhoi' }
    =
      if m = 0
      then assert { sp = subst_id_fo_term }
      else (
        let sp' = power rho0' (m-1) in
        assert { power_rel rho0' 1 rho0' &&
          power_rel rho0' m (sc rho0' sp') &&
          sc rho0' sp' = sp } ;
        aux3 (m-1) sp' ;
        assert { forall x:int.
          (forall y:int.
            is_fo_term_free_var_in_fo_term y (rhoi x) ->
            st (rhoi x) rho0 = st (rhoi x) subst_id_fo_term &&
            rho0 y = subst_id_fo_term y &&
            rho0'' y = uf y) &&
          (forall y:int.
            is_fo_term_free_var_in_fo_term y (rhoi x) ->
              rho0'' y = uf y) &&
          (forall y:int.
            is_symbol_free_var_in_fo_term y (rhoi x) ->
              subst_id_symbol y = subst_id_symbol y) &&
          st (rhoi x) rho0'' = st (rhoi x) uf &&
          sc rhoi rho0'' x = sc rhoi uf x } ;
        assert { extensionalEqual (sc rhoi rho0'') (sc rhoi uf) &&
          sc rhoi' rho0' = sc rhoi' rho0 = sc rhoi (sc uf rho0)
          = sc rhoi rho0'' = sc rhoi uf = rhoi' &&
          sc rhoi' sp = sc rhoi' sp' = rhoi' }
      ) in
    aux3 (n0+1) (sc rho0' sp3) ;*)
    (* Main difficulty done : rhoi' is indeed the idempotent limit of rho0'. *)
    (*assert { rhoi_ = rhoi' } ;
    aux3 n1 rhoi_ ;*)
    (*assert { sc rhoi' rhoi' = rhoi' } ;*)
660
    (*let rec ghost aux4 (m:int) (sp:int -> (fo_term int int)) : unit
661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704
      requires { m >= 0 }
      requires { power_rel rho0 m sp }
      variant { m }
      ensures { sc rhoi' sp = rhoi' }
    =
      if m = 0
      then assert { sp = subst_id_fo_term }
      else (
        let sp' = power rho0 (m-1) in
        assert { power_rel rho0 1 rho0 &&
          power_rel rho0 m (sc rho0 sp') &&
          sc rho0 sp' = sp } ;
        aux4 (m-1) sp' ;
        assert { sc rhoi' sp = sc (sc rhoi' rho0) sp' = sc rhoi' sp' }
      ) in
    aux4 n0 rhoi ;
    assert { forall x:int, t0:nlimpl_fo_term.
      AS.model rho'' x = Some t0 ->
        ((x = z -> t0 = t) /\ (x <> z ->
          AS.model rho.unifier_base x = AS.model rho'.unifier_base x
            = AS.model rho'' x &&
          AS.model rho.unifier_base x = Some t0))
        && nlimpl_fo_term_ok t0 } ;
    assert { ugly_hack rho'' } ;*)
    free_var_equivalence_of_subst_fo_term stm subst_id_symbol
       subst_id_symbol uf subst_id_fo_term ;
    assert { rhoi' z = st (rhoi z) uf = st (Var_fo_term z) uf
      = stm = st stm uf = st tm rhoi' } ;
    assert { ((forall x:int.
      x <> z -> uf x = Var_fo_term x && sc uf rhoi' x = rhoi' x) /\
      (sc uf rhoi' z = st stm rhoi' = st (st stm rhoi) uf = st (st tm rhoi) uf
        = st stm uf = stm = uf z = st (Var_fo_term z) uf =
        sc rhoi uf z = rhoi' z
      )) && extensionalEqual (sc uf rhoi') rhoi' &&
      sc rhoi' rhoi' = rhoi' } ;
    (*assert { forall x y:int.
      mem x fv /\ is_fo_term_free_var_in_fo_term y (rho0' x) ->
      ((x = z -> rho0' x = tm && mem y fv) /\
       (x <> z -> rho0' x = rho0 x && mem y fv)) && mem y fv } ;
    assert { forall x:int.
      mem x fv /\
      AS.model rho'' x = None ->
      x <> z && AS.model rho'' x = AS.model rho.unifier_base x &&
      mem x s && mem x (remove z s) } ;*)
705
    assert { forall s0:int -> (fo_term int int).
706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730
      let s0' = sc rhoi s0 in
      s0' z = st tm s0' ->
      st stm s0 = s0' z = st (rhoi z) s0 = s0 z &&
      (forall x:int. x <> z ->
        update s0 z (st stm s0) x = s0 x = st (uf x) s0 &&
        update s0 z (st stm s0) x = sc uf s0 x) &&
      (update s0 z (st stm s0) z = st stm s0 = st (uf z) s0 &&
        update s0 z (st stm s0) z = sc uf s0 z) &&
      extensionalEqual (sc uf s0) (update s0 z (st stm s0)) &&
      extensionalEqual (update s0 z (s0 z)) s0 &&
      sc uf s0 = s0 &&
      sc rhoi' s0 = sc rhoi (sc uf s0) = sc rhoi s0 } ;
    assert { sc rho0 rhoi' = sc (sc rho0 rhoi) uf = rhoi' } ;
    assert { sc rhoi rhoi' = sc (sc rhoi rhoi) uf = rhoi' } ;
    assert { sc rhoi' rho0 = sc rhoi rho0'' = sc rhoi' rho0' } ;
    assert { (forall x:int. let tx = rhoi x in
        st tx rho0 = st tx subst_id_fo_term &&
        (forall y:int. is_fo_term_free_var_in_fo_term y tx ->
          rho0 y = subst_id_fo_term y) &&
        (forall y:int. is_fo_term_free_var_in_fo_term y tx ->
          rho0'' y = uf y) &&
        st tx rho0'' = st tx uf
      ) &&
      extensionalEqual (sc rhoi rho0'') rhoi' &&
      sc rhoi' rho0 = rhoi' = sc rhoi' rho0' } ;
731
    let ghost rhoi'' = rhoi[z <- stm] in
732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757
    assert { ((forall x:int. x <> z ->
      uf x = Var_fo_term x &&
      rhoi'' x = rhoi x = sc uf rhoi x) /\
      (rhoi'' z = stm = st stm rhoi = sc uf rhoi z)
      ) && extensionalEqual rhoi'' (sc uf rhoi) } ;
    assert { (forall x:int. let tx = rhoi x in
        st tx rhoi = st tx subst_id_fo_term &&
        (forall y:int. is_fo_term_free_var_in_fo_term y tx ->
          rhoi y = subst_id_fo_term y) &&
        (forall y:int. is_fo_term_free_var_in_fo_term y tx ->
          rhoi'' y = uf y) &&
        st tx rhoi'' = st tx uf
      ) &&
      extensionalEqual (sc rhoi rhoi'') rhoi' &&
      sc rhoi' rhoi = rhoi' } ;
    assert { ((forall x:int. x <> z ->
      sc rho0' rhoi' x = st (rho0 x) rhoi' = rhoi' x) /\
      (sc rho0' rhoi' z = st (st tm rhoi) uf = st stm uf = stm
        = uf z = st (rhoi z) uf = rhoi' z)) &&
      extensionalEqual (sc rho0' rhoi') rhoi' && sc rho0' rhoi' = rhoi' } ;
    assert { forall x:int.
      (rho0' x = Var_fo_term x -> x <> z &&
      ((rho0' x = rho0 x = Var_fo_term x &&
      rhoi x = Var_fo_term x &&
      rhoi' x = uf x = Var_fo_term x) /\
      (table (current_timestamp rhob) x =
758
       table (current_timestamp (rhob at Init)) x &&
759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779
       unassigned (current_timestamp rhob) x)))
       && (rho0' x = Var_fo_term x -> rhoi' x = Var_fo_term x)
       && (rho0' x = Var_fo_term x ->
         unassigned (current_timestamp rhob) x)
    } ;(*
    assert { forall y:int,yt:int.
      is_fo_term_free_var_in_fo_term yt tm /\
      is_fo_term_free_var_in_fo_term y (rhoi' yt) ->
      (yt <> z -> rhoi' yt = rhoi yt
        && is_fo_term_free_var_in_fo_term y (st tm rhoi) && y >= 0) /\
      (yt = z -> rhoi' yt = stm && y >= 0) && y >= 0
    } ;*)
    let rhou = {(*
      unifier_base = rho'' ;*)
      unifier_base_model = rho0' ;
      (*iteration = n1 ;*)
      unifier = rhoi' } in
    let res = { final_unifier = rhou ;
      unifier_factor = uf (*;
      unassigned_set = remove z s*) } in
    res
780

781 782 783
  (*
  meta "remove_logic" predicate ugly_hack
  *)
784

785
  (* Forced because of the model fields. *)
786
  val ghost unassigned_vars (rhob:subst) : int -> bool
787 788
    ensures { forall x:int.
      result x <-> unassigned (current_timestamp rhob) x }
789

790
  let rec unification_term (t1 t2:nlimpl_fo_term) (lv:ref (list int))
791
    (rhob:subst) (ghost rho:unifier_subst) (ghost lp:int -> bool)
792
    (*(ghost fv s:S.set int) (ghost it1 it2:int)*) : unification_return
793

794 795 796 797 798 799 800 801
    (* Invariant requirements. *)
    requires { nlimpl_fo_term_ok t1 }
    requires { nlimpl_fo_term_ok t2 }
    requires { unifier_subst_ok rhob rho }
    requires { forall y:int. is_fo_term_free_var_in_fo_term y
      t1.model_fo_term_field -> y >= 0 }
    requires { forall y:int. is_fo_term_free_var_in_fo_term y
      t2.model_fo_term_field -> y >= 0 }
802

803 804 805 806 807 808 809 810 811 812 813
    (* Variant requirements. *)
    (*requires { forall x:int.
      is_fo_term_free_var_in_fo_term x t1.model_fo_term_field -> mem x fv }
    requires { forall x:int.
      is_fo_term_free_var_in_fo_term x t2.model_fo_term_field -> mem x fv }
    requires { forall x y:int.
      mem x fv /\
      is_fo_term_free_var_in_fo_term y (eval rho.unifier_base_model x)
        -> mem y fv }
    requires { forall x:int.
      mem x fv /\ AS.model rho.unifier_base x = None -> mem x s }
814
    requires { forall sp:int -> (fo_term int int).
815 816 817 818
      let tm = t1.model_fo_term_field in
      power_rel rho.unifier_base_model it1 sp ->
      st tm sp = st tm rho.unifier }
    requires { it1 >= 0 }
819
    requires { forall sp:int -> (fo_term int int).
820 821 822 823
      let tm = t2.model_fo_term_field in
      power_rel rho.unifier_base_model it2 sp ->
      st tm sp = st tm rho.unifier }
    requires { it2 >= 0 }*)
824

825 826 827
    (* Invariant ensures. *)
    ensures { unifier_subst_ok rhob result.final_unifier }
    ensures { precede (old rhob) rhob }
828

829 830 831 832 833 834
    requires { forall x:int. mem x !lv ->
      lp x /\ x >= 0 }
    requires { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
    ensures { forall x:int. mem x !lv ->
      lp x /\ x >= 0 }
    ensures { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
835

836 837 838 839 840 841 842 843
    (* Unifier properties. *)
    (* The final unifier is obtained by composition with
       the first one and some given factor. *)
    ensures { sc rho.unifier result.unifier_factor =
      result.final_unifier.unifier }
    (* Any possible unifier obtained in such a way can be
       factorised with the final unifier as factor. In fact,
       the factorisation is trivial, so we can avoid existentials. *)
844
    ensures { forall s:int -> (fo_term int int).
845 846 847 848 849 850 851 852 853 854 855 856
      let s' = sc rho.unifier s in
      st t1.model_fo_term_field s' = st t2.model_fo_term_field s' ->
      s' = sc result.final_unifier.unifier s }
    (* It is of course an unifier. *)
    ensures { let s0 = result.final_unifier.unifier in
      st t1.model_fo_term_field s0 = st t2.model_fo_term_field s0 }
    ensures { let s0 = result.final_unifier.unifier in
      let s1 = rho.unifier_base_model in
      sc s0 s1 = s0 = sc s1 s0 }
    ensures { let s0 = result.final_unifier.unifier in
      let s1 = rho.unifier in
      sc s0 s1 = s0 = sc s1 s0 }
857

858 859 860 861 862 863 864 865 866 867 868 869 870 871 872
    (* Variant postconditions. *)
    (*ensures { result.unassigned_set = s ->
      rho.unifier = result.final_unifier.unifier /\
      rho.unifier_base_model = result.final_unifier.unifier_base_model }
    ensures { result.unassigned_set <> s ->
      cardinal result.unassigned_set < cardinal s }
    ensures { forall x:int.
      mem x fv /\ AS.model result.final_unifier.unifier_base x = None ->
      mem x result.unassigned_set }
    ensures { forall x y:int.
      mem x fv /\
      is_fo_term_free_var_in_fo_term y (
        eval result.final_unifier.unifier_base_model x)
        -> mem y fv }*)
    raises { UnificationFailure -> precede (old rhob) rhob /\ correct rhob
873
    (*-> forall s:int -> (fo_term int int).
874 875
      let s' = sc rho.unifier s in
      st t1.model_fo_term_field s' <> st t2.model_fo_term_field s'*) }
876
    diverges (* variant { 0 } *)
877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898
    (*variant { S.cardinal s , it1 + it2 ,
      size_fo_term t1.model_fo_term_field +
      size_fo_term t2.model_fo_term_field }*)
  =
    let t1m = t1.model_fo_term_field in
    let t2m = t2.model_fo_term_field in
    match destruct_fo_term t1 , destruct_fo_term t2 with
      | NLCVar_fo_term x , NLCVar_fo_term y ->
        assert { t1m = Var_fo_term x } ;
        assert { t2m = Var_fo_term y } ;
        if x = y
        then { final_unifier = rho ;
          unifier_factor = subst_id_fo_term (*;
          unassigned_set = s*) }
        else let bx = BA.get rhob x in
          match bx with
            | Cons (Assign bx) _ -> (*checkit rho x it1 ;*)
              let bxm = bx.model_fo_term_field in
              let rhobm = rho.unifier_base_model in
              let rhoi = rho.unifier in
              assert { bxm = rhobm x (*/\ mem x fv*) } ;
              assert { st bxm rhoi = sc rhobm rhoi x = rhoi x = st t1m rhoi
899
                && forall s:int -> (fo_term int int).
900 901 902 903 904 905 906
                  st bxm (sc rhoi s) = st t1m (sc rhoi s) } ;
              let res = unification_term bx t2 lv rhob rho lp (*
                fv s (it1-1) it2*) in
              let rhoi' = res.final_unifier.unifier in
              assert { st bxm rhoi' = sc rhobm rhoi' x
                = rhoi' x = st t1m rhoi' && st bxm rhoi' = st t1m rhoi' } ;
              res
907 908 909 910
            | _ -> let by' = BA.get rhob y in
              match by' with
                | Cons (Assign by') _ -> (*checkit rho y it2 ;*)
                  let bym = by'.model_fo_term_field in
911 912
                  let rhobm = rho.unifier_base_model in
                  let rhoi = rho.unifier in
913
                  assert { sdata_inv (Assign by') } ;
914 915
                  assert { bym = rhobm y (*/\ mem y fv*) } ;
                  assert { st bym rhoi = sc rhobm rhoi y = rhoi y = st t2m rhoi
916
                    && forall s:int -> (fo_term int int).
917
                      st bym (sc rhoi s) = st t2m (sc rhoi s) } ;
918
                  let res = unification_term t1 by' lv rhob rho lp (*fv s it1 (it2-1)*) in
919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940
                  let rhoi' = res.final_unifier.unifier in
                  assert { st bym rhoi' = sc rhobm rhoi' y
                    = rhoi' y = st t2m rhoi' && st bym rhoi' = st t2m rhoi' } ;
                  res
                | _ -> bottomvar rhob rho y ;
                  bottomvar rhob rho x ;
                  if x < y
                  then assign x t2 lv rhob rho lp (*fv s*)
                  else assign y t1 lv rhob rho lp
              end
          end
      | NLC_App f1 l1 , NLC_App f2 l2 ->
        let l1m = l1.model_fo_term_list_field in
        let l2m = l2.model_fo_term_list_field in
        let f1m = f1.model_symbol_field in
        let f2m = f2.model_symbol_field in
        assert { t1m = App f1m l1m } ;
        assert { t2m = App f2m l2m } ;
        match destruct_symbol f1 , destruct_symbol f2 with
          | NLCVar_symbol f1 , NLCVar_symbol f2 -> if f1 = f2
            then (
              assert { forall l1 l2:fo_term_list int int,
941
                s1 s2:int -> (fo_term int int).
942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961
                st (App f1m l1) s1 = st (App f2m l2) s2 <->
                stl l1 s1 = stl l2 s2 } ;
                unification_term_list l1 l2 lv rhob rho lp (*fv s it1 it2*)
              )
            else raise UnificationFailure
        end
      | NLCVar_fo_term x , NLC_App f l ->
        let fm = f.model_symbol_field in
        let lm = l.model_fo_term_list_field in
        assert { t1m = Var_fo_term x } ;
        assert { t2m = App fm lm } ;
        let bx = BA.get rhob x in
        match bx with
          | Cons (Assign bx) _ ->
            (*checkit rho x it1 ;*)
            let bxm = bx.model_fo_term_field in
            let rhobm = rho.unifier_base_model in
            let rhoi = rho.unifier in
            assert { bxm = rhobm x } ;
            assert { st bxm rhoi = sc rhobm rhoi x = rhoi x = st t1m rhoi
962
              && forall s:int -> (fo_term int int).
963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984
                st bxm (sc rhoi s) = st t1m (sc rhoi s) } ;
            let res = unification_term bx t2 lv rhob rho lp (*
              fv s (it1-1) it2*) in
            let rhoi' = res.final_unifier.unifier in
            assert { st bxm rhoi' = sc rhobm rhoi' x
              = rhoi' x = st t1m rhoi' && st bxm rhoi' = st t1m rhoi' } ;
            res
          | _ -> assign x t2 lv rhob rho lp (*fv s*)
        end
      | NLC_App f l , NLCVar_fo_term x ->
        let fm = f.model_symbol_field in
        let lm = l.model_fo_term_list_field in
        assert { t2m = Var_fo_term x } ;
        assert { t1m = App fm lm } ;
        let bx = BA.get rhob x in
        match bx with
          | Cons (Assign bx) _ -> (*checkit rho x it2 ;*)
            let bxm = bx.model_fo_term_field in
            let rhobm = rho.unifier_base_model in
            let rhoi = rho.unifier in
            assert { bxm = rhobm x } ;
            assert { st bxm rhoi = sc rhobm rhoi x = rhoi x = st t2m rhoi
985
              && forall s:int -> (fo_term int int).
986 987 988 989 990 991 992 993 994 995
                st bxm (sc rhoi s) = st t2m (sc rhoi s) } ;
            let res = unification_term t1 bx lv rhob rho lp
              (*fv s it1 (it2-1)*) in
            let rhoi' = res.final_unifier.unifier in
            assert { st bxm rhoi' = sc rhobm rhoi' x
              = rhoi' x = st t2m rhoi' && st bxm rhoi' = st t2m rhoi' } ;
            res
          | _ -> assign x t1 lv rhob rho lp (*fv s*)
        end
    end
996

997
  with unification_term_list (t1 t2:nlimpl_fo_term_list) (lv:ref (list int))
998
    (rhob:subst) (ghost rho:unifier_subst) (ghost lp:int -> bool)
999 1000 1001 1002 1003 1004 1005 1006 1007 1008
    (*(ghost fv s:S.set int) (ghost it1 it2:int)*) :
    unification_return
    (* Invariant requirements. *)
    requires { nlimpl_fo_term_list_ok t1 }
    requires { nlimpl_fo_term_list_ok t2 }
    requires { unifier_subst_ok rhob rho }
    requires { forall y:int. is_fo_term_free_var_in_fo_term_list y
      t1.model_fo_term_list_field -> y >= 0 }
    requires { forall y:int. is_fo_term_free_var_in_fo_term_list y
      t2.model_fo_term_list_field -> y >= 0 }
1009

1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022
    (* Variant requirements. *)
    (*requires { forall x:int.
      is_fo_term_free_var_in_fo_term_list x t1.model_fo_term_list_field ->
        mem x fv }
    requires { forall x:int.
      is_fo_term_free_var_in_fo_term_list x t2.model_fo_term_list_field ->
        mem x fv }
    requires { forall x y:int.
      mem x fv /\
      is_fo_term_free_var_in_fo_term y (eval rho.unifier_base_model x) ->
        mem y fv }
    requires { forall x:int.
      mem x fv /\ AS.model rho.unifier_base x = None -> mem x s }
1023
    requires { forall sp:int -> (fo_term int int).
1024 1025 1026 1027
      let tm = t1.model_fo_term_list_field in
      power_rel rho.unifier_base_model it1 sp ->
      stl tm sp = stl tm rho.unifier }
    requires { it1 >= 0 }
1028
    requires { forall sp:int -> (fo_term int int).
1029 1030 1031 1032
      let tm = t2.model_fo_term_list_field in
      power_rel rho.unifier_base_model it2 sp ->
      stl tm sp = stl tm rho.unifier }
    requires { it2 >= 0 }*)
1033

1034 1035 1036
    (* Invariant ensures. *)
    ensures { unifier_subst_ok rhob result.final_unifier }
    ensures { precede (old rhob) rhob }
1037

1038 1039 1040 1041 1042 1043
    requires { forall x:int. mem x !lv ->
      lp x /\ x >= 0 }
    requires { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
    ensures { forall x:int. mem x !lv ->
      lp x /\ x >= 0 }
    ensures { forall x:int. unassigned (current_timestamp rhob) x -> lp x }
1044

1045 1046 1047
    (* Unifier properties. *)
    ensures { sc rho.unifier result.unifier_factor =
      result.final_unifier.unifier }
1048
    ensures { forall s:int -> (fo_term int int).
1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060
      let s' = sc rho.unifier s in
      stl t1.model_fo_term_list_field s' = stl t2.model_fo_term_list_field s' ->
      s' = sc result.final_unifier.unifier s }
    ensures { let s0 = result.final_unifier.unifier in
      stl t1.model_fo_term_list_field s0 =
        stl t2.model_fo_term_list_field s0 }
    ensures { let s0 = result.final_unifier.unifier in
      let s1 = rho.unifier_base_model in
      sc s0 s1 = s0 = sc s1 s0 }
    ensures { let s0 = result.final_unifier.unifier in
      let s1 = rho.unifier in
      sc s0 s1 = s0 = sc s1 s0 }
1061

1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076
    (* Variant postconditions. *)
    (*ensures { result.unassigned_set = s ->
      rho.unifier = result.final_unifier.unifier /\
      rho.unifier_base_model = result.final_unifier.unifier_base_model }
    ensures { result.unassigned_set <> s ->
      cardinal result.unassigned_set < cardinal s }
    ensures { forall x:int.
      mem x fv /\ AS.model result.final_unifier.unifier_base x = None ->
      mem x result.unassigned_set }
    ensures { forall x y:int.
      mem x fv /\
      is_fo_term_free_var_in_fo_term y (
        eval result.final_unifier.unifier_base_model x)
        -> mem y fv }*)
    raises { UnificationFailure -> precede (old rhob) rhob /\ correct rhob
1077
    (*-> forall s:int -> (fo_term int int).
1078 1079 1080
      let s' = sc rho.unifier s in
      stl t1.model_fo_term_list_field s' <>
        stl t2.model_fo_term_list_field s'*) }
1081
    diverges (* variant { 0 } *)
1082
     (*variant { S.cardinal s , it1 + it2 ,
1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098
      size_fo_term_list t1.model_fo_term_list_field +
      size_fo_term_list t2.model_fo_term_list_field }*)
  =
    let t1m = t1.model_fo_term_list_field in
    let t2m = t2.model_fo_term_list_field in
    match destruct_fo_term_list t1 , destruct_fo_term_list t2 with
      | NLC_FONil , NLC_FONil -> { final_unifier = rho ;
        unifier_factor = subst_id_fo_term (*;
        unassigned_set = s*) }
      | NLC_FOCons u1 q1 , NLC_FOCons u2 q2 ->
        let u1m = u1.model_fo_term_field in
        let u2m = u2.model_fo_term_field in
        let q1m = q1.model_fo_term_list_field in
        let q2m = q2.model_fo_term_list_field in
        assert { t1m = FOCons u1m q1m /\ t2m = FOCons u2m q2m } ;
        assert { forall a c:fo_term int int,b d:fo_term_list int int,
1099
          s1 s2:int -> (fo_term int int).
1100 1101 1102 1103 1104 1105
          stl (FOCons a b) s1 = stl (FOCons c d) s2 <->
          st a s1 = st c s2 /\ stl b s1 = stl d s2 } ;
        let rho0 = rho.unifier in
        let rho2 = unification_term_list q1 q2 lv rhob rho lp (*fv s it1 it2*) in
        let rho2f = rho2.final_unifier in
        let rho20 = rho2f.unifier in
1106
        assert { forall s:int -> (fo_term int int).
1107 1108 1109 1110 1111 1112 1113 1114
          stl t1m (sc rho0 s) = stl t2m (sc rho0 s) ->
            stl q1m (sc rho0 s) = stl q2m (sc rho0 s) &&
            sc rho0 s = sc rho20 s &&
            st u1m (sc rho20 s) = st u2m (sc rho20 s) } ;
        (*let u = rho2f.iteration in*)
        (*let ghost aux_ (u_:unit) : (int,int)
          returns { (it'1,it'2) ->
            (rho2.unassigned_set = s -> it1=it'1 /\ it2 = it'2) /\
1115
            (forall sp:int -> (fo_term int int).
1116 1117
              power_rel rho2f.unifier_base_model it'1 sp ->
              stl t1m sp = stl t1m rho20) /\
1118
            (forall sp:int -> (fo_term int int).
1119 1120 1121 1122 1123 1124
              power_rel rho2f.unifier_base_model it'2 sp ->
              stl t2m sp = stl t2m rho20) /\
              it'1 >= 0 /\
              it'2 >= 0 }
        = if rho2.unassigned_set = s
          then (it1,it2)
1125
          else ( assert { forall sp:int -> (fo_term int int).
1126 1127 1128 1129 1130 1131
            power_rel rho2f.unifier_base_model u sp ->
            sp = rho2f.unifier } ; (u,u) ) in
        let (it1,it2) = aux_ () in*)
        let rho3 = unification_term u1 u2 lv rhob rho2f lp
          (*fv rho2.unassigned_set it1 it2*) in
        let rho30 = rho3.final_unifier.unifier in
1132
        assert { forall s:int -> (fo_term int int).
1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143
          stl t1m (sc rho0 s) = stl t2m (sc rho0 s) ->
            sc rho0 s = sc rho20 s &&
            st u1m (sc rho20 s) = st u2m (sc rho20 s) &&
            sc rho30 s = sc rho0 s } ;
        let rhof3 = rho3.unifier_factor in
        assert { stl q1m rho30 = stl (stl q1m rho20) rhof3
          = stl (stl q2m rho20) rhof3 = stl q2m rho30 } ;
        { final_unifier = rho3.final_unifier ;
          unifier_factor = ghost sc rho2.unifier_factor rho3.unifier_factor (*;
          unassigned_set = rho3.unassigned_set*) }
      | NLC_FONil , NLC_FOCons u q ->
1144
        (*assert { forall s:int -> (fo_term int int).
1145 1146 1147 1148 1149 1150
          subst_fo_term_list t1m subst_id_symbol s = FONil /\
          let um = u.model_fo_term_field in
          let qm = q.model_fo_term_list_field in
          stl t2m s = FOCons (st um s) (stl qm s) } ;*)
        raise UnificationFailure
      | NLC_FOCons u q , NLC_FONil ->
1151
        (*assert { forall s:int -> (fo_term int int).
1152 1153 1154 1155 1156 1157
          subst_fo_term_list t2m subst_id_symbol s = FONil /\
          let um = u.model_fo_term_field in
          let qm = q.model_fo_term_list_field in
          stl t1m s = FOCons (st um s) (stl qm s) } ;*)
        raise UnificationFailure
    end
1158

1159 1160 1161
  let conflict (t1 t2:nlimpl_fo_term_list) (rhob:subst) (ghost rho:unifier_subst) : unit
    requires { sdata_inv (PConflict t1 t2) }
    requires { unifier_subst_ok rhob rho }
MARCHE Claude's avatar
MARCHE Claude committed
1162
    diverges
1163 1164 1165 1166 1167 1168 1169 1170 1171 1172
    ensures { unifier_subst_ok rhob rho }
    (* Useless : trivial consequence of unifier_subst_ok rhob rho.
    ensures { smodel (current_timestamp rhob) =
      smodel (current_timestamp (old rhob)) }*)
    ensures { precede (old rhob) rhob }
    (*raises { UnificationFailure -> unifier_subst_ok rhob rho }*)
    (*raises { UnificationFailure -> (current_timestamp rhob).table =
      (current_timestamp (old rhob).table }*)
    raises { UnificationFailure -> precede (old rhob) rhob /\ correct rhob }
  =
1173
    label Init in
1174 1175 1176 1177 1178
    let l = ref Nil in
    let t = stamp rhob in
    let lp = unassigned_vars rhob in
    let u = try Some (unification_term_list t1 t2 l rhob rho lp)
    with UnificationFailure -> None end in
1179
    label Mid0 in
1180 1181 1182 1183
    match u with
      | Some _ -> match !l with
          | Nil -> raise UnificationFailure
          | Cons v _ -> backtrack t rhob ;
1184 1185
            assert { backtrack_to (rhob at Init) (rhob at Mid0) rhob } ;
            label Middle in
1186 1187 1188 1189 1190 1191 1192 1193 1194
            add v (PConflict t1 t2) rhob ;
            assert { (forall t:timesubst,x:int. unassigned t x ->
              let u = smodel t x in match table t x with
                | Nil -> u = Var_fo_term x
                | Cons (PConflict _ _) _ -> u = Var_fo_term x
                | _ -> false end &&
              u = Var_fo_term x) &&
              (forall x:int.
              x <> v -> smodel (current_timestamp rhob) x =
1195
                smodel (current_timestamp (rhob at Middle)) x) &&
1196
              lp v &&
1197
              unassigned (current_timestamp (rhob at Middle)) v &&
1198 1199
              unassigned (current_timestamp rhob) v &&
              (let u = current_timestamp rhob in
1200
               let u' = current_timestamp (rhob at Middle) in
1201 1202 1203 1204 1205 1206
               let ut = u.time in
               let utb = u.table in
               let us = u.size in
               u = { time = u.time ; table = u.table ; size = u.size } /\
               u' = { time = u'.time ; table = u'.table ; size = u'.size }) &&
              smodel (current_timestamp rhob) v = Var_fo_term v =
1207
              smodel (current_timestamp (rhob at Middle)) v &&
1208
              extensionalEqual (smodel (current_timestamp rhob))
1209 1210
                (smodel (current_timestamp (rhob at Middle))) &&
              smodel (current_timestamp rhob) = smodel (current_timestamp (rhob at Middle)) } ;
1211
            assert { (forall x:int.
1212
              x <> v -> unassigned (current_timestamp (rhob at Middle)) x ->
1213 1214 1215
              unassigned (current_timestamp rhob) x) &&
              (forall x:int.
                unifier_base_model rho x = Var_fo_term x ->
1216
                unassigned (current_timestamp (rhob at Middle)) x &&
1217 1218 1219
                unassigned (current_timestamp rhob) x) }
        end
      | None -> backtrack t rhob ;
1220
        assert { backtrack_to (rhob at Init) (rhob at Mid0) rhob }
1221
    end
1222

1223 1224 1225 1226 1227 1228
  let rec conflicts (lv:list sdata) (rhob:subst) (ghost rho:unifier_subst) : unit
    requires { list_forall sdata_inv lv }
    requires { unifier_subst_ok rhob rho }
    ensures { unifier_subst_ok rhob rho }
    (*ensures { smodel (current_timestamp rhob) = smodel (current_timestamp (old rhob)) }*)
    ensures { precede (old rhob) rhob }
MARCHE Claude's avatar
MARCHE Claude committed
1229
    diverges (* variant { lv } *)
1230 1231 1232 1233 1234 1235 1236
    raises { UnificationFailure -> correct rhob /\ precede (old rhob) rhob }
  =
    match lv with
      | Nil -> ()
      | Cons (Assign _) q -> conflicts q rhob rho
      | Cons (PConflict t1 t2) q -> conflict t1 t2 rhob rho ; conflicts q rhob rho
    end
1237

1238 1239 1240 1241 1242
  let rec unif_conflicts (lv:list int) (rhob:subst) (ghost rho:unifier_subst) : unit
    requires { forall x:int. mem x lv -> x >= 0 }
    requires { unifier_subst_ok rhob rho }
    ensures { unifier_subst_ok rhob rho }
    ensures { precede (old rhob) rhob }
MARCHE Claude's avatar
MARCHE Claude committed
1243
    diverges (* variant { lv } *)
1244 1245 1246 1247 1248 1249
    raises { UnificationFailure -> correct rhob /\ precede (old rhob) rhob }
  =
    match lv with
      | Nil -> ()
      | Cons v0 q -> conflicts (get rhob v0) rhob rho ; unif_conflicts q rhob rho
    end
1250

1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261
  let unify_term_list (t1 t2:nlimpl_fo_term_list) (watch:ref (list int))
    (rhob:subst) (ghost rho:unifier_subst) :
    unification_return
    requires { !watch = Nil }
    requires { nlimpl_fo_term_list_ok t1 }
    requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
      t1.model_fo_term_list_field -> x >= 0 }
    requires { nlimpl_fo_term_list_ok t2 }
    requires { forall x:int. is_fo_term_free_var_in_fo_term_list x
      t2.model_fo_term_list_field -> x >= 0 }
    requires { unifier_subst_ok rhob rho }
MARCHE Claude's avatar
MARCHE Claude committed
1262
    diverges
1263 1264 1265
    ensures { unifier_subst_ok rhob result.final_unifier }
    ensures { result.final_unifier.unifier = sc rho.unifier result.unifier_factor }
    ensures { precede (old rhob) rhob }
1266
    ensures { forall s:int -> (fo_term int int).
1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278
      let s' = sc rho.unifier s in
      stl t1.model_fo_term_list_field s' = stl t2.model_fo_term_list_field s' ->
      s' = sc result.final_unifier.unifier s }
    ensures { let s0 = result.final_unifier.unifier in
      stl t1.model_fo_term_list_field s0 =
        stl t2.model_fo_term_list_field s0 }
    raises { UnificationFailure -> correct rhob /\ precede (old rhob) rhob }
  =
    let lp = unassigned_vars rhob in
    let u = unification_term_list t1 t2 watch rhob rho lp in
    unif_conflicts !watch rhob u.final_unifier ;
    u
1279

1280 1281 1282 1283 1284
  (*let rec conflicts (lv:list sdata) (rhob:subst) (ghost rho:unifier_subst) : unit
    requires { list_forall sdata_inv lv }
    requires { unifier_subst_ok rhob rho }
    ensures { unifier_subst_ok rhob rho }
    raises { UnificationFailure ->  }*)
1285

1286 1287 1288 1289 1290
  (*
  let rec ghost term_free_var_set (t:fo_term int int) (it:int)
    (rho:unifier_subst) : set int
    requires { unifier_subst_ok rho }
    requires { it >= 0 }
1291
    requires { forall sp:int -> (fo_term int int).
1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309
      power_rel rho.unifier_base_model it sp ->
      st t sp = st t rho.unifier }
    ensures { forall x:int. is_fo_term_free_var_in_fo_term x t ->
      mem x result }
    ensures { forall x y:int.
      is_fo_term_free_var_in_fo_term x (eval rho.unifier_base_model y) /\
      mem y result -> mem x result }
    variant { it , size_fo_term t }
  =
    match t with
      | Var_fo_term x -> let rho0 = rho.unifier_base_model in
        let rhoi = rho.unifier in
        if it = 0
        then (assert { t = st t subst_id_fo_term = st t rhoi &&
          t = st t (sc rhoi rho0) = st t rho0 && rho0 x = t } ;
          assert { forall y:int. is_fo_term_free_var_in_fo_term y (rho0 x) ->
            y = x } ;
          add x empty)
1310
        else
1311
          let t2 = eval rho0 x in
1312
          (assert { forall sp:int -> (fo_term int int).
1313 1314 1315 1316 1317
            power_rel rho0 (it-1) sp ->
            power_rel rho0 it (sc rho0 sp) &&
            st t2 sp = st t (sc rho0 sp) = st t rhoi =
            st t (sc rho0 rhoi) = st t2 rhoi && st t2 sp = st t2 rhoi } ;
            add x (term_free_var_set t2 (it-1) rho))
1318
      | App _ l -> assert { forall s s2:int -> (fo_term int int).
1319 1320 1321
        st t s = st t s2 <-> stl l s = stl l s2 } ;
        term_list_free_var_set l it rho
    end
1322

1323 1324 1325 1326
  with ghost term_list_free_var_set (t:fo_term_list int int) (it:int)
    (rho:unifier_subst) : set int
    requires { unifier_subst_ok rho }
    requires { it >= 0 }