Update links: vmware-research -> anvil-verifier

Signed-off-by: Xudong Sun <[email protected]>

.github/workflows/package-deletion.yml

@@ -16,4 +16,4 @@ jobs:
         env:
           GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-            gh api --method DELETE -H "Accept: application/vnd.github+json" -H "X-GitHub-Api-Version: 2022-11-28" /orgs/vmware-research/packages/container/verifiable-controllers%2F${{ inputs.image }}
+            gh api --method DELETE -H "Accept: application/vnd.github+json" -H "X-GitHub-Api-Version: 2022-11-28" /orgs/anvil-verifier/packages/container/verifiable-controllers%2F${{ inputs.image }}

README.md

@@ -1,5 +1,5 @@
-[![License](https://img.shields.io/badge/License-MIT-green.svg)](https://github.com/vmware-research/verifiable-controllers/blob/main/LICENSE)
-[![CI](https://github.com/vmware-research/verifiable-controllers/actions/workflows/ci.yml/badge.svg)](https://github.com/vmware-research/verifiable-controllers/actions/workflows/ci.yml)
+[![License](https://img.shields.io/badge/License-MIT-green.svg)](https://github.com/anvil-verifier/anvil/blob/main/LICENSE)
+[![CI](https://github.com/anvil-verifier/anvil/actions/workflows/ci.yml/badge.svg)](https://github.com/anvil-verifier/anvil/actions/workflows/ci.yml)
 
 # Anvil: Building Formally Verified Kubernetes Controllers
 
@@ -9,7 +9,7 @@ So far, we have built and verified three Kubernetes controllers (for managing Zo
 
 For now, the best way to use Anvil is to download the source code and import its components into your controller projects, like what we did for our controller [examples](src/controller_examples/). To use Anvil, you will need to install [Verus](https://github.com/verus-lang/verus) (See the [installation instructions](https://github.com/verus-lang/verus/blob/main/INSTALL.md)). Currently Anvil uses Verus version `0d7b766446cd33521132cff03b6108705e83884f`.
 
-If you want to reproduce the results in the OSDI'24 paper "Anvil: Verifying Liveness of Cluster Management Controllers", please refer to the [osdi24](https://github.com/vmware-research/verifiable-controllers/tree/osdi24) branch.
+If you want to reproduce the results in the OSDI'24 paper "Anvil: Verifying Liveness of Cluster Management Controllers", please refer to the [osdi24](https://github.com/anvil-verifier/anvil/tree/osdi24) branch.
 
 ## Implementing controllers with Anvil
 

deploy/consumer/deploy_remote.yaml

@@ -16,6 +16,6 @@ spec:
         app.kubernetes.io/name: consumer-controller
     spec:
       containers:
-        - image: ghcr.io/vmware-research/verifiable-controllers/consumer-controller:latest
+        - image: ghcr.io/anvil-verifier/anvil/consumer-controller:latest
           name: controller
       serviceAccountName: consumer-controller

deploy/fluent/deploy_remote.yaml

@@ -16,6 +16,6 @@ spec:
         app.kubernetes.io/name: fluent-controller
     spec:
       containers:
-        - image: ghcr.io/vmware-research/verifiable-controllers/fluent-controller:latest
+        - image: ghcr.io/anvil-verifier/anvil/fluent-controller:latest
           name: controller
       serviceAccountName: fluent-controller

deploy/producer/deploy_remote.yaml

@@ -16,6 +16,6 @@ spec:
         app.kubernetes.io/name: producer-controller
     spec:
       containers:
-        - image: ghcr.io/vmware-research/verifiable-controllers/producer-controller:latest
+        - image: ghcr.io/anvil-verifier/anvil/producer-controller:latest
           name: controller
       serviceAccountName: producer-controller

deploy/rabbitmq/deploy_remote.yaml

@@ -16,6 +16,6 @@ spec:
         app.kubernetes.io/name: rabbitmq-controller
     spec:
       containers:
-        - image: ghcr.io/vmware-research/verifiable-controllers/rabbitmq-controller:latest
+        - image: ghcr.io/anvil-verifier/anvil/rabbitmq-controller:latest
           name: controller
       serviceAccountName: rabbitmq-controller

deploy/vreplicaset/deploy_remote.yaml

@@ -16,6 +16,6 @@ spec:
         app.kubernetes.io/name: vreplicaset-controller
     spec:
       containers:
-        - image: ghcr.io/vmware-research/verifiable-controllers/vreplicaset-controller:latest
+        - image: ghcr.io/anvil-verifier/anvil/vreplicaset-controller:latest
           name: controller
       serviceAccountName: vreplicaset-controller

deploy/zookeeper/deploy_remote.yaml

@@ -16,6 +16,6 @@ spec:
         app.kubernetes.io/name: zookeeper-controller
     spec:
       containers:
-        - image: ghcr.io/vmware-research/verifiable-controllers/zookeeper-controller:latest
+        - image: ghcr.io/anvil-verifier/anvil/zookeeper-controller:latest
           name: controller
       serviceAccountName: zookeeper-controller

docker/ae/Dockerfile

@@ -1,4 +1,4 @@
-FROM ghcr.io/vmware-research/verifiable-controllers/verus:latest as builder
+FROM ghcr.io/anvil-verifier/anvil/verus:latest as builder
 
 WORKDIR /anvil
 

docker/controller/Dockerfile

@@ -1,4 +1,4 @@
-FROM ghcr.io/vmware-research/verifiable-controllers/verus:latest as builder
+FROM ghcr.io/anvil-verifier/anvil/verus:latest as builder
 
 ARG APP
 WORKDIR /anvil

src/controller_examples/zookeeper_controller/exec/reconciler.rs

@@ -114,7 +114,7 @@ pub fn reconcile_core(
                     // the zookeeper cluster might be unavailable because of losing the quorum.
                     // So the controller needs to correctly prompt membership change before reducing the replica
                     // size of the stateful set, by writing the new replica size into the zookeeper API.
-                    // Details can be found in https://github.com/vmware-research/verifiable-controllers/issues/174.
+                    // Details can be found in https://github.com/anvil-verifier/anvil/issues/174.
                     let state_prime = ZookeeperReconcileState {
                         reconcile_step: ZookeeperReconcileStep::AfterExistsZKNode,
                         ..state