diff options
| author | James Pollard <james@pollard.dev> | 2020-06-18 17:12:20 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-18 17:12:20 +0100 |
| commit | 6b20fbbeaad23724ca7fbcc10c9445f5cb94b699 (patch) | |
| tree | cbfa0c83d6d010286ce5e20c0803dd0a17f0c8d1 | |
| parent | f5172e5c66ab7175d5e90acee69e88ac214f4b0f (diff) | |
| download | vericert-6b20fbbeaad23724ca7fbcc10c9445f5cb94b699.tar.gz vericert-6b20fbbeaad23724ca7fbcc10c9445f5cb94b699.zip | |
Tidy up proof.
| -rw-r--r-- | src/translation/HTLgenproof.v | 27 | ||||
| -rw-r--r-- | src/verilog/Array.v | 2 |
2 files changed, 16 insertions, 13 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index f37fc8d..a5396af 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -482,8 +482,8 @@ Section CORRECTNESS. (** Here we are assuming that any stack read will be within the bounds of the activation record. *) - assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. + assert (0 <= Integers.Ptrofs.unsigned i0 / 4) as READ_BOUND_LOW by admit. + assert (Integers.Ptrofs.unsigned i0 / 4 < f.(RTL.fn_stacksize) / 4) as READ_BOUND_HIGH by admit. eexists. split. eapply Smallstep.plus_one. @@ -507,18 +507,21 @@ Section CORRECTNESS. apply regs_lessdef_add_match. (** Equality proof *) - assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) by admit. (* FIXME: 32-bit issue. *) - (* Modular arithmetic facts. *) - assert (0 <= Integers.Ptrofs.unsigned i0 / 4 < RTL.fn_stacksize f / 4) by admit. - assert (4 * (Integers.Ptrofs.unsigned i0 / 4) = Integers.Ptrofs.unsigned i0) by admit. - rewrite H0. + (* FIXME: 32-bit issue. *) + assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) as VALUE_IDENTITY by admit. + assert (4 * (Integers.Ptrofs.unsigned i0 / 4) = Integers.Ptrofs.unsigned i0) as MOD_IDENTITY. + { + rewrite Z.mul_comm. + rewrite ZLib.div_mul_undo; lia. + } + rewrite VALUE_IDENTITY. specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)). rewrite Z2Nat.id in H5; try lia. - apply H5 in H4. - rewrite H6 in H4. - rewrite Integers.Ptrofs.repr_unsigned in H4. - rewrite H1 in H4. - invert H4. assumption. + exploit H5; auto; intros. + rewrite MOD_IDENTITY in H0. + rewrite Integers.Ptrofs.repr_unsigned in H0. + rewrite H1 in H0. + invert H0. assumption. apply regs_lessdef_add_greater. apply greater_than_max_func. diff --git a/src/verilog/Array.v b/src/verilog/Array.v index 705dea7..fc52f04 100644 --- a/src/verilog/Array.v +++ b/src/verilog/Array.v @@ -104,7 +104,7 @@ Proof. apply not_iff_compat in H1. apply <- H1 in H0. - destruct (nth_error (arr_contents a) i ) eqn:EQ; try contradiction; eauto. + destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto. Qed. Lemma array_get_error_set_bound {A : Type} : |