Downgrading raises type level

[ssoelvsten]

Notice the following lines of code in rt/downgrading.mts

Troupe/rt/src/downgrading.mts

Lines 85 to 87 in a4ebfdc

	const r = typeOnly
	? new LCopyVal(data, lub(data.lev, taintedLevTo), taintedLevTo)
	: new LCopyVal(data, taintedLevTo);

If it is a value downgrade (downgrade), this will raise the type level. That is, the following program returns 42@{alice}%{alice} rather than 42@{alice}%{} as expected.

import IfcUtil

let val x = 42 raisedTo `{alice, bob}`
in pdowngrade (x, authority, `{alice}`)
end

For simplicity, this example requires --no-nmifc

[aslanix]

Indeed. This is unnecessary restrictive. What's the right fix? Is it just changing line 87 to something like

new LCopyVal(data, taintedLevTo, glb(data.tlev, taintedLevTo) );

[ssoelvsten]

I think that is the solution, yes.