This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| cyclic-def | ⊦ cyclic(str, r, st) ↔ (∃ refs. dups(refs) ∧ refs .first = r ∧ validrefs(str, refs, mkclasstype(`java.lang.Object' .class), st)) | An Axiom |
| 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))) | An Axiom |
| 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))) | An Axiom |
| validrefs-is-junk | ⊦ r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ ty) → ¬ validrefs(str, r ' + refs, ty, st) | An Axiom |
| validrefs-null | ⊦ r = jvmref → (validrefs(str, r ' + refs, ty, st) ↔ refs = []) | An Axiom |
| validrefs-empty | ⊦ validrefs(str, [], ty, st) | An Axiom |
| pathex-def | ⊦ path∃(str, r, r0, st) ↔ (∃ refs. refs ≠ [] ∧ refs .first = r ∧ refs .last = r0 ∧ validrefs(str, refs, mkclasstype(`java.lang.Object' .class), st)) | An Axiom |
| 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) | An Axiom |
| 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)) | An Axiom |
| cyclic-addarray-noreftype | ⊦ (∀ val. val ∈ vals → okprimtype(val, ty0)) ∧ is_primtype(ty0) → ¬ cyclic(str, r, addarray(r, ty0, vals, st)) | A User Theorem |
| cyclic-addarray-other | ⊦ ¬ cyclic(str, r, st) ∧ ¬ junkref(str, r, st) ∧ newref(r0, st) ∧ r ≠ r0 → ¬ cyclic(str, r, addarray(r0, ty, vals, st)) | A User Theorem |
| cyclic-addarray-this | ⊦ newref(r, st) → ¬ cyclic(str, r, addarray(r, ty, i, st)) | A User Theorem |
| cyclic-addarray-this-01 | ⊦ newref(r, st) ∧ (∀ r. refval(r) ∈ vals → ¬ junkref(str, r, st) ∧ ¬ cyclic(str, r, st)) → ¬ cyclic(str, r, addarray(r, ty, vals, st)) | A User Theorem |
| cyclic-addobj | ⊦ (∀ fs, r0. fs ' × refval(r0) ∈ fis → ¬ junkref(str, r0, st) ∧ ¬ cyclic(str, r0, st)) ∧ newref(r, st) ∧ is_obj(str, r, addobj(r, class, fis, st)) ∧ ¬ _type ∈ fis ∧ validfieldinits(fis, st) ∧ fis .keys = instfields(class) → (cyclic(str, r, addobj(r, class, fis, st)) ↔ (∃ fs. fs ' ∈ fis ∧ fs ' ∈ instfields(class) ∧ fis[fs '] = refval(r))) | A User Theorem |
| cyclic-addobj-other | ⊦ ¬ cyclic(str, r, st) ∧ ¬ junkref(str, r, st) ∧ newref(r0, st) ∧ r ≠ r0 → ¬ cyclic(str, r, addobj(r0, class, fis, st)) | A User Theorem |
| cyclic-addobj-other-01 | ⊦ ¬ junkref(str, r, st) ∧ newref(r0, st) ∧ r ≠ r0 → (cyclic(str, r, addobj(r0, class, fis, st)) ↔ cyclic(str, r, st)) | A User Theorem |
| cyclic-addrefarray | ⊦ (∀ val. val ∈ vals → ¬ junkref(str, val .refval, st) ∧ ¬ cyclic(str, val .refval, st) ∧ is_referencevalue(val) ∧ (val .refval ≠ jvmref → st[val .refval -- _type] .type ≤ ty)) ∧ newref(r, st) ∧ type∃(str, ty) ∧ is_reftype(ty) ∧ ty .jtelemtype ≠ void_type ∧ ty .jtelemtype ≠ abstract_type → ¬ cyclic(str, r, addarray(r, ty, vals, st)) | A User Theorem |
| cyclic-array | ⊦ cyclic(str, r0, st) ∧ is_array(str, r, st) ∧ st[r -- i '] = refval(r0) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_reftype(st[r -- _type] .type .type) ∧ st[r0 -- _type] .type ≤ st[r -- _type] .type .type → cyclic(str, r, st) | A User Theorem |
| cyclic-class | ⊦ cyclic(str, r0, st) ∧ is_obj(str, r, st) ∧ st[r -- fs '] = refval(r0) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_reftype(fs .type) ∧ st[r0 -- _type] .type ≤ fs .type → cyclic(str, r, st) | A User Theorem |
| cyclic-def-object | ⊦ is_obj(str, r, st) → (cyclic(str, r, st) ↔ (∃ refs. dups(refs) ∧ refs .first = r ∧ validrefs(str, refs, st[r -- _type] .type, st))) | A User Theorem |
| cyclic-def-shortest | ⊦ cyclic(str, r, st) ↔ (∃ refs, r0. ¬ dups(refs) ∧ r0 ∈ refs ∧ refs .first = r ∧ validrefs(str, refs + r0 ', st[r -- _type] .type, st)) | A User Theorem |
| cyclic-def-simple | ⊦ cyclic(str, r, st) ↔ (∃ refs. dups(refs) ∧ refs .first = r ∧ validrefs(str, refs, st[r -- _type] .type, st)) | A User Theorem |
| cyclic-delete | ⊦ ¬ cyclic(str, r, st) → ¬ cyclic(str, r, st -- r0) | A User Theorem |
| cyclic-not-null | ⊦ ¬ cyclic(str, jvmref, st) | A User Theorem |
| cyclic-one | ⊦ st[r -- fs '] = refval(r) ∧ is_obj(str, r, st) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ st[r -- _type] .type ≤ fs .type → cyclic(str, r, st) | A User Theorem |
| cyclic-put-badarrayfield | ⊦ ¬ junkref(str, r, st) ∧ fs ' ≠ _type ∧ is_arraytype(st[r0 -- _type] .type) ∧ fs ' ≠ _length → (cyclic(str, r, st[r0 -- fs ', val]) ↔ cyclic(str, r, st)) | A User Theorem |
| cyclic-put-badclassfield | ⊦ ¬ junkref(str, r, st) ∧ fs ' ≠ _type ∧ is_classtype(st[r0 -- _type] .type) ∧ ¬ fs ' ∈ instfields(st[r0 -- _type] .type .class) → (cyclic(str, r, st[r0 -- fs ', val]) ↔ cyclic(str, r, st)) | A User Theorem |
| cyclic-put-nopathex | ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ junkref(str, r, st) ∧ sk ≠ _type → (cyclic(str, r, st[r0 -- sk, val]) ↔ cyclic(str, r, st)) | A User Theorem |
| cyclic-put-statfield | ⊦ ¬ cyclic(str, r, st) → ¬ cyclic(str, r, st[jvmref -- sk, val]) | A User Theorem |
| cyclic-put-statfield-01 | ⊦ cyclic(str, r, st[jvmref -- sk, val]) ↔ cyclic(str, r, st) | A User Theorem |
| cyclic-putbar | ⊦ okbytearray(r1, st) → (cyclic(str, r, putByteArray(bytes, r1, i, st)) ↔ cyclic(str, r, st)) | A User Theorem |
| cyclic-putbar-01 | ⊦ okbytearray(r1, st) ∧ r ≠ r1 ∧ ¬ cyclic(`docs2store', r, st) → ¬ cyclic(`docs2store', r, putByteArray(bytes, r1, i, st)) | A User Theorem |
| cyclic-putbar-02 | ⊦ okbytearray(r1, st) ∧ r ≠ r1 ∧ cyclic(`docs2store', r, putByteArray(bytes, r1, st)) → cyclic(`docs2store', r, st) | A User Theorem |
| cyclic-putbar-03 | ⊦ okbytearray(r1, st) ∧ r ≠ r1 ∧ ¬ cyclic(`docs2store', r, st) → ¬ cyclic(`docs2store', r, putByteArray(bytes, r1, st)) | A User Theorem |
| cyclic-putbar-04 | ⊦ okbytearray(r1, st) ∧ r ≠ r1 ∧ cyclic(`docs2store', r, putByteArray(bytes, r1, i, st)) → cyclic(`docs2store', r, st) | A User Theorem |
| cyclic-putbar-05 | ⊦ okbytearray(r1, st) ∧ ¬ cyclic(`docs2store', r, st) → ¬ cyclic(`docs2store', r, putByteArray(bytes, r1, st)) | A User Theorem |
| cyclic-putbyte | ⊦ okbytearray(r1, st) ∧ cyclic(str, r, st[r1 -- i ', byteval(by)]) → cyclic(str, r, st) | A User Theorem |
| cyclic-putbyte-01 | ⊦ okbytearray(r1, st) → (cyclic(str, r, st[r1 -- i ', byteval(by)]) ↔ cyclic(str, r, st)) | A User Theorem |
| cyclic-subset | ⊦ ¬ cyclic(str, r, st) ∧ st ⊆ st0 ∧ ¬ junkref(str, r, st) → ¬ cyclic(str, r, st0) | A User Theorem |
| cyclic-subset-01 | ⊦ cyclic(str, r, st) ∧ st ⊆ st0 ∧ ¬ junkref(str, r, st) → cyclic(str, r, st0) | A User Theorem |
| exvalidrefs | ¬ junkref(str, r, st), ¬ cyclic(str, r, st), is_obj(str, r, st), r ≠ jvmref, ∀ ty. type∃(str, ty) → (ty ≤ st[r -- _type] .type ↔ ty = st[r -- _type] .type), ∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ fs .type = st[r -- _type] .type ⊦ ∃ refs. validrefs(str, refs, st[r -- _type] .type, st) ∧ refs ≠ [] ∧ refs .first = r ∧ refs .last = jvmref | A User Theorem |
| exvalidrefs-03 | ¬ junkref(str, r, st), ¬ cyclic(str, r, st), is_obj(str, r, st), r ≠ jvmref, ∃ fs, class. fs ' ∈ instfields(class) ∧ fs .type ≤ mkclasstype(class) ∧ st[r -- _type] .type ≤ fs .type ⊦ ∃ refs. validrefs(str, refs, st[r -- _type] .type, st) ∧ refs ≠ [] ∧ refs .first = r ∧ refs .last = jvmref | A User Theorem |
| exvalidrefs-maxlength | ¬ junkref(str, r, st), ¬ cyclic(str, r, st) ⊦ ∃ refs. validrefs(str, refs, st[r -- _type] .type, st) ∧ refs ≠ [] ∧ ¬ dups(refs) ∧ refs .first = r ∧ ¬ has_reffield(refs .last, st) | A User Theorem |
| exvalidrefs-nodups | ¬ junkref(str, r, st), ¬ cyclic(str, r, st), is_obj(str, r, st), r ≠ jvmref, ∃ fs, class. fs ' ∈ instfields(class) ∧ fs .type ≤ mkclasstype(class) ∧ st[r -- _type] .type ≤ fs .type ⊦ ∃ refs. validrefs(str, refs, st[r -- _type] .type, st) ∧ refs ≠ [] ∧ ¬ dups(refs) ∧ refs .first = r ∧ refs .last = jvmref | A User Theorem |
| junkref-put-nopathex | ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ junkref(str, r, st) ∧ sk ≠ _type → ¬ junkref(str, r, st[r0 -- sk, val]) | A User Theorem |
| junkref-put-nopathex-equiv-01 | ⊦ ¬ path∃(str, r, r0, st) ∧ sk ≠ _type ∧ is_valid_ref(str, r0, st) → (junkref(str, r, st[r0 -- sk, val]) ↔ junkref(str, r, st)) | A User Theorem |
| junkref-put-nopathexplus-equiv | ⊦ ¬ path∃+(str, r, r0, st) ∧ sk ≠ _type → (junkref(str, r, st[r0 -- sk, val]) ↔ junkref(str, r, st)) | A User Theorem |
| junkref-update | ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ _type ∈ fis ∧ ¬ junkref(str, r, st) → ¬ junkref(str, r, update(r0, fis, st)) | A User Theorem |
| junkref-update-equiv | ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ _type ∈ fis ∧ is_valid_ref(str, r0, st) ∧ validFields(r0, fis, st) → (junkref(str, r, update(r0, fis, st)) ↔ junkref(str, r, st)) | A User Theorem |
| junkrefs-put-nopathex | ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ junkrefs(str, refs, ty, st) ∧ sk ≠ _type ∧ refs ≠ [] ∧ refs .first = r → ¬ junkrefs(str, refs, ty, st[r0 -- sk, val]) | A User Theorem |
| junkrefs-put-nopathex-equiv | ⊦ ¬ path∃(str, r, r0, st) ∧ is_valid_ref(str, r0, st) ∧ sk ≠ _type ∧ refs ≠ [] ∧ refs .first = r → (junkrefs(str, refs, ty, st[r0 -- sk, val]) ↔ junkrefs(str, refs, ty, st)) | A User Theorem |
| junkrefs-put-nopathexplus-equiv | ⊦ ¬ path∃+(str, r, r0, st) ∧ sk ≠ _type ∧ refs ≠ [] ∧ refs .first = r → (junkrefs(str, refs, ty, st[r0 -- sk, val]) ↔ junkrefs(str, refs, ty, st)) | A User Theorem |
| nopathex-update | ⊦ ¬ junkref(str, r, st) ∧ ¬ _type ∈ fis ∧ ¬ path∃(str, r, r0, st) → ¬ path∃(str, r, r0, update(r0, fis, st)) | A User Theorem |
| okarray-put-nopath | ⊦ ¬ path∃(str, r, r0, st) ∧ is_valid_ref(str, r0, st) ∧ okarray(r, byte_type, st) → okarray(r, byte_type, st[r0 -- sk, val]) | A User Theorem |
| okarray-put-nopath-01 | ⊦ ¬ path∃(str, val .refval, r0, st) ∧ is_valid_ref(str, r0, st) ∧ okarray(val, byte_type, i, st) → okarray(val, byte_type, i, st[r0 -- sk, val1]) | A User Theorem |
| okbar-nopath | ⊦ r ≠ r0 ∧ okbytearray(r, st) → ¬ path∃(str, r, r0, st) | A User Theorem |
| pathex-addobj | ⊦ validFields(r, fis, addobj(r, class, fis, st)) ∧ fis .keys = instfields(class) ∧ newref(r, st) ∧ validref(str, r, mkclasstype(class), addobj(r, class, fis, st)) ∧ fs ' × refval(r1) ∈ fis ∧ fs ' ∈ instfields(class) ∧ path∃(str, r1, r0, st) → path∃(str, r, r0, addobj(r, class, fis, st)) | A User Theorem |
| pathex-array | ⊦ is_array(str, r, st) ∧ r ≠ r0 → ( path∃(str, r, r0, st) ↔ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ ( st[r -- i '] .refval ≠ jvmref ∧ st[st[r -- i '] .refval -- _type] .type ≤ st[r -- _type] .type .type ∧ path∃(str, st[r -- i '] .refval, r0, st) ∨ st[r -- i '] .refval = jvmref ∧ r0 = jvmref))) | A User Theorem |
| pathex-class | ⊦ is_obj(str, r, st) ∧ r ≠ r0 → ( path∃(str, r, r0, st) ↔ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ ( st[r -- fs '] .refval ≠ jvmref ∧ st[st[r -- fs '] .refval -- _type] .type ≤ fs .type ∧ path∃(str, st[r -- fs '] .refval, r0, st) ∨ st[r -- fs '] .refval = jvmref ∧ r0 = jvmref))) | A User Theorem |
| pathex-def-nodups | ⊦ r ≠ r0 → (path∃(str, r, r0, st) ↔ (∃ refs. refs ≠ [] ∧ refs .first = r ∧ refs .last = r0 ∧ ¬ dups(refs) ∧ validrefs(str, refs, st[r -- _type] .type, st))) | A User Theorem |
| pathex-def-simple | ⊦ path∃(str, r, r0, st) ↔ (∃ refs. refs ≠ [] ∧ refs .first = r ∧ refs .last = r0 ∧ validrefs(str, refs, st[r -- _type] .type, st)) | A User Theorem |
| pathex-junkref | ⊦ path∃(str, r, r0, st) ∧ junkref(str, r0, st) → junkref(str, r, st) | A User Theorem |
| pathex-junkref-01 | ⊦ junkref(str, r0, st) ∧ ¬ junkref(str, r, st) → ¬ path∃(str, r, r0, st) | A User Theorem |
| pathex-junkref-02 | ⊦ path∃(str, r, r0, st) ∧ ¬ junkref(str, r, st) → ¬ junkref(str, r0, st) | A User Theorem |
| pathex-levelsubset | ⊦ level⊆(str, str0) ∧ path∃(str, r, r0, st) → path∃(str0, r, r0, st) | A User Theorem |
| pathex-levelsubset-01 | ⊦ level⊆(str, str0) ∧ path∃(str0, r, r0, st) ∧ validref(str, r, ty, st) → path∃(str, r, r0, st) | A User Theorem |
| pathex-levelsubset-equiv | ⊦ level⊆(str, str0) ∧ ¬ junkref(str, r, st) → (path∃(str0, r, r0, st) ↔ path∃(str, r, r0, st)) | A User Theorem |
| pathex-lookup-put-other | ⊦ ¬ path∃(str, r0, r1, st) ∧ is_valid_ref(str, r1, st) → (st[r1 -- sk, val][r0 -- sk0]) = st[r0 -- sk0] | A User Theorem |
| pathex-no-newref | ⊦ newref(r1, st) → ¬ path∃(str, r, r1, st) | A User Theorem |
| pathex-nopathex-diff | ⊦ validrefnotnull(str, r, ty, st) ∧ ¬ path∃(str, r, r1, st) ∧ path∃(str, r, r2, st) → r1 ≠ r2 | A User Theorem |
| pathex-noreftype | ⊦ ¬ is_reftype(st[r0 -- _type] .type) ∧ r0 ≠ jvmref → ¬ path∃(str, r, r0, st) | A User Theorem |
| pathex-not-is-validref | ⊦ ¬ is_valid_ref(r1, st) ∧ r1 ≠ jvmref → ¬ path∃(str, r, r1, st) | A User Theorem |
| pathex-not-is-validref-01 | ⊦ ¬ is_valid_ref(str, r1, st) ∧ r1 ≠ jvmref → ¬ path∃(str, r, r1, st) | A User Theorem |
| pathex-not-is-validref-02 | ⊦ ¬ is_valid_ref(str, r, st) ∧ r ≠ jvmref → ¬ path∃(str, r, r1, st) | A User Theorem |
| pathex-null | ⊦ r ≠ jvmref → ¬ path∃(str, jvmref, r, st) | A User Theorem |
| pathex-null-01 | ⊦ path∃(str, jvmref, r0, st) ↔ r0 = jvmref | A User Theorem |
| pathex-one | ⊦ path∃(str, r, r, st) ↔ r = jvmref ∨ r ≠ jvmref ∧ is_valid_ref(str, r, st) | A User Theorem |
| pathex-put-array-badindex | ⊦ i < 0 → (path∃(str, r, r1, st[r0 -- i ', val]) ↔ path∃(str, r, r1, st)) | A User Theorem |
| pathex-put-cyclic | ⊦ path∃(str, r0, r, st) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ st[r0 -- _type] .type ≤ fs .type ∧ is_classtype(st[r -- _type] .type) ∧ r ≠ jvmref ∧ r0 ≠ jvmref → cyclic(str, r, st[r -- fs ', refval(r0)]) | A User Theorem |
| pathex-put-last | ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ junkref(str, r, st) ∧ sk ≠ _type → ¬ path∃(str, r, r0, st[r0 -- sk, val]) | A User Theorem |
| pathex-put-nopathex | ⊦ ¬ path∃(str, r, r0, st) ∧ ¬ junkref(str, r, st) ∧ sk ≠ _type → (path∃(str, r, r1, st[r0 -- sk, val]) ↔ path∃(str, r, r1, st)) | A User Theorem |
| pathex-put-pathex-array-refval | ⊦ path∃(str, r, r1, st[r0 -- sk, val]) ∧ path∃(str, r, r0, st) ∧ ¬ path∃(str, val .refval, r1, st) ∧ is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r0 -- _length] .intval ∧ is_referencevalue(val) ∧ validref(str, val .refval, st[r0 -- _type] .type .type, st) ∧ r0 ≠ jvmref ∧ is_arraytype(st[r0 -- _type] .type) ∧ (val .refval = jvmref → is_reftype(st[r0 -- _type] .type .type)) → path∃(str, r, r1, st) | A User Theorem |
| pathex-putbar | ⊦ okbytearray(r2, st) → (path∃(str, r, r1, putByteArray(bytes, r2, i, st)) ↔ path∃(str, r, r1, st)) | A User Theorem |
| pathex-putbar-01 | ⊦ okbytearray(r2, st) ∧ ¬ junkref(`docs2store', r, st) ∧ ¬ path∃(`docs2store', r, r1, st) → ¬ path∃(`docs2store', r, r1, putByteArray(bytes, r2, i, st)) | A User Theorem |
| pathex-putbar-02 | ⊦ okbytearray(r2, st) ∧ validref(`docs2store', r, ty, st) ∧ ¬ path∃(`docs2store', r, r1, st) → ¬ path∃(`docs2store', r, r1, putByteArray(bytes, r2, st)) | A User Theorem |
| pathex-putbar-03 | ⊦ okbytearray(r2, st) ∧ ¬ junkref(`docs2store', r, st) ∧ path∃(`docs2store', r, r1, putByteArray(bytes, r2, i, st)) → path∃(`docs2store', r, r1, st) | A User Theorem |
| pathex-putbyte | ⊦ okbytearray(r1, st) → (path∃(str, r, r0, st[r1 -- i ', byteval(by)]) ↔ path∃(str, r, r0, st)) | A User Theorem |
| pathex-putbyte-field | ⊦ ¬ junkref(str, r0, st) ∧ path∃(str, r0, r1, st[r -- mkfs(class, byte_type, fieldvar) ', byteval(by)]) → path∃(str, r0, r1, st) | A User Theorem |
| pathex-putbyte-field-01 | ⊦ ¬ junkref(str, r0, st) ∧ ¬ path∃(str, r0, r1, st) → ¬ path∃(str, r0, r1, st[r -- mkfs(class, byte_type, fieldvar) ', byteval(by)]) | A User Theorem |
| pathex-putbyteval | ⊦ okbytearray(r2, st) ∧ ¬ junkref(`docs2store', r, st) ∧ ¬ path∃(`docs2store', r, r1, st) → ¬ path∃(`docs2store', r, r1, st[r2 -- i ', byteval(by)]) | A User Theorem |
| pathex-putbyteval-01 | ⊦ okbytearray(r2, st) ∧ ¬ junkref(str, r, st) ∧ ¬ path∃(str, r, r1, st) → ¬ path∃(str, r, r1, st[r2 -- i ', byteval(by)]) | A User Theorem |
| pathex-putshortfield | ⊦ is_shortvalue(st[r -- mkfs(class, short_type, fieldvar) ']) ∧ path∃(str, r0, r1, st[r -- mkfs(class, short_type, fieldvar) ', shortval(sho)]) ∧ ¬ junkref(str, r0, st) → path∃(str, r0, r1, st) | A User Theorem |
| pathex-putshortfield-01 | ⊦ is_shortvalue(st[r -- mkfs(class, short_type, fieldvar) ']) ∧ ¬ path∃(str, r0, r1, st) ∧ ¬ junkref(str, r0, st) → ¬ path∃(str, r0, r1, st[r -- mkfs(class, short_type, fieldvar) ', shortval(sho)]) | A User Theorem |
| pathex-putstatfield | ⊦ path∃(str, r, r0, st) ↔ path∃(str, r, r0, st[jvmref -- sk, val]) | A User Theorem |
| pathex-putstatfield-01 | ⊦ path∃(str, r, r0, st[jvmref -- sk, val]) ↔ path∃(str, r, r0, st) | A User Theorem |
| pathex-subset | ⊦ validref(str, r, ty, st) ∧ path∃(str, r, r1, st) ∧ st ⊆ st0 → path∃(str, r, r1, st0) | A User Theorem |
| pathex-subset-01 | ⊦ validref(str, r, ty, st) ∧ ¬ path∃(str, r, r1, st0) ∧ st ⊆ st0 → ¬ path∃(str, r, r1, st) | A User Theorem |
| pathex-subset-02 | ⊦ ¬ junkref(str, r, st) ∧ path∃(str, r, r1, st) ∧ st ⊆ st0 → path∃(str, r, r1, st0) | A User Theorem |
| pathex-subset-equiv | ⊦ ¬ junkref(str, r, st) ∧ st ⊆ st0 → (path∃(str, r, r0, st0) ↔ path∃(str, r, r0, st)) | A User Theorem |
| pathex-trans | ⊦ path∃(str, r, r0, st) ∧ path∃(str, r0, r1, st) → path∃(str, r, r1, st) | A User Theorem |
| pathex-validrefs-in | ⊦ validrefs(str, r ' + refs, ty, st) ∧ r0 ∈ refs → path∃(str, r, r0, st) | A User Theorem |
| pathexplus-pathex | ⊦ path∃(str, r, r0, st) → path∃+(str, r, r0, st) | A User Theorem |
| validref-nopath-superset | ⊦ validrefnotnull(str, r, st[r -- _type] .type, st) ∧ st ⊆ st0 ∧ newref(r1, st) → ¬ path∃(str, r, r1, st0) | A User Theorem |
| validref-nopathex-put | ⊦ is_valid_ref(str, r0, st) ∧ sk ≠ _type ∧ ¬ path∃(str, r, r0, st) → (validref(str, r, ty, st[r0 -- sk, val]) ↔ validref(str, r, ty, st)) | A User Theorem |
| validref-refs-last-valid-subset | ⊦ r ∈ refs0 ∧ validrefs(str, refs0 + r1, ty, st0) ∧ validref(str, r, st[r -- _type] .type, st) ∧ st ⊆ st0 → validref(str, r1, st[r1 -- _type] .type, st) | A User Theorem |
| validrefs-addarray | ⊦ ¬ validrefs(str, refs, ty, st) ∧ newref(r, st) ∧ ¬ r ∈ refs → ¬ validrefs(str, refs, ty, addarray(r, ty0, vals, st)) | A User Theorem |
| validrefs-addarray-junkref | ⊦ validrefs(str, refs, ty0, addarray(r, ty, vals, st)) ∧ newref(r, st) ∧ r ∈ refs ∧ r0 = refs .first → junkref(str, r0, st) | A User Theorem |
| validrefs-addobj | ⊦ ¬ validrefs(str, refs, ty, st) ∧ ¬ r ∈ refs → ¬ validrefs(str, refs, ty, addobj(r, class, fis, st)) | A User Theorem |
| validrefs-addobj-01 | ⊦ validFields(r, fis, addobj(r, class, fis, st)) ∧ fis .keys = instfields(class) ∧ newref(r, st) ∧ class+∃(str, class) ∧ ¬ is_abstract(class) ∧ validref(str, r, mkclasstype(class), addobj(r, class, fis, st)) ∧ fs ' × refval(refs .first) ∈ fis ∧ fs ' ∈ instfields(class) ∧ refs ≠ [] ∧ validrefs(str, refs, ty, st) → validrefs(str, r ' + refs, (addobj(r, class, fis, st)[r -- _type]) .type, addobj(r, class, fis, st)) | A User Theorem |
| validrefs-addobj-junkref | ⊦ validrefs(str, refs, ty0, addobj(r, class, fis, st)) ∧ newref(r, st) ∧ r ∈ refs ∧ r0 = refs .first → junkref(str, r0, st) | A User Theorem |
| validrefs-addobj-new | ⊦ validrefs(str, refs, ty, st) ∧ newref(r, st) → validrefs(str, refs, ty, addobj(r, class, fis, st)) | A User Theorem |
| validrefs-addobj-notin | ⊦ validrefs(str, refs, ty, st) ∧ ¬ r ∈ refs → validrefs(str, refs, ty, addobj(r, class, fis, st)) | A User Theorem |
| validrefs-all-same | ⊦ validrefs(str, refs, ty, st) ∧ (∀ r. r ∈ refs ∧ r ≠ jvmref → st[r -- _type] = st0[r -- _type] ∧ (is_classtype(st[r -- _type] .type) → (∀ sk. sk ∈ instfields(st[r -- _type] .type .class) → st[r -- sk] = st0[r -- sk])) ∧ ( is_arraytype(st[r -- _type] .type) → st[r -- _length] = st0[r -- _length] ∧ (∀ i. 0 ≤ i ∧ i < st[r -- _length] .intval → st[r -- i '] = st0[r -- i ']))) → validrefs(str, refs, ty, st0) | A User Theorem |
| validrefs-append | ⊦ validrefs(str, refs + r ', ty, st) ∧ validrefs(str, r ' + refs0, ty0, st) → validrefs(str, refs + r ' + refs0, ty, st) | A User Theorem |
| validrefs-append-01 | ⊦ validrefs(str, refs, ty, st) ∧ validrefs(str, refs0, ty0, st) ∧ refs .last = refs0 .first ∧ refs ≠ [] ∧ refs0 ≠ [] → validrefs(str, refs + refs0 .rest, ty, st) | A User Theorem |
| validrefs-applast-array | ⊦ validrefs(str, refs + r ', ty, st) ∧ st[r -- i '] .refval = r0 ∧ is_array(str, r, st) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ st[r0 -- _type] .type ≤ st[r -- _type] .type .type ∧ is_valid_ref(str, r0, st) ∧ type∃(str, st[r0 -- _type] .type) → validrefs(str, refs + r ' + r0 ', ty, st) | A User Theorem |
| validrefs-applast-array-null | ⊦ validrefs(str, refs + r ', ty, st) ∧ st[r -- i '] .refval = jvmref ∧ is_array(str, r, st) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_reftype(st[r -- _type] .type .type) → validrefs(str, refs + r ' + jvmref ', ty, st) | A User Theorem |
| validrefs-applast-class | ⊦ validrefs(str, refs + r ', ty, st) ∧ st[r -- fs '] .refval = r0 ∧ is_referencevalue(st[r -- fs ']) ∧ is_obj(str, r, st) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ st[r0 -- _type] .type ≤ fs .type ∧ is_valid_ref(str, r0, st) ∧ type∃(str, st[r0 -- _type] .type) → validrefs(str, refs + r ' + r0 ', ty, st) | A User Theorem |
| validrefs-applast-class-null | ⊦ validrefs(str, refs + r ', ty, st) ∧ st[r -- fs '] .refval = jvmref ∧ is_referencevalue(st[r -- fs ']) ∧ is_obj(str, r, st) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_reftype(fs .type) → validrefs(str, refs + r ' + jvmref ', ty, st) | A User Theorem |
| validrefs-bytearray | ⊦ validrefs(str, r ' + refs, mkarraytype(byte_type), st) ↔ refs = [] ∧ (r = jvmref ∨ okbytearray(r, st)) | A User Theorem |
| validrefs-bytearray-01 | ⊦ validrefs(str, refs, mkarraytype(byte_type), st) ↔ refs = [] ∨ refs = jvmref ' ∨ okbytearray(refs .first, st) ∧ refs .rest = [] | A User Theorem |
| validrefs-contains-null | ⊦ validrefs(str, refs + jvmref ' + refs0, ty, st) ↔ validrefs(str, refs + jvmref ', ty, st) ∧ refs0 = [] | A User Theorem |
| validrefs-del | ⊦ r ∈ refs ∧ r ≠ jvmref → ¬ validrefs(str, refs, ty, st -- r) | A User Theorem |
| validrefs-del-junkrefs | ⊦ junkrefs(str, (r0 ' + refs) + r ', ty, st -- r) ∧ ¬ junkref(str, r0, st) ∧ r ≠ r0 ∧ ¬ r ∈ refs ∧ st[r0 -- _type] .type ≤ ty → validrefs(str, r0 ' + refs + r ', ty, st) | A User Theorem |
| validrefs-delcycle | ⊦ validrefs(str, refs + r ' + refs0 + r ' + refs1, ty, st) ∧ refs1 ≠ [] ∧ refs1 .last = jvmref → validrefs(str, refs + r ' + refs1, ty, st) | A User Theorem |
| validrefs-delcycle-01 | ⊦ ¬ validrefs(str, refs + r ' + refs1, ty, st) → ¬ validrefs(str, refs + r ' + refs0 + r ' + refs1, ty, st) | A User Theorem |
| validrefs-delete | ⊦ ¬ validrefs(str, refs, ty, st) → ¬ validrefs(str, refs, ty, st -- r) | A User Theorem |
| validrefs-delete-01 | ⊦ ¬ validrefs(str, refs, ty0, st) ∧ ty ≤ ty0 → ¬ validrefs(str, refs, ty, st -- r) | A User Theorem |
| validrefs-delete-02 | ⊦ validrefs(str, r ' + refs, ty, st -- r) ↔ r = jvmref ∧ refs = [] | A User Theorem |
| validrefs-delete-03 | ⊦ validrefs(str, refs, ty, st) ∧ ¬ r ∈ refs → validrefs(str, refs, ty, st -- r) | A User Theorem |
| validrefs-has-null | ⊦ jvmref ∈ refs ∧ refs0 ≠ [] → ¬ validrefs(str, refs + refs0, ty, st) | A User Theorem |
| validrefs-junkrefs | ⊦ junkrefs(str, refs, ty, st) → (∃ refs0, r, refs1. refs = refs0 + r ' + refs1 ∧ validrefs(str, refs0, ty, st) ∧ r ≠ jvmref ∧ ( ¬ is_valid_ref(str, r, st) ∨ refs0 = [] ∧ ¬ st[r -- _type] .type ≤ ty ∨ refs0 ≠ [] ∧ ( is_obj(refs0 .last, st) ∧ (∃ fs. fs ' ∈ instfields(st[refs0 .last -- _type] .type .class) ∧ is_referencevalue(st[refs0 .last -- fs ']) ∧ r = st[refs0 .last -- fs '] .refval ∧ ¬ st[r -- _type] .type ≤ fs .type) ∨ is_array(refs0 .last, st) ∧ (∃ i. 0 ≤ i ∧ i < st[refs0 .last -- _length] .intval ∧ is_referencevalue(st[refs0 .last -- i ']) ∧ r = st[refs0 .last -- i '] .refval ∧ ¬ st[r -- _type] .type ≤ st[refs0 .last -- _type] .type .type)))) | A User Theorem |
| validrefs-junkrefs-01 | ⊦ junkrefs(str, refs + refs0, ty, st) ∧ ¬ junkrefs(str, refs, ty, st) → validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-junkrefs-append | ⊦ validrefs(str, refs, ty, st) ∧ junkrefs(str, refs0, st[refs0 .first -- _type] .type, st) ∧ refs .last = refs0 .first ∧ refs0 ≠ [] ∧ refs ≠ [] → junkrefs(str, refs + refs0 .rest, ty, st) | A User Theorem |
| validrefs-lastelem | validrefs(str, refs, ty, st) ∧ refs ≠ [] ∧ ¬ has_reffield(refs .last, st) ⊦ ∀ r. ¬ validrefs(str, refs + r ', ty, st) | A User Theorem |
| validrefs-levelsubset | ⊦ level⊆(str, str0) ∧ validrefs(str, refs, ty0, st) → validrefs(str0, refs, ty0, st) | A User Theorem |
| validrefs-levelsubset-01 | ⊦ level⊆(str, str0) ∧ validrefs(str0, refs, ty0, st) ∧ validref(str, refs .first, ty, st) → validrefs(str, refs, ty0, st) | A User Theorem |
| validrefs-maxlen | ⊦ validrefs(str, refs, ty, st) ∧ refs ≠ [] ∧ ¬ dups(refs) → # refs ≤ # st .refs + 1 | A User Theorem |
| validrefs-newref | ⊦ r ∈ refs ∧ newref(r, st) → ¬ validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-nodups | validrefs(str, refs, ty, st) ∧ refs ≠ [] ∧ refs .last = jvmref ⊦ ∃ refs0. validrefs(str, refs0, ty, st) ∧ refs0 ≠ [] ∧ refs0 .last = jvmref ∧ refs .first = refs0 .first ∧ ¬ dups(refs0) ∧ refs0 ⊆ refs | A User Theorem |
| validrefs-nodups-01 | validrefs(str, refs, ty, st) ∧ refs ≠ [] ⊦ ∃ refs0. validrefs(str, refs0, ty, st) ∧ refs0 ≠ [] ∧ refs0 .last = refs .last ∧ refs .first = refs0 .first ∧ ¬ dups(refs0) | A User Theorem |
| validrefs-nopathex | ⊦ ¬ path∃(str, r, r0, st) ∧ r0 ∈ refs → ¬ validrefs(str, r ' + refs, ty, st) | A User Theorem |
| validrefs-nopathex-01 | ⊦ ¬ path∃(str, r, r0, st) → ¬ validrefs(str, r ' + refs + r0 ', ty, st) | A User Theorem |
| validrefs-not | ⊦ ¬ is_valid_ref(str, r, st) → (validrefs(str, r ' + refs, ty, st) ↔ r = jvmref ∧ refs = []) | A User Theorem |
| validrefs-not-in | ⊦ r ∈ refs ∧ r ≠ jvmref ∧ ¬ (is_valid_ref(r, st) ∧ type∃(str, st[r -- _type] .type)) → ¬ validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-not-in-01 | ⊦ r ∈ refs ∧ r ≠ jvmref ∧ ¬ is_valid_ref(str, r, st) → ¬ validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-not-typeex | ⊦ r ∈ refs ∧ ¬ type∃(str, st[r -- _type] .type) ∧ r ≠ jvmref → ¬ validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-null-01 | ⊦ validrefs(str, jvmref ', ty, st) | A User Theorem |
| validrefs-null-02 | ⊦ validrefs(str, jvmref ' + refs, ty, st) ↔ refs = [] | A User Theorem |
| validrefs-object | ⊦ ¬ validrefs(str, r ' + refs, st[r -- _type] .type, st) → ¬ validrefs(str, r ' + refs, mkclasstype(`java.lang.Object' .class), st) | A User Theorem |
| validrefs-one | ⊦ validrefs(str, r ', ty, st) ↔ r = jvmref ∨ r ≠ jvmref ∧ is_valid_ref(str, r, st) ∧ st[r -- _type] .type ≤ ty | A User Theorem |
| validrefs-postfix | ⊦ ¬ validrefs(str, refs0, st[refs0 .first -- _type] .type, st) ∧ refs0 ≠ [] → ¬ validrefs(str, refs + refs0, ty, st) | A User Theorem |
| validrefs-prefix | ⊦ ¬ validrefs(str, refs, ty, st) → ¬ validrefs(str, refs + refs0, ty, st) | A User Theorem |
| validrefs-primarray | ⊦ is_primtype(ty) → (validrefs(str, refs, mkarraytype(ty), st) ↔ refs = [] ∨ refs = jvmref ' ∨ okarray(refs .first, ty, st) ∧ refs .rest = []) | A User Theorem |
| validrefs-primtype | ⊦ ¬ is_reftype(ty) → (validrefs(str, refs, ty, st) ↔ refs = [] ∨ refs = jvmref ') | A User Theorem |
| validrefs-primtype-01 | ⊦ validrefs(str, refs, byte_type, st) ↔ refs = [] ∨ refs = jvmref ' | A User Theorem |
| validrefs-primtype-02 | ⊦ validrefs(str, refs, short_type, st) ↔ refs = [] ∨ refs = jvmref ' | A User Theorem |
| validrefs-primtype-03 | ⊦ validrefs(str, refs, int_type, st) ↔ refs = [] ∨ refs = jvmref ' | A User Theorem |
| validrefs-put-array-badindex | ⊦ i < 0 → (validrefs(str, refs, ty, st[r -- i ', val]) ↔ validrefs(str, refs, ty, st)) | A User Theorem |
| validrefs-put-badarrayfield | ⊦ ¬ validrefs(str, refs, ty, st) ∧ ¬ junkref(str, refs .first, st) ∧ fs ' ≠ _type ∧ is_arraytype(st[r0 -- _type] .type) ∧ fs ' ≠ _length ∧ refs ≠ [] ∧ ¬ dups(refs .butlast) → ¬ validrefs(str, refs, ty, st[r0 -- fs ', val]) | A User Theorem |
| validrefs-put-badarrayfield-01 | ⊦ validrefs(str, refs, ty, st) ∧ ¬ junkref(str, refs .first, st) ∧ fs ' ≠ _type ∧ is_arraytype(st[r0 -- _type] .type) ∧ fs ' ≠ _length ∧ refs ≠ [] ∧ ¬ dups(refs .butlast) → validrefs(str, refs, ty, st[r0 -- fs ', val]) | A User Theorem |
| validrefs-put-badclassfield | ⊦ ¬ validrefs(str, refs, ty, st) ∧ ¬ junkref(str, refs .first, st) ∧ fs ' ≠ _type ∧ is_classtype(st[r0 -- _type] .type) ∧ ¬ fs ' ∈ instfields(st[r0 -- _type] .type .class) ∧ refs ≠ [] ∧ ¬ dups(refs .butlast) → ¬ validrefs(str, refs, ty, st[r0 -- fs ', val]) | A User Theorem |
| validrefs-put-badclassfield-01 | ⊦ validrefs(str, refs, ty, st) ∧ ¬ junkref(str, refs .first, st) ∧ fs ' ≠ _type ∧ is_classtype(st[r0 -- _type] .type) ∧ ¬ fs ' ∈ instfields(st[r0 -- _type] .type .class) ∧ refs ≠ [] ∧ ¬ dups(refs .butlast) → validrefs(str, refs, ty, st[r0 -- fs ', val]) | A User Theorem |
| validrefs-put-last | ⊦ ¬ validrefs(str, refs + r0 ', ty, st) ∧ ¬ junkref(str, refs .first, st) ∧ refs ≠ [] ∧ ¬ r0 ∈ refs ∧ sk ≠ _type → ¬ validrefs(str, refs + r0 ', ty, st[r0 -- sk, val]) | A User Theorem |
| validrefs-put-notin | ⊦ ¬ r ∈ refs → (validrefs(str, refs, ty, st[r -- sk, val]) ↔ validrefs(str, refs, ty, st)) | A User Theorem |
| validrefs-put-notin-01 | ⊦ ¬ r ∈ refs ∧ fs ' ≠ _type ∧ fs ' ≠ _length ∧ oktype(val, fs .type, st) ∧ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) → (validrefs(str, refs + r0 ', ty, st[r -- fs ', val]) ↔ validrefs(str, refs + r0 ', ty, st)) | A User Theorem |
| validrefs-put-notin-02 | ⊦ validrefs(str, refs + r0 ', ty, st) ∧ ¬ r ∈ refs ∧ fs ' ≠ _type ∧ fs ' ≠ _length ∧ oktype(val, fs .type, st) → validrefs(str, refs + r0 ', ty, st[r -- fs ', val]) | A User Theorem |
| validrefs-put-notin-03 | ⊦ val .refval ≠ refs0 .first ∧ refs0 .first ≠ st[r -- sk] .refval ∧ refs0 ≠ [] ∧ sk ≠ _type ∧ sk ≠ _length ∧ ¬ dups(refs + r ' + refs0) ∧ (is_valid_ref(str, r, st) ↔ is_valid_ref(str, r, st[r -- sk, val])) → (validrefs(str, refs + r ' + refs0, ty, st[r -- sk, val]) ↔ validrefs(str, refs + r ' + refs0, ty, st)) | A User Theorem |
| validrefs-put-statfield | ⊦ validrefs(str, refs, ty, st[jvmref -- sk, val]) ↔ validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-putbar | okbytearray(r1, st), validrefs(`docs2store', refs0, ty, putByteArray(bytes, r1, i, st)) ⊦ validrefs(`docs2store', refs0, ty, st) | A User Theorem |
| validrefs-putbar-01 | ⊦ validrefs(str, refs, ty, putByteArray(bytes, r, i, st)) ∧ okbytearray(r, st) ∧ refs ≠ [] ∧ ¬ junkref(str, refs .first, st) → validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-putbyte | ⊦ okbytearray(r, st) ∧ ¬ validrefs(str, refs, ty, st[r -- i ', byteval(by)]) → ¬ validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-putbyte-01 | ⊦ okbytearray(r, st) ∧ ¬ validrefs(str, refs, ty, st) → ¬ validrefs(str, refs, ty, st[r -- i ', byteval(by)]) | A User Theorem |
| validrefs-putbyte-field | ⊦ validrefs(str, refs, ty, st[r -- mkfs(class, byte_type, fieldvar) ', byteval(by)]) ∧ ¬ junkref(str, refs .first, st) ∧ refs ≠ [] → validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-putshort-field | ⊦ is_shortvalue(st[r -- mkfs(class, short_type, fieldvar) ']) ∧ refs0 ≠ [] ∧ validrefs(str, refs0, ty, st[r -- mkfs(class, short_type, fieldvar) ', shortval(sho)]) ∧ ¬ junkref(str, refs0 .first, st) → validrefs(str, refs0, ty, st) | A User Theorem |
| validrefs-sametype | ⊦ ¬ validrefs(str, r ' + refs, st[r -- _type] .type, st) → ¬ validrefs(str, r ' + refs, ty, st) | A User Theorem |
| validrefs-sametype-01 | ⊦ validrefs(str, refs, ty, st) ∧ refs ≠ [] ∧ refs .first ≠ jvmref → validrefs(str, refs, st[refs .first -- _type] .type, st) | A User Theorem |
| validrefs-sametype-02 | ⊦ validrefs(str, refs, ty, st) ∧ refs ≠ [] ∧ refs .first ≠ jvmref ∧ r = refs .first → validrefs(str, refs, st[r -- _type] .type, st) | A User Theorem |
| validrefs-sametype-03 | ⊦ validrefs(str, refs, ty, st) ∧ ty0 = st[r -- _type] .type ∧ refs ≠ [] ∧ refs .first ≠ jvmref ∧ r = refs .first → validrefs(str, refs, ty0, st) | A User Theorem |
| validrefs-set-null | ⊦ validrefs(str, refs + refs0, ty, st) ∧ ¬ dups(refs) ∧ refs ≠ [] ∧ is_obj(str, refs .last, st) ∧ fs ' ∈ instfields(st[refs .last -- _type] .type .class) ∧ is_reftype(fs .type) ∧ refs0 ≠ [] → validrefs(str, refs + jvmref ', ty, st[refs .last -- fs ', refval(jvmref)]) | A User Theorem |
| validrefs-subset | ⊦ validrefs(str, refs, ty, st0) ∧ st ⊆ st0 ∧ ¬ junkref(str, r, st) ∧ refs ≠ [] ∧ refs .first = r → validrefs(str, refs, ty, st) | A User Theorem |
| validrefs-subset-01 | ⊦ validrefs(str, refs, ty, st) ∧ st ⊆ st0 ∧ ¬ junkref(str, r, st) ∧ refs ≠ [] ∧ refs .first = r → validrefs(str, refs, ty, st0) | A User Theorem |
| validrefs-subset-equiv | ⊦ validref(str, r, st[r -- _type] .type, st) ∧ st ⊆ st0 → (validrefs(str, r ' + refs, ty, st0) ↔ validrefs(str, r ' + refs, ty, st)) | A User Theorem |
| validrefs-subset-equiv-01 | ⊦ ¬ junkref(str, r, st) ∧ st ⊆ st0 → (validrefs(str, r ' + refs, ty, st0) ↔ validrefs(str, r ' + refs, ty, st)) | A User Theorem |
| validrefs-subset-notnew | ⊦ r ∈ refs0 ∧ validrefs(str, refs0 + r1, ty, st0) ∧ validrefnotnull(str, r, st[r -- _type] .type, st) ∧ st ⊆ st0 → ¬ newref(r1, st) | A User Theorem |
| validrefs-subtype | ⊦ ty ≤ ty0 ∧ st[r -- _type] = typeval(ty) ∧ ¬ validrefs(str, r ' + refs, ty, st) → ¬ validrefs(str, r ' + refs, ty0, st) | A User Theorem |
| validrefs-superclass | ⊦ validrefs(str, refs, ty, st) ∧ ty ≤ ty0 → validrefs(str, refs, ty0, st) | A User Theorem |
| validrefs-superset-junkref | ⊦ validrefs(str, r ' + refs, ty, st0) ∧ r0 ∈ refs ∧ newref(r0, st) ∧ st ⊆ st0 → junkref(str, r, st) | A User Theorem |
| validrefs-trans | ⊦ refs ≠ [] ∧ validrefs(str, refs, mkclasstype(`java.lang.Object' .class), st) ∧ validrefs(str, refs .last + refs1, mkclasstype(`java.lang.Object' .class), st) → validrefs(str, refs + refs1, mkclasstype(`java.lang.Object' .class), st) | A User Theorem |
| validrefs-trans-01 | ⊦ refs ≠ [] ∧ validrefs(str, refs, ty, st) ∧ validrefs(str, refs .last + refs1, ty0, st) → validrefs(str, refs + refs1, ty, st) | A User Theorem |
| validrefs-type | ⊦ st[r0 -- _type] = typeval(ty1) ∧ ty1 ≤ ty0 ∧ validrefs(str, r0 ' + refs0, ty, st) → validrefs(str, r0 ' + refs0, ty0, st) | A User Theorem |
| validrefs-void | ⊦ validrefs(str, refs, void_type, st) ↔ refs = [] ∨ refs = jvmref ' | A User Theorem |