Skip to content

Commit c755f04

Browse files
committed
docs: add proof of equivalence examples
1 parent 5ccba16 commit c755f04

3 files changed

Lines changed: 95 additions & 0 deletions

File tree

examples/proof.go

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
package main
2+
3+
import (
4+
"fmt"
5+
"log"
6+
"os"
7+
8+
semanticfw "github.com/BlackVectorOps/semantic_firewall"
9+
)
10+
11+
// PROOF OF EQUIVALENCE
12+
// The following three functions are syntactically distinct but semantically identical.
13+
// The Semantic Firewall (sfw) proves this by generating identical fingerprints for all three.
14+
15+
// Implementation 1: Idiomatic Go Range Loop
16+
const srcRange = `package main
17+
func sum(items []int) int {
18+
total := 0
19+
for _, x := range items {
20+
total += x
21+
}
22+
return total
23+
}
24+
`
25+
26+
// Implementation 2: C-Style Index Loop
27+
const srcIndex = `package main
28+
func sum(items []int) int {
29+
total := 0
30+
for i := 0; i < len(items); i++ {
31+
total += items[i]
32+
}
33+
return total
34+
}
35+
`
36+
37+
// Implementation 3: Raw Goto Loop (The "Assembly" Approach)
38+
const srcGoto = `package main
39+
func sum(items []int) int {
40+
total := 0
41+
i := 0
42+
loop:
43+
if i >= len(items) {
44+
goto done
45+
}
46+
total += items[i]
47+
i++
48+
goto loop
49+
done:
50+
return total
51+
}
52+
`
53+
54+
func main() {
55+
// 1. Analyze
56+
// Note: We use the advanced policy to ensure we capture the logic correctly
57+
resRange, _ := semanticfw.FingerprintSource("range.go", srcRange, semanticfw.DefaultLiteralPolicy)
58+
resIndex, _ := semanticfw.FingerprintSource("index.go", srcIndex, semanticfw.DefaultLiteralPolicy)
59+
resGoto, _ := semanticfw.FingerprintSource("goto.go", srcGoto, semanticfw.DefaultLiteralPolicy)
60+
61+
// 2. Extract Fingerprints
62+
// We access the first function found in each file (which is 'sum')
63+
h1 := resRange[0].Fingerprint
64+
h2 := resIndex[0].Fingerprint
65+
h3 := resGoto[0].Fingerprint
66+
67+
// 3. Verify
68+
fmt.Printf("\n[Semantic Firewall Proof]\n")
69+
fmt.Printf("1. Range Loop Hash: %s\n", h1)
70+
fmt.Printf("2. Index Loop Hash: %s\n", h2)
71+
fmt.Printf("3. Goto Loop Hash: %s\n", h3)
72+
73+
if h1 == h2 && h2 == h3 {
74+
fmt.Printf("\n[SUCCESS] All three implementations are logically identical.\n")
75+
os.Exit(0)
76+
} else {
77+
log.Fatalf("\n[FAIL] Logic divergence detected.\n")
78+
}
79+
}

examples/v1/range.go

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
package main
2+
func sum(items []int) int {
3+
total := 0
4+
for _, x := range items {
5+
total += x
6+
}
7+
return total
8+
}

examples/v2/index.go

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
package main
2+
func sum(items []int) int {
3+
total := 0
4+
for i := 0; i < len(items); i++ {
5+
total += items[i]
6+
}
7+
return total
8+
}

0 commit comments

Comments
 (0)