@@ -96,25 +96,31 @@ function genRegion(rng, name, existingRegions) {
9696}
9797
9898/// Generate a random function declaration.
99+ /// Effects use the typed-wasm grammar syntax: effects { ReadRegion(Name), ... }
99100function genFunction ( rng , regions ) {
100101 const name = `fn_${ rng . next ( ) % 1000 } ;
101102 const retType = rng . pick ( PRIMITIVE_TYPES ) ;
102103 const effects = [ ] ;
103- if ( rng . nextFloat ( ) < 0.5 ) effects . push ( "read" ) ;
104- if ( rng . nextFloat ( ) < 0.3 ) effects . push ( "write" ) ;
105- if ( rng . nextFloat ( ) < 0.1 ) effects . push ( "alloc" ) ;
104+
105+ // Generate effects using the real grammar: ReadRegion(X) / WriteRegion(X).
106+ if ( regions . length > 0 ) {
107+ if ( rng . nextFloat ( ) < 0.5 ) effects . push ( `ReadRegion(${ rng . pick ( regions ) } ) ;
108+ if ( rng . nextFloat ( ) < 0.3 ) effects . push ( `WriteRegion(${ rng . pick ( regions ) } ) ;
109+ }
106110
107111 const params = [ ] ;
108112 if ( regions . length > 0 && rng . nextFloat ( ) < 0.7 ) {
109113 const r = rng . pick ( regions ) ;
110- params . push ( `handle: &${ r } ) ;
114+ const mode = rng . nextFloat ( ) < 0.5 ? "&" : "&mut " ;
115+ params . push ( `handle: ${ mode } ${ r } ) ;
111116 }
112117 if ( rng . nextFloat ( ) < 0.5 ) {
113- params . push ( `index : i32` ) ;
118+ params . push ( `idx : i32` ) ;
114119 }
115120
116- const effectStr = effects . length > 0 ? ` effects(${ effects . join ( ", " ) } : "" ;
117- return `fn ${ name } ${ params . join ( ", " ) } ${ retType } ${ effectStr } ;
121+ const effectStr = effects . length > 0 ? `\n effects { ${ effects . join ( ", " ) } : "" ;
122+ const paramStr = params . join ( ",\n " ) ;
123+ return `fn ${ name } ${ paramStr } ${ retType } ${ effectStr } ;
118124}
119125
120126/// Generate a random memory declaration.
@@ -200,6 +206,39 @@ console.log("=== ECHIDNA Prover Oracle: typed-wasm ===\n");
200206console . log ( `Iterations: ${ iterations } ) ;
201207console . log ( `ECHIDNA: ${ echidnaUrl } ) ;
202208
209+ // ============================================================================
210+ // ReScript ADT TAG constants
211+ // ============================================================================
212+ //
213+ // ReScript compiles custom variants to JS objects with integer TAG fields.
214+ // The integer is the constructor's 0-based position in the type declaration.
215+ // Standard library types like Result use string tags ("Ok"/"Error").
216+ //
217+ // declaration (src/parser/Ast.res):
218+ const TAG_RegionDecl = 0 ;
219+ const TAG_ImportRegionDecl = 1 ;
220+ const TAG_ExportRegionDecl = 2 ;
221+ const TAG_FunctionDecl = 3 ;
222+ const TAG_MemoryDecl = 4 ;
223+ const TAG_InvariantDecl = 5 ;
224+
225+ // fieldType (src/parser/Ast.res):
226+ const TAG_Primitive = 0 ;
227+ const TAG_RegionRef = 1 ;
228+ const TAG_PointerType = 2 ;
229+ const TAG_OptionalType = 3 ;
230+ const TAG_ArrayFieldType = 4 ;
231+ const TAG_UnionType = 5 ;
232+
233+ // effect — mixed (no-payload = integer value, payload = { TAG: n } object):
234+ // ReadEffect=0, WriteEffect=1, AllocEffect=2, FreeEffect=3 (bare integers)
235+ // ReadRegionEffect=0, WriteRegionEffect=1 (objects with TAG field — separate
236+ // tag space from the no-payload variants since ReScript splits them)
237+ const EFFECT_ReadEffect = 0 ;
238+ const EFFECT_WriteEffect = 1 ;
239+ const EFFECT_AllocEffect = 2 ;
240+ const EFFECT_FreeEffect = 3 ;
241+
203242// Property 1: Parse determinism — same input always gives same result.
204243console . log ( "Property 1: Parse determinism" ) ;
205244for ( let i = 0 ; i < iterations ; i ++ ) {
@@ -230,7 +269,7 @@ for (let i = 0; i < iterations; i++) {
230269 property ( `well-formed regions seed=${ i } , ( ) => {
231270 const decls = result . _0 . declarations ;
232271 for ( const d of decls ) {
233- if ( typeof d . node === "object" && d . node . TAG === "RegionDecl" ) {
272+ if ( typeof d . node === "object" && d . node . TAG === TAG_RegionDecl ) {
234273 if ( d . node . _0 . fields . length === 0 ) {
235274 throw new Error ( `Empty region at seed ${ i } ) ;
236275 }
@@ -253,16 +292,17 @@ for (let i = 0; i < Math.min(iterations, 50); i++) {
253292 property ( `reflexivity seed=${ i } , ( ) => {
254293 const decls = result . _0 . declarations ;
255294 const regions = decls
256- . filter ( ( d ) => typeof d . node === "object" && d . node . TAG === "RegionDecl" )
295+ . filter ( ( d ) => typeof d . node === "object" && d . node . TAG === TAG_RegionDecl )
257296 . map ( ( d ) => d . node . _0 ) ;
258297
259- // Every region's field types must be consistent with themselves .
298+ // Every region's field types must be a known fieldType variant (TAG 0-5) .
260299 for ( const r of regions ) {
261300 for ( const f of r . fields ) {
262301 const t = f . node . fieldType . node ;
263- // Type tag must be a known variant.
264- if ( ! [ "Primitive" , "RegionRef" , "ArrayFieldType" , "OptionalType" ] . includes ( t . TAG ) ) {
265- throw new Error ( `Unknown type tag ${ t . TAG } ${ r . name } ${ f . node . name } ) ;
302+ // Integer TAG for custom ADTs; valid range is 0..5 (Primitive..UnionType).
303+ const tag = typeof t === "object" ? t . TAG : t ;
304+ if ( typeof tag !== "number" || tag < TAG_Primitive || tag > TAG_UnionType ) {
305+ throw new Error ( `Unknown fieldType TAG ${ JSON . stringify ( tag ) } ${ r . name } ${ f . node . name } ) ;
266306 }
267307 }
268308 }
@@ -281,17 +321,28 @@ for (let i = 0; i < Math.min(iterations, 50); i++) {
281321 property ( `effects seed=${ i } , ( ) => {
282322 const decls = result . _0 . declarations ;
283323 const fns = decls
284- . filter ( ( d ) => typeof d . node === "object" && d . node . TAG === "FunctionDecl" )
324+ . filter ( ( d ) => typeof d . node === "object" && d . node . TAG === TAG_FunctionDecl )
285325 . map ( ( d ) => d . node . _0 ) ;
286326
287327 for ( const fn of fns ) {
288- // If function has effects, they must be from the valid set.
328+ // If function has effects, each must be a valid effect variant.
329+ // No-payload effects (Read/Write/Alloc/Free) compile to integers 0-3.
330+ // Payload effects (ReadRegion/WriteRegion) compile to { TAG: 0|1, _0: name }.
289331 if ( fn . effects ) {
290- const validEffects = [ "read" , "write" , "alloc" , "free" ] ;
291- for ( const eff of fn . effects ) {
292- const effName = typeof eff === "string" ? eff : eff . node || eff . _0 ;
293- if ( typeof effName === "string" && ! validEffects . includes ( effName ) ) {
294- throw new Error ( `Invalid effect '${ effName } ${ fn . name } ) ;
332+ for ( const locEff of fn . effects ) {
333+ const eff = locEff . node ;
334+ if ( typeof eff === "number" ) {
335+ // No-payload: must be ReadEffect(0)..FreeEffect(3)
336+ if ( eff < EFFECT_ReadEffect || eff > EFFECT_FreeEffect ) {
337+ throw new Error ( `Invalid no-payload effect tag ${ eff } ${ fn . name } ) ;
338+ }
339+ } else if ( typeof eff === "object" && eff !== null ) {
340+ // Payload: ReadRegionEffect=TAG 0, WriteRegionEffect=TAG 1
341+ if ( eff . TAG < 0 || eff . TAG > 1 ) {
342+ throw new Error ( `Invalid payload effect TAG ${ eff . TAG } ${ fn . name } ) ;
343+ }
344+ } else {
345+ throw new Error ( `Unexpected effect shape ${ JSON . stringify ( eff ) } ${ fn . name } ) ;
295346 }
296347 }
297348 }
@@ -314,8 +365,10 @@ import { readFileSync as _readFileSync } from "node:fs";
314365import { resolve as _resolve } from "node:path" ;
315366import { fileURLToPath as _fileURLToPath } from "node:url" ;
316367
317- const _thisDir = _fileURLToPath ( import . meta. url ) ;
318- const _layoutDir = _resolve ( _thisDir , ".." , ".." , ".." , "src" , "abi" , "layout" ) ;
368+ // _thisFile is the path to this harness file, not a directory.
369+ // The resolve chain strips the filename (first ..) then navigates to the layout dir.
370+ const _thisFile = _fileURLToPath ( import . meta. url ) ;
371+ const _layoutDir = _resolve ( _thisFile , ".." , ".." , ".." , "src" , "abi" , "layout" ) ;
319372
320373/**
321374 * Scan an Idris2 source file for banned safety patterns.
0 commit comments