provenance.pl

Explanatory context, separate from executable IR and safety evidence.

A context(Function, Records) item accompanies a func/5. Bindings and origins have function-local identities. Origins are shallow typed nodes at the enclosing statement's location, not expression spans. Values retain their original identities and hints even when removed; alias/4 records substitution without renaming the surviving value.

site(inst(Label, Index), Origins) uses a zero-based index in THIS stage's instruction list. Passes produce explicit old-to-new site maps while rewriting. Phis and jumps have stable sites phi(Temp) and jump(Label). Context never participates in CFG or safety proofs.

Records

Record	Meaning
`bindingId, Name, CType, Location`	declaration identity and spelling; shadowed names have distinct IDs
`originId, Location, Description, Parents`	a typed lowering node, enclosing statement, or generated operation, linked by origin IDs
`valueTemp, Hint, Origins`	original definition, retained as history if eliminated
`siteSite, Origins`	provenance of a live instruction, phi or terminator
`aliasTemp, Replacement, Hint, Origins`	copy/phi substitution, including replacement by a constant
`historyId, Temp, Hint, Origins, Replacement`	retired definition when an executable name is reused; Replacement is none or replaced(Value)

Location is at(File, Line) or none. A typed description is typed(val|obj|fun, CType, ShallowForm), a statement is statement(Kind), and a synthesized operation is generated(Pass, Reason). Parents express containment or contributing origins, not executable uses. Hint is none or named(BindingId, value|address|piece). C types are explanations of source nodes, never substitutes for IR classes.

If a pass reuses a deleted temporary's spelling, its old definition moves to history/5. Incoming alias/history replacements then use historical(Id), referencing that history record, not the new value. This metadata-only reference can never be an executable operand.

Promotion conservatively cites the slot's declaration/initial value and stores, not an assertion that every store reaches every phi. Copies preserve the survivor's primary name. Raw accesses and their adjacent checks inherit the same access origin; checks and poll edges additionally have generated origins. Erasure cannot authorize an otherwise-invalid check/access pair.

moduleprovenance

exportscode_items/2 context_records/3 with_context/3 remap_sites/3 site_origins/3 valid_contexts/1 legacy_context/2 emission_sites/7 site_index/2 origin_ids/2 fresh_origin/4 retire_values/5

useslists

usesassoc

51code_itemsItems, Code ←

excludeis_context, Items, Code

52is_contextcontext_, _

54context_recordsItems, Name, Records ←

memberchkcontextName, Rs, Items

→

Records = Rs

else

Records = []

57with_contextF, [], F ←

58with_contextF, Rs, F, contextName, Rs ←

F = funcName, _, _, _, _

60site_indexRs, Sites ←

findallS−Os, membersiteS, Os, Rs, Pairs

list_to_assocPairs, Sites

63site_originsSites, Site, Os ←

get_assocSite, Sites, Origins

→

Os = Origins

else

Os = []

66origin_idsRs, Ids ←

findallId−true, memberoriginId, _, _, _, Rs, Pairs

list_to_assocPairs, Ids

Only metadata names consult metadata. Executable fresh names remain exactly what the metadata-free transformation would choose.

71fresh_originBase, Ids₀, Ids, Id ←

get_assocBase, Ids₀, _

→

unused_originBase, 0, Ids₀, Id

else

Id = Base

put_assocId, Ids₀, true, Ids

74unused_originBase, N, Ids, Id ←

Candidate = derivedBase, N

get_assocCandidate, Ids, _

→

N₁ is N + 1

unused_originBase, N₁, Ids, Id

else

Id = Candidate

79retire_valuesRs₀, Temps, Ids₀, Ids, Rs ←

findallT−true, memberT, Temps, NewPairs

list_to_assocNewPairs, New

findallT−V, memberaliasT, V, _, _, Rs₀, APairs

list_to_assocAPairs, Aliases

findallT−true, membervalueT, _, _, Rs₀, VPairs

list_to_assocVPairs, Values

findallT,

memberR, Rs₀

historical_tempR, T

get_assocT, New, _

, Ts₀

sortTs₀, Ts

retirement_idsTs, Ids₀, Ids, Pairs

list_to_assocPairs, Retired

retire_recordsRs₀, Retired, Aliases, Values, Records

findallRs₁,

memberT−Id, Pairs

¬get_assocT, Values, _

¬get_assocT, Aliases, _

retiredT, none, [], none, Id, Rs₁, []

, Missing

appendRecords|Missing, All

maplistretired_referenceRetired, All, Rs

historical_temp
90	valueT, _, _	T
91	aliasT, _, _, _	T
92	alias_, tmpT, _, _	T
93	history_, _, _, _, replacedtmpT	T

95retirement_ids[], Ids, Ids, []

96retirement_idsT|Ts, Ids₀, Ids, T−Id|Pairs ←

fresh_originretiredT, Ids₀, Ids₁, Id

retirement_idsTs, Ids₁, Ids, Pairs

99retire_records[], _, _, _, []

100retire_recordsvalueT, H, Os|Rs₀, New, As, Vs, Rs ←

get_assocT, New, Id

get_assocT, As, V

→

Replacement = replacedV

else

Replacement = none

retiredT, H, Os, Replacement, Id, Rs, Rest

retire_recordsRs₀, New, As, Vs, Rest

105retire_recordsaliasT, V, H, Os|Rs₀, New, As, Vs, Rs ←

get_assocT, New, Id

get_assocT, Vs, _

→

Rs = Rest

else

retiredT, H, Os, replacedV, Id, Rs, Rest

retire_recordsRs₀, New, As, Vs, Rest

110retire_recordsR|Rs₀, New, As, Vs, R|Rs ←

retire_recordsRs₀, New, As, Vs, Rs

113retiredT, H, Os, Replacement, Id, originId, none, generatedcontext, retiredT, Os, historyId, T, H, Os, Replacement|Rest, Rest

Incoming references identify the old definition, not a new proof that happens to reuse its spelling. Historical references are not IR values.

119retired_referenceIds, aliasT, tmpOld, H, Os, aliasT, historicalId, H, Os ←

get_assocOld, Ids, Id

121retired_referenceIds, historyHId, T, H, Os, replacedtmpOld, historyHId, T, H, Os, replacedhistoricalId ←

get_assocOld, Ids, Id

124retired_reference_, R, R

Map is OldSite-NewSite, with one pair per emitted instruction. An instruction that expands has several destinations; one erased has none.

128remap_sitesRs₀, Map, Rs ←

site_indexRs₀, Sites

excludeinstruction_site, Rs₀, Kept

findallsiteNew, Os,

memberOld−New, Map

get_assocOld, Sites, Os

, NewSites

appendKept, NewSites, Rs

135instruction_sitesiteinst_, _, _

The rewriting loop calls this with the instructions it just emitted.

138emission_sites_, _, J, [], Rest, Rest, J

139emission_sitesL, I, J, _|Is, instL, I−instL, J|Ms, Rest, End ←

J₁ is J + 1

emission_sitesL, I, J₁, Is, Ms, Rest, End

Legacy loc markers remain valid input. At unchecked transformation boundaries they become context, never before checked-IR validation.

144legacy_contextM, M ←

ir:module_stageM, checked

145legacy_contextmoduleIs₀, moduleIs ←

maplistlegacy_itemIs₀, Is₀, Groups

appendGroups, Is

148legacy_itemAll, funcN, L, R, Ps, Bs₀, Items ←

context_recordsAll, N, Rs₀

origin_idsRs₀, Ids

legacy_blocksBs₀, Bs, Ids, _, Added, Map

remap_sitesRs₀, Map, Rs₁

site_indexRs₁, Sites₀

foldllegacy_site, Added, Sites₀, Sites

assoc_to_listSites, Pairs

findallsiteS, Os, memberS−Os, Pairs, SiteRecords

appendRs₁, Added, AllRecords

excludeis_site, AllRecords, Kept

appendKept, SiteRecords, Rs

with_contextfuncN, L, R, Ps, Bs, Rs, Items

157legacy_item_, context_, _, [] ←

158legacy_item_, I, I

160is_sitesite_, _

161legacy_sitesiteS, Os, Sites₀, Sites ←

site_originsSites₀, S, Before

appendBefore, Os, Both

sortBoth, Merged

put_assocS, Sites₀, Merged, Sites

164legacy_site_, Sites, Sites

166legacy_blocks[], [], Ids, Ids, [], []

167legacy_blocksblockL, Ps, Is₀, J|Bs₀, blockL, Ps, Is, J|Bs, Ids₀, Ids, Rs, Map ←

legacy_instsIs₀, L, 0, 0, none, Is, IRs, Last, Ids₀, Ids₁, M₀

Is₀ = loc_, _|_

IRs = originFirst, _, _, _|_

→

findallsitephiT, First, memberphitmpT, _, _, Ps, PRs

else

PRs = []

Last ≡ none

→

JRs = []

else

JRs = sitejumpL, Last

legacy_blocksBs₀, Bs, Ids₁, Ids, Rest, M₁

appendPRs, IRs, JRs, Rest, Rs

appendM₀, M₁, Map

176legacy_insts[], _, _, _, Loc, [], [], Loc, Ids, Ids, []

177legacy_instslocF, Line|Is₀, L, Old, New, _, Is, originId, atF, Line, statementlegacy, []|Rs, Last, Ids₀, Ids, Map ←

fresh_originlegacyL, Old, Ids₀, Ids₁, Id

Next is Old + 1

legacy_instsIs₀, L, Next, New, Id, Is, Rs, Last, Ids₁, Ids, Map

181legacy_instsInst|Is₀, L, Old, New, Loc, Inst|Is, Rs, Last, Ids₀, Ids, instL, Old−instL, New|Map ←

Loc ≡ none

→

Rs = Rest

else

Rs = siteinstL, New, Loc|Rest

Old₁ is Old + 1

New₁ is New + 1

legacy_instsIs₀, L, Old₁, New₁, Loc, Is, Rest, Last, Ids₀, Ids, Map

187valid_contextsItems ←

findallN, membercontextN, _, Items, Names

sortNames, Unique

lengthNames, Count

lengthUnique, Count

maplistvalid_contextItems, Names

192valid_contextItems, Name ←

memberchkfuncName, _, _, _, Bs, Items

memberchkcontextName, Rs, Items

groundRs

is_listRs

findallId−true, memberoriginId, _, _, _, Rs, Ids

unique_assocIds, Origins

findallB−true, memberbindingB, _, _, _, Rs, Bindings₀

unique_assocBindings₀, Bindings

findallT−true, membervalueT, _, _, Rs, Values

unique_assocValues, _

findallT−true, memberaliasT, _, _, _, Rs, Aliases

unique_assocAliases, _

findallId−true, memberhistoryId, _, _, _, _, Rs, Hs

unique_assocHs, Histories

findallS−true, membersiteS, _, Rs, Sites

unique_assocSites, _

findallL−N,

memberblockL, _, Is, _, Bs

lengthIs, N

, Sizes

list_to_assocSizes, Blocks

findallT−true,

memberblock_, Ps, _, _, Bs

memberphitmpT, _, _, Ps

, Phis₀

list_to_assocPhis₀, Phis

maplistvalid_recordindexOrigins, Bindings, Histories, sitesBlocks, Phis, Rs

206unique_assocPairs, Assoc ←

findallK, memberK−_, Pairs, Keys

sortKeys, Unique

lengthKeys, N

lengthUnique, N

list_to_assocPairs, Assoc

210valid_record_, _, binding_, Name, _, Loc ←

atomName

locationLoc

211valid_recordRs, _, origin_, Loc, Description, Parents ←

locationLoc

descriptionDescription

originsRs, Parents

213valid_recordRs, _, valueT, Hint, Os ←

atomT

hintRs, Hint

originsRs, Os

214valid_recordRs, _, aliasT, V, Hint, Os ←

atomT

replacementRs, V

hintRs, Hint

originsRs, Os

216valid_recordRs, _, historyId, T, Hint, Os, Replacement ←

origin_existsRs, Id

atomT

hintRs, Hint

originsRs, Os

Replacement ≡ none

Replacement = replacedV

replacementRs, V

219valid_recordRs, Bs, siteS, Os ←

valid_siteBs, S

originsRs, Os

221locationnone

222locationatF, L ←

atomF

integerL

L ≥ 0

223descriptionstatementK ←

atomK

224descriptiontypedC, _, _ ←

memberchkC, val, obj, fun

225descriptiongeneratedP, _ ←

atomP

226hint_, none

227hintindex_, Bs, _, namedB, Role ←

memberchkRole, value, address, piece

get_assocB, Bs, _

229originsRs, Os ←

is_listOs

maplistorigin_existsRs, Os

230origin_existsindexOrigins, _, _, O ←

get_assocO, Origins, _

231replacement_, tmpT ←

atomT

232replacement_, constN ←

integerN

233replacement_, globalN ←

atomN

234replacementindex_, _, Hs, historicalId ←

get_assocId, Hs, _

235valid_sitesitesBs, _, instL, I ←

get_assocL, Bs, N

integerI

I ≥ 0

I < N

237valid_sitesites_, Ps, phiT ←

get_assocT, Ps, _

238valid_sitesitesBs, _, jumpL ←

get_assocL, Bs, _