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: |
|---|---|---|
| hasSharing-def | ⊦ hasSharing(r, st) ↔ (∃ sks1, sks2. fits(r, sks1, st) ∧ fits(r, sks2, st) ∧ sks1 ≠ sks2 ∧ sks1 ≠ [] ∧ sks2 ≠ [] ∧ st[r -- sks1] .refval ≠ jvmref ∧ st[r -- sks1] = st[r -- sks2]) | An Axiom |
| hasRefSharing-def | ⊦ hasRefSharing(str, r, st) ↔ (∃ refs, refs0. refs ≠ [] ∧ refs0 ≠ [] ∧ refs ≠ refs0 ∧ refs .first = r ∧ refs0 .first = r ∧ refs .last = refs0 .last ∧ refs0 .last ≠ jvmref ∧ validrefs(str, refs, st[r -- _type] .type, st) ∧ validrefs(str, refs0, st[r -- _type] .type, st)) | An Axiom |
| disjoint-def | ⊦ disjoint(str, refs, st) ↔ ¬ (∃ refs1, refs2. refs1 ≠ [] ∧ refs2 ≠ [] ∧ refs1 .first ∈ refs ∧ refs2 .first ∈ refs ∧ refs1 .first ≠ refs2 .first ∧ refs1 .last = refs2 .last ∧ refs1 .last ≠ jvmref ∧ validrefs(str, refs1, st[refs1 .first -- _type] .type, st) ∧ validrefs(str, refs2, st[refs2 .first -- _type] .type, st)) | An Axiom |
| fits-storekeys-empty | ⊦ fits(r, [], st) | An Axiom |
| fits-storekeys-rec | ⊦ fits(r, sk ' + sks, st) ↔ r ≠ jvmref ∧ is_referencevalue(st[r -- sk]) ∧ (is_classtype(st[r -- _type] .type) → sk ∈ instfields(st[r -- _type] .type .class)) ∧ (is_arraytype(st[r -- _type] .type) → is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r -- _length] .intval) ∧ fits(st[r -- sk] .refval, sks, st) | An Axiom |
| fits-fieldinits-empty | ⊦ fits(r, [], st) | An Axiom |
| fits-fieldinits-rec | ⊦ fits(r, (sk × val) ' + fis, st) ↔ r ≠ jvmref ∧ st[r -- sk] = val ∧ is_referencevalue(val) ∧ (is_classtype(st[r -- _type] .type) → sk ∈ instfields(st[r -- _type] .type .class)) ∧ (is_arraytype(st[r -- _type] .type) → is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r -- _length] .intval) ∧ fits(st[r -- sk] .refval, fis, st) | An Axiom |
| onlymodified-def | ⊦ onlyModified(str, r, st, st0) ↔ (∀ r0, sk. ¬ path∃(str, r, r0, st) → st[r0 -- sk] = st0[r0 -- sk]) | An Axiom |
| hasSharing-list-def | ⊦ hasSharing(refs, st) ↔ (∃ r. r ∈ refs ∧ hasSharing(r, st)) | An Axiom |
| addarray-disjoint-nosharing | ⊦ disjoint(str, refs, st) ∧ ¬ hasSharing(refs, st) ∧ ¬ dups(refs) ∧ validreflist(str, mkjavavalues(refs), ty, st) ∧ newref(r, st) → ¬ hasSharing(r, addarray(r, ty, mkjavavalues(refs), st)) | A User Theorem |
| addarray-disjoint-nosharing-01 | ⊦ disjoint(str, vals .nonnullrefs, st) ∧ ¬ hasSharing(vals .nonnullrefs, st) ∧ ¬ dups(vals .nonnullrefs) ∧ validreflist(str, vals, ty, st) ∧ newref(r, st) → ¬ hasSharing(r, addarray(r, ty, vals, st)) | A User Theorem |
| at-put-prim | ⊦ ¬ is_referencevalue(st[r -- sk]) ∧ fits(r0, sks, st) ∧ ¬ junkref(str, r, st) ∧ ¬ junkref(str, r0, st) ∧ is_referencevalue(st[r0 -- sks]) ∧ sks ≠ [] → (st[r -- sk, val][r0 -- sks]) = st[r0 -- sks] | A User Theorem |
| disjoint-def-fits | ⊦ validreflist(str, mkjavavalues(refs), mkclasstype(`java.lang.Object' .class), st) → ( disjoint(str, refs, st) ↔ ¬ (∃ r1, sks1, r2, sks2. r1 ∈ refs ∧ r2 ∈ refs ∧ r1 ≠ r2 ∧ fits(r1, sks1, st) ∧ fits(r2, sks2, st) ∧ st[r1 -- sks1] = st[r2 -- sks2] ∧ st[r1 -- sks1] .refval ≠ jvmref)) | A User Theorem |
| disjoint-def-pathex | ⊦ disjoint(str, refs, st) ↔ ¬ (∃ r, r0, r1. r ∈ refs ∧ r0 ∈ refs ∧ r ≠ r0 ∧ r1 ≠ jvmref ∧ path∃(str, r, r1, st) ∧ path∃(str, r0, r1, st)) | A User Theorem |
| disjoint-forward-array | ⊦ r ∈ refs ∧ r1 ∈ refs ∧ r ≠ r1 ∧ ¬ junkref(str, r1, st) ∧ ¬ disjoint(str, (refs -l r1) + st[r1 -- i '] .refval, st) ∧ 0 ≤ i ∧ i < st[r1 -- _length] .intval ∧ r1 ≠ jvmref ∧ is_arraytype(st[r1 -- _type] .type) → ¬ disjoint(str, refs, st) | A User Theorem |
| disjoint-forward-array-01 | ⊦ r ≠ r1 ∧ ¬ junkref(str, r1, st) ∧ ¬ disjoint(str, r + st[r1 -- i '] .refval, st) ∧ 0 ≤ i ∧ i < st[r1 -- _length] .intval ∧ r1 ≠ jvmref ∧ is_arraytype(st[r1 -- _type] .type) → ¬ disjoint(str, r ' + r1 ', st) | A User Theorem |
| disjoint-forward-field | ⊦ r ∈ refs ∧ r1 ∈ refs ∧ r ≠ r1 ∧ ¬ junkref(str, r1, st) ∧ ¬ disjoint(str, (refs -l r1) + st[r1 -- sk '] .refval, st) ∧ sk ∈ instfields(st[r1 -- _type] .type .class) ∧ r1 ≠ jvmref ∧ is_classtype(st[r1 -- _type] .type) → ¬ disjoint(str, refs, st) | A User Theorem |
| disjoint-forward-field-02 | ⊦ r ≠ r1 ∧ ¬ junkref(str, r1, st) ∧ ¬ disjoint(str, r + st[r1 -- sk '] .refval, st) ∧ sk ∈ instfields(st[r1 -- _type] .type .class) ∧ r1 ≠ jvmref ∧ is_classtype(st[r1 -- _type] .type) → ¬ disjoint(str, r ' + r1 ', st) | A User Theorem |
| disjoint-newref | ⊦ r = newref(st) ∧ r1 ≠ newref(st) → disjoint(str, r ' + r1 ', st) | A User Theorem |
| disjoint-newref-01 | ⊦ newref(r, st) ∧ r ≠ r1 → disjoint(str, r1 ' + r ', st) | A User Theorem |
| disjoint-newref-02 | ⊦ newref(r, st) ∧ r ≠ r1 → disjoint(str, r ' + r1 ', st) | A User Theorem |
| disjoint-nojunk-newref-subset | ⊦ st ⊆ st1 ∧ ¬ junkref(str, r1, st) ∧ newref(r, st) ∧ (∀ r0. path∃(str, r, r0, st1) → newref(r0, st) ∨ r0 = jvmref) → disjoint(str, r ' + r1 ', st1) | A User Theorem |
| disjoint-nojunk-newref-subset-01 | ⊦ st ⊆ st1 ∧ ¬ junkref(str, r1, st) ∧ newref(r, st) ∧ (∀ r0. path∃(str, r, r0, st1) → newref(r0, st) ∨ r0 = jvmref) → disjoint(str, r1 ' + r ', st1) | A User Theorem |
| disjoint-nopath-both | ⊦ disjoint(str, r ' + r0 ', st) ∧ path∃(str, r, r1, st) ∧ path∃(str, r0, r2, st) ∧ r ≠ r0 ∧ r1 ≠ jvmref ∧ r2 ≠ jvmref → ¬ path∃(str, r1, r2, st) | A User Theorem |
| disjoint-nopathex | ⊦ disjoint(str, r ' + r0 ', st) ∧ path∃(str, r, r1, st) ∧ r ≠ r0 ∧ r1 ≠ jvmref → ¬ path∃(str, r0, r1, st) | A User Theorem |
| disjoint-nopathex-same | ⊦ disjoint(str, r ' + r0 ', st) ∧ r ≠ r0 ∧ r ≠ jvmref ∧ r0 ≠ jvmref → ¬ path∃(str, r, r0, st) | A User Theorem |
| disjoint-one | ⊦ disjoint(str, r ', st) | A User Theorem |
| disjoint-pathex-forward | ⊦ disjoint(str, r ' + r0 ', st) ∧ path∃(str, r, r1, st) ∧ r ≠ r0 → disjoint(str, r1 ' + r0 ', st) | A User Theorem |
| disjoint-pathex-forward-both | ⊦ disjoint(str, r ' + r0 ', st) ∧ path∃(str, r, r1, st) ∧ path∃(str, r0, r2, st) ∧ r ≠ r0 → disjoint(str, r1 ' + r2 ', st) | A User Theorem |
| disjoint-subset | ⊦ (∀ r. r ∈ refs → ¬ junkref(str, r, st)) ∧ disjoint(str, refs, st) ∧ st ⊆ st1 → disjoint(str, refs, st1) | A User Theorem |
| disjoint-subset-01 | ⊦ ¬ junkref(str, r, st) ∧ ¬ junkref(str, r1, st) ∧ disjoint(str, r ' + r1 ', st) ∧ st ⊆ st1 → disjoint(str, r ' + r1 ', st1) | A User Theorem |
| disjoint-symmetric | ⊦ disjoint(str, r ' + r0 ', st) ↔ disjoint(str, r0 ' + r ', st) | A User Theorem |
| ex-fits-validrefs | ¬ junkref(str, r, st), fits(r, sks, st) ⊦ ∃ refs. validrefs(str, r ' + refs, st[r -- _type] .type, st) ∧ st[r -- sks] .refval = (r ' + refs) .last | A User Theorem |
| ex-fits-validrefs-stronger | ¬ junkref(str, r, st), fits(r, sks, st) ⊦ ∃ refs. validrefs(str, r ' + refs, st[r -- _type] .type, st) ∧ # refs = # sks ∧ (∀ sks0. sks0 ⊑ sks ∧ sks0 ≠ [] → st[r -- sks0] .refval = (r ' + refs)[# sks0]) | A User Theorem |
| ex-validrefs-fits | validrefs(str, refs, ty, st), refs ≠ [] ⊦ ∃ sks. fits(refs .first, sks, st) ∧ st[refs .first -- sks] .refval = refs .last | A User Theorem |
| ex-validrefs-fits-stronger | validrefs(str, refs, ty, st), refs ≠ [] ⊦ ∃ sks. fits(refs .first, sks, st) ∧ 1 + # sks = # refs ∧ (∀ n. 0 < n ∧ n ≤ # sks → st[refs .first -- firstn(n, sks)] .refval = refs[n]) | A User Theorem |
| fits-append | ⊦ fits(r, sks + sks0, st) ↔ fits(r, sks, st) ∧ fits(st[r -- sks] .refval, sks0, st) | A User Theorem |
| fits-in | ⊦ sks ≠ [] ∧ ¬ junkref(str, r, st) ∧ fits(r, sks, st) → r -- sks ∈ st | A User Theorem |
| fits-in-01 | ⊦ ¬ junkref(str, r, st) ∧ fits(r, sks, st) ∧ r ≠ jvmref → r -- sks ∈ st | A User Theorem |
| fits-no-reftype | ⊦ fits(r, sks, st) ∧ ¬ is_reftype(ty) ∧ ¬ junkref(str, r, st) → (mkfs(class, ty, fieldvar) ' ∈ sks ↔ ¬ ¬ (mkfs(class, ty, fieldvar) ' = sks .last ∧ sks ≠ [])) | A User Theorem |
| fits-no-reftype-01 | ⊦ mkfs(class, ty, fieldvar) ' ∈ sks .butlast ∧ ¬ is_reftype(ty) ∧ ¬ junkref(str, r, st) ∧ sks ≠ [] → ¬ fits(r, sks, st) | A User Theorem |
| fits-no-refval | ⊦ sks0 ⊑ sks .butlast ∧ ¬ is_referencevalue(st[r -- sks0]) ∧ ¬ junkref(str, r, st) ∧ sks ≠ [] → ¬ fits(r, sks, st) | A User Theorem |
| fits-no-refval-01 | ⊦ ¬ is_referencevalue(st[r -- sks]) ∧ ¬ junkref(str, r, st) → ¬ fits(r, sks + sk ', st) | A User Theorem |
| fits-null | ⊦ fits(jvmref, sks, st) ↔ sks = [] | A User Theorem |
| fits-pathex | ⊦ ¬ junkref(str, r, st) ∧ fits(r, sks, st) → path∃(str, r, st[r -- sks] .refval, st) | A User Theorem |
| fits-pathex-01 | ⊦ validrefnotnull(str, r, ty, st) ∧ fits(r, sks0, st) → path∃(str, r, st[r -- sks0] .refval, st) | A User Theorem |
| fits-put | ⊦ is_referencevalue(st[r -- sks]) ∧ ¬ junkref(str, r, st) ∧ fits(r, sks, st) ∧ okarray(r1, byte_type, st) → (st[r1 -- i ', byteval(by)][r -- sks]) = st[r -- sks] | A User Theorem |
| fits-put-01 | ⊦ ¬ junkref(str, r, st) ∧ is_referencevalue(st[r -- sks]) ∧ okarray(r1, byte_type, st) ∧ fits(r, sks, st) → fits(r, sks, st[r1 -- i ', byteval(by)]) | A User Theorem |
| fits-put-02 | ⊦ ¬ junkref(str, r, st) ∧ is_referencevalue(st[r -- sks]) ∧ okarray(r1, byte_type, st) ∧ fits(r, sks, st[r1 -- i ', byteval(by)]) → fits(r, sks, st) | A User Theorem |
| fits-put-02-stronger | ⊦ ¬ junkref(str, r, st) ∧ okarray(r1, byte_type, st) ∧ fits(r, sks, st[r1 -- i ', byteval(by)]) → fits(r, sks, st) | A User Theorem |
| fits-put-03 | ⊦ ¬ junkref(str, r, st) ∧ fits(r, sks, st) ∧ is_bytevalue(st[r1 -- fs ']) → (st[r1 -- fs ', byteval(by)][r -- sks]) = st[r -- sks] | A User Theorem |
| fits-put-04 | ⊦ ¬ junkref(str, r, st) ∧ is_referencevalue(st[r -- sks]) ∧ is_bytevalue(st[r1 -- fs ']) ∧ fits(r, sks, st) → fits(r, sks, st[r1 -- fs ', byteval(by)]) | A User Theorem |
| fits-put-05 | ⊦ ¬ junkref(str, r, st) ∧ is_referencevalue(st[r -- sks]) ∧ is_bytevalue(st[r1 -- fs ']) ∧ fits(r, sks, st[r1 -- fs ', byteval(by)]) → fits(r, sks, st) | A User Theorem |
| fits-put-05-stronger | ⊦ ¬ junkref(str, r, st) ∧ is_bytevalue(st[r1 -- fs ']) ∧ fits(r, sks, st[r1 -- fs ', byteval(by)]) → fits(r, sks, st) | A User Theorem |
| fits-put-other | ⊦ ¬ (∃ sks0, sks1. sks = sks0 + (sk + sks1) ∧ st[r -- sks0] .refval = r0 ∧ (∀ sks2. sks2 + sk ⊑ sks0 → st[r -- sks2] .refval ≠ r0)) ∧ sk ≠ _type ∧ sk ≠ _length → (fits(r, sks, st[r0 -- sk, val]) ↔ fits(r, sks, st)) | A User Theorem |
| fits-put-short | ⊦ ¬ junkref(str, r, st) ∧ fits(r, sks, st) ∧ is_shortvalue(st[r1 -- fs ']) → (st[r1 -- fs ', val][r -- sks]) = st[r -- sks] | A User Theorem |
| fits-put-short-01 | ⊦ ¬ junkref(str, r, st) ∧ is_shortvalue(st[r1 -- fs ']) ∧ fits(r, sks, st[r1 -- fs ', shortval(sho)]) → fits(r, sks, st) | A User Theorem |
| fits-put-short-02 | ⊦ ¬ junkref(str, r, st) ∧ is_shortvalue(st[r1 -- fs ']) ∧ fits(r, sks, st) → fits(r, sks, st[r1 -- fs ', shortval(sho)]) | A User Theorem |
| fits-put-statfield | ⊦ ¬ junkref(str, r, st) → (fits(r, sks, st[jvmref -- sk, val]) ↔ fits(r, sks, st)) | A User Theorem |
| fits-put-stronger | ⊦ ¬ junkref(str, r, st) ∧ fits(r, sks, st) ∧ okarray(r1, byte_type, st) → (st[r1 -- i ', byteval(by)][r -- sks]) = st[r -- sks] | A User Theorem |
| fits-rec | ⊦ sks ≠ [] → ( fits(r, sks, st) ↔ r ≠ jvmref ∧ is_referencevalue(st[r -- sks .first]) ∧ (is_classtype(st[r -- _type] .type) → sks .first ∈ instfields(st[r -- _type] .type .class)) ∧ (is_arraytype(st[r -- _type] .type) → is_indexkey(sks .first) ∧ 0 ≤ sks .first .index ∧ sks .first .index < st[r -- _length] .intval) ∧ fits(st[r -- sks .first] .refval, sks .rest, st)) | A User Theorem |
| fits-storekeys-one | ⊦ fits(r, sk ', st) ↔ r ≠ jvmref ∧ is_referencevalue(st[r -- sk]) ∧ (is_classtype(st[r -- _type] .type) → sk ∈ instfields(st[r -- _type] .type .class)) ∧ (is_arraytype(st[r -- _type] .type) → is_indexkey(sk) ∧ 0 ≤ sk .index ∧ sk .index < st[r -- _length] .intval) | A User Theorem |
| fits-subset | ⊦ ¬ junkref(str, r, st0) ∧ fits(r, sks, st) ∧ st0 ⊆ st → fits(r, sks, st0) | A User Theorem |
| fits-subset-01 | ⊦ st ⊆ st0 ∧ ¬ junkref(str, r, st) → (fits(r, sks, st0) ↔ fits(r, sks, st)) | A User Theorem |
| fits-superset | ⊦ ¬ junkref(str, r, st) ∧ fits(r, sks, st) ∧ st ⊆ st0 → fits(r, sks, st0) | A User Theorem |
| getbar-onlyModified | ⊦ okbytearray(r, st) ∧ okbytearray(r1, st) ∧ r ≠ r1 ∧ ¬ junkref(str, r0, st) ∧ onlyModified(str, r, st, st0) → getbytearray(r1, st) = getbytearray(r1, st0) | A User Theorem |
| getbar-onlyModified-all | ⊦ 0 ≤ i ∧ 0 ≤ j ∧ r ≠ r1 ∧ okbytearray(r, st) ∧ okbytearray(r1, st) ∧ onlyModified(str, r, st, st0) → getbytearray(r1, i, j, st) = getbytearray(r1, i, j, st0) | A User Theorem |
| hasSharing-addarray | ⊦ ¬ junkref(str, r, st) ∧ ¬ hasSharing(r, st) → ¬ hasSharing(r, addarray(newref(st), ty, vals, st)) | A User Theorem |
| hasSharing-addobj-same | ⊦ newref(r, st) ∧ validfieldinits(str, fis, st) ∧ ¬ junkref(str, r, addobj(r, class, fis, st)) ∧ fis .keys = instfields(class) → ( hasSharing(r, addobj(r, class, fis, st)) ↔ ¬ (¬ dups(fis .vals .nonnullrefs) ∧ ¬ hasSharing(fis .vals .nonnullrefs, st) ∧ disjoint(str, fis .vals .nonnullrefs, st))) | A User Theorem |
| hasSharing-array-forward | ⊦ ¬ hasSharing(r, st) ∧ st[r -- i '] = refval(r0) ∧ r ≠ jvmref ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_arraytype(st[r -- _type] .type) → ¬ hasSharing(r0, st) | A User Theorem |
| hasSharing-dd-help | (r2 ' + refs1) .last = (r1 ' + refs0) .last, validrefs(str, r1 ' + refs0, st[r1 -- _type] .type, st), validrefs(str, r2 ' + refs1, st[r2 -- _type] .type, st), path∃(str, r, r1, st), path∃(str, r, r2, st) ⊦ (r1 ' + refs0) .last = jvmref, r2 = r1, path∃(str, r2, r1, st), path∃(str, r1, r2, st), hasSharing(r, st) | A User Theorem |
| hasSharing-def-better | ⊦ hasSharing(r, st) ↔ (∃ sks1, sks2. fits(r, sks1, st) ∧ fits(r, sks2, st) ∧ sks1 ≠ sks2 ∧ st[r -- sks1] .refval ≠ jvmref ∧ st[r -- sks1] = st[r -- sks2]) | A User Theorem |
| hasSharing-different-disjoint | ⊦ ¬ hasSharing(r, st) ∧ path∃(str, r, r1, st) ∧ path∃(str, r, r2, st) ∧ ¬ path∃(str, r1, r2, st) ∧ ¬ path∃(str, r2, r1, st) → disjoint(str, r1 ' + r2 ', st) | A User Theorem |
| hasSharing-dups-array | ¬ hasSharing(r, st) ∧ is_arraytype(st[r -- _type] .type) ∧ r ≠ jvmref ⊦ ∀ i, j. i ≠ j ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ 0 ≤ j ∧ j < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ st[r -- i '] .refval ≠ jvmref → st[r -- i '] ≠ st[r -- j '] | A User Theorem |
| hasSharing-dups-object | ¬ hasSharing(r, st) ∧ is_classtype(st[r -- _type] .type) ∧ r ≠ jvmref ⊦ ∀ sk, sk0. sk ≠ sk0 ∧ sk ∈ instfields(st[r -- _type] .type .class) ∧ sk0 ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- sk]) ∧ st[r -- sk] .refval ≠ jvmref → st[r -- sk] ≠ st[r -- sk0] | A User Theorem |
| hasSharing-object-rec | ⊦ ¬ hasSharing(r, st) ∧ st[r -- sk] = refval(r0) ∧ r ≠ jvmref ∧ sk ∈ instfields(st[r -- _type] .type .class) ∧ is_classtype(st[r -- _type] .type) → ¬ hasSharing(r0, st) | A User Theorem |
| hasSharing-pathex | ⊦ ¬ hasSharing(r, st) ∧ path∃(str, r, r0, st) → ¬ hasSharing(r0, st) | A User Theorem |
| hasSharing-put-byteval | ⊦ ¬ junkref(str, r, st) ∧ 0 ≤ i ∧ i < st[r1 -- _length] .intval ∧ okarray(r1, byte_type, st) → (¬ hasSharing(r, st[r1 -- i ', byteval(by)]) ↔ ¬ hasSharing(r, st)) | A User Theorem |
| hasSharing-put-byteval-01 | ⊦ is_bytevalue(st[r -- sk]) ∧ r ≠ jvmref ∧ sk ≠ _length ∧ sk ≠ _type ∧ sk .fs .type = byte_type ∧ ¬ is_indexkey(sk) ∧ ¬ junkref(str, r0, st) → (¬ hasSharing(r0, st[r -- sk, byteval(by)]) ↔ ¬ hasSharing(r0, st)) | A User Theorem |
| hasSharing-put-index-refval | ⊦ disjoint(str, r ' + r2 ', st) ∧ ¬ hasSharing(r, st) ∧ ¬ hasSharing(r2, st) ∧ ¬ junkref(str, r, st) ∧ r ≠ r2 ∧ validref(str, r2, st[r0 -- _type] .type .type, st) ∧ r0 ≠ jvmref ∧ is_arraytype(st[r0 -- _type] .type) ∧ (r2 = jvmref → is_reftype(st[r0 -- _type] .type .type)) → ¬ hasSharing(r, st[r0 -- i ', refval(r2)]) | A User Theorem |
| hasSharing-put-shortval | ⊦ r ≠ jvmref ∧ sk ≠ _length ∧ sk .fs .type = short_type ∧ ¬ is_indexkey(sk) ∧ is_shortvalue(st[r -- sk]) ∧ ¬ junkref(str, r0, st) → (¬ hasSharing(r0, st[r -- sk, shortval(sho)]) ↔ ¬ hasSharing(r0, st)) | A User Theorem |
| hasSharing-put-statfield | ⊦ ¬ junkref(str, r, st) → (¬ hasSharing(r, st[jvmref -- sk, val]) ↔ ¬ hasSharing(r, st)) | A User Theorem |
| hasSharing-putbar | ⊦ ¬ junkref(str, r, st) ∧ ¬ hasSharing(r, st) ∧ okbytearray(r0, st) → ¬ hasSharing(r, putByteArray(bytes, r0, i, st)) | A User Theorem |
| hasSharing-rec | ⊦ hasSharing(r ' + refs, st) ↔ hasSharing(r, st) ∨ hasSharing(refs, st) | A User Theorem |
| hasSharing-self | ⊦ st[r -- sks] = refval(r) ∧ fits(r, sks, st) ∧ sks ≠ [] ∧ r ≠ jvmref → hasSharing(r, st) | A User Theorem |
| hasSharing-subset | ⊦ ¬ junkref(str, r, st) ∧ st ⊆ st1 ∧ ¬ hasSharing(r, st) → ¬ hasSharing(r, st1) | A User Theorem |
| hassharing-bytearray | ⊦ okbytearray(r, st) → ¬ hasSharing(r, st) | A User Theorem |
| hassharing-one | ⊦ hasSharing(r ', st) ↔ hasSharing(r, st) | A User Theorem |
| hassharing-validrefs-dups | ⊦ dups(refs) ∧ validrefs(str, refs, st[refs .first -- _type] .type, st) → hasSharing(refs .first, st) | A User Theorem |
| lookup-statfield | ⊦ ¬ junkref(str, r, st) ∧ fits(r, sks, st) ∧ r ≠ jvmref → (st[jvmref -- sk, val][r -- sks]) = st[r -- sks] | A User Theorem |
| nosharing-forward | ⊦ is_classtype(st[r -- _type] .type) ∧ validrefnotnull(str, r, ty, st) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ ¬ hasSharing(r, st) → ¬ hasSharing(st[r -- fs '] .refval, st) | A User Theorem |
| nosharing-nocycle | ⊦ validref(str, r, ty, st) ∧ ¬ hasSharing(r, st) → ¬ cyclic(str, r, st) | A User Theorem |
| put-switch-primval-field-field | ⊦ is_fskey(sks .last) ∧ is_fskey(sks0 .last) ∧ (st[r -- sks .butlast] ≠ st[r0 -- sks0 .butlast] ∨ sks .last ≠ sks0 .last) ∧ fits(r, sks, st) ∧ fits(r0, sks0, st) ∧ ¬ is_referencevalue(val) ∧ ¬ is_referencevalue(val0) ∧ ¬ is_reftype(sks .last .fs .type) ∧ ¬ is_reftype(sks0 .last .fs .type) ∧ ¬ junkref(str, r, st) ∧ ¬ junkref(str, r0, st) ∧ sks ≠ [] ∧ sks0 ≠ [] → (st[r -- sks, val][r0 -- sks0, val0]) = (st[r0 -- sks0, val0][r -- sks, val]) | A User Theorem |
| put-switch-primval-field-index | ⊦ is_fskey(sks .last) ∧ is_indexkey(sks0 .last) ∧ (st[r -- sks .butlast] ≠ st[r0 -- sks0 .butlast] ∨ sks .last ≠ sks0 .last) ∧ fits(r, sks, st) ∧ fits(r0, sks0, st) ∧ ¬ is_referencevalue(val) ∧ ¬ is_referencevalue(val0) ∧ ¬ is_reftype(sks .last .fs .type) ∧ ¬ is_referencevalue(st[r0 -- sks0]) ∧ ¬ junkref(str, r, st) ∧ ¬ junkref(str, r0, st) ∧ sks ≠ [] ∧ sks0 ≠ [] → (st[r -- sks, val][r0 -- sks0, val0]) = (st[r0 -- sks0, val0][r -- sks, val]) | A User Theorem |
| put-switch-primval-index-field | ⊦ is_indexkey(sks .last) ∧ is_fskey(sks0 .last) ∧ (st[r -- sks .butlast] ≠ st[r0 -- sks0 .butlast] ∨ sks .last ≠ sks0 .last) ∧ fits(r, sks, st) ∧ fits(r0, sks0, st) ∧ ¬ is_referencevalue(val) ∧ ¬ is_referencevalue(val0) ∧ ¬ is_referencevalue(st[r -- sks]) ∧ ¬ is_reftype(sks0 .last .fs .type) ∧ ¬ junkref(str, r, st) ∧ ¬ junkref(str, r0, st) ∧ sks ≠ [] ∧ sks0 ≠ [] → (st[r -- sks, val][r0 -- sks0, val0]) = (st[r0 -- sks0, val0][r -- sks, val]) | A User Theorem |
| put-switch-primval-index-index | ⊦ is_indexkey(sks .last) ∧ is_indexkey(sks0 .last) ∧ (st[r -- sks .butlast] ≠ st[r0 -- sks0 .butlast] ∨ sks .last ≠ sks0 .last) ∧ fits(r, sks, st) ∧ fits(r0, sks0, st) ∧ ¬ is_referencevalue(val) ∧ ¬ is_referencevalue(val0) ∧ ¬ is_referencevalue(st[r -- sks]) ∧ ¬ is_referencevalue(st[r0 -- sks0]) ∧ ¬ junkref(str, r, st) ∧ ¬ junkref(str, r0, st) ∧ sks ≠ [] ∧ sks0 ≠ [] → (st[r -- sks, val][r0 -- sks0, val0]) = (st[r0 -- sks0, val0][r -- sks, val]) | A User Theorem |
| putBar-onlyMod | ⊦ okbytearray(r, st) ∧ st0 = putByteArray(bytes, r, st) → onlyModified(str, r, st, st0) | A User Theorem |
| putbar-classfield-onlymod | ⊦ ¬ junkref(str, r, st) ∧ r ≠ jvmref ∧ is_classtype(st[r -- _type] .type) ∧ sk ∈ instfields(st[r -- _type] .type .class) ∧ okbytearray(st[r -- sk] .refval, st) ∧ st0 = putByteArray(bytes, st[r -- sk] .refval, st) → onlyModified(str, r, st, st0) | A User Theorem |
| sharing-pathex-field-self | ⊦ r ≠ jvmref ∧ is_classtype(st[r -- _type] .type) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ path∃(`docs2store', st[r -- fs '] .refval, r, st) → hasSharing(r, st) | A User Theorem |
| sharing-pathex-field-self-01 | ⊦ r ≠ jvmref ∧ is_classtype(st[r -- _type] .type) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ path∃(str, st[r -- fs '] .refval, r, st) → hasSharing(r, st) | A User Theorem |
| sharing-twopaths | ⊦ sks ≠ [] ∧ sks0 ≠ [] ∧ st[r -- sks] .refval ≠ jvmref ∧ st[r -- sks0] .refval ≠ jvmref ∧ r ≠ jvmref ∧ path∃(str, st[r -- sks] .refval, st[r -- sks0] .refval, st) ∧ sks ≠ sks0 ∧ fits(r, sks, st) ∧ fits(r, sks0, st) ∧ ¬ sks ⊑ sks0 → hasSharing(r, st) | A User Theorem |
| unchanged-fits | ⊦ ¬ junkref(str, r, st) ∧ fits(r, sks, st) ∧ unchanged(str, r, st, st0) → fits(r, sks, st0) | A User Theorem |
| unchanged-lookup-list-generic | ⊦ unchanged(str, r, st, st0) ∧ ¬ junkref(str, r, st) ∧ fits(r, sks, st) → st[r -- sks] = st0[r -- sks] | A User Theorem |
| unchanged-put-nosharing | ⊦ disjoint(str, r ' + r0 ', st) ∧ path∃(str, r, r1, st) ∧ ¬ junkref(str, r0, st) ∧ r ≠ r0 ∧ r1 ≠ jvmref ∧ sk ≠ _type → unchanged(str, r0, st, st[r1 -- sk, val]) | A User Theorem |