build(extract): run containerized under CONTAINER=1

This no longer requires a local Dockerfile to layer Make on top of
cryspen/hax's Dockerfile, but I'll leave that commit in history in case
it's useful in the future.

Author: cfm

securedrop-protocol/protocol-minimal/Makefile

@@ -4,9 +4,8 @@
 
 include versions.env
 
-HAX_IMAGE = securedrop-protocol-hax
 HAX_VERSION = $(shell cargo pkgid hax-lib 2>/dev/null | sed 's/.*@//')
-HAX_BASE_IMAGE = hax:$(HAX_VERSION)
+HAX_IMAGE = hax:$(HAX_VERSION)
 
 HAX_TARGETS := +**
 HAX_TARGETS += -securedrop_protocol_minimal::storage::**
@@ -23,6 +22,19 @@ HAX_ADMITS += Securedrop_protocol_minimal.Ciphertext.fst
 REPO_ROOT = $(shell git rev-parse --show-toplevel)
 PROOF_DIR = proofs/fstar/extraction
 
+# Targets below MAY prefix their commands with `$(CONTAINER_RUN)` to run inside
+# the $HAX_IMAGE when $CONTAINER is set.  Targets that do so SHOULD be redefined
+# here to establish a dependency on `hax-compat`.
+ifdef CONTAINER
+CONTAINER_RUN = docker run --rm \
+	--volume $(REPO_ROOT):/work \
+	--workdir /work/$(CURDIR:$(REPO_ROOT)/%=%) \
+	--env CARGO_TARGET_DIR=/work/securedrop-protocol/target/container \
+	$(HAX_IMAGE)
+
+extract: compat-hax
+endif
+
 .DEFAULT_GOAL := help
 
 .PHONY: clean
@@ -44,32 +56,25 @@ compat-fstar:  # Internal: Check F* version.
 	  { echo "Error: expected fstar.exe version '$(FSTAR_EXPECTED_VERSION)', got '$(FSTAR_ACTUAL_VERSION)'"; exit 1; }
 
 .PHONY: compat-hax-image
-compat-hax-image:  # Internal: Check that $HAX_BASE_IMAGE is present.
+compat-hax-image:  # Internal: Check that $HAX_IMAGE is present.
 	@[ -n "$(HAX_VERSION)" ] || \
 	  { echo "Error: could not determine the hax-lib version; is Cargo working?"; exit 1; }
-	@docker image inspect $(HAX_BASE_IMAGE) >/dev/null 2>&1 || \
-	  { echo "Error: missing image '$(HAX_BASE_IMAGE)'; build and tag it per <https://github.com/cryspen/hax#installation>."; exit 1; }
+	@docker image inspect $(HAX_IMAGE) >/dev/null 2>&1 || \
+	  { echo "Error: missing image '$(HAX_IMAGE)'; build and tag it per <https://github.com/cryspen/hax#installation>."; exit 1; }
 
 .PHONY: compat-hax
-compat-hax: compat-hax-image  # Internal: Check that $HAX_BASE_IMAGE has the expected $HAX_VERSION.
-	@actual=$$(docker run --rm $(HAX_BASE_IMAGE) cargo-hax --version 2>/dev/null | sed -n 's/^version=//p'); \
+compat-hax: compat-hax-image  # Internal: Check that $HAX_IMAGE has the expected $HAX_VERSION.
+	@actual=$$(docker run --rm $(HAX_IMAGE) cargo-hax --version 2>/dev/null | sed -n 's/^version=//p'); \
 	[ "$$actual" = "$(HAX_VERSION)" ] || \
 	  { echo "Error: expected cargo-hax version '$(HAX_VERSION)', got '$$actual'"; exit 1; }
 
 .PHONY: extract
-extract:  # Internal/CI: Run hax extraction.
-	cargo-hax into -i '$(HAX_TARGETS)' fstar
+extract:  ## Run hax extraction, without verifying. (Prefix with "CONTAINER=1" to run containerized.)
+	$(CONTAINER_RUN) cargo-hax into -i '$(HAX_TARGETS)' fstar
 
 .PHONY: hax
 hax: compat extract verify  ## Run hax extraction, then type-check and verify extracted proofs.
 
-.PHONY: hax-image
-hax-image: compat-hax  ## Build a container image for hax extraction.
-	docker build \
-		--build-arg HAX_BASE_IMAGE=$(HAX_BASE_IMAGE) \
-		-t $(HAX_IMAGE):$(HAX_VERSION) \
-		- < hax.Dockerfile
-
 .PHONY: verify
 verify:  # Internal/CI: Type-check and verify extracted proofs.
 	# Type-check (fail fast):