Skip to content

Commit 23cfebc

Browse files
nomeatanomeata
committed
Verify the late-failing implementation of lookup
in issue haskell/containers#794 and PR haskell/containers#800 an alternative implementation of `lookup` is proposed which checks if the key is as expected only when reaching the leaf. This means less branching in the success case or when the lookup key shares long prefixes with existing values, but may do more work when the lookup key is far away from existing keys. Not saying that it’s particularly doubtful that the changed code is correct, but since we have the machinery, why not verify it? So here we go, and yes, it goes through. I don’t think we need to merge the PR like this, and can probably wait for the code to reach a containers release, and then include it there. Also, this PR currently contains a bunch of local hacks that I used to get going again (now that I use NixOS), which need to be removed, merged separately, or made obsolete by better changes to the setup.
1 parent 0435b74 commit 23cfebc

File tree

9 files changed

+167
-35
lines changed

9 files changed

+167
-35
lines changed

‎common.mk

Lines changed: 21 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,25 @@
11
HAVE_STACK := $(shell command -v stack 2> /dev/null)
22

3-
ifdef HAVE_STACK
4-
ifdef FOREIGN_HS_TO_COQ
5-
ifndef HS_TO_COQ_DIR
6-
$(error "Using `hs-to-coq/common.mk' outside the hs-to-coq directory requires setting `HS_TO_COQ_DIR'")
7-
endif
8-
HS_TO_COQ = $(shell cd $(HS_TO_COQ_DIR) && stack exec env | perl -ne 'print "$$1/hs-to-coq\n" if /^PATH=([^:]+)/')
9-
else
10-
HS_TO_COQ = stack exec hs-to-coq --
11-
endif
12-
else
13-
ifndef FOREIGN_HS_TO_COQ
14-
$(error "Using `hs-to-coq/common.mk' outside the hs-to-coq directory requires `stack'")
15-
endif
16-
ifeq ($(HS_TO_COQ_COVERAGE),True)
17-
CABAL_OPTS = --enable-coverage
18-
endif
19-
TOP := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
20-
HS_TO_COQ = cabal new-run --project-file=$(TOP)/cabal.project -v0 $(CABAL_OPTS) exe:hs-to-coq --
21-
endif
3+
# ifdef HAVE_STACK
4+
# ifdef FOREIGN_HS_TO_COQ
5+
# ifndef HS_TO_COQ_DIR
6+
# $(error "Using `hs-to-coq/common.mk' outside the hs-to-coq directory requires setting `HS_TO_COQ_DIR'")
7+
# endif
8+
# HS_TO_COQ = $(shell cd $(HS_TO_COQ_DIR) && stack exec env | perl -ne 'print "$$1/hs-to-coq\n" if /^PATH=([^:]+)/')
9+
# else
10+
# HS_TO_COQ = stack exec hs-to-coq --
11+
# endif
12+
# else
13+
# ifndef FOREIGN_HS_TO_COQ
14+
# $(error "Using `hs-to-coq/common.mk' outside the hs-to-coq directory requires `stack'")
15+
# endif
16+
# ifeq ($(HS_TO_COQ_COVERAGE),True)
17+
# CABAL_OPTS = --enable-coverage
18+
# endif
19+
# TOP := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
20+
# HS_TO_COQ = cabal new-run --project-file=$(TOP)/cabal.project -v0 $(CABAL_OPTS) exe:hs-to-coq --
21+
# endif
22+
23+
HS_TO_COQ = /home/jojo/uni/UPenn/hs-to-coq/result/bin/hs-to-coq
2224

2325
SHELL = bash

‎default.nix

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,11 +7,11 @@
77
# nix-build -A haskellPackages.hs-to-coq
88
# After building, you can run result/bin/hs-to-coq
99

10-
{ coqPackages ? "coqPackages_8_8"
10+
{ coqPackages ? "coqPackages_8_10"
1111
, ghcVersion ? "ghc882"
1212

13-
, rev ? "1fe82110febdf005d97b2927610ee854a38a8f26"
14-
, sha256 ? "08x6saa7iljyq2m0j6p9phy0v17r3p8l7vklv7y7gvhdc7a85ppi"
13+
, rev ? "4c2e7becf1c942553dadd6527996d25dbf5a7136"
14+
, sha256 ? "10dzi5xizgm9b3p5k963h5mmp0045nkcsabqyarpr7mj151f6jpm"
1515

1616
, pkgs ? import (builtins.fetchTarball {
1717
url = "https://github.com/NixOS/nixpkgs/archive/${rev}.tar.gz";
@@ -46,7 +46,7 @@ let
4646

4747
env = pkgs.buildEnv { name = name; paths = buildInputs; };
4848
passthru = {
49-
compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" ];
49+
compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.10" ];
5050
};
5151
};
5252
};

‎examples/containers/Makefile

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ SRC_FILE_Data/IntSet/InternalWord = containers/Data/IntSet/Internal.hs
4747
TEST_MODULES = \
4848

4949
# generated from drop-in/
50-
DROPIN =
50+
DROPIN = FastLookup
5151

5252
# also generated from drop-in/
5353
SPECIAL_MODULES =
@@ -142,16 +142,16 @@ $(VFILES_MAN): $(OUT)/%.v : manual/%.v
142142
lndir ../manual $(OUT)/
143143

144144

145-
$(VFILES_DROPIN): $(OUT)/%.v : module-edits/%/edits edits module-edits/%/preamble.v drop-in/%.hs $(OUT)/README.md
146-
$(HS_TO_COQ) -e module-edits/$*/edits \
147-
-e edits \
148-
-o $(OUT) \
149-
-N \
150-
-p module-edits/$*/preamble.v \
151-
--ghc -icontainers \
152-
--ghc -icontainers/dist-install/build \
153-
-Icontainers/include \
154-
drop-in/$*.hs
145+
.SECONDEXPANSION:
146+
$(VFILES_DROPIN): $(OUT)/%.v : $$(wildcard module-edits/$$*/preamble.v) $$(wildcard module-edits/$$*/midamble.v) $$(wildcard module-edits/$$*/edits) $$(wildcard module-edits/$$*/flags) edits drop-in/$$*.hs
147+
$(HS_TO_COQ) $(addprefix -e , $(wildcard module-edits/$*/edits)) \
148+
$(addprefix -p , $(wildcard module-edits/$*/preamble.v)) \
149+
$(addprefix --midamble , $(wildcard module-edits/$*/midamble.v)) \
150+
$(addprefix `cat , $(addsuffix ` , $(wildcard module-edits/$*/flags))) \
151+
$(HS_TO_COQ_OPTS) \
152+
-o $(OUT) \
153+
drop-in/$*.hs
154+
test -e $@
155155

156156
clean:
157157
rm -rf $(OUT) $(HS_SPEC)

‎examples/containers/drop-in/FastLookup.hs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
{-# LANGUAGE BangPatterns #-}
2+
3+
module FastLookup where
4+
5+
import Data.IntMap.Internal
6+
import Prelude hiding (lookup)
7+
8+
fastLookup :: Key -> IntMap a -> Maybe a
9+
fastLookup !k = go
10+
where
11+
go (Bin _p m l r) | zero k m = go l
12+
| otherwise = go r
13+
go (Tip kx x) | k == kx = Just x
14+
| otherwise = Nothing
15+
go Nil = Nothing
16+

‎examples/containers/lib/FastLookup.h2ci

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
{}

‎examples/containers/lib/FastLookup.v

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
(* Default settings (from HsToCoq.Coq.Preamble) *)
2+
3+
Generalizable All Variables.
4+
5+
Unset Implicit Arguments.
6+
Set Maximal Implicit Insertion.
7+
Unset Strict Implicit.
8+
Unset Printing Implicit Defensive.
9+
10+
Require Coq.Program.Tactics.
11+
Require Coq.Program.Wf.
12+
13+
(* Converted imports: *)
14+
15+
Require Data.IntMap.Internal.
16+
Require Data.IntSet.Internal.
17+
Require GHC.Base.
18+
Import GHC.Base.Notations.
19+
20+
(* No type declarations to convert. *)
21+
22+
(* Converted value declarations: *)
23+
24+
Definition fastLookup {a : Type}
25+
: Data.IntSet.Internal.Key -> Data.IntMap.Internal.IntMap a -> option a :=
26+
fun k =>
27+
let fix go arg_0__
28+
:= match arg_0__ with
29+
| Data.IntMap.Internal.Bin _p m l r =>
30+
if Data.IntSet.Internal.zero k m : bool then go l else
31+
go r
32+
| Data.IntMap.Internal.Tip kx x =>
33+
if k GHC.Base.== kx : bool then Some x else
34+
None
35+
| Data.IntMap.Internal.Nil => None
36+
end in
37+
go.
38+
39+
(* External variables:
40+
None Some Type bool option Data.IntMap.Internal.Bin Data.IntMap.Internal.IntMap
41+
Data.IntMap.Internal.Nil Data.IntMap.Internal.Tip Data.IntSet.Internal.Key
42+
Data.IntSet.Internal.zero GHC.Base.op_zeze__
43+
*)

‎examples/containers/lib/_CoqProject

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@
33
Utils/Containers/Internal/PtrEquality.v CTZ.v BitTerminationProofs.v Test/QuickCheck/Property.v Test/QuickCheck/Arbitrary.v Test/QuickCheck/Gen.v IntWord.v
44
Data/Set/Internal.v Utils/Containers/Internal/BitUtil.v Data/IntSet/Internal.v Data/IntSet/InternalWord.v Data/IntMap/Internal.v Data/Map/Internal.v IntSetValidity.v
55

6-
6+
FastLookup.v

‎examples/containers/module-edits/FastLookup/edits

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
rename type GHC.Types.Int = Coq.Numbers.BinNums.N
2+
3+
# `complement x` does not work at type `N`, as the complement of a natural
4+
# number is negative. But in this module, all uses of `complement` are meant to be
5+
# 64bit numbers anyways, so we can complement just these bits.
6+
rewrite forall x, (Data.Bits.complement x) = (complement' x)
7+
8+
rewrite forall x, (x Data.Bits..&. Data.IntSet.Internal.prefixBitMask) = Coq.NArith.BinNat.N.ldiff x Data.IntSet.Internal.suffixBitMask
9+
10+
# Share bit stuff with IntSet
11+
rename value Data.IntMap.Internal.mask = Data.IntSet.Internal.mask
12+
skip Data.IntSet.Internal.mask
13+
rename value Data.IntMap.Internal.zero = Data.IntSet.Internal.zero
14+
skip Data.IntSet.Internal.zero
15+
16+
17+
# Local issue on Joachim’s PC?
18+
rename type GHC.Maybe.Maybe = option
19+
rename value GHC.Maybe.Just = Some
20+
rename value GHC.Maybe.Nothing = None

‎examples/containers/theories/IntMapProofs.v

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -646,6 +646,28 @@ Proof.
646646
Nomega.
647647
Qed.
648648

649+
(* Sometimes the code does not check nomatch first. But we still
650+
want a similar lemma.
651+
*)
652+
Lemma zero_without_nomatch:
653+
forall {a} i r (P : a -> Prop) left right,
654+
(0 < rBits r)%N ->
655+
(inRange i (halfRange r false) = false -> inRange i (halfRange r true) = false -> P left) ->
656+
(inRange i (halfRange r false) = false -> inRange i (halfRange r true) = false -> P right) ->
657+
(inRange i (halfRange r false) = true -> inRange i (halfRange r true) = false -> P left) ->
658+
(inRange i (halfRange r false) = false -> inRange i (halfRange r true) = true -> P right) ->
659+
P (if zero i (rMask r) then left else right).
660+
Proof.
661+
intros.
662+
(* I’m lazy, so I’ll reduce it to the previous lemma. *)
663+
erewrite <- ssrbool.if_same.
664+
apply nomatch_zero; try assumption.
665+
intro.
666+
destruct (zero i (rMask r));
667+
[apply H0|apply H1];
668+
eapply inRange_isSubrange_false; try apply H4;
669+
apply isSubrange_halfRange; assumption.
670+
Qed.
649671

650672
(** *** Verification of [equal] *)
651673

@@ -755,6 +777,34 @@ Proof.
755777
Qed.
756778

757779

780+
(* Verification of the fast-lookup function propoesd in
781+
https://github.com/haskell/containers/pull/800 *)
782+
783+
Require Import FastLookup.
784+
785+
Lemma fastLookup_Desc:
786+
forall {a}{s : IntMap a}{r f i}, Desc s r f -> fastLookup i s = f i.
787+
Proof.
788+
intros ????? HD.
789+
induction HD; subst.
790+
* simpl.
791+
unfoldMethods.
792+
rewrite H.
793+
destruct (i =? k) eqn:Ei; simpl; auto.
794+
* rewrite H4. clear H4.
795+
simpl fastLookup.
796+
rewrite IHHD1 IHHD2. clear IHHD1 IHHD2.
797+
apply zero_without_nomatch; [apply H|..]; intros.
798+
+ rewrite (Desc_outside HD2) ; last inRange_false.
799+
rewrite oro_None_r. reflexivity.
800+
+ rewrite (Desc_outside HD1) ; last inRange_false.
801+
rewrite oro_None_l. reflexivity.
802+
+ rewrite (Desc_outside HD2) ; last inRange_false.
803+
rewrite oro_None_r. reflexivity.
804+
+ rewrite (Desc_outside HD1) ; last inRange_false.
805+
rewrite oro_None_l. reflexivity.
806+
Qed.
807+
758808
(* For the sake of simplicity, we are writing a new findWithdefault that returns an option *)
759809

760810
Definition findWithDefaultOption {a} (def : a) (k : Key) (s : IntMap a) :=

0 commit comments

Comments
 (0)