Erasure

Erasing a person is a generated operation, User.erase(user_id). You call it from an action you write, for example behind a "delete my account" route or in a support tool. It erases the person's record and decides what happens to every record that belongs to them.

What happens to each of those records follows from the on_delete: setting of the reference that links it to the person, so most references need nothing more:

• OnDelete.cascade means the record is deleted (Erasure.deleted).
• OnDelete.cleared means the record is kept and anonymised (Erasure.anonymised).
• OnDelete.restricted must say what erasure does, with erase:.

A restricted reference must say, because "a user with todos can't be deleted" is the right rule for a mistaken click, but not for a person's legal request to be forgotten. Most apps write one or two erase: lines, and the compiler refuses an erasure it can't complete.

A marked field is one with a personal: setting, which says it holds personal data, or one typed Email, EmailWithName, PhoneNumber, PersonName, GivenName, FamilyName or PostalAddress, which holds it without saying so (Contact details and names need no mark). A record that belongs to someone else too keeps its marked fields until the last of its people is erased (Records that belong to several people). A nullable field is one whose type ends in ?, so it can hold no value (Values that may be missing).

Erasure follows the references from every record it deletes, however deep, so a reference to one of the person's todos decides what erasure does to its record in the same way. A record erasure keeps stays with whatever refers to it, as it does when an ordinary delete clears a reference. Everything goes in one statement, so an erasure is never left half done.

Deleting the person's records: Erasure.deleted

Use it for records that are only the person's, such as their todos. Here Todo's reference to its owner is restricted, so ordinary code can't delete a user who still has todos, but erasing the owner deletes their todos:

// domains/accounts/entities/todo.jadpouse accounts/entities { User }use accounts/types { TodoTitle }/// Something a user means to do, deleted with them.entity Todo {    id: Uuid    owner_id: User.id {        on_delete: OnDelete.restricted        erase: Erasure.deleted    }    title: TodoTitle    policy: {        create: [owner_id]        read: [owner_id]    }}

Keeping a record without the person: Erasure.retained

Use it for records the law makes you keep. Invoices are the usual case: tax law requires them for several years, which GDPR Article 17(3) allows. The invoice keeps its own copy of the billing name and address, so it no longer needs the user. Erasing the user clears customer_id and keeps the invoice:

// domains/accounts/entities/invoice.jadpouse accounts/entities { User }use accounts/types { BillingName }/// A bill, kept for the tax years without its customer.entity Invoice {    id: Uuid    customer_id: User.id? {        on_delete: OnDelete.restricted        erase: Erasure.retained    }    billing_name: BillingName {        personal: PersonalData.identifying    }    issued_at: Instant {        generated: Generated.on_create    }    policy: {        create: [customer_id]        read: [customer_id]    }    retention: {        after: config.invoice_retention        since: issued_at    }}

The invoice is then deleted when its own retention ends, here config.invoice_retention after it was issued (six years in the UK).

A record you keep this way holds its own copy of the details it needs, as the invoice holds the billing name. It never points at a stub left in place of the person. It also needs a retention: of its own, which says when it is deleted.

Erasing someone

An action erases a person by their id. Here a signed-in user closes their own account, which User's delete: [id] allows only for themselves (Who may erase and export):

// domains/accounts/actions/close_account.jadpouse accounts/entities { User, UserNotFound }/// Erases the signed-in user: their todos are deleted, and their/// invoices kept without them.action close_account(me: Principal.user) fails UserNotFound -> Unit {    attempt User.erase(me.id)}

User.erase takes no block, since what it does to each record is written on the references, and nothing can refuse it but policy. A person who isn't there, or whom the caller may not delete, is the person's not-found failure, UserNotFound. A person a lifecycle hides, such as one who deleted their account earlier, is erased too.

This test signs a user up, gives them a todo and an invoice, and closes their account:

// domains/accounts/actions/close_account.test.jadpouse accounts/entities { Invoice, Todo, TodoNotFound, User, UserNotFound }use accounts/actions { add_todo, bill, sign_up }test "closing an account deletes the todos and keeps the invoices" {    var ada: User = attempt sign_up("ada@example.com")    var me: Principal.user = Principal.user(ada)    var todo: Todo = add_todo(me, "Buy milk")    var invoice: Invoice = bill(me, "Ada Lovelace")    attempt close_account(me)    assert User.get(ada.id) fails UserNotFound    assert Todo.get(todo.id) fails TodoNotFound    var still_billed: Invoice = attempt Invoice.get(invoice.id)    assert still_billed.customer_id == none    assert still_billed.billing_name == "Ada Lovelace"}

Records that belong to several people

A record can belong to more than one person: a postcard from one user to another belongs to both. Erasing one person never clears another person's data. Erasing either user clears only their own reference, and the postcard keeps its marked fields while the other remains; they are cleared when the last of them is erased.

The people a record belongs to are those it refers to directly. A reply someone writes on another user's todo belongs to its author alone, so erasing the todo's owner clears only the reply's todo_id, and erasing its author clears its marked fields too. A record kept that refers to no person at all has no one left, so it loses its marked fields when erasure deletes what it refers to.

Another person's own record is never anonymised: a user whose invited_by_id refers to the person erased keeps their own fields, and only the reference is cleared.

// domains/accounts/entities/postcard.jadpouse accounts/entities { User }use accounts/types { CardText, SignedName }/// A postcard one user sends another, which belongs to both of them.entity Postcard {    id: Uuid    sender_id: User.id? {        on_delete: OnDelete.cleared    }    recipient_id: User.id? {        on_delete: OnDelete.cleared    }    body: CardText    signed_as: SignedName? {        personal: PersonalData.identifying    }    policy: {        create: [sender_id]        read: [sender_id, recipient_id]    }}

// domains/accounts/actions/write_postcard.test.jadpouse accounts/entities { Postcard, User }use accounts/actions { close_account, sign_up }test "a postcard keeps its signature until both its users are erased" {    var ada: User = attempt sign_up("ada@example.com")    var bob: User = attempt sign_up("bob@example.com")    var card: Postcard = write_postcard(Principal.user(ada), bob, "See you on Tuesday", "Ada")    attempt close_account(Principal.user(ada))    var after_ada: Postcard = attempt Postcard.get(card.id)    assert after_ada.sender_id == none    assert after_ada.signed_as == "Ada"    attempt close_account(Principal.user(bob))    var after_both: Postcard = attempt Postcard.get(card.id)    assert after_both.signed_as == none    assert after_both.body == "See you on Tuesday"}

A reply shows the difference:

// domains/accounts/entities/reply.jadpouse accounts/entities { Todo, User }use accounts/types { CardText, SignedName }/// What someone writes on a todo, which belongs to whoever wrote it.entity Reply {    id: Uuid    todo_id: Todo.id? {        on_delete: OnDelete.cleared    }    author_id: User.id? {        on_delete: OnDelete.cleared    }    body: CardText    signed_as: SignedName? {        personal: PersonalData.identifying    }    policy: {        create: [author_id]        read: [author_id]    }}

// domains/accounts/actions/write_reply.test.jadpouse accounts/entities { Reply, Todo, User }use accounts/actions { add_todo, close_account, sign_up }test "a reply's signature goes with its author, not the todo's owner" {    var ada: User = attempt sign_up("ada@example.com")    var bob: User = attempt sign_up("bob@example.com")    var todo: Todo = add_todo(Principal.user(ada), "Buy milk")    var reply: Reply = write_reply(Principal.user(bob), todo, "Which kind?", "Bob")    attempt close_account(Principal.user(ada))    var after_owner: Reply = attempt Reply.get(reply.id)    assert after_owner.todo_id == none    assert after_owner.signed_as == "Bob"    attempt close_account(Principal.user(bob))    var after_author: Reply = attempt Reply.get(reply.id)    assert after_author.signed_as == none    assert after_author.body == "Which kind?"}

The person's own record

The person's own record is erased field by field, because it can't always go: an insurer, for example, must keep policy records for at least five years.

• Where nothing must be kept, the record is deleted.
• Otherwise a field that says erase: Erasure.retained stays, and so does every field not marked personal:. Every other marked field is cleared.

Here erasing a customer clears their name and keeps their policy number until their retention ends:

// domains/cover/entities/customer.jadpouse cover/types { AccountHandle, CustomerName, PolicyNumber }/// Someone with a policy, part of whose record the law makes us keep.entity Customer {    id: Uuid    handle: AccountHandle {        unique: true    }    customer_name: CustomerName? {        personal: PersonalData.identifying    }    policy_number: PolicyNumber {        personal: PersonalData.identifying        erase: Erasure.retained    }    policy_ended_at: Instant?    policy: {        create: [Access.public]        read: [Access.public]        delete: [id]    }    person: true    retention: {        after: config.policy_retention        since: policy_ended_at    }}

• A field that stays is marked personal:, since an unmarked field stays anyway (data.erase_own_field).
• No reference of theirs deletes them with another entity's records, since what the law keeps doesn't depend on who else is erased (data.erase_own_field). Their references to records erasure deletes are cleared.
• The entity needs a retention:, or what stays would stay for ever (data.erase_retention_required). It applies to every record, erased or not, so count from something like the end of the policy: a record whose since: field is none isn't counted, and a customer whose policy hasn't ended stays. When the time is up, the purge schedule deletes the rest.
• Every marked field that doesn't stay can be none (data.erase_field_required). What someone signs in with must always have a value, so it stays too, or holds nothing personal, as handle does here.
• A column retired on a record whose marked fields erasure clears is cleared with them, since nothing says any more whether it held personal data. A sealed field (Encrypted fields) is treated like any other.

A record kept this way is hidden, as a lifecycle hides one. No query, get or include finds it, and no update, delete or transition reaches it, so the person receives nothing. Their sessions, API tokens, service keys, passkeys and sign-in links go with the erasure, and they can't sign in again, however they try: every way in looks them up, and finds no one. Erasing them again finds them and changes nothing.

Reading what is kept: include_erased:

A query that serves the reason the record was kept says so, with include_erased: true. It finds erased people as well as everyone else. It may read nothing but their id and the fields that say erase: Erasure.retained, in its result, its conditions and its order, and it brings no other records with it (query.include_erased_reads). The personal-data report lists every such query.

// domains/cover/types/kept_policy.jadpouse cover/entities { Customer }/// What the law makes us keep of a customer.type KeptPolicy = Output {    pick: [Customer.id, Customer.policy_number]}

// domains/cover/queries/kept_policies.jadpouse cover/entities { Customer }use cover/types { KeptPolicy }/// Whoever holds a policy number, erased or not, for a regulator's audit.query kept_policies(number: Customer.policy_number) -> List<KeptPolicy> {    from: Customer    where: Customer.policy_number == number    order: [Customer.id asc]    limit: 10    include_erased: true}

On an entity that keeps nothing of an erased person there is nothing for it to find, so it is refused (query.include_erased_unused).

// domains/cover/actions/close_account.test.jadpouse cover/entities { Customer, CustomerNotFound }use cover/actions { take_out_policy }use cover/queries { kept_policies }test "closing an account hides the customer and keeps the policy number" {    var ada: Customer = attempt take_out_policy("ada", "Ada Lovelace", "P-100")    attempt close_account(Principal.user(ada))    assert Customer.get(ada.id) fails CustomerNotFound    assert list.map(kept_policies("P-100"), kept -> kept.policy_number) == ["P-100"]}

What erasure reaches

• Every store and cache. The main store's records go in one transaction, and cached copies are wiped at once (Caches). An action can write to only one store, so records your app keeps in another store are erased straight after, by an event subscriber that Jadpo generates. Such a record refers to the person with a reference that says erase: and has no on_delete:. It isn't a foreign key, since no database holds one across stores: the subscriber applies what erase: says in that store, after the main store commits. Any other reference across stores, with an on_delete: or to an entity that isn't a person, is data.reference_across_stores.
• Records with a lifecycle are removed outright, not soft-deleted. Your own code can't do that, but erasure, like purge, is an operation the compiler generates, so it can (Lifecycle).
• Files attached to erased records are deleted with them (Files).
• History. An audited record erasure deletes takes its history with it, in the same statement (Audit trail).
• OAuth grants, the permissions a person gave your app to act for them at a provider, are deleted with the person or record that owns them (OAuth grants). They are revoked at the provider where its package declares how.
• Other companies. Data already sent to a provider, such as an email or payment provider, is outside your database. Providers that can erase are asked to (see "Erasure at providers" below). The personal-data report lists every connection that receives a marked field, and whether its copy is erased.

What erasure doesn't rewrite

• Backups aren't rewritten. Each erasure leaves an entry in an erasure log, holding the person entity's name, the person's id and the time and nothing else. Your app names where the log is kept, in privacy: { erasure_log: { store: } }: a store that holds no person's records, or a store of files, so restoring a person's database can't take the log back with it. The runtime replays the log every time it starts, erasing again anyone logged who is still there, so a restored backup is erased before the app serves anything. Backups themselves expire on the hosting platform's schedule, which the report states. This is what the UK regulator, the ICO, calls putting data "beyond use".
• There are no per-person encryption keys, so erasure never works by deleting a person's key ("crypto-shredding").
• Logs aren't rewritten either. They hold identifiers and hashes, never marked values, and expire on their own retention.

Legal holds and restricted use

A legal hold, which stops a person's data being erased while a case is open, is application data that you write. An action checks a hold flag and refuses with its own failure before it calls User.erase. Restricting use of someone's data while a complaint is open (Article 18) works the same way.