diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | src/translation/HTLgenproof.v | 3 | ||||
| -rw-r--r-- | src/verilog/Array.v | 2 | ||||
| -rw-r--r-- | src/verilog/Value.v | 4 | ||||
| -rw-r--r-- | src/verilog/ValueInt.v | 1 |
5 files changed, 8 insertions, 7 deletions
@@ -17,6 +17,8 @@ COQINCLUDES := -R src/common vericert.common -R src/verilog vericert.verilog \ COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source COQMAKE := $(COQBIN)coq_makefile +COQDOCFLAGS := --no-lib-name + VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v) PREFIX ?= . @@ -41,6 +43,9 @@ proof: Makefile.coq $(MAKE) -f Makefile.coq @rm -f src/extraction/STAMP +doc: Makefile.coq + $(MAKE) COQDOCFLAGS="$(COQDOCFLAGS)" -f Makefile.coq html + extraction: src/extraction/STAMP test: diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 403a97f..bf63800 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -753,7 +753,6 @@ Section CORRECTNESS. - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. - rewrite Heqb in Heqb0. discriminate. (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu, - Search Int.repr. repeat (rewrite Int.unsigned_repr). auto.*) - unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2. + unfold translate_eff_addressing in *. repeat (unfold_match H1). @@ -1105,7 +1104,7 @@ Section CORRECTNESS. rewrite Ptrofs.unsigned_repr by (unfold_constants; lia). rewrite Int.unsigned_repr by (unfold_constants; lia). - unfold Ptrofs.of_int. Search Int.add. rewrite Int.add_commut. + unfold Ptrofs.of_int. rewrite Int.add_commut. pose proof Integers.Ptrofs.agree32_add as AGR. unfold Ptrofs.agree32 in *. erewrite AGR. 3: { unfold uvalueToZ. rewrite Ptrofs.unsigned_repr. trivial. apply Int.unsigned_range_2. } diff --git a/src/verilog/Array.v b/src/verilog/Array.v index 02b6d33..fe0f6b2 100644 --- a/src/verilog/Array.v +++ b/src/verilog/Array.v @@ -156,7 +156,7 @@ Proof. intros. unfold array_get. - info_eauto with array. + eauto with array. Qed. Lemma array_get_get_error {A : Type} : diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 41a41b4..d6a3d8b 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -40,8 +40,6 @@ Record value : Type := vword: word vsize }. -Search N.of_nat. - (** ** Value conversions Various conversions to different number types such as [N], [Z], [positive] and @@ -490,7 +488,7 @@ Qed. Proof. intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). rewrite (@vadd_vplus v1 v2 EQ). trivial. - unfold uvalueToZ. Search word "bound". pose proof (@uwordToZ_bound (vsize v2) (vword v2)). + unfold uvalueToZ. pose proof (@uwordToZ_bound (vsize v2) (vword v2)). rewrite H in EQ. rewrite <- EQ in H0 at 3.*) (*rewrite zadd_vplus3. trivia*) diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v index 2220998..f1fd056 100644 --- a/src/verilog/ValueInt.v +++ b/src/verilog/ValueInt.v @@ -77,7 +77,6 @@ Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i. Definition valueToPtr (i : value) : Integers.ptrofs := Ptrofs.of_int i. -Search Ptrofs.of_int Ptrofs.to_int. Definition valToValue (v : Values.val) : option value := match v with | Values.Vint i => Some (intToValue i) |