feat: Halmos assert mode

package.json

@@ -1,7 +1,7 @@
 {
   "name": "@recon-fuzz/log-parser",
   "description": "Fuzzer log parser for Recon Fuzz",
-  "version": "0.0.37",
+  "version": "0.0.38",
   "license": "GPL-2.0-only",
   "main": "./lib/cjs/index.js",
   "module": "./lib/esm/index.js",

src/halmos/functionGenerator.ts

@@ -21,14 +21,41 @@ export function parseAddressBook(input: string): AddressBook {
 
 export function parseFailedProperties(input: string): Set<string> {
   const set = new Set<string>();
+  // 1) Regular FAIL lines, capture function name without params
   const re = /^\[FAIL\]\s+([^\(\[]+)/gm;
   let m: RegExpExecArray | null;
   while ((m = re.exec(input))) {
     set.add(m[1].trim());
   }
+  // 2) Inline assertion failures
+  // Example: Assertion failure detected in CryticToFoundry.doomsday_increment_never_reverts()
+  const assertionRe = /Assertion failure detected in\s+[\w$]+\.([^\)]+)\(\)/g;
+  const targetFns = parseTargetFunctions(input); // Full names incl. params, e.g. foo(uint256) or bar()
+  while ((m = assertionRe.exec(input))) {
+    const fn = (m[1] || "").trim(); // name without parens
+    // Only count as failed if it's one of the initial target functions (by name only)
+    const matchInTargets = Array.from(targetFns).some((full) => full.replace(/\(.*/, "") === fn);
+    if (matchInTargets) set.add(fn);
+  }
   return set;
 }
 
+// Parse list of target function signatures from the "Initial Invariant Target Functions" section
+export function parseTargetFunctions(input: string): Set<string> {
+  const out = new Set<string>();
+  const section = /Initial Invariant Target Functions([\s\S]*?)\n╰/m.exec(input);
+  if (!section) return out;
+  const body = section[1];
+  // Lines look like: "│ ├── add_new_asset(uint8)" or "│ └── switchActor(uint256)"
+  const lineRe = /^[\s\u2502]+[├└]──\s+([^\s]+\([^)]*\))/gm;
+  let m: RegExpExecArray | null;
+  while ((m = lineRe.exec(body))) {
+    const sig = (m[1] || "").trim(); // e.g., add_new_asset(uint8)
+    if (sig) out.add(sig);
+  }
+  return out;
+}
+
 interface CounterexampleBlock {
   headerLine: string; // The [FAIL] line
   traceFirstLine: string; // The first CALL line of the Trace: block (the final failing call)
@@ -177,17 +204,34 @@ function renderFoundryTest(
   }
 
   // Render final call from Trace first line, always last
+  // But avoid duplication when the same function already appears in the Sequence
   if (block.traceFirstLine) {
+    const traceFn = extractFnNameFromCall(block.traceFirstLine);
+    const seqFns = new Set(
+      block.sequenceCalls.map((s) => extractFnNameFromCall(s)).filter((x): x is string => !!x)
+    );
+    const duplicate = traceFn && seqFns.has(traceFn);
+    if (!duplicate) {
     const { call, prank, pre } = renderCall(block.traceFirstLine, block.counterexampleVars, addressBook);
     if (pre && pre.length) pre.forEach((l) => bodyLines.push(`   ${l}`));
     if (prank) bodyLines.push(`   vm.prank(${prank});`);
     bodyLines.push(`   ${call};`);
+    }
   }
 
   const footer = "}";
   return [header, ...bodyLines, footer].join("\n");
 }
 
+function extractFnNameFromCall(traceCallLine: string): string | null {
+  const sanitized = stripMetaTags(traceCallLine).replace(/^\s+/, "");
+  const m1 = /^CALL\s+[^:]+::([^\(]+)\(/.exec(sanitized);
+  if (m1 && m1[1]) return m1[1].trim();
+  const m2 = /^CALL\s+(0x[a-fA-F0-9]{8,40})::([^\(]+)\(/.exec(sanitized);
+  if (m2 && m2[2]) return m2[2].trim();
+  return null;
+}
+
 function sanitizeTestName(s: string): string {
   return s.replace(/[^a-zA-Z0-9_]/g, "_");
 }

src/halmos/index.ts

@@ -3,6 +3,7 @@ import {
     buildReprosFromHalmosLogs,
     parseAddressBook,
     parseFailedProperties,
+    parseTargetFunctions,
 } from "./functionGenerator";
 
 // Parse the entire Halmos log and update the jobStats counters and results list
@@ -15,39 +16,75 @@ export const processHalmos = (logs: string, jobStats: FuzzingResults, maxCounter
     jobStats.results.push(...resultLines);
 
     jobStats.passed = resultLines.filter((l) => l.startsWith("[PASS]")).length;
+    // failed will be finalized later from parseFailedProperties (which includes inline assertions)
     jobStats.failed = resultLines.filter((l) => l.startsWith("[FAIL]")).length;
     // TIMEOUT is informational here; we don't store a separate counter in FuzzingResults
 
     // Extract the address section once so we can prefix sequences for proper address mapping
     const addressSection = extractAddressSection(logs);
 
-    // Extract each Trace/Counterexample/Sequence block and attach it as a brokenProperty entry,
-    // capped by maxCounterexamples per property, preferring empty counterexamples when present.
-    const traceBlocks = extractTraceBlocks(logs);
-    const byProp = new Map<string, Array<{ block: string; empty: boolean }>>();
-    for (const tb of traceBlocks) {
-        if (!tb.property) continue;
-        const arr = byProp.get(tb.property) ?? [];
-        arr.push({ block: tb.block, empty: tb.empty });
-        byProp.set(tb.property, arr);
+    // Only produce broken properties when we detect failures ([FAIL] lines or inline assertion failures)
+    const allowedFailedProps = parseFailedProperties(logs);
+    // Also synthesize result lines for each target function based on whether it failed via inline assertion
+    const targets = Array.from(parseTargetFunctions(logs)); // e.g., fn(uint256)
+    const existingProps = new Set(
+        jobStats.results
+            .map((l) => /\[(?:PASS|FAIL|TIMEOUT)\]\s+([^\(\[]+)/.exec(l)?.[1]?.trim())
+            .filter((x): x is string => !!x)
+    );
+    for (const sig of targets) {
+        const nameOnly = sig.replace(/\(.*/, "");
+        // Skip if already present in result lines
+        if (existingProps.has(nameOnly)) continue;
+        if (allowedFailedProps.has(nameOnly)) {
+            // Use full signature when synthesizing FAIL entries
+            jobStats.results.push(`[FAIL] ${sig} (paths: -, time: -, bounds: [])`);
+        } else {
+            jobStats.results.push(`[PASS] ${sig} (paths: -, time: -, bounds: [])`);
+        }
     }
-    for (const [prop, arr] of byProp) {
-        const empty = arr.find((x) => x.empty);
-        if (empty) {
-            jobStats.brokenProperties.push({
-                brokenProperty: prop,
-                sequence: `${addressSection}\n${empty.block}`,
-            });
-            continue;
+    if (allowedFailedProps.size > 0) {
+        // Extract each Trace/Counterexample/Sequence block and attach it as a brokenProperty entry,
+        // capped by maxCounterexamples per property, preferring empty counterexamples when present.
+        const traceBlocks = extractTraceBlocks(logs);
+        const byProp = new Map<string, Array<{ block: string; empty: boolean }>>();
+        for (const tb of traceBlocks) {
+            if (!tb.property) continue;
+            // Filter to only properties considered failed
+            if (!allowedFailedProps.has(tb.property)) continue;
+            const arr = byProp.get(tb.property) ?? [];
+            arr.push({ block: tb.block, empty: tb.empty });
+            byProp.set(tb.property, arr);
         }
-        const limited = arr.slice(0, Math.max(0, maxCounterexamples));
-        for (const it of limited) {
-            jobStats.brokenProperties.push({
-                brokenProperty: prop,
-                sequence: `${addressSection}\n${it.block}`,
-            });
+        for (const [prop, arr] of byProp) {
+            const empty = arr.find((x) => x.empty);
+            if (empty) {
+                jobStats.brokenProperties.push({
+                    brokenProperty: prop,
+                    sequence: `${addressSection}\n${empty.block}`,
+                });
+                continue;
+            }
+            const limited = arr.slice(0, Math.max(0, maxCounterexamples));
+            for (const it of limited) {
+                jobStats.brokenProperties.push({
+                    brokenProperty: prop,
+                    sequence: `${addressSection}\n${it.block}`,
+                });
+            }
         }
     }
+    // Finalize failed count as number of unique failed properties (including inline assertions and [FAIL] lines)
+    const failedFromResults = new Set(
+        jobStats.results
+            .filter((l) => l.startsWith("[FAIL]"))
+            .map((l) => /\[FAIL\]\s+([^\(\[]+)/.exec(l)?.[1]?.trim())
+            .filter((x): x is string => !!x)
+    );
+    allowedFailedProps.forEach((p) => failedFromResults.add(p));
+    jobStats.failed = failedFromResults.size;
+    // Recompute passed based on results after synthesis
+    jobStats.passed = jobStats.results.filter((l) => l.startsWith("[PASS]")).length;
 
     // Parse final symbolic result summary for duration and (optionally) number of tests
     // Example: "Symbolic test result: 1 passed; 20 failed; time: 3.21s"
@@ -108,5 +145,8 @@ export const halmosLogsToFunctions = (
         ? new Set<string>([brokenProp])
         : parseFailedProperties(input);
 
+    if (failedProps.size === 0) {
+        return "// No failed properties found in Halmos logs";
+    }
     return buildReprosFromHalmosLogs(input, prefix, addressBook, failedProps, { maxCounterexamples });
 };

src/reportBuilder/reportBuilder.ts

@@ -116,14 +116,15 @@ export const prepareProperties = (
     };
   // Capture Halmos
   } else if (propRaw.includes("[PASS]")) {
-      const m = propRaw.match(/\[PASS\]\s+([A-Za-z_][A-Za-z0-9_]*)\s*\(/);
-      return { property: m?.[1] ?? "Unknown", status: "✅" };
+    // Show full signature inside the parentheses
+    const m = propRaw.match(/\[PASS\]\s+([A-Za-z_][A-Za-z0-9_]*\([^)]*\))/);
+    return { property: m?.[1] ?? "Unknown", status: "✅" };
   } else if (propRaw.includes("[FAIL]")) {
-      const m = propRaw.match(/\[FAIL\]\s+([A-Za-z_][A-Za-z0-9_]*)\s*\(/);
-      return { property: m?.[1] ?? "Unknown", status: "❌" };
+    const m = propRaw.match(/\[FAIL\]\s+([A-Za-z_][A-Za-z0-9_]*\([^)]*\))/);
+    return { property: m?.[1] ?? "Unknown", status: "❌" };
   } else if (propRaw.includes("[TIMEOUT]")) {
-      const m = propRaw.match(/\[TIMEOUT\]\s+([A-Za-z_][A-Za-z0-9_]*)\s*\(/);
-      return { property: m?.[1] ?? "Unknown", status: "⏳" };
+    const m = propRaw.match(/\[TIMEOUT\]\s+([A-Za-z_][A-Za-z0-9_]*\([^)]*\))/);
+    return { property: m?.[1] ?? "Unknown", status: "⏳" };
   } else {
     return {
       property: "Unknown",