diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 17:03:03 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 17:03:03 +0200 |
| commit | a908ebe6567b06ce2b642851354164fea902fdf8 (patch) | |
| tree | 71bda54f9a0d26db417d3a6fd4f3cd13f8aa0e9c | |
| parent | 3f922756808ccdf2516f097047d758820cdf5177 (diff) | |
| download | vericert-a908ebe6567b06ce2b642851354164fea902fdf8.tar.gz vericert-a908ebe6567b06ce2b642851354164fea902fdf8.zip | |
Add expr_ok proof
| -rw-r--r-- | src/translation/HTLgenproof.v | 36 |
1 files changed, 25 insertions, 11 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index ab607ef..f6b90cb 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -1006,17 +1006,31 @@ Section CORRECTNESS. apply regs_lessdef_add_match; big_tac. (** Equality proof *) - match goal with - | [ |- context [valueToNat ?x] ] => - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat x) - as EXPR_OK by admit - end. + assert (EXPR_OK : Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat (Int.divu (Int.add asr # r0 (ZToValue z)) (ZToValue 4))). + { simplify_val. unfold valueToNat. unfold Int.divu, Ptrofs.divu. + rewrite HeqOFFSET. + pose proof Integers.Ptrofs.agree32_add as AGR. + unfold Integers.Ptrofs.agree32 in AGR. + assert (Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr (Int.unsigned asr # r0)) + (Ptrofs.repr (Int.unsigned (Int.repr z)))) = + Int.unsigned (Int.add asr # r0 (ZToValue z))). + apply AGR; auto. + apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2. + apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2. + rewrite H11. replace (Ptrofs.unsigned (Ptrofs.repr 4)) with 4. + replace (Int.unsigned (ZToValue 4)) with 4. Search Ptrofs.agree32. + pose proof Ptrofs.agree32_repr. unfold Ptrofs.agree32 in *. + rewrite H16. trivial. auto. + unfold ZToValue. symmetry. apply Int.unsigned_repr. + unfold_constants. lia. + unfold ZToValue. symmetry. apply Int.unsigned_repr. + unfold_constants. lia. } rewrite <- EXPR_OK. specialize (H9 (Integers.Ptrofs.unsigned |