More progress on verif_sha

git-svn-id: https://svn.princeton.edu/appel/vst@5800 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
renamed myBlocksSrc/Tgt into locBlocksSrc/Tgt

git-svn-id: https://svn.princeton.edu/appel/vst@5801 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Fixed admits introduced by CompCert update by replacing eval_cast with force_val (sem_cast). 

This introduced a bug in verif_sha.v, probably because of the rewrite in norm rules in client_lemmas.v, but I can't figure out what it is.

git-svn-id: https://svn.princeton.edu/appel/vst@5802 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
filled some holes

git-svn-id: https://svn.princeton.edu/appel/vst@5803 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
modified ptr_eq to only be True for pointers (not all equal ints)

git-svn-id: https://svn.princeton.edu/appel/vst@5804 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Eliminated some unnecessary meminj_preserves_globals
assertions from at_external and after_external rules of the LSR;
these already hold due to match_genv

git-svn-id: https://svn.princeton.edu/appel/vst@5805 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Removed an unneeded premise from semax_array_store.

Removed an exponential blowup from the treatment of
 (initialized _a (initialized _b (... (initialized _z Delta)))),
in the new simplify_Delta, called from abbreviate_semax.

More progress on the verification of SHA.


git-svn-id: https://svn.princeton.edu/appel/vst@5806 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Added the definition "eval_cast" in expr.v to have better-control
"simpl" of formulas.

Better handling of "return" and "break" in the forward tactic.

First argument of ZnthV is no longer implicit.


git-svn-id: https://svn.princeton.edu/appel/vst@5807 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Fiddle with the new_load_tac;
closed_wrt_TT lemma in assert_lemmas;
prove the read32_reversed_in_bytearray lemma in verif_sha.


git-svn-id: https://svn.princeton.edu/appel/vst@5809 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Added meminj_globals onditions in LSR rules.
Strengthened effect_interpolation results to enable
derivation of initial_inject_split.

git-svn-id: https://svn.princeton.edu/appel/vst@5812 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Added more auxiliary results on globalenvs, moved some lemmas
into separate file.

git-svn-id: https://svn.princeton.edu/appel/vst@5813 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
More progress on verif_sha.v.

Moved writable_share_top to assert_lemmas.v.

In malloc_lemmas:
 new Definition array_at_.

In loadstore_lemmas:
removed premise typecheck_store from various lemmas.

In array_lemmas:
New lemmas array_at__array_at, mul_repr, 
  repinject_typed_mapsto_, offset_val_array_at,
  semax_pre_later (moved from forward.v),

New unproved lemmas split_array, split_array_





git-svn-id: https://svn.princeton.edu/appel/vst@5814 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Switched to more symmetric representation of structured injections.



git-svn-id: https://svn.princeton.edu/appel/vst@5815 e2b0c78b-04ed-0310-b50c-832c51d4eb4a
Support for load/store from partially initialized arrays; more progress on verif_sha

git-svn-id: https://svn.princeton.edu/appel/vst@5816 e2b0c78b-04ed-0310-b50c-832c51d4eb4a