diff --git a/.ci/docker/Dockerfile b/.ci/docker/Dockerfile
deleted file mode 100644
index 118cb441..00000000
--- a/.ci/docker/Dockerfile
+++ /dev/null
@@ -1,41 +0,0 @@
-FROM ubuntu:focal
-ARG GHC_VERSION
-
-ENV DEBIAN_FRONTEND=noninteractive LANG=C.UTF-8 LC_ALL=C.UTF-8 PATH=/opt/bin:/root/.ghcup/bin:$PATH
-
-ENV LATEST_STACK=linux-x86_64.tar.gz
-ENV STACK_DEPS="g++ gcc libc6-dev libffi-dev libgmp-dev make xz-utils zlib1g-dev git gnupg netbase"
-ARG GHC_DEPS="curl libc6-dev libgmp-dev pkg-config libnuma-dev build-essential"
-
-ENV CABAL_VERSION=3.2.0.0
-
-ARG GHCUP_URL="https://downloads.haskell.org/~ghcup/x86_64-linux-ghcup"
-ARG GHCUP_BIN=/root/.ghcup/bin/ghcup
-
-# Install GHC + Cabal
-RUN apt-get update \
- && apt-get install -y $GHC_DEPS curl \
- && mkdir -p $(dirname $GHCUP_BIN) \
- && curl $GHCUP_URL --output $GHCUP_BIN \
- && chmod +x $GHCUP_BIN \
- && ghcup upgrade \
- && ghcup install ghc ${GHC_VERSION} \
- && ghcup set ghc ${GHC_VERSION} \
- && ghcup install cabal ${CABAL_VERSION} \
- && ghcup set cabal ${CABAL_VERSION}
-
-# Install Stack
-RUN  apt-get update \
-  && apt-get -y install wget \
-  && apt-get -y install $STACK_DEPS \
-  && wget https://get.haskellstack.org/stable/$LATEST_STACK \
-  && tar xzf $LATEST_STACK && rm $LATEST_STACK \
-  && mv stack*/stack /usr/bin
-
-# Clash dependency
-RUN  apt-get update \
-  && apt-get -y install libtinfo-dev
-
-# Compression utils
-RUN  apt-get update \
-  && apt-get -y install tar zip zstd
diff --git a/.ci/docker/build-and-publish-docker-image.sh b/.ci/docker/build-and-publish-docker-image.sh
deleted file mode 100755
index aef2d56c..00000000
--- a/.ci/docker/build-and-publish-docker-image.sh
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/usr/bin/env bash
-
-set -xeo pipefail
-
-REPO="docker.pkg.github.com/clash-lang/clash-protocols"
-DIR=$(dirname "$0")
-now=$(date +%F)
-
-for GHC_VERSION in "8.6.5" "8.10.2"
-do
-  NAME="protocols-focal-ghc-cabal-stack-${GHC_VERSION}"
-
-  docker build -t "${REPO}/${NAME}:$now" "$DIR" --build-arg GHC_VERSION=${GHC_VERSION}
-  docker tag "${REPO}/${NAME}:$now" "${REPO}/${NAME}:latest"
-
-  read -p "Push to GitHub? (y/N) " push
-
-  if [[ $push =~ ^[Yy]$ ]]; then
-          docker push "${REPO}/${NAME}:$now"
-          docker push "${REPO}/${NAME}:latest"
-  else
-          echo "Skipping push to container registry"
-  fi
-done
diff --git a/.ci/setup.sh b/.ci/setup.sh
deleted file mode 100755
index 43fb83a4..00000000
--- a/.ci/setup.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/bin/bash
-set -xou pipefail
-
-grep \
-  -E ' $' -n -r . \
-  --include=*.{hs,hs-boot,sh,cabal,md,yml} \
-  --exclude-dir=dist-newstyle --exclude-dir=deps
-if [[ $? == 0 ]]; then
-    echo "EOL whitespace detected. See ^"
-    exit 1;
-fi
-
-set -e
-
-ghcup set ghc ${GHC_VERSION}
-ghcup set cabal ${CABAL_VERSION}
-
-cabal --version
-ghc --version
-
-# run new-update first to generate the cabal config file that we can then modify
-# retry 5 times, as hackage servers are not perfectly reliable
-NEXT_WAIT_TIME=0
-until cabal update || [ $NEXT_WAIT_TIME -eq 5 ]; do
-   sleep $(( NEXT_WAIT_TIME++ ))
-done
diff --git a/.ci/test_whitespace.sh b/.ci/test_whitespace.sh
new file mode 100755
index 00000000..fb4ea880
--- /dev/null
+++ b/.ci/test_whitespace.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+set -xou pipefail
+
+grep \
+  -E ' $' -n -r . \
+  --include=*.{hs,hs-boot,sh,cabal,md,yml} \
+  --exclude-dir=dist-newstyle --exclude-dir=deps
+if [[ $? == 0 ]]; then
+    echo "EOL whitespace detected. See ^"
+    exit 1;
+fi
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 00000000..7f8e5542
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,96 @@
+name: CI
+
+# Trigger the workflow on all pull requests and pushes/merges to master branch
+on:
+  pull_request:
+  push:
+    branches: [master]
+
+jobs:
+  stack:
+    name: Stack tests
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+
+      - name: Setup Stack / GHC
+        uses: haskell/actions/setup@v1
+        with:
+          ghc-version: '8.10.7' # Exact version of ghc to use
+          enable-stack: true
+          stack-version: 'latest'
+
+      - name: Cache dependencies
+        uses: actions/cache@v2
+        with:
+          path: ~/.stack
+          key: ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-${{ github.sha }}
+          restore-keys: |
+            ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-${{ github.sha }}
+            ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-
+            ${{ runner.os }}-ghc-${{ matrix.ghc }}-
+
+      # Ask Stack to use system GHC instead of installing its own copy
+      - name: Use system GHC
+        run: |
+          stack config set system-ghc --global true
+
+      - name: Test with Stack
+        run: |
+          .ci/test_stack.sh
+
+  cabal:
+    name: Cabal tests - ${{ matrix.os }} / ghc ${{ matrix.ghc }}
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest]
+        cabal:
+          - "3.2"
+        ghc:
+          - "8.10.7"
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+
+      - name: Setup Haskell
+        uses: haskell/actions/setup@v1
+        id: setup-haskell-cabal
+        with:
+          ghc-version: ${{ matrix.ghc }}
+          cabal-version: ${{ matrix.cabal }}
+
+      - name: Cache dependencies
+        uses: actions/cache@v2
+        with:
+          path: ~/.cabal
+          key: ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-${{ github.sha }}
+          restore-keys: |
+            ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-${{ github.sha }}
+            ${{ runner.os }}-ghc-${{ matrix.ghc }}-${{ github.ref }}-
+            ${{ runner.os }}-ghc-${{ matrix.ghc }}-
+
+      - name: Build
+        run: |
+          cabal build all -fci
+
+      - name: Test
+        run: |
+          .ci/test_cabal.sh
+
+      - name: Documentation
+        run: |
+          .ci/build_docs.sh
+
+  linting:
+    name: Source code linting
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+
+      - name: Whitespace
+        run: |
+          .ci/test_whitespace.sh
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
deleted file mode 100644
index 803c289a..00000000
--- a/.gitlab-ci.yml
+++ /dev/null
@@ -1,48 +0,0 @@
-.common:
-  timeout: 1 hour
-  retry:
-    max: 2
-    when:
-      - runner_system_failure
-      - stuck_or_timeout_failure
-  cache:
-    key: $CI_JOB_NAME
-    paths:
-      - cache.tar.zstd
-  tags:
-    - local
-  before_script:
-    - export THREADS=$(nproc)
-    - export CABAL_JOBS=$(nproc)
-    - tar -xf cache.tar.zstd -C / || true
-    - .ci/setup.sh
-    - export
-  after_script:
-    - tar -cf - $(ls -d /root/.cabal /root/.stack /nix || true) | zstd -T0 -3 > cache.tar.zstd
-
-.common-810:
-  extends: .common
-  image: docker.pkg.github.com/clash-lang/clash-protocols/protocols-focal-ghc-cabal-stack-8.10.2:2020-12-07
-  variables:
-    GHC_VERSION: "8.10.2"
-    CABAL_VERSION: "3.2.0.0"
-
-# Haddock is broken on 865.
-haddock:
-  extends: .common-810
-  artifacts:
-    paths:
-      - docs/*
-    expire_in: 1 month
-  script:
-    - .ci/build_docs.sh
-
-cabal-8.10.2:
-  extends: .common-810
-  script:
-    - .ci/test_cabal.sh
-
-stack:
-  extends: .common-810
-  script:
-    - .ci/test_stack.sh
diff --git a/cabal.project b/cabal.project
index f2b2371b..93e00d27 100644
--- a/cabal.project
+++ b/cabal.project
@@ -11,7 +11,7 @@ package clash-prelude
 source-repository-package
     type: git
     location: https://github.com/cchalmers/circuit-notation.git
-    tag: 0fe897cb95bd1be87abed044f4072f104dec2f7d
+    tag: 2574640364eef12222517af059b9e4a7e6b503a7
 
 source-repository-package
     type: git
diff --git a/clash-protocols.cabal b/clash-protocols.cabal
index 352e6534..9b1ac996 100644
--- a/clash-protocols.cabal
+++ b/clash-protocols.cabal
@@ -124,12 +124,13 @@ library
   build-depends:
       -- inline-circuit-notation
       circuit-notation
-    , extra
     , data-default
     , deepseq
-    , hedgehog >= 1.0.2
+    , extra
     , ghc >= 8.6
+    , hedgehog >= 1.0.2
     , pretty-show
+    , strict-tuple
 
       -- To be removed; we need 'Test.Tasty.Hedgehog.Extra' to fix upstream issues
     , tasty >= 1.2 && < 1.5
@@ -137,6 +138,15 @@ library
 
   exposed-modules:
     Protocols
+
+    Protocols.Axi4.Common
+
+    Protocols.Axi4.ReadAddress
+    Protocols.Axi4.ReadData
+    Protocols.Axi4.WriteAddress
+    Protocols.Axi4.WriteData
+    Protocols.Axi4.WriteResponse
+
     Protocols.Df
     Protocols.DfLike
     Protocols.Hedgehog
diff --git a/src/Protocols.hs b/src/Protocols.hs
index 627c3c62..427e6a47 100644
--- a/src/Protocols.hs
+++ b/src/Protocols.hs
@@ -47,7 +47,7 @@ module Protocols
   , def
 
     -- * Circuit notation plugin
-  , circuit
+  , circuit, (-<)
   ) where
 
 import Data.Default (def)
diff --git a/src/Protocols/Axi4/Common.hs b/src/Protocols/Axi4/Common.hs
new file mode 100644
index 00000000..4afe799c
--- /dev/null
+++ b/src/Protocols/Axi4/Common.hs
@@ -0,0 +1,278 @@
+{-|
+Types and utilities shared between AXI4, AXI4-Lite, and AXI3.
+-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Protocols.Axi4.Common where
+
+-- base
+import Data.Kind (Type)
+import GHC.Generics (Generic)
+import GHC.TypeNats (Nat)
+
+-- clash-prelude
+import qualified Clash.Prelude as C
+import Clash.Prelude (type (^), type (-), type (*))
+
+-- strict-tuple
+import Data.Tuple.Strict (T3, T4)
+
+-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol
+data IdWidth = IdWidth Nat deriving (Show, Eq)
+
+-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol
+data AddrWidth = AddrWidth Nat deriving (Show, Eq)
+
+-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol
+data LengthWidth = LengthWidth Nat deriving (Show, Eq)
+
+-- | Simple wrapper to achieve "named arguments" when instantiating an AXI protocol
+data UserType = UserType Type KeepStrobe
+
+-- | Keep or remove Burst, see 'BurstMode'
+data KeepBurst = KeepBurst | NoBurst deriving (Show, Eq)
+
+-- | Keep or remove Burst Length, see 'BurstSize'
+data KeepBurstLength = KeepBurstLength | NoBurstLength deriving (Show, Eq)
+
+-- | Keep or remove cache field, see 'Cache'
+data KeepCache = KeepCache | NoCache deriving (Show, Eq)
+
+-- | Keep or remove last field
+data KeepLast = KeepLast | NoLast deriving (Show, Eq)
+
+-- | Keep or remove lock, see 'AtomicAccess'
+data KeepLock = KeepLock | NoLock deriving (Show, Eq)
+
+-- | Keep or remove permissions, see 'Privileged', 'Secure', and
+-- 'InstructionOrData'.
+data KeepPermissions = KeepPermissions | NoPermissions deriving (Show, Eq)
+
+-- | Keep or remove quality of service field. See 'Qos'.
+data KeepQos = KeepQos | NoQos deriving (Show, Eq)
+
+-- | Keep or remove region field
+data KeepRegion = KeepRegion | NoRegion deriving (Show, Eq)
+
+-- | Keep or remove response field. See 'Resp'.
+data KeepResponse = KeepResponse | NoResponse deriving (Show, Eq)
+
+-- | Keep or remove burst size field. See 'BurstSize'.
+data KeepSize = KeepSize | NoSize deriving (Show, Eq)
+
+-- | Keep or remove strobe field. See 'Strobe'
+data KeepStrobe = KeepStrobe | NoStrobe deriving (Show, Eq)
+
+-- | Type used to introduce strobe information on the term level
+data SKeepStrobe (strobeType :: KeepStrobe) where
+  SKeepStrobe :: SKeepStrobe 'KeepStrobe
+  SNoStrobe :: SKeepStrobe 'NoStrobe
+
+-- | Extracts Nat from 'IdWidth', 'AddrWidth', and 'LengthWidth'
+type family Width (a :: k) :: Nat where
+  Width ('IdWidth n) = n
+  Width ('AddrWidth n) = n
+  Width ('LengthWidth n) = n
+
+-- | Enables or disables 'BurstMode'
+type family BurstType (keepBurst :: KeepBurst) where
+  BurstType 'KeepBurst = BurstMode
+  BurstType 'NoBurst = ()
+
+-- | Enables or disables burst length
+type family BurstLengthType (keepBurstLength :: KeepBurstLength) where
+  BurstLengthType 'KeepBurstLength = C.Index (2^8)
+  BurstLengthType 'NoBurstLength = ()
+
+-- | Enables or disables 'Cache'
+type family CacheType (keepCache :: KeepCache) where
+  CacheType 'KeepCache = Cache
+  CacheType 'NoCache = ()
+
+-- | Enables or disables a boolean indicating whether a transaction is done
+type family LastType (keepLast :: KeepLast) where
+  LastType 'KeepLast = Bool
+  LastType 'NoLast = ()
+
+-- | Enables or disables 'AtomicAccess'
+type family LockType (keepLockType :: KeepLock) where
+  LockType 'KeepLock = AtomicAccess
+  LockType 'NoLock = ()
+
+-- | Enables or disables 'Privileged', 'Secure', and 'InstructionOrData'
+type family PermissionsType (keepPermissions :: KeepPermissions) where
+  PermissionsType 'KeepPermissions = T3 Privileged Secure InstructionOrData
+  PermissionsType 'NoPermissions = ()
+
+-- | Enables or disables 'Qos'
+type family QosType (keepQos :: KeepQos) where
+  QosType 'KeepQos = Qos
+  QosType 'NoQos = ()
+
+-- | Enables or disables region type
+type family RegionType (keepRegion :: KeepRegion) where
+  RegionType 'KeepRegion = C.BitVector 4
+  RegionType 'NoRegion = ()
+
+-- | Enables or disables 'Resp'
+type family ResponseType (keepResponse :: KeepResponse) where
+  ResponseType 'KeepResponse = Resp
+  ResponseType 'NoResponse = ()
+
+-- | Enables or disables 'BurstSize'
+type family SizeType (keepSize :: KeepSize) where
+  SizeType 'KeepSize = BurstSize
+  SizeType 'NoSize = ()
+
+-- | Enable or disable 'Strobe'
+type family StrobeType (byteSize :: Nat) (keepStrobe :: KeepStrobe) where
+  StrobeType byteSize 'KeepStrobe = Strobe byteSize
+  StrobeType byteSize 'NoStrobe = ()
+
+-- | Enable or disable 'Strobe'
+type family StrictStrobeType (byteSize :: Nat) (keepStrobe :: KeepStrobe) where
+  StrictStrobeType byteSize 'KeepStrobe = C.Vec byteSize (Maybe (C.BitVector 8))
+  StrictStrobeType byteSize 'NoStrobe = C.BitVector (byteSize * 8)
+
+-- | Indicates valid bytes on data field.
+type Strobe (byteSize :: Nat) = C.BitVector byteSize
+
+-- | The protocol does not specify the exact use of the QoS identifier. This
+-- specification recommends that AxQOS is used as a priority indicator for the
+-- associated write or read transaction. A higher value indicates a higher
+-- priority transaction.
+--
+-- A default value of 0 indicates that the interface is not participating in any
+-- QoS scheme.
+type Qos = C.Index ((2^4) - 1)
+
+-- | The burst type and the size information, determine how the address for
+-- each transfer within the burst is calculated.
+data BurstMode
+  -- | In a fixed burst, the address is the same for every transfer in the
+  -- burst. This burst type is used for repeated accesses to the same location
+  -- such as when loading or emptying a FIFO
+  = BmFixed
+  -- | Incrementing. In an incrementing burst, the address for each transfer in
+  -- the burst is an increment of the address for the previous transfer. The
+  -- increment value depends on the size of the transfer. For example, the
+  -- address for each transfer in a burst with a size of four bytes is the
+  -- previous address plus four. This burst type is used for accesses to normal
+  -- sequential memory.
+  | BmIncr
+  -- | A wrapping burst is similar to an incrementing burst, except that the
+  -- address wraps around to a lower address if an upper address limit is
+  -- reached. The following restrictions apply to wrapping bursts:
+  --
+  --   * the start address must be aligned to the size of each transfer
+  --   * the length of the burst must be 2, 4, 8, or 16 transfers.
+  --
+  -- The behavior of a wrapping burst is:
+  --
+  --   * The lowest address used by the burst is aligned to the total size of
+  --     the data to be transferred, that is, to ((size of each transfer in the
+  --     burst) × (number of transfers in the burst)). This address is defined
+  --     as the _wrap boundary_.
+  --
+  --   * After each transfer, the address increments in the same way as for an
+  --     INCR burst. However, if this incremented address is ((wrap boundary) +
+  --     (total size of data to be transferred)) then the address wraps round to
+  --     the wrap boundary.
+  --
+  --   * The first transfer in the burst can use an address that is higher than
+  --     the wrap boundary, subject to the restrictions that apply to wrapping
+  --     bursts. This means that the address wraps for any WRAP burst for which
+  --     the first address is higher than the wrap boundary.
+  --
+  -- This burst type is used for cache line accesses.
+  --
+  | BmWrap
+  deriving (Show, C.ShowX, Generic, C.NFDataX, Eq)
+
+-- | The maximum number of bytes to transfer in each data transfer, or beat,
+-- in a burst.
+data BurstSize
+  = Bs1
+  | Bs2
+  | Bs4
+  | Bs8
+  | Bs16
+  | Bs32
+  | Bs64
+  | Bs128
+  deriving (Show, C.ShowX, Generic, C.NFDataX)
+
+-- | Convert burst size to a numeric value
+burstSizeToNum :: Num a => BurstSize -> a
+burstSizeToNum = \case
+  Bs1 -> 1
+  Bs2 -> 2
+  Bs4 -> 4
+  Bs8 -> 8
+  Bs16 -> 16
+  Bs32 -> 32
+  Bs64 -> 64
+  Bs128 -> 128
+
+-- | Whether a transaction is bufferable
+data Bufferable = NonBufferable | Bufferable
+
+-- | When set to "LookupCache", it is recommended that this transaction is
+-- allocated in the cache for performance reasons.
+data Allocate = NoLookupCache | LookupCache
+
+-- | When set to "OtherLookupCache", it is recommended that this transaction is
+-- allocated in the cache for performance reasons.
+data OtherAllocate = OtherNoLookupCache | OtherLookupCache
+
+-- | See Table A4-3 AWCACHE bit allocations
+type Cache = T4 Bufferable Modifiable OtherAllocate Allocate
+
+-- | Status of the write transaction.
+data Resp
+  -- | Normal access success. Indicates that a normal access has been
+  -- successful. Can also indicate an exclusive access has failed.
+  = ROkay
+  -- | Exclusive access okay. Indicates that either the read or write portion
+  -- of an exclusive access has been successful.
+  | RExclusiveOkay
+  -- | Slave error. Used when the access has reached the slave successfully, but
+  -- the slave wishes to return an error condition to the originating master.
+  | RSlaveError
+  -- | Decode error. Generated, typically by an interconnect component, to
+  -- indicate that there is no slave at the transaction address.
+  | RDecodeError
+  deriving (Show, C.ShowX, Generic, C.NFDataX)
+
+-- | Whether a resource is accessed with exclusive access or not
+data AtomicAccess
+  = NonExclusiveAccess
+  | ExclusiveAccess
+
+-- | Whether transaction can be modified
+data Modifiable
+  = Modifiable
+  | NonModifiable
+
+-- | An AXI master might support Secure and Non-secure operating states, and
+-- extend this concept of security to memory access.
+data Secure
+  = Secure
+  | NonSecure
+
+-- | An AXI master might support more than one level of operating privilege,
+-- and extend this concept of privilege to memory access.
+data Privileged
+  = NotPrivileged
+  | Privileged
+
+-- | Whether the transaction is an instruction access or a data access. The AXI
+-- protocol defines this indication as a hint. It is not accurate in all cases,
+-- for example, where a transaction contains a mix of instruction and data
+-- items. This specification recommends that a master sets it to "Data", to
+-- indicate a data access unless the access is specifically known to be an
+-- instruction access.
+data InstructionOrData
+  = Data
+  | Instruction
diff --git a/src/Protocols/Axi4/ReadAddress.hs b/src/Protocols/Axi4/ReadAddress.hs
new file mode 100644
index 00000000..d6e2c10d
--- /dev/null
+++ b/src/Protocols/Axi4/ReadAddress.hs
@@ -0,0 +1,203 @@
+{-|
+Defines ReadAddress channel of full AXI4 protocol with port names corresponding
+to the AXI4 specification.
+-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wno-missing-fields #-}
+
+module Protocols.Axi4.ReadAddress
+  ( M2S_ReadAddress(..)
+  , S2M_ReadAddress(..)
+  , Axi4ReadAddress
+  , mapFull
+  ) where
+
+-- base
+import Data.Coerce
+import Data.Kind (Type)
+import Data.Proxy
+import GHC.Generics (Generic)
+
+-- clash-prelude
+import qualified Clash.Prelude as C
+
+-- me
+import Protocols.Axi4.Common
+import Protocols.Internal
+import Protocols.DfLike (DfLike)
+import qualified Protocols.DfLike as DfLike
+
+-- | AXI4 Read Address channel protocol
+data Axi4ReadAddress
+  (dom :: C.Domain)
+  (kb :: KeepBurst)
+  (ksz :: KeepSize)
+  (lw :: LengthWidth)
+  (iw :: IdWidth)
+  (aw :: AddrWidth)
+  (kr :: KeepRegion)
+  (kbl :: KeepBurstLength)
+  (kl :: KeepLock)
+  (kc :: KeepCache)
+  (kp :: KeepPermissions)
+  (kq :: KeepQos)
+  (userType :: Type)
+
+instance Protocol (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where
+  type Fwd (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    C.Signal dom (M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)
+  type Bwd (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    C.Signal dom S2M_ReadAddress
+
+instance Backpressure (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where
+  boolsToBwd _ = C.fromList_lazy . coerce
+
+instance DfLike dom (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType where
+  type Data (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType =
+    M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType
+
+  type Payload userType = userType
+
+  type Ack (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType =
+    S2M_ReadAddress
+
+  getPayload _ (M2S_ReadAddress{_aruser}) = Just _aruser
+  getPayload _ M2S_NoReadAddress = Nothing
+  {-# INLINE getPayload #-}
+
+  setPayload _ _ dat (Just b) = dat{_aruser=b}
+  setPayload _ dfB _ Nothing = DfLike.noData dfB
+  {-# INLINE setPayload #-}
+
+  noData _ = M2S_NoReadAddress
+  {-# INLINE noData #-}
+
+  boolToAck _ = coerce
+  {-# INLINE boolToAck #-}
+
+  ackToBool _ = coerce
+  {-# INLINE ackToBool #-}
+
+instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) =>
+  Simulate (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where
+
+  type SimulateType (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    [M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType]
+
+  type ExpectType (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    [M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType]
+
+  type SimulateChannels (Axi4ReadAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = 1
+
+  toSimulateType _ = id
+  fromSimulateType _ = id
+
+  driveC = DfLike.drive Proxy
+  sampleC = DfLike.sample Proxy
+  stallC conf (C.head -> (stallAck, stalls)) =
+    DfLike.stall Proxy conf stallAck stalls
+
+-- | See Table A2-5 "Read address channel signals"
+
+data M2S_ReadAddress
+  (kb :: KeepBurst)
+  (ksz :: KeepSize)
+  (lw :: LengthWidth)
+  (iw :: IdWidth)
+  (aw :: AddrWidth)
+  (kr :: KeepRegion)
+  (kbl :: KeepBurstLength)
+  (kl :: KeepLock)
+  (kc :: KeepCache)
+  (kp :: KeepPermissions)
+  (kq :: KeepQos)
+  (userType :: Type)
+  = M2S_NoReadAddress
+  | M2S_ReadAddress
+    { -- | Read address id*
+      _arid :: !(C.BitVector (Width iw))
+
+      -- | Read address
+    , _araddr :: !(C.BitVector (Width aw))
+
+      -- | Read region*
+    , _arregion :: !(RegionType kr)
+
+      -- | Burst length*
+    , _arlen :: !(BurstLengthType kbl)
+
+      -- | Burst size*
+    , _arsize :: !(SizeType ksz)
+
+      -- | Burst type*
+    , _arburst :: !(BurstType kb)
+
+      -- | Lock type*
+    , _arlock :: !(LockType kl)
+
+      -- | Cache type* (has been renamed to modifiable in AXI spec)
+    , _arcache :: !(CacheType kc)
+
+      -- | Protection type
+    , _arprot :: !(PermissionsType kp)
+
+      -- | QoS value
+    , _arqos :: !(QosType kq)
+
+      -- | User data
+    , _aruser :: !userType
+    }
+  deriving (Generic)
+
+-- | See Table A2-5 "Read address channel signals"
+newtype S2M_ReadAddress = S2M_ReadAddress
+  { _arready :: Bool }
+  deriving (Show, Generic, C.NFDataX)
+
+deriving instance
+  ( C.KnownNat (Width iw)
+  , C.KnownNat (Width aw)
+  , Show (SizeType ksz)
+  , Show (BurstType kb)
+  , Show userType
+  , Show (RegionType kr)
+  , Show (BurstLengthType kbl)
+  , Show (LockType kl)
+  , Show (CacheType kc)
+  , Show (PermissionsType kp)
+  , Show (QosType kq) ) =>
+  Show (M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)
+
+deriving instance
+  ( C.NFDataX userType
+  , C.NFDataX (BurstType kb)
+  , C.NFDataX (SizeType ksz)
+  , C.NFDataX (BurstType kb)
+  , C.NFDataX userType
+  , C.NFDataX (RegionType kr)
+  , C.NFDataX (BurstLengthType kbl)
+  , C.NFDataX (LockType kl)
+  , C.NFDataX (CacheType kc)
+  , C.NFDataX (PermissionsType kp)
+  , C.NFDataX (QosType kq) ) =>
+  C.NFDataX (M2S_ReadAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)
+
+-- | Circuit that transforms the LHS 'Axi4ReadAddress' protocol to a
+-- version using different type parameters according to two functions
+-- that can transform the data and ack signal to and from the other protocol.
+mapFull ::
+  forall dom
+    kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 t1
+    kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 t2 .
+  (M2S_ReadAddress kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 t1 ->
+    M2S_ReadAddress kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 t2) ->
+  (S2M_ReadAddress -> S2M_ReadAddress) ->
+  Circuit
+    (Axi4ReadAddress dom kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 t1)
+    (Axi4ReadAddress dom kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 t2)
+mapFull = DfLike.mapDfLike Proxy Proxy
diff --git a/src/Protocols/Axi4/ReadData.hs b/src/Protocols/Axi4/ReadData.hs
new file mode 100644
index 00000000..03901d1b
--- /dev/null
+++ b/src/Protocols/Axi4/ReadData.hs
@@ -0,0 +1,425 @@
+{-|
+Defines ReadData channel of full AXI4 protocol with port names corresponding
+to the AXI4 specification.
+-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wno-missing-fields #-}
+
+module Protocols.Axi4.ReadData
+  ( M2S_ReadData(..)
+  , S2M_ReadData(..)
+  , Axi4ReadData
+  , mapFull
+
+    -- * Operations on Df like protocols
+  , const, void, pure
+  , map, bimap
+  , fst, snd
+  , mapMaybe, catMaybes
+  , filter
+  , either
+  , first, {-firstT,-} mapLeft
+  , second, {-secondT,-} mapRight
+  , zipWith, zip
+  , partition
+  , route
+  , select
+  , selectN
+  , selectUntil
+  , fanin
+  , mfanin
+  , fanout
+  , bundleVec
+  , unbundleVec
+  , roundrobin
+  , roundrobinCollect
+  , registerFwd
+  , registerBwd
+
+  ) where
+
+-- base
+import Data.Coerce (coerce)
+import Data.Bifunctor (Bifunctor)
+import Data.Kind (Type)
+import GHC.Generics (Generic)
+import Data.Proxy
+import           Prelude hiding
+  ((!!), map, zip, zipWith, filter, fst, snd, either, const, pure)
+
+-- clash-prelude
+import qualified Clash.Prelude as C
+
+-- me
+import Protocols.Axi4.Common
+import Protocols.Internal
+import Protocols.DfLike (DfLike)
+import qualified Protocols.DfLike as DfLike
+
+-- | AXI4 Read Data channel protocol
+data Axi4ReadData
+  (dom :: C.Domain)
+  (kr :: KeepResponse)
+  (iw :: IdWidth)
+  (userType :: Type)
+  (dataType :: Type)
+
+instance Protocol (Axi4ReadData dom kr iw userType dataType) where
+  type Fwd (Axi4ReadData dom kr iw userType dataType) =
+    C.Signal dom (S2M_ReadData kr iw userType dataType)
+  type Bwd (Axi4ReadData dom kr iw userType dataType) =
+    C.Signal dom M2S_ReadData
+
+instance Backpressure (Axi4ReadData dom kr iw userType dataType) where
+  boolsToBwd _ = C.fromList_lazy . coerce
+
+instance DfLike dom (Axi4ReadData dom kr iw userType) dataType where
+  type Data (Axi4ReadData dom kr iw userType) dataType =
+    S2M_ReadData kr iw userType dataType
+
+  type Payload dataType = dataType
+
+  type Ack (Axi4ReadData dom kr iw userType) dataType  =
+    M2S_ReadData
+
+  getPayload _ (S2M_ReadData{_rdata}) = Just _rdata
+  getPayload _ S2M_NoReadData = Nothing
+  {-# INLINE getPayload #-}
+
+  setPayload _ _ dat (Just b) = dat{_rdata=b}
+  setPayload _ dfB _ Nothing = DfLike.noData dfB
+  {-# INLINE setPayload #-}
+
+  noData _ = S2M_NoReadData
+  {-# INLINE noData #-}
+
+  boolToAck _ = coerce
+  {-# INLINE boolToAck #-}
+
+  ackToBool _ = coerce
+  {-# INLINE ackToBool #-}
+
+instance (C.KnownDomain dom, C.NFDataX dataType, C.ShowX dataType, Show dataType) =>
+  Simulate (Axi4ReadData dom kr iw userType dataType) where
+
+  type SimulateType (Axi4ReadData dom kr iw userType dataType) =
+    [S2M_ReadData kr iw userType dataType]
+
+  type ExpectType (Axi4ReadData dom kr iw userType dataType) =
+    [S2M_ReadData kr iw userType dataType]
+
+  type SimulateChannels (Axi4ReadData dom kr iw userType dataType) = 1
+
+  toSimulateType _ = id
+  fromSimulateType _ = id
+
+  driveC = DfLike.drive Proxy
+  sampleC = DfLike.sample Proxy
+  stallC conf (C.head -> (stallAck, stalls)) =
+    DfLike.stall Proxy conf stallAck stalls
+
+-- | See Table A2-6 "Read data channel signals"
+data S2M_ReadData
+  (kr :: KeepResponse)
+  (iw :: IdWidth)
+  (userType :: Type)
+  (dataType :: Type)
+  = S2M_NoReadData
+  | S2M_ReadData
+    { -- | Read address id*
+      _rid :: !(C.BitVector (Width iw))
+
+    , -- | Read data
+      _rdata :: !dataType
+
+      -- | Read response
+    , _rresp :: !(ResponseType kr)
+
+      -- | Read last
+    , _rlast :: !Bool
+
+      -- | User data
+    , _ruser :: !userType
+    }
+  deriving (Generic)
+
+-- | See Table A2-6 "Read data channel signals"
+newtype M2S_ReadData = M2S_ReadData { _rready :: Bool }
+  deriving (Show, Generic, C.NFDataX)
+
+deriving instance
+  ( C.NFDataX userType
+  , C.NFDataX dataType
+  , C.NFDataX (ResponseType kr) ) =>
+  C.NFDataX (S2M_ReadData kr iw userType dataType)
+
+deriving instance
+  ( C.KnownNat (Width iw)
+  , Show userType
+  , Show dataType
+  , Show (ResponseType kr) ) =>
+  Show (S2M_ReadData kr iw userType dataType)
+
+
+-- | Like 'P.map', but over the data in the AXI4 read channel.
+map :: (a -> b) -> Circuit
+  (Axi4ReadData dom kr iw userType a)
+  (Axi4ReadData dom kr iw userType b)
+map = DfLike.map Proxy Proxy
+
+-- | Like 'bimap', but over the data in the AXI4 read channel.
+bimap :: Bifunctor p => (a -> b) -> (c -> d) -> Circuit
+  (Axi4ReadData dom kr iw userType (p a c))
+  (Axi4ReadData dom kr iw userType (p b d))
+bimap = DfLike.bimap
+
+-- | Like 'P.fst', but over the data in the AXI4 read channel.
+fst :: Circuit
+  (Axi4ReadData dom kr iw userType (a, b))
+  (Axi4ReadData dom kr iw userType a)
+fst = DfLike.fst
+
+-- | Like 'P.snd', but over the data in the AXI4 read channel.
+snd :: Circuit
+  (Axi4ReadData dom kr iw userType (a, b))
+  (Axi4ReadData dom kr iw userType b)
+snd = DfLike.snd
+
+-- | Like 'Data.Bifunctor.first', but over the data in the AXI4 read channel.
+first :: Bifunctor p => (a -> b) -> Circuit
+  (Axi4ReadData dom kr iw userType (p a c))
+  (Axi4ReadData dom kr iw userType (p b c))
+first = DfLike.first
+
+-- | Like 'Data.Bifunctor.second', but over the data in the AXI4 read channel.
+second :: Bifunctor p => (b -> c) -> Circuit
+  (Axi4ReadData dom kr iw userType (p a b))
+  (Axi4ReadData dom kr iw userType (p a c))
+second = DfLike.second
+
+-- | Acknowledge but ignore data from LHS protocol. Send a static value /b/.
+const :: C.HiddenReset dom => S2M_ReadData kr iw userType b -> Circuit
+  (Axi4ReadData dom kr iw userType a)
+  (Axi4ReadData dom kr iw userType b)
+const = DfLike.const Proxy Proxy
+
+-- | Drive a constant value composed of /a/.
+pure :: S2M_ReadData kr iw userType a -> Circuit
+  ()
+  (Axi4ReadData dom kr iw userType a)
+pure = DfLike.pure Proxy
+
+-- | Drive a constant value composed of /a/.
+void :: C.HiddenReset dom => Circuit (Axi4ReadData dom kr iw userType a) ()
+void = DfLike.void Proxy
+
+-- | Like 'Data.Maybe.catMaybes', but over a AXI4 read data stream.
+catMaybes :: Circuit
+  (Axi4ReadData dom kr iw userType (Maybe a))
+  (Axi4ReadData dom kr iw userType a)
+catMaybes = DfLike.catMaybes Proxy Proxy
+
+-- | Like 'Data.Maybe.mapMaybe', but over payload (/a/) of a AXI4 read data stream.
+mapMaybe :: (a -> Maybe b) -> Circuit
+  (Axi4ReadData dom kr iw userType a)
+  (Axi4ReadData dom kr iw userType b)
+mapMaybe = DfLike.mapMaybe
+
+-- | Like 'P.filter', but over a AXI4 read data stream.
+filter :: forall dom a kr iw userType. (a -> Bool) -> Circuit
+  (Axi4ReadData dom kr iw userType a)
+  (Axi4ReadData dom kr iw userType a)
+filter = DfLike.filter Proxy
+
+-- | Like 'Data.Either.Combinators.mapLeft', but over the data in the AXI4 read channel.
+mapLeft :: (a -> b) -> Circuit
+  (Axi4ReadData dom kr iw userType (Either a c))
+  (Axi4ReadData dom kr iw userType (Either b c))
+mapLeft = DfLike.mapLeft
+
+-- | Like 'Data.Either.Combinators.mapRight', but over the data in the AXI4 read channel.
+mapRight :: (b -> c) -> Circuit
+  (Axi4ReadData dom kr iw userType (Either a b))
+  (Axi4ReadData dom kr iw userType (Either a c))
+mapRight = DfLike.mapRight
+
+-- | Like 'Data.Either.either', but over a AXI4 read data stream.
+either :: (a -> c) -> (b -> c) -> Circuit
+  (Axi4ReadData dom kr iw userType (Either a b))
+  (Axi4ReadData dom kr iw userType c)
+either = DfLike.either
+
+
+-- | Like 'P.zipWith', but over two AXI4 read data streams.
+zipWith ::
+  forall dom a b c kr iw userType .
+  (a -> b -> c) ->
+  Circuit
+    (Axi4ReadData dom kr iw userType a, Axi4ReadData dom kr iw userType b)
+    (Axi4ReadData dom kr iw userType c)
+zipWith = DfLike.zipWith Proxy Proxy Proxy
+
+-- | Like 'P.zip', but over two AXI4 read data streams.
+zip :: forall a b dom kr iw userType . Circuit
+  (Axi4ReadData dom kr iw userType a, Axi4ReadData dom kr iw userType b)
+  (Axi4ReadData dom kr iw userType (a, b))
+zip = DfLike.zip Proxy Proxy Proxy
+
+-- | Like 'P.partition', but over AXI4 read data streams
+partition :: forall dom a kr iw userType. (a -> Bool) -> Circuit
+  (Axi4ReadData dom kr iw userType a)
+  (Axi4ReadData dom kr iw userType a, Axi4ReadData dom kr iw userType a)
+partition = DfLike.partition Proxy
+
+
+-- | Route a AXI4 read data stream to another corresponding to the index
+route ::
+  forall n dom a kr iw userType .
+  C.KnownNat n => Circuit
+    (Axi4ReadData dom kr iw userType (C.Index n, a))
+    (C.Vec n (Axi4ReadData dom kr iw userType a))
+route = DfLike.route Proxy Proxy
+
+
+-- | Select data from the channel indicated by the AXI4 read data stream carrying
+-- @Index n@.
+select ::
+  forall n dom a kr iw userType .
+  C.KnownNat n =>
+  Circuit
+    (C.Vec n (Axi4ReadData dom kr iw userType a), Axi4ReadData dom kr iw userType (C.Index n))
+    (Axi4ReadData dom kr iw userType a)
+select = DfLike.select
+
+
+
+-- | Select /selectN/ samples from channel /n/.
+selectN ::
+  forall n selectN dom a kr iw userType.
+  ( C.HiddenClockResetEnable dom
+  , C.KnownNat selectN
+  , C.KnownNat n
+  ) =>
+  Circuit
+    (C.Vec n (Axi4ReadData dom kr iw userType a), Axi4ReadData dom kr iw userType (C.Index n, C.Index selectN))
+    (Axi4ReadData dom kr iw userType a)
+selectN = DfLike.selectN Proxy Proxy
+
+-- | Selects samples from channel /n/ until the predicate holds. The cycle in
+-- which the predicate turns true is included.
+selectUntil ::
+  forall n dom a kr iw userType .
+  C.KnownNat n =>
+  (a -> Bool) ->
+  Circuit
+    (C.Vec n (Axi4ReadData dom kr iw userType a), Axi4ReadData dom kr iw userType (C.Index n))
+    (Axi4ReadData dom kr iw userType a)
+selectUntil = DfLike.selectUntil Proxy Proxy
+
+-- | Copy data of a single AXI4 read data stream to multiple. LHS will only receive
+-- an acknowledgement when all RHS receivers have acknowledged data.
+fanout ::
+  forall n dom a kr iw userType .
+  (C.KnownNat n, C.HiddenClockResetEnable dom, 1 C.<= n) =>
+  Circuit
+    (Axi4ReadData dom kr iw userType a)
+    (C.Vec n (Axi4ReadData dom kr iw userType a))
+fanout = DfLike.fanout Proxy
+
+-- | Merge data of multiple AXI4 read data streams using a user supplied function
+fanin ::
+  forall n dom a kr iw userType .
+  (C.KnownNat n, 1 C.<= n) =>
+  (a -> a -> a) ->
+  Circuit
+    (C.Vec n (Axi4ReadData dom kr iw userType a))
+    (Axi4ReadData dom kr iw userType a)
+fanin = DfLike.fanin
+
+-- | Merge data of multiple AXI4 read data streams using Monoid's '<>'.
+mfanin ::
+  forall n dom a kr iw userType .
+  (C.KnownNat n, Monoid a, 1 C.<= n) =>
+  Circuit
+    (C.Vec n (Axi4ReadData dom kr iw userType a))
+    (Axi4ReadData dom kr iw userType a)
+mfanin = DfLike.mfanin
+
+-- | Bundle a vector of AXI4 read data streams into one.
+bundleVec ::
+  forall n dom a kr iw userType .
+  (C.KnownNat n, 1 C.<= n) =>
+  Circuit
+    (C.Vec n (Axi4ReadData dom kr iw userType a))
+    (Axi4ReadData dom kr iw userType (C.Vec n a))
+bundleVec = DfLike.bundleVec Proxy Proxy
+
+-- | Split up a AXI4 read data stream of a vector into multiple independent AXI4 read data streams.
+unbundleVec ::
+  forall n dom a kr iw userType .
+  (C.KnownNat n, C.NFDataX a, C.HiddenClockResetEnable dom, 1 C.<= n) =>
+  Circuit
+    (Axi4ReadData dom kr iw userType (C.Vec n a))
+    (C.Vec n (Axi4ReadData dom kr iw userType a))
+unbundleVec = DfLike.unbundleVec Proxy Proxy
+
+-- | Distribute data across multiple components on the RHS. Useful if you want
+-- to parallelize a workload across multiple (slow) workers. For optimal
+-- throughput, you should make sure workers can accept data every /n/ cycles.
+roundrobin ::
+  forall n dom a kr iw userType .
+  (C.KnownNat n, C.HiddenClockResetEnable dom, 1 C.<= n) =>
+  Circuit
+    (Axi4ReadData dom kr iw userType a)
+    (C.Vec n (Axi4ReadData dom kr iw userType a))
+roundrobin = DfLike.roundrobin Proxy
+
+-- | Opposite of 'roundrobin'. Useful to collect data from workers that only
+-- produce a result with an interval of /n/ cycles.
+roundrobinCollect ::
+  forall n dom a kr iw userType .
+  (C.KnownNat n, C.HiddenClockResetEnable dom, 1 C.<= n) =>
+  DfLike.CollectMode ->
+  Circuit
+    (C.Vec n (Axi4ReadData dom kr iw userType a))
+    (Axi4ReadData dom kr iw userType a)
+roundrobinCollect = DfLike.roundrobinCollect Proxy
+
+-- | Place register on /forward/ part of a circuit.
+registerFwd ::
+  forall dom a kr iw userType .
+  (C.NFDataX a, C.HiddenClockResetEnable dom, C.NFDataX (ResponseType kr), C.NFDataX userType) =>
+  Circuit
+    (Axi4ReadData dom kr iw userType a)
+    (Axi4ReadData dom kr iw userType a)
+registerFwd = DfLike.registerFwd Proxy
+
+-- | Place register on /backward/ part of a circuit. This is implemented using a
+-- in-logic two-element shift register.
+registerBwd ::
+  (C.NFDataX a, C.HiddenClockResetEnable dom, C.NFDataX (ResponseType kr), C.NFDataX userType) =>
+  Circuit
+    (Axi4ReadData dom kr iw userType a)
+    (Axi4ReadData dom kr iw userType a)
+registerBwd = DfLike.registerBwd Proxy
+
+
+-- | Circuit that transforms the LHS version of the 'Axi4ReadData' protocol to a
+-- version using different parameters according to two functions
+-- that can transform the data and ack signal accordingly to and from the other protocol.
+mapFull ::
+  forall dom
+    kr1 iw1 userType1 dataType1
+    kr2 iw2 userType2 dataType2 .
+  (S2M_ReadData kr1 iw1 userType1 dataType1 -> S2M_ReadData kr2 iw2 userType2 dataType2) ->
+  (M2S_ReadData -> M2S_ReadData) ->
+  Circuit
+    (Axi4ReadData dom kr1 iw1 userType1 dataType1)
+    (Axi4ReadData dom kr2 iw2 userType2 dataType2)
+mapFull = DfLike.mapDfLike Proxy Proxy
+
diff --git a/src/Protocols/Axi4/WriteAddress.hs b/src/Protocols/Axi4/WriteAddress.hs
new file mode 100644
index 00000000..143cb2e8
--- /dev/null
+++ b/src/Protocols/Axi4/WriteAddress.hs
@@ -0,0 +1,201 @@
+{-|
+Defines WriteAddress channel of full AXI4 protocol with port names corresponding
+to the AXI4 specification.
+-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wno-missing-fields #-}
+
+module Protocols.Axi4.WriteAddress
+  ( M2S_WriteAddress(..)
+  , S2M_WriteAddress(..)
+  , Axi4WriteAddress
+  , mapFull
+  ) where
+
+-- base
+import Data.Coerce (coerce)
+import Data.Kind (Type)
+import Data.Proxy
+import GHC.Generics (Generic)
+
+-- clash-prelude
+import qualified Clash.Prelude as C
+
+-- me
+import Protocols.Axi4.Common
+import Protocols.Internal
+import Protocols.DfLike (DfLike)
+import qualified Protocols.DfLike as DfLike
+
+-- | AXI4 Write Address channel protocol
+data Axi4WriteAddress
+  (dom :: C.Domain)
+  (kb :: KeepBurst)
+  (ksz :: KeepSize)
+  (lw :: LengthWidth)
+  (iw :: IdWidth)
+  (aw :: AddrWidth)
+  (kr :: KeepRegion)
+  (kbl :: KeepBurstLength)
+  (kl :: KeepLock)
+  (kc :: KeepCache)
+  (kp :: KeepPermissions)
+  (kq :: KeepQos)
+  (userType :: Type)
+
+instance Protocol (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where
+  type Fwd (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    C.Signal dom (M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)
+  type Bwd (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    C.Signal dom S2M_WriteAddress
+
+instance Backpressure (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where
+  boolsToBwd _ = C.fromList_lazy . coerce
+
+instance DfLike dom (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType where
+  type Data (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType =
+    M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType
+
+  type Payload userType = userType
+
+  type Ack (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq) userType =
+    S2M_WriteAddress
+
+  getPayload _ (M2S_WriteAddress{_awuser}) = Just _awuser
+  getPayload _ M2S_NoWriteAddress = Nothing
+  {-# INLINE getPayload #-}
+
+  setPayload _ _ dat (Just b) = dat{_awuser=b}
+  setPayload _ dfB _ Nothing = DfLike.noData dfB
+  {-# INLINE setPayload #-}
+
+  noData _ = M2S_NoWriteAddress
+  {-# INLINE noData #-}
+
+  boolToAck _ = coerce
+  {-# INLINE boolToAck #-}
+
+  ackToBool _ = coerce
+  {-# INLINE ackToBool #-}
+
+instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) =>
+  Simulate (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) where
+
+  type SimulateType (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    [M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType]
+
+  type ExpectType (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) =
+    [M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType]
+
+  type SimulateChannels (Axi4WriteAddress dom kb ksz lw iw aw kr kbl kl kc kp kq userType) = 1
+
+  toSimulateType _ = id
+  fromSimulateType _ = id
+
+  driveC = DfLike.drive Proxy
+  sampleC = DfLike.sample Proxy
+  stallC conf (C.head -> (stallAck, stalls)) =
+    DfLike.stall Proxy conf stallAck stalls
+
+-- | See Table A2-2 "Write address channel signals"
+data M2S_WriteAddress
+  (kb :: KeepBurst)
+  (ksz :: KeepSize)
+  (lw :: LengthWidth)
+  (iw :: IdWidth)
+  (aw :: AddrWidth)
+  (kr :: KeepRegion)
+  (kbl :: KeepBurstLength)
+  (kl :: KeepLock)
+  (kc :: KeepCache)
+  (kp :: KeepPermissions)
+  (kq :: KeepQos)
+  (userType :: Type)
+  = M2S_NoWriteAddress
+  | M2S_WriteAddress
+    { -- | Write address id*
+      _awid :: !(C.BitVector (Width iw))
+
+      -- | Write address
+    , _awaddr :: !(C.BitVector (Width aw))
+
+      -- | Write region*
+    , _awregion:: !(RegionType kr)
+
+      -- | Burst length*
+    , _awlen :: !(BurstLengthType kbl)
+
+      -- | Burst size*
+    , _awsize :: !(SizeType ksz)
+
+      -- | Burst type*
+    , _awburst :: !(BurstType kb)
+
+      -- | Lock type*
+    , _awlock :: !(LockType kl)
+
+      -- | Cache type*
+    , _awcache :: !(CacheType kc)
+
+      -- | Protection type
+    , _awprot :: !(PermissionsType kp)
+
+      -- | QoS value
+    , _awqos :: !(QosType kq)
+
+      -- | User data
+    , _awuser :: !userType
+    }
+  deriving (Generic)
+
+-- | See Table A2-2 "Write address channel signals"
+newtype S2M_WriteAddress = S2M_WriteAddress { _awready :: Bool }
+  deriving (Show, Generic, C.NFDataX)
+
+deriving instance
+  ( C.KnownNat (Width iw)
+  , C.KnownNat (Width aw)
+  , Show (SizeType ksz)
+  , Show (BurstType kb)
+  , Show userType
+  , Show (RegionType kr)
+  , Show (BurstLengthType kbl)
+  , Show (LockType kl)
+  , Show (CacheType kc)
+  , Show (PermissionsType kp)
+  , Show (QosType kq) ) =>
+  Show (M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)
+
+deriving instance
+  ( C.NFDataX userType
+  , C.NFDataX (BurstType kb)
+  , C.NFDataX (SizeType ksz)
+  , C.NFDataX (BurstType kb)
+  , C.NFDataX userType
+  , C.NFDataX (RegionType kr)
+  , C.NFDataX (BurstLengthType kbl)
+  , C.NFDataX (LockType kl)
+  , C.NFDataX (CacheType kc)
+  , C.NFDataX (PermissionsType kp)
+  , C.NFDataX (QosType kq) ) =>
+  C.NFDataX (M2S_WriteAddress kb ksz lw iw aw kr kbl kl kc kp kq userType)
+
+-- | Circuit that transforms the LHS 'Axi4WriteAddress' protocol to a
+-- version using different type parameters according to two functions
+-- that can transform the data and ack signal to and from the other protocol.
+mapFull ::
+  forall dom
+    kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 userType1
+    kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 userType2 .
+  (M2S_WriteAddress kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 userType1 ->
+    M2S_WriteAddress kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 userType2) ->
+  (S2M_WriteAddress -> S2M_WriteAddress) ->
+  Circuit
+    (Axi4WriteAddress dom kb1 ksz1 lw1 iw1 aw1 kr1 kbl1 kl1 kc1 kp1 kq1 userType1)
+    (Axi4WriteAddress dom kb2 ksz2 lw2 iw2 aw2 kr2 kbl2 kl2 kc2 kp2 kq2 userType2)
+mapFull = DfLike.mapDfLike Proxy Proxy
diff --git a/src/Protocols/Axi4/WriteData.hs b/src/Protocols/Axi4/WriteData.hs
new file mode 100644
index 00000000..e8679eba
--- /dev/null
+++ b/src/Protocols/Axi4/WriteData.hs
@@ -0,0 +1,142 @@
+{-|
+Defines WriteData channel of full AXI4 protocol with port names corresponding
+to the AXI4 specification.
+-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wno-missing-fields #-}
+
+module Protocols.Axi4.WriteData
+  ( M2S_WriteData(..)
+  , S2M_WriteData(..)
+  , Axi4WriteData
+  , mapFull
+  ) where
+
+-- base
+import Data.Coerce (coerce)
+import Data.Kind (Type)
+import GHC.Generics (Generic)
+import GHC.TypeNats (Nat)
+import Data.Proxy
+import Prelude hiding
+  ((!!), map, zip, zipWith, filter, fst, snd, either, const, pure)
+
+-- clash-prelude
+import qualified Clash.Prelude as C
+
+-- me
+import Protocols.Axi4.Common
+import Protocols.Internal
+import Protocols.DfLike (DfLike)
+import qualified Protocols.DfLike as DfLike
+
+-- | AXI4 Write Data channel protocol
+data Axi4WriteData
+  (dom :: C.Domain)
+  (ks :: KeepStrobe)
+  (nBytes :: Nat)
+  (userType :: Type)
+
+instance Protocol (Axi4WriteData dom ks nBytes userType) where
+  type Fwd (Axi4WriteData dom ks nBytes userType) =
+    C.Signal dom (M2S_WriteData ks nBytes userType)
+  type Bwd (Axi4WriteData dom ks nBytes userType) =
+    C.Signal dom S2M_WriteData
+
+instance Backpressure (Axi4WriteData dom ks dataType userType) where
+  boolsToBwd _ = C.fromList_lazy . coerce
+
+instance DfLike dom (Axi4WriteData dom ks dataType) userType where
+  type Data (Axi4WriteData dom ks dataType) userType =
+    M2S_WriteData ks dataType userType
+
+  type Payload userType = userType
+
+  type Ack (Axi4WriteData dom ks dataType) userType =
+    S2M_WriteData
+
+  getPayload _ (M2S_WriteData{_wuser}) = Just _wuser
+  getPayload _ _ = Nothing
+  {-# INLINE getPayload #-}
+
+  setPayload _ _ dat (Just b) = dat{_wuser=b}
+  setPayload _ dfB _ Nothing = DfLike.noData dfB
+  {-# INLINE setPayload #-}
+
+  noData _ = M2S_NoWriteData
+  {-# INLINE noData #-}
+
+  boolToAck _ = coerce
+  {-# INLINE boolToAck #-}
+
+  ackToBool _ = coerce
+  {-# INLINE ackToBool #-}
+
+instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) =>
+  Simulate (Axi4WriteData dom ks nBytes userType) where
+
+  type SimulateType (Axi4WriteData dom ks nBytes userType) =
+    [M2S_WriteData ks nBytes userType]
+
+  type ExpectType (Axi4WriteData dom ks nBytes userType) =
+    [M2S_WriteData ks nBytes userType]
+
+  type SimulateChannels (Axi4WriteData dom ks nBytes userType) = 1
+
+  toSimulateType _ = id
+  fromSimulateType _ = id
+
+  driveC = DfLike.drive Proxy
+  sampleC = DfLike.sample Proxy
+  stallC conf (C.head -> (stallAck, stalls)) =
+    DfLike.stall Proxy conf stallAck stalls
+
+-- | See Table A2-3 "Write data channel signals". If strobing is kept, the data
+-- will be a vector of 'Maybe' bytes. If strobing is not kept, data will be a
+-- 'C.BitVector'.
+data M2S_WriteData
+  (ks :: KeepStrobe)
+  (nBytes :: Nat)
+  (userType :: Type)
+  = M2S_NoWriteData
+  | M2S_WriteData
+    { -- | Write data
+      _wdata :: !(StrictStrobeType nBytes ks)
+
+      -- | Write last
+    , _wlast :: !Bool
+
+      -- | User data
+    , _wuser :: !userType
+    }
+  deriving (Generic)
+
+-- | See Table A2-3 "Write data channel signals"
+newtype S2M_WriteData = S2M_WriteData { _wready :: Bool }
+  deriving (Show, Generic, C.NFDataX)
+
+deriving instance
+  ( C.NFDataX userType
+  , C.NFDataX (StrictStrobeType nBytes ks) ) =>
+  C.NFDataX (M2S_WriteData ks nBytes userType)
+
+deriving instance
+  ( Show userType
+  , Show (StrictStrobeType nBytes ks)
+  , C.KnownNat nBytes ) =>
+  Show (M2S_WriteData ks nBytes userType)
+
+-- | Circuit that transforms the LHS 'Axi4WriteData' protocol to a
+-- version using different type parameters according to two functions
+-- that can transform the data and ack signal to and from the other protocol.
+mapFull ::
+  forall dom ks1 ks2 nBytes1 nBytes2 t1 t2.
+  (M2S_WriteData ks1 nBytes1 t1 -> M2S_WriteData ks2 nBytes2 t2) ->
+  (S2M_WriteData -> S2M_WriteData) ->
+  Circuit ((Axi4WriteData dom ks1 nBytes1) t1) ((Axi4WriteData dom ks2 nBytes2) t2)
+mapFull = DfLike.mapDfLike Proxy Proxy
diff --git a/src/Protocols/Axi4/WriteResponse.hs b/src/Protocols/Axi4/WriteResponse.hs
new file mode 100644
index 00000000..a437d248
--- /dev/null
+++ b/src/Protocols/Axi4/WriteResponse.hs
@@ -0,0 +1,141 @@
+{-|
+Defines WriteResponse channel of full AXI4 protocol with port names corresponding
+to the AXI4 specification.
+-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wno-missing-fields #-}
+
+module Protocols.Axi4.WriteResponse
+  ( M2S_WriteResponse(..)
+  , S2M_WriteResponse(..)
+  , Axi4WriteResponse
+  , mapFull
+  ) where
+
+-- base
+import Data.Coerce (coerce)
+import Data.Kind (Type)
+import GHC.Generics (Generic)
+import Data.Proxy
+
+-- clash-prelude
+import qualified Clash.Prelude as C
+
+-- me
+import Protocols.Axi4.Common
+import Protocols.Internal
+import Protocols.DfLike (DfLike)
+import qualified Protocols.DfLike as DfLike
+
+-- | AXI4 Read Data channel protocol
+data Axi4WriteResponse
+  (dom :: C.Domain)
+  (kr :: KeepResponse)
+  (iw :: IdWidth)
+  (userType :: Type)
+
+instance Protocol (Axi4WriteResponse dom kr iw userType) where
+  type Fwd (Axi4WriteResponse dom kr iw userType) =
+    C.Signal dom (S2M_WriteResponse kr iw userType)
+  type Bwd (Axi4WriteResponse dom kr iw userType) =
+    C.Signal dom M2S_WriteResponse
+
+instance Backpressure (Axi4WriteResponse dom kr iw userType) where
+  boolsToBwd _ = C.fromList_lazy . coerce
+
+instance DfLike dom (Axi4WriteResponse dom kr iw) userType where
+  type Data (Axi4WriteResponse dom kr iw) userType =
+    S2M_WriteResponse kr iw userType
+
+  type Payload userType = userType
+
+  type Ack (Axi4WriteResponse dom kr iw) userType =
+    M2S_WriteResponse
+
+  getPayload _ (S2M_WriteResponse{_buser}) = Just _buser
+  getPayload _ _ = Nothing
+  {-# INLINE getPayload #-}
+
+  setPayload _ _ dat (Just b) = dat{_buser=b}
+  setPayload _ dfB _ Nothing = DfLike.noData dfB
+  {-# INLINE setPayload #-}
+
+  noData _ = S2M_NoWriteResponse
+  {-# INLINE noData #-}
+
+  boolToAck _ = coerce
+  {-# INLINE boolToAck #-}
+
+  ackToBool _ = coerce
+  {-# INLINE ackToBool #-}
+
+instance (C.KnownDomain dom, C.NFDataX userType, C.ShowX userType, Show userType) =>
+  Simulate (Axi4WriteResponse dom kr iw userType) where
+
+  type SimulateType (Axi4WriteResponse dom kr iw userType) =
+    [S2M_WriteResponse kr iw userType]
+
+  type ExpectType (Axi4WriteResponse dom kr iw userType) =
+    [S2M_WriteResponse kr iw userType]
+
+  type SimulateChannels (Axi4WriteResponse dom kr iw userType) = 1
+
+  toSimulateType _ = id
+  fromSimulateType _ = id
+
+  driveC = DfLike.drive Proxy
+  sampleC = DfLike.sample Proxy
+  stallC conf (C.head -> (stallAck, stalls)) =
+    DfLike.stall Proxy conf stallAck stalls
+
+-- | See Table A2-4 "Write response channel signals"
+data S2M_WriteResponse
+  (kr :: KeepResponse)
+  (iw :: IdWidth)
+  (userType :: Type)
+  = S2M_NoWriteResponse
+  | S2M_WriteResponse
+    { -- | Response ID
+      _bid :: !(C.BitVector (Width iw))
+
+      -- | Write response
+    , _bresp :: !(ResponseType kr)
+
+      -- | User data
+    , _buser :: !userType
+    }
+  deriving (Generic)
+
+-- | See Table A2-4 "Write response channel signals"
+newtype M2S_WriteResponse = M2S_WriteResponse { _bready :: Bool }
+  deriving (Show, Generic, C.NFDataX)
+
+deriving instance
+  ( C.NFDataX userType
+  , C.NFDataX (ResponseType kr) ) =>
+  C.NFDataX (S2M_WriteResponse kr iw userType)
+
+deriving instance
+  ( Show userType
+  , Show (ResponseType kr)
+  , C.KnownNat (Width iw) ) =>
+  Show (S2M_WriteResponse kr iw userType)
+
+-- | Circuit that transforms the LHS 'Axi4WriteResponse' protocol to a
+-- version using different type parameters according to two functions
+-- that can transform the data and ack signal to and from the other protocol.
+mapFull ::
+  forall dom
+    kr1 iw1 userType1
+    kr2 iw2 userType2 .
+  (S2M_WriteResponse kr1 iw1 userType1 -> S2M_WriteResponse kr2 iw2 userType2) ->
+  (M2S_WriteResponse -> M2S_WriteResponse) ->
+  Circuit
+    (Axi4WriteResponse dom kr1 iw1 userType1)
+    (Axi4WriteResponse dom kr2 iw2 userType2)
+mapFull = DfLike.mapDfLike Proxy Proxy
diff --git a/src/Protocols/Df.hs b/src/Protocols/Df.hs
index 26f18707..4148a295 100644
--- a/src/Protocols/Df.hs
+++ b/src/Protocols/Df.hs
@@ -16,7 +16,7 @@ carries data, no metadata. For documentation see:
 
 module Protocols.Df
   ( -- * Types
-    Df, Data(..), Ack(..)
+    Df, Data(..)
 
     -- * Operations on Df like protocols
   , const, void, pure
@@ -65,7 +65,6 @@ import           Prelude hiding
 
 import           Data.Bifunctor (Bifunctor)
 import           Data.Coerce (coerce)
-import           Data.Default (Default)
 import           Data.Kind (Type)
 import qualified Data.Maybe as Maybe
 import           Data.Proxy
@@ -77,7 +76,7 @@ import           Clash.Signal.Internal (Signal)
 import qualified Clash.Prelude as C
 
 -- me
-import           Protocols.Internal hiding (Ack(..))
+import           Protocols.Internal
 import           Protocols.DfLike (DfLike)
 import qualified Protocols.DfLike as DfLike
 
@@ -98,11 +97,11 @@ instance Protocol (Df dom a) where
   -- | Forward part of simple dataflow: @Signal dom (Data meta a)@
   type Fwd (Df dom a) = Signal dom (Data a)
 
-  -- | Backward part of simple dataflow: @Signal dom (Ack meta a)@
-  type Bwd (Df dom a) = Signal dom (Ack a)
+  -- | Backward part of simple dataflow: @Signal dom Bool@
+  type Bwd (Df dom a) = Signal dom Ack
 
 instance Backpressure (Df dom a) where
-  boolsToBwd = C.fromList_lazy . coerce
+  boolsToBwd _ = C.fromList_lazy . coerce
 
 -- | Data sent over forward channel of 'Df'. Note that this data type is strict
 -- on its data field.
@@ -135,14 +134,6 @@ dataToMaybe :: Data a -> Maybe a
 dataToMaybe NoData = Nothing
 dataToMaybe (Data a) = Just a
 
--- | Like 'Protocols.Df.Ack', but carrying phantom type variables to satisfy
--- 'Bwd's injectivity requirement.
-newtype Ack a = Ack Bool
-  deriving (Show)
-
-instance Default (Ack a) where
-  def = Ack True
-
 instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom a) where
   type SimulateType (Df dom a) = [Data a]
   type ExpectType (Df dom a) = [a]
@@ -158,7 +149,7 @@ instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom
 instance DfLike dom (Df dom) a where
   type Data (Df dom) a = Data a
   type Payload a = a
-  type Ack (Df dom) a = Ack a
+  type Ack (Df dom) a = Ack
 
   getPayload _ (Data a) = Just a
   getPayload _ NoData = Nothing
@@ -177,20 +168,6 @@ instance DfLike dom (Df dom) a where
   ackToBool _ = coerce
   {-# INLINE ackToBool #-}
 
--- | Interpret simple dataflow carrying a tuple as 'Df' with /meta/ and /payload/
--- asDf :: Circuit (Df dom (meta, payload)) (Df dom meta payload)
--- asDf = Df.mapInternal (B.swapMap go coerce)
---  where
---   go (Data (meta, a)) = Df.Data meta a
---   go NoData = Df.NoData
-
--- -- | Interpret 'Df' as simple dataflow carrying a tuple of /meta/ and /payload/
--- asDf :: Circuit (Df dom meta payload) (Df dom (meta, payload))
--- asDf = Df.mapInternal (B.swapMap go coerce)
---  where
---   go (Df.Data meta a) = Data (meta, a)
---   go Df.NoData = NoData
-
 -- | Force a /nack/ on the backward channel and /no data/ on the forward
 -- channel if reset is asserted.
 forceResetSanity :: forall dom a. C.HiddenClockResetEnable dom => Circuit (Df dom a) (Df dom a)
diff --git a/src/Protocols/DfLike.hs b/src/Protocols/DfLike.hs
index f6e7cc59..1abc4d55 100644
--- a/src/Protocols/DfLike.hs
+++ b/src/Protocols/DfLike.hs
@@ -21,6 +21,7 @@ module Protocols.DfLike
 
     -- * Operations on Df like protocols
   , const, pure, void
+  , mapDfLike
   , map, bimap
   , fst, snd
   , mapMaybe, catMaybes
@@ -67,6 +68,7 @@ import           Data.Kind (Type)
 import qualified Data.Maybe as Maybe
 import           Data.Proxy (Proxy(..))
 import qualified Data.List.NonEmpty
+import           Data.List ((\\))
 import           GHC.Stack (HasCallStack)
 
 -- me
@@ -77,7 +79,6 @@ import           Clash.Prelude (Domain, type (+), type (-), type (<=))
 import           Clash.Signal.Internal (Signal(..))
 import qualified Clash.Prelude as C
 import qualified Clash.Explicit.Prelude as CE
-import Data.List ((\\))
 
 
 -- | Generalization of Df-like protocols (Df, DfMeta, AXI, Avalon, ..). This
@@ -96,7 +97,7 @@ class ( Protocol (df a)
   type Payload a = (r :: Type) | r -> a
 
   -- | Acknowledgement data carried on backward channel
-  type Ack df a = (r :: Type) | r -> a
+  type Ack df a
 
   noData ::
     Proxy (df a) ->
@@ -108,6 +109,7 @@ class ( Protocol (df a)
     Maybe (Payload a)
 
   setPayload ::
+    HasCallStack =>
     DfLike dom df b =>
     Proxy (df a) ->
     Proxy (df b) ->
@@ -122,7 +124,7 @@ hasPayload :: DfLike dom df a => Proxy (df a) -> Data df a -> Bool
 hasPayload dfA = Maybe.isJust . getPayload dfA
 {-# INLINE hasPayload #-}
 
-mapData ::
+mapPayload ::
   forall df dom a b.
   ( DfLike dom df a
   , DfLike dom df b ) =>
@@ -131,9 +133,27 @@ mapData ::
   (Payload a -> Payload b) ->
   Data df a ->
   Data df b
-mapData dfA dfB f fwdA =
+mapPayload dfA dfB f fwdA =
   setPayload dfA dfB fwdA (fmap f (getPayload dfA fwdA))
-{-# INLINE mapData #-}
+{-# INLINE mapPayload #-}
+
+
+-- | Allows conversion of one DfLike protocol into another, given two functions that
+-- transform the data and ack type of one protocol to the other.
+mapDfLike ::
+  forall df1 df2 dom a1 a2.
+  ( DfLike dom df1 a1
+  , DfLike dom df2 a2 ) =>
+  Proxy (df1 a1) ->
+  Proxy (df2 a2) ->
+  (Data df1 a1 -> Data df2 a2) ->
+  (Ack df2 a2 -> Ack df1 a1) ->
+  Circuit (df1 a1) (df2 a2)
+mapDfLike Proxy Proxy fData fAck = Circuit (CE.unbundle . fmap go . CE.bundle)
+  where
+    go :: (Data df1 a1, Ack df2 a2) -> (Ack df1 a1, Data df2 a2)
+    go (d, ack) = (fAck ack, fData d)
+
 
 -- | Like 'P.map'
 map ::
@@ -148,7 +168,7 @@ map dfA dfB f = Circuit (uncurry go)
  where
   go fwd bwd =
     ( boolToAck dfA . ackToBool dfB <$> bwd
-    , mapData dfA dfB f <$> fwd )
+    , mapPayload dfA dfB f <$> fwd )
 {-# INLINE map #-}
 
 -- | Like 'P.fst'
diff --git a/src/Protocols/Internal.hs b/src/Protocols/Internal.hs
index 066482eb..07c4d2e1 100644
--- a/src/Protocols/Internal.hs
+++ b/src/Protocols/Internal.hs
@@ -98,19 +98,16 @@ import           GHC.Generics (Generic)
 -- data. Similar to /Bool/ we define:
 --
 -- @
---   data Ack a = DfNack | Ack
+--   newtype Ack = Ack Bool
 -- @
 --
--- (For technical reasons[1] we need the type variable /a/ in this definition,
--- even though we don't use it on the right hand side.)
---
 -- With these three definitions we're ready to make an instance for /Fwd/ and
 -- /Bwd/:
 --
 -- @
 -- instance Protocol (Df dom a) where
 --   type Fwd (Df dom a) = Signal dom (Data a)
---   type Bwd (Df dom a) = Signal dom (Ack a)
+--   type Bwd (Df dom a) = Signal dom Ack
 -- @
 --
 -- Having defined all this, we can take a look at /Circuit/ once more: now
@@ -128,7 +125,7 @@ import           GHC.Generics (Generic)
 --  +------------------------>+           +------------------------->
 --                            |           |
 --                            |           |
---       Signal dom (Ack a)   |           |  Signal dom (Ack b)
+--       Signal dom Ack       |           |  Signal dom Ack
 --  <-------------------------+           +<------------------------+
 --                            |           |
 --                            +-----------+
@@ -141,15 +138,6 @@ import           GHC.Generics (Generic)
 --
 --   2. It eliminates the need for manually routing acknowledgement lines
 --
--- Footnotes:
---
--- 1. Fwd and Bwd are injective type families. I.e., something on
---    the right hand side of a type instance must uniquely identify the left
---    hand side and vice versa. This helps type inference and error messages
---    substantially, in exchange for a slight syntactical artifact. As a
---    result, any type variables on the left hand side must occur on the right
---    hand side too.
---
 newtype Circuit a b =
   Circuit ( (Fwd a, Bwd b) -> (Bwd a, Fwd b) )
 
@@ -157,11 +145,17 @@ newtype Circuit a b =
 newtype Ack = Ack Bool
   deriving (Generic, C.NFDataX)
 
+-- | Acknowledge. Used in circuit-notation plugin to drive ignore components.
+instance Default Ack where
+  def = Ack True
+
 -- | Circuit protocol with /CSignal dom a/ in its forward direction, and
 -- /CSignal dom ()/ in its backward direction. Convenient for exposing
 -- protocol internals.
 data CSignal dom a = CSignal (Signal dom a)
 
+instance Default a => Default (CSignal dom a) where
+  def = CSignal def
 
 -- | A protocol describes the in- and outputs of one side of a 'Circuit'.
 class Protocol a where
@@ -171,7 +165,7 @@ class Protocol a where
 
   -- | Receiver to sender type family. See 'Circuit' for an explanation on the
   -- existence of 'Bwd'.
-  type Bwd (a :: Type) = (r :: Type) | r -> a
+  type Bwd (a :: Type)
 
 instance Protocol () where
   type Fwd () = ()
@@ -196,7 +190,7 @@ instance C.KnownNat n => Protocol (C.Vec n a) where
 -- XXX: Type families with Signals on LHS are currently broken on Clash:
 instance Protocol (CSignal dom a) where
   type Fwd (CSignal dom a) = CSignal dom a
-  type Bwd (CSignal dom a) = CSignal dom (Const () a)
+  type Bwd (CSignal dom a) = CSignal dom ()
 
 -- | Left-to-right circuit composition.
 --
@@ -231,22 +225,25 @@ infixr 1 |>
 class Protocol a => Backpressure a where
   -- | Interpret list of booleans as a list of acknowledgements at every cycle.
   -- Implementations don't have to account for finite lists.
-  boolsToBwd :: [Bool] -> Bwd a
+  boolsToBwd :: Proxy a -> [Bool] -> Bwd a
 
 instance Backpressure () where
-  boolsToBwd _ = ()
+  boolsToBwd _ _ = ()
 
 instance (Backpressure a, Backpressure b) => Backpressure (a, b) where
-  boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs)
+  boolsToBwd _ bs = (boolsToBwd (Proxy @a) bs, boolsToBwd (Proxy @b) bs)
 
 instance (Backpressure a, Backpressure b, Backpressure c) => Backpressure (a, b, c) where
-  boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs, boolsToBwd bs)
+  boolsToBwd _ bs =
+    ( boolsToBwd (Proxy @a) bs
+    , boolsToBwd (Proxy @b) bs
+    , boolsToBwd (Proxy @c) bs )
 
 instance (C.KnownNat n, Backpressure a) => Backpressure (C.Vec n a) where
-  boolsToBwd bs = C.repeat (boolsToBwd bs)
+  boolsToBwd _ bs = C.repeat (boolsToBwd (Proxy @a) bs)
 
 instance Backpressure (CSignal dom a) where
-  boolsToBwd _ = CSignal (pure (Const ()))
+  boolsToBwd _ _ = CSignal (pure ())
 
 -- | Right-to-left circuit composition.
 --
@@ -480,7 +477,7 @@ instance (Simulate a, Simulate b) => Simulate (a, b) where
   sampleC conf (Circuit f) =
     let
       bools = replicate (resetCycles conf) False <> repeat True
-      (_, (fwd1, fwd2)) = f ((), (boolsToBwd bools, boolsToBwd bools))
+      (_, (fwd1, fwd2)) = f ((), (boolsToBwd (Proxy @a) bools, boolsToBwd (Proxy @b) bools))
     in
       ( sampleC conf (Circuit $ \_ -> ((), fwd1))
       , sampleC conf (Circuit $ \_ -> ((), fwd2)) )
@@ -517,7 +514,7 @@ instance (C.KnownNat n, Simulate a) => Simulate (C.Vec n a) where
   sampleC conf (Circuit f) =
     let
       bools = replicate (resetCycles conf) False <> repeat True
-      (_, fwds) = f ((), (C.repeat (boolsToBwd bools)))
+      (_, fwds) = f ((), (C.repeat (boolsToBwd (Proxy @a) bools)))
     in
       C.map (\fwd -> sampleC conf (Circuit $ \_ -> ((), fwd))) fwds
 
@@ -625,3 +622,9 @@ simulateCSE c = simulateCS (c clk rst ena)
 circuit :: Any
 circuit =
   error "'protocol' called: did you forget to enable \"Protocols.Plugin\"?"
+
+-- | Picked up by "Protocols.Plugin" to tie circuits together. See
+-- "Protocols.Plugin" for more information.
+(-<) :: Any
+(-<) =
+  error "(-<) called: did you forget to enable \"Protocols.Plugin\"?"
diff --git a/stack.yaml b/stack.yaml
index 2c9506e2..e4d6850c 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,4 +1,4 @@
-resolver: nightly-2020-12-14
+resolver: lts-18.21 # ghc-8.10.7
 
 packages:
   - .
@@ -9,7 +9,8 @@ extra-deps:
   subdirs:
     - hedgehog
 - git: https://github.com/cchalmers/circuit-notation.git
-  commit: 0fe897cb95bd1be87abed044f4072f104dec2f7d
+  commit: 2574640364eef12222517af059b9e4a7e6b503a7
+- clash-prelude-1.2.5
 
 flags:
   clash-prelude: