# `deep_verify_memo` and fixpoint

Two single threaded cases where Salsa accesses interned values
without veryfing that they're green (`maybe_changed_after` returns `false`).

#[salsa::tracked(cycle_initial=cycle_initial)]
fn query_a(db) -> Interned {
    let interned = query_b(db);
    let value = interned.value(db);

    if value < 10 {
        Interned::new(db, value + 1)
    } else {
        interned
    }
}

fn query_b(db) -> Interned {
    let interned = query_a(db);
    let _ = query_x(db, interned);
    interned
}

fn query_x(db, i: Interned) {
    ...    
}

fn cycle_initial(db, ...) -> Interned {
    Interned::new(db, 0)
}

#[salsa::interned]
struct Interned {
    value: u32
}

Collected input/outputs by query:

* `query_a`
* `query_b`
* `Interned::new(1)`
<hr>
* `Interned::new(2)`
<hr>
* `Interned::new(3)`
<hr>
* ...
* `Interned::new(10)`
* `query_b`
* `Interned::new(0)`
* `query_a`
* `query_x(Interned(0))`
<hr>
* `query_x(Interned(1))`
<hr>
* `query_x(Interned(2))`
<hr>
* ...
* `query_x(Interned(10))`
* `query_x`: Not important

Traversal order in `maybe_changed_after`:

1. `query_a`
1. `query_b`
1. `Interned::new(0)`
3. `query_a` (returns unchanged, fixpoint initial)
4. `query_x(0)`
5. `query_x(1)`
6. `query_x(2)`
7. `query_x(...)`
8. `query_x(10)`
1. `Interned::new(1)`
2. `Interned::new(2)`
3. `Interned::new(...)`
4. `Interned::new(10)`

* We'd need to record the query dependencies multiple times?
* Record when a new iteration starts
* TLDR: Track input-outputs per iteration instead of merging them all-together?
* When calling maybe_changed_after, pass the iteration so that it can lookup its dependencies

But I don't think just tracking the iterations on its own is sufficient because the query where we hit fixpoint initial depends on the entry query. We also need a way to ensure that `maybe_changed_after` starts from the same cycle head:

#[salsa::tracked(cycle_initial=a_cycle_initial)]
fn query_a(db: &dyn Database) {
    let b = query_b(db);
    query_d(db, b);
}

fn a_cycle_initial(_db: &dyn Database) -> () {
    ()
}

#[salsa::interned]
struct Interned {
    value: u32,
}

#[salsa::tracked(cycle_initial=|| Interned::new(0))]
fn query_b(db: &dyn Database) -> Interned {
    query_c(db);
    Interned::new(db, 2)
}

#[salsa::tracked]
fn query_c(db: &dyn Database) {
    query_a(db);
}

#[salsa::tracked]
fn query_d<'db>(db: &'db dyn Database, i: Interned<'db>) {
    // reads some input
}

Input/Outputs:
* `query_a`
* `query_c`
* `Interned::new(2)`
* `query_d(Interned(2))`
* `query_b`
* `query_c`
* `Interned::new(2)`
* `query_c`:
* `query_a`

Traversal order in `maybe_changed_after` starting from a:

1. `query_a`
1. `query_b`
1. `query_c`:
1.1. `query_a` (fixpoint initial)
2.`Interned::new(2)`
1. `query_d(Interned(2))`

Traversal order in `maybe_changed_after` starting from b:

1. `query_b`
2. `query_c`
3. `query_a`
4. `query_b` (fixpoint initial)
5. `query_d(Interned(2))` (panic)
6. `Interned::new(0)`

-> `maybe_changed_after` needs to call `maybe_changed_after` on the cycle head. This should now be "easier". We can iterate over all cycle heads and find the one head with no
cycle heads (we only clear cycle heads for the outer most head). Then claim the head, and transfer the lock of the nested cycle to the head (which should never block). Then call `maybe_changed_after` on the head

## Multithreading

Things get even weirder with multi-threading as there's no clear execution order anymore with how fixpoint is implemented today (there's no global ordering). The iteration count isn't unique enough as well, because it lags behind (the iteration count is 0 for fixpoint initial as well as when a nested cycle completes the first time)