enrich junkrefs with
   predicates 
      validrefs : string × references × javatype × store;
      comment: last reference
                        may be null.;
       
      path∃ : string × reference × reference × store;
      comment: based on validrefs, second ref may be null.;
       
      path∃+ : string × reference × reference × store;
      comment: stronger version of path∃, last ref could be invalid.;
       
      step∃ : string × reference × reference × store;
      cyclic : string × reference × store;
      comment: based on validrefs.;
       
   
   axioms 
      cyclic-def :  ⊦ cyclic(str, r, st) ↔ (∃ refs. dups(refs) ∧ refs .first = r ∧ validrefs(str, refs, mkclasstype(`java.lang.Object' .class), st));
      pathex-def
      : ⊦ 
          path∃(str, r, r0, st)
        ↔ (∃ refs. refs ≠ [] ∧ refs .first = r ∧ refs .last = r0 ∧ validrefs(str, refs, mkclasstype(`java.lang.Object' .class), st));
      pathex-plus-def
      : ⊦ 
          path∃+(str, r, r0, st)
        ↔   r = r0
          ∨ (∃ refs. refs ≠ [] ∧ refs .first = r ∧ validrefs(str, refs, mkclasstype(`java.lang.Object' .class), st) ∧ step∃(str, refs .last, r0, st));
      step-exists-def
      : ⊦ 
          step∃(str, r, r0, st)
        ↔     r ≠ jvmref ∧ is_classtype(st[r -- _type] .type)
            ∧ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ st[r -- fs '] .refval = r0)
          ∨   is_arraytype(st[r -- _type] .type)
            ∧ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ st[r -- i '] .refval = r0);
      validrefs-empty :  ⊦ validrefs(str, [], ty, st);
      used for : s, ls;
       
      validrefs-null :  ⊦ r = jvmref → (validrefs(str, r ' + refs, ty, st) ↔ refs = []);
      validrefs-is-junk :  ⊦ r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ ty) → ¬ validrefs(str, r ' + refs, ty, st);
      validrefs-class
      : ⊦ 
          is_obj(str, r, st) ∧ st[r -- _type] .type ≤ ty
        → (  validrefs(str, r ' + refs, ty, st)
           ↔   refs = []
             ∨ (∃ fs. 
                   fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ refs .first = st[r -- fs '] .refval
                 ∧ validrefs(str, refs, fs .type, st)));
      validrefs-array
      : ⊦ 
          is_array(str, r, st) ∧ st[r -- _type] .type ≤ ty
        → (  validrefs(str, r ' + refs, ty, st)
           ↔   refs = []
             ∨ (∃ i. 
                   0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ refs .first = st[r -- i '] .refval
                 ∧ validrefs(str, refs, st[r -- _type] .type .type, st)));
end enrich