Proof step 29 from proof decode (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 30:

  # vtbl1 = m0 + 1, err = ESUCCESS, n0 = n2 + n, n2 = ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), n5 = (m0 + 1) + # vtbl, is-encoded(vtbl0, buf), is-encoded((m0 + 1) + # vtbl, subarray(buf, 0, ENCODED_NAT_SIZE)), is-encoded-rec(vtbl, subarray(buf, ENCODED_NAT_SIZE, # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE))), is-encoded-rec (vtbl1, subarray (buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * m0 + ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE)), 2 * ENCODED_NAT_SIZE + (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * (m0 + # vtbl) + ENCODED_VOLID_SIZE ≤ # buf, vtbl ⊥ vtbl1, err = ESUCCESS → is-encoded(v, subarray(buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), ENCODED_VOLID_SIZE)) ∧ ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) + ENCODED_VOLID_SIZE ≤ # buf ∧ n = ENCODED_VOLID_SIZE, err0 = ESUCCESS → ENCODED_NAT_SIZE ≤ # buf ∧ n3 = ENCODED_NAT_SIZE, err = ESUCCESS ∨ ⌊err⌋ , err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ ⟪decode_nat#(n0, buf; m, n; err); if err = ESUCCESS then {n0 := n0 + n; vtbl[v] := m}; n1 := m0⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → (∃ vtbl2. vtbl ⊥ vtbl2 ∧ # vtbl2 + # vtbl = n5 ∧ # vtbl2 = n1 ∧ ENCODED_NAT_SIZE + (# vtbl2 + # vtbl) * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) ≤ # buf ∧ n0 = ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) ∧ is-encoded(# vtbl2 + # vtbl, subarray(buf, 0, ENCODED_NAT_SIZE)) ∧ is-encoded-rec(vtbl, subarray(buf, ENCODED_NAT_SIZE, # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE))) ∧ is-encoded-rec (vtbl2, subarray (buf, ENCODED_NAT_SIZE + # vtbl * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE), # vtbl2 * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE))))) ∧ n1 < # vtbl1), vtbl1 = ∅

Rule argument

Additional information