Program equivalence wherein the programs are known to always halt Say I have two programs with possibly infinite state spaces and some oracle has asserted that they both always halt. Can I always decide if they're contextually equivalent? If yes, is there a known effective algorithm (or approach that when applied on a case-by-case or language-by-language basis provides an effective algorithm) to do so?

The answer is obviously yes/yes for finite input domains, but for infinite input domains: does the decidability depend at all on how infinitely huge (e.g. countable vs. uncountable) the input domains are?
As a counter-example to this, consider the Context-Free Equivalence problem: it's undecidable to determine, given two context free languages, whether they accept the same set.

If your problem were decidable, we could use it to determine CFL equivalence, since it's always possible to turn a CFL into an always-halting Turing machine.

So even for countably infinite inputs, the problem is undecidable.

It's also worth mentioning that, for standard Turing Machines, all input domains are countably infinite, since they're sets of finite strings.