Description:
cc: @jcp19
During the verification of router logic within the VerifiedSCION project, I encountered a possible problem in the scionPacketProcessor's validateEgressID function that might miss an additional check. The code snippet in question is as follows:

func (p *scionPacketProcessor) validateEgressID() (processResult, error) {
	pktEgressID := p.egressInterface()
	_, ih := p.d.internalNextHops[pktEgressID]
	_, eh := p.d.external[pktEgressID]
	if !ih && !eh {
		errCode := slayers.SCMPCodeUnknownHopFieldEgress
	....

This checks whether a received packet can be forwarded either internally or externally based on the pktEgressID. My concern revolves around the scenario where p.ingressID == 0, indicating that the packet has already entered the Autonomous System (AS) and will be forwarded by the router internally. This situation seems to contradict the SCION protocol's design, where a packet is only handled twice within an AS: once by the ingress router and once by the egress router. This case is also not included in the following comment in the scionPacketProcessor's process function:

// Outbound: pkt leaving the local IA. This Could be:
// * Pure outbound: from this AS, in via internal, out via external.
// * ASTransit in: from another AS, in via external, out via internal to other BR.
// * ASTransit out: from another AS, in via internal from other BR, out via external.
// * BRTransit: from another AS, in via external, out via external.`

Question:

Whenever a packet is leaving the AS through another Border Router, shouldn't it be ensured that p.ingressID != 0?

func (p *scionPacketProcessor) process() (processResult, error) {
	...
	...
	// Is it required to ensure that p.ingressID != 0 at this stage?
	// ASTransit in: pkt leaving this AS through another BR.
	if a, ok := p.d.internalNextHops[egressID]; ok {

Am I misunderstanding something, or is there actually a situation where p.ingressID == 0 and the packet is still meant to be forwarded internally?