feat: Halmos assert mode

[0kn0t]

sample output:

Recon Recap for create-chimera-app [WSL: Ubuntu]

Fuzzer overview

• Fuzzer: HALMOS
• Duration: 3.29s
• Coverage: 0
• Failed: 1
• Passed: 10
• Number of tests: 1

Results

Property	Status
invariant_number_never_zero()	✅
add_new_asset(uint8)	✅
asset_approve(address,uint128)	✅
asset_mint(address,uint128)	✅
counter_increment()	✅
counter_increment_asAdmin()	✅
counter_setNumber1(uint256)	✅
counter_setNumber2(uint256)	✅
doomsday_increment_never_reverts()	❌
switchActor(uint256)	✅
switch_asset(uint256)	✅

Broken Properties

Broken property

doomsday_increment_never_reverts

Sequence

// forge test --match-test test_doomsday_increment_never_reverts__0 -vv 
 function test_doomsday_increment_never_reverts__0() public {
   counter_setNumber1(115792089237316195423570985008687907853269984665640564039457584007913129639935);
   doomsday_increment_never_reverts();
}

[Copilot]

Pull Request Overview

This PR adds support for Halmos assert mode, which allows the tool to handle inline assertion failures in addition to standard [FAIL] lines. The changes enable proper detection and reporting of assertion failures that occur within target functions, improving coverage reporting accuracy.

Key changes:

• Enhanced parsing to detect inline assertion failures alongside standard [FAIL] lines
• Added target function signature parsing with full parameter information in reports
• Improved counterexample generation logic to avoid duplicates and filter by failed properties

Reviewed Changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.

File	Description
src/reportBuilder/reportBuilder.ts	Updates regex patterns to capture full function signatures with parameters in property names
src/halmos/index.ts	Adds comprehensive logic for parsing target functions, handling inline assertions, and synthesizing results
src/halmos/functionGenerator.ts	Implements target function parsing and inline assertion failure detection with deduplication logic
package.json	Version bump to 0.0.38

---

_{Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.}

[Copilot]

The regex pattern has an unescaped closing parenthesis ) inside the character class. This should be escaped as \) to match a literal closing parenthesis.

[Copilot]

[nitpick] The two regex patterns are very similar and could be consolidated into a single pattern. Consider using /^CALL\s+(?:[^:]+|(0x[a-fA-F0-9]{8,40}))::([^\(]+)\(/ and adjusting the capture group handling accordingly.

Suggested change

	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();
	const m = /^CALL\s+(?:[^:]+|(0x[a-fA-F0-9]{8,40}))::([^\(]+)\(/.exec(sanitized);
	if (m && m[2]) return m[2].trim();