同余最短路是指什么，如何证明正确性，代码如何实现

同余最短路是指在模一个数的意义下求解最短路的问题。具体来说，给定一个有向图 $G=(V,E)$，每个边 $e\in E$ 都有一个非负的权值 $w_e$，以及一个模数 $p$。同时给定一个起点 $s$ 和一个终点 $t$。求一条从 $s$ 到 $t$ 的路径，使得路径上所有边权的和在模 $p$ 意义下最小。

证明正确性：

同余最短路算法基于 Bellman-Ford 算法，可以证明其正确性。Bellman-Ford 算法通过松弛每条边 $e$，对于每个顶点 $v$，维护从起点 $s$ 到 $v$ 的最短距离 $d_v$。同余最短路算法也是基于松弛每条边，但是对于每个顶点 $v$，维护从起点 $s$ 到 $v$ 在模 $p$ 意义下的最短距离 $d_v$。

因为同余最短路算法是在模 $p$ 意义下计算距离，所以需要使用模运算。在松弛每条边时，需要更新到达每个顶点的最短距离。具体地，设 $v$ 是边 $e=(u,v)$ 的终点，$w_e$ 是边 $e$ 的边权，则松弛边 $e$ 的操作可以表示为：

$$d_v\leftarrow\min(d_v,d_u+w_e\mod p)$$

其中，$d_u$ 表示从起点 $s$ 到 $u$ 的最短距离。

同余最短路算法的正确性证明可以参考 Bellman-Ford 算法的正确性证明。同余最短路算法的时间复杂度为 $O(VE)$。

代码实现：

以下是同余最短路算法的 Python 代码实现：

from collections import deque

def shortest_path_mod_p(graph, s, t, p):
    n = len(graph)
    INF = float('inf')
    dist = [INF] * n
    dist[s] = 0
    q = deque([s])
    in_queue = [False] * n
    in_queue[s] = True
    while q:
        u = q.popleft()
        in_queue[u] = False
        for v, w in graph[u]:
            d = (dist[u] + w) % p
            if dist[v] > d:
                dist[v] = d
                if not in_queue[v]:
                    q.append(v)
                    in_queue[v] = True
    return dist[t]

其中，`graph` 是图的邻接表表示，每个元素是一个二元组 `(v, w)`，表示从节点 `u` 到节点 `v` 有一条边权为 `w` 的边。`s` 和 `t` 分别是起点和终点的编号，`p` 是模数。函数返回从起点 `s` 到终点 `t` 在模 `p` 意义下的最短距离。