@@ -13,52 +13,160 @@ export function registerCodeLensProvider(context: LspContext) {
1313 const doc = context . documents . get ( uri ) ;
1414 const text = doc ?. getText ( ) ;
1515
16+ const proofMap = context . validationService ?. modelicaProofResultsByUri ?. get ( uri ) ;
17+ const daeMap = context . validationService ?. modelicaDaeVerificationResultsByUri ?. get ( uri ) ;
18+ const emittedProofClasses = new Set < string > ( ) ;
19+ const emittedDaeClasses = new Set < string > ( ) ;
20+
1621 if ( text ) {
1722 const lines = text . split ( / \r ? \n / ) ;
23+ let currentClassName : string | undefined = undefined ;
24+
1825 for ( let lineIdx = 0 ; lineIdx < lines . length ; lineIdx ++ ) {
19- const line = lines [ lineIdx ] ;
26+ const line = lines [ lineIdx ] ! ;
2027
21- // Model / Block / Study declaration
22- const classMatch = / ^ \s * (?: m o d e l | b l o c k | s t u d y | p r o c e s s ) \s + ( [ A - Z a - z 0 - 9 _ ] + ) / . exec ( line ) ;
28+ // Model / Block / Study / Class / Function / Record declaration
29+ const classMatch = / ^ \s * (?: m o d e l | b l o c k | s t u d y | p r o c e s s | c l a s s | f u n c t i o n | r e c o r d ) \s + ( [ A - Z a - z 0 - 9 _ ] + ) / . exec ( line ) ;
2330 if ( classMatch ) {
24- const name = classMatch [ 1 ] ;
31+ const name = classMatch [ 1 ] ! ;
32+ currentClassName = name ;
2533 const col = line . indexOf ( name ) ;
2634 const range = Range . create ( lineIdx , col , lineIdx , col + name . length ) ;
2735
28- if ( name === "DroneSimulation" || uri . includes ( "DroneSimulation" ) || uri . includes ( "drone-reachability" ) ) {
36+ const rawKind = classMatch [ 0 ] . trim ( ) . split ( / \s + / ) [ 0 ] ! ;
37+ if ( rawKind === "model" || rawKind === "block" || rawKind === "study" || rawKind === "process" ) {
38+ if ( name === "DroneSimulation" || uri . includes ( "DroneSimulation" ) || uri . includes ( "drone-reachability" ) ) {
39+ lenses . push ( {
40+ range,
41+ command : {
42+ title : "▶ Estimate Reachability Envelope (linearized zonotope, non-rigorous)" ,
43+ command : "modelscript.openDroneReachabilityDemo" ,
44+ arguments : [ uri ] ,
45+ } ,
46+ } ) ;
47+ lenses . push ( {
48+ range,
49+ command : {
50+ title : "▶ Simulate Model (RK4 / CVODE DAE)" ,
51+ command : "modelscript.openSimulationView" ,
52+ arguments : [ uri , name ] ,
53+ } ,
54+ } ) ;
55+ lenses . push ( {
56+ range,
57+ command : {
58+ title : "🌐 Digital Thread Explorer" ,
59+ command : "modelscript.openThreadExplorer" ,
60+ arguments : [ uri ] ,
61+ } ,
62+ } ) ;
63+ } else {
64+ const title = rawKind === "study" ? "▶ Run Study" : `▶ Simulate ${ rawKind } ;
65+ lenses . push ( {
66+ range,
67+ command : {
68+ title,
69+ command : "modelscript.openSimulationView" ,
70+ arguments : [ uri , name ] ,
71+ } ,
72+ } ) ;
73+ }
74+ }
75+
76+ // Formal proof badge for this model/class/function on this exact declaration line
77+ const proof = proofMap ?. get ( name ) ;
78+ if ( proof ) {
79+ emittedProofClasses . add ( name ) ;
80+ let proofTitle = "✓ Formally Verified (0 RTEs, 100% Proven Safe)" ;
81+ if ( proof . definiteBugs . length > 0 ) {
82+ proofTitle = `✗ Formal Defect: ${ proof . definiteBugs . length } ;
83+ } else if ( proof . potentialBugs . length > 0 ) {
84+ const oobCount = proof . potentialBugs . filter ( ( b : any ) => b . category === "array_out_of_bounds" ) . length ;
85+ if ( oobCount > 0 ) {
86+ proofTitle = `⚠ Formal Proof: ${ proof . potentialBugs . length } ;
87+ } else {
88+ proofTitle = `⚠ Formal Proof: ${ proof . potentialBugs . length } ;
89+ }
90+ }
91+
2992 lenses . push ( {
3093 range,
3194 command : {
32- title : "▶ Estimate Reachability Envelope (linearized zonotope, non-rigorous)" ,
33- command : "modelscript.openDroneReachabilityDemo " ,
34- arguments : [ uri ] ,
95+ title : proofTitle ,
96+ command : "modelscript.showProofDetails " ,
97+ arguments : [ uri , name , proof . formattedMatrix ] ,
3598 } ,
3699 } ) ;
100+ }
101+
102+ // DAE BLT verification badge for this model/class on this exact declaration line
103+ const daeProof = daeMap ?. get ( name ) ;
104+ if ( daeProof ) {
105+ emittedDaeClasses . add ( name ) ;
106+ let daeTitle =
107+ daeProof . verdict ?. kind === "proven"
108+ ? "✓ DAE: no singularities (interval analysis, all variables bounded)"
109+ : `◌ DAE: no singularity found among bounded variables (${ daeProof . unboundedVariables ?? "some" } ;
110+ if ( daeProof . issues . length > 0 ) {
111+ const definite = daeProof . issues . find ( ( i : any ) => i . severity === "definite" ) ;
112+ if ( definite ) {
113+ daeTitle = `✗ DAE Defect: ${ definite . message } ;
114+ } else {
115+ daeTitle = `⚠ DAE Invariant: ${ daeProof . issues [ 0 ] . message } ;
116+ }
117+ }
118+
37119 lenses . push ( {
38120 range,
39121 command : {
40- title : "▶ Simulate Model (RK4 / CVODE DAE)" ,
41- command : "modelscript.openSimulationView " ,
42- arguments : [ uri , name ] ,
122+ title : daeTitle ,
123+ command : "modelscript.showDaeVerificationDetails " ,
124+ arguments : [ uri , name , daeProof ] ,
43125 } ,
44126 } ) ;
127+ }
128+ }
129+
130+ // Reset current class when leaving its definition
131+ if ( currentClassName && new RegExp ( `^\\s*end\\s+${ currentClassName } ) . test ( line ) ) {
132+ currentClassName = undefined ;
133+ }
134+
135+ // For loop formal verification lens (positioned above the loop)
136+ const forMatch = / ^ \s * f o r \s + ( [ a - z A - Z _ ] [ a - z A - Z 0 - 9 _ ] * ) \s + i n \s + ( [ ^ \s ] + ) \s + l o o p \b / . exec ( line ) ;
137+ if ( forMatch && currentClassName ) {
138+ const proof = proofMap ?. get ( currentClassName ) ;
139+ if ( proof ) {
140+ const col = line . indexOf ( "for" ) ;
141+ const loopRange = Range . create ( lineIdx , col , lineIdx , col + 3 ) ;
142+
143+ const loopBug =
144+ proof . definiteBugs . find ( ( b : any ) => b . category === "array_out_of_bounds" ) ??
145+ proof . potentialBugs . find ( ( b : any ) => b . category === "array_out_of_bounds" ) ??
146+ proof . definiteBugs [ 0 ] ??
147+ proof . potentialBugs [ 0 ] ;
148+
149+ let loopTitle : string ;
150+ if ( loopBug ) {
151+ if ( loopBug . category === "array_out_of_bounds" ) {
152+ const w = loopBug . witnessValues ;
153+ const detail = w ?. index && w ?. arrayLength ? ` [${ w . index } ${ w . arrayLength } : "" ;
154+ loopTitle = `⚠ Formal Proof: Array index out of bounds${ detail } ;
155+ } else {
156+ loopTitle = `⚠ Formal Proof: ${ loopBug . description } ;
157+ }
158+ } else if ( proof . isCertifiedSafe ) {
159+ loopTitle = "✓ Loop Formally Verified (Safe Bounds)" ;
160+ } else {
161+ loopTitle = "✓ Loop Invariants Verified" ;
162+ }
163+
45164 lenses . push ( {
46- range,
47- command : {
48- title : "🌐 Digital Thread Explorer" ,
49- command : "modelscript.openThreadExplorer" ,
50- arguments : [ uri ] ,
51- } ,
52- } ) ;
53- } else {
54- const kind = classMatch [ 0 ] . trim ( ) . split ( / \s + / ) [ 0 ] ;
55- const title = kind === "study" ? "▶ Run Study" : `▶ Simulate ${ kind } ;
56- lenses . push ( {
57- range,
165+ range : loopRange ,
58166 command : {
59- title,
60- command : "modelscript.openSimulationView " ,
61- arguments : [ uri , name ] ,
167+ title : loopTitle ,
168+ command : "modelscript.showProofDetails " ,
169+ arguments : [ uri , currentClassName , proof . formattedMatrix ] ,
62170 } ,
63171 } ) ;
64172 }
@@ -130,18 +238,32 @@ export function registerCodeLensProvider(context: LspContext) {
130238 }
131239 }
132240
133- // Check formal proof results & DAE BLT results from validationService
241+ // Fallback: check formal proof results & DAE BLT results from symbol index for any un-emitted classes
134242 const index = (
135243 typeof context . workspaceManager ?. getWorkspaceIndex === "function"
136244 ? context . workspaceManager . getWorkspaceIndex ( "modelica" )
137245 : context . workspaceManager ?. globalWorkspaceIndex
138246 ) ?. getFileIndex ( uri ) ;
139247
140248 if ( index ) {
249+ const norm = ( u : string | undefined ) => ( u ? u . replace ( / ^ ( [ a - z 0 - 9 + - ] + ) : \/ { 1 , 3 } / i, "$1:///" ) . toLowerCase ( ) : "" ) ;
250+ const targetUri = norm ( uri ) ;
251+
141252 for ( const [ , symbol ] of index . symbols . entries ( ) ) {
142253 const sym = symbol as any ;
143- const proofMap = context . validationService . modelicaProofResultsByUri ?. get ( uri ) ;
144- const proof = proofMap ?. get ( sym . name ) ;
254+ // Guard: never process symbols belonging to other files in the workspace
255+ if ( sym . resourceId && norm ( sym . resourceId ) !== targetUri ) continue ;
256+ if (
257+ sym . kind !== "Class" &&
258+ sym . kind !== "Def" &&
259+ sym . kind !== "Function" &&
260+ sym . classKind !== "function" &&
261+ sym . classKind !== "model" &&
262+ sym . classKind !== "block" &&
263+ sym . classKind !== "class"
264+ ) {
265+ continue ;
266+ }
145267
146268 let startLine = sym . selectionRange ?. start . line ?? sym . range ?. start ?. line ;
147269 let startChar = sym . selectionRange ?. start . character ?? sym . range ?. start ?. character ;
@@ -154,12 +276,19 @@ export function registerCodeLensProvider(context: LspContext) {
154276 startChar = startChar ?? 0 ;
155277 const range = Range . create ( startLine , startChar , startLine , startChar ) ;
156278
157- if ( proof ) {
279+ const proof = proofMap ?. get ( sym . name ) ;
280+ if ( proof && ! emittedProofClasses . has ( sym . name ) ) {
281+ emittedProofClasses . add ( sym . name ) ;
158282 let proofTitle = "✓ Formally Verified (0 RTEs, 100% Proven Safe)" ;
159283 if ( proof . definiteBugs . length > 0 ) {
160284 proofTitle = `✗ Formal Defect: ${ proof . definiteBugs . length } ;
161285 } else if ( proof . potentialBugs . length > 0 ) {
162- proofTitle = `⚠ Formal Proof: ${ proof . potentialBugs . length } ;
286+ const oobCount = proof . potentialBugs . filter ( ( b : any ) => b . category === "array_out_of_bounds" ) . length ;
287+ if ( oobCount > 0 ) {
288+ proofTitle = `⚠ Formal Proof: ${ proof . potentialBugs . length } ;
289+ } else {
290+ proofTitle = `⚠ Formal Proof: ${ proof . potentialBugs . length } ;
291+ }
163292 }
164293
165294 lenses . push ( {
@@ -172,9 +301,9 @@ export function registerCodeLensProvider(context: LspContext) {
172301 } ) ;
173302 }
174303
175- const daeMap = context . validationService . modelicaDaeVerificationResultsByUri ?. get ( uri ) ;
176304 const daeProof = daeMap ?. get ( sym . name ) ;
177- if ( daeProof ) {
305+ if ( daeProof && ! emittedDaeClasses . has ( sym . name ) ) {
306+ emittedDaeClasses . add ( sym . name ) ;
178307 // Never display "verified" for anything other than a proven verdict.
179308 let daeTitle =
180309 daeProof . verdict ?. kind === "proven"
0 commit comments