Update formal spec, add libcurl via Conan, update documentation

Co-authored-by: johndoe6345789 <224850594+johndoe6345789@users.noreply.github.com>

spec/WizardMergeSpec.tla

@@ -15,6 +15,11 @@ EXTENDS Naturals, FiniteSets
     * Identical changes from both sides
     * Whitespace-only differences
   - Command-line interface (wizardmerge-cli)
+  - Pull request URL processing and conflict resolution:
+    * Parse GitHub PR URLs
+    * Fetch PR data via GitHub API
+    * Apply merge algorithm to PR files
+    * HTTP API endpoint for PR resolution
   
   NOT YET IMPLEMENTED (Future phases):
   - Dependency graph construction (SDG analysis)
@@ -22,11 +27,26 @@ EXTENDS Naturals, FiniteSets
   - Edge classification (safe vs. violated)
   - Fine-grained DCB (Definition-Code Block) tracking
   - Mirror mapping and matching
+  - Git branch creation for resolved PRs
   
   The current implementation in backend/src/merge/three_way_merge.cpp provides
   a foundation for the full dependency-aware algorithm specified here. Future
   phases will enhance it with the SDG analysis, edge classification, and
   dependency-aware conflict resolution described in this specification.
+  
+  PR Resolution Workflow (Phase 1.2):
+  The PR resolution feature extends the core merge algorithm to work with
+  GitHub pull requests. The workflow is:
+    1. Accept PR URL: Parse URL to extract owner, repo, and PR number
+    2. Fetch PR metadata: Use GitHub API to retrieve PR information
+    3. Fetch file versions: Retrieve base and head versions of modified files
+    4. Apply merge algorithm: For each file, perform three-way merge
+    5. Auto-resolve conflicts: Apply heuristic resolution where possible
+    6. Return results: Provide merged content and conflict status
+  
+  This workflow enables batch processing of PR conflicts using the same
+  dependency-aware merge principles, with future integration planned for
+  automatic branch creation and PR updates.
 *)
 
 (*
@@ -316,4 +336,98 @@ Inv ==
 
 THEOREM Spec => []Inv
 
+(***************************************************************************)
+(* Pull Request Resolution Specification (Phase 1.2)                      *)
+(***************************************************************************)
+
+(*
+  This section extends the core merge specification to model the PR resolution
+  workflow. It describes how WizardMerge processes GitHub pull requests to
+  identify and resolve conflicts across multiple files.
+*)
+
+CONSTANTS
+  (*
+    PR_FILES: the set of all files in the pull request
+  *)
+  PR_FILES,
+  
+  (*
+    FileStatus: maps each file to its modification status in the PR
+    Possible values: "modified", "added", "removed", "renamed"
+  *)
+  FileStatus,
+  
+  (*
+    BaseSHA, HeadSHA: commit identifiers for base and head of the PR
+  *)
+  BaseSHA, HeadSHA
+
+(*
+  A file is resolvable if it was modified (not removed) and we can fetch
+  both its base and head versions.
+*)
+Resolvable(f) ==
+  FileStatus[f] \in {"modified", "added"}
+
+(*
+  PR_MergeResult: for each file f in PR_FILES, we compute a merge result
+  using the three-way merge algorithm. This is a function from PR_FILES
+  to merge outcomes.
+  
+  Possible outcomes:
+    - "success": file merged without conflicts
+    - "conflict": file has unresolved conflicts
+    - "error": failed to fetch or process file
+    - "skipped": file was removed or not applicable
+*)
+
+VARIABLE PR_MergeResults
+
+PR_Init ==
+  PR_MergeResults = [f \in PR_FILES |-> "pending"]
+
+(*
+  Process a single file by applying the three-way merge algorithm.
+  This abstracts the actual merge computation but captures the key decision:
+  whether the file can be auto-resolved or requires manual intervention.
+*)
+ProcessFile(f) ==
+  /\ PR_MergeResults[f] = "pending"
+  /\ IF ~Resolvable(f)
+     THEN PR_MergeResults' = [PR_MergeResults EXCEPT ![f] = "skipped"]
+     ELSE \/ PR_MergeResults' = [PR_MergeResults EXCEPT ![f] = "success"]
+          \/ PR_MergeResults' = [PR_MergeResults EXCEPT ![f] = "conflict"]
+          \/ PR_MergeResults' = [PR_MergeResults EXCEPT ![f] = "error"]
+
+(*
+  PR completion: all files have been processed
+*)
+PR_Complete ==
+  \A f \in PR_FILES : PR_MergeResults[f] # "pending"
+
+(*
+  PR success metric: percentage of files successfully merged
+*)
+PR_SuccessRate ==
+  LET successful == {f \in PR_FILES : PR_MergeResults[f] = "success"}
+  IN  Cardinality(successful) * 100 \div Cardinality(PR_FILES)
+
+(*
+  PR resolution quality property: a "good" PR resolution is one where
+  all resolvable files are either successfully merged or marked as conflicts
+  (no errors in fetching or processing).
+*)
+GoodPRResolution ==
+  \A f \in PR_FILES :
+    Resolvable(f) => PR_MergeResults[f] \in {"success", "conflict"}
+
+PR_Spec ==
+  PR_Init /\ [][(\E f \in PR_FILES : ProcessFile(f))]_<<PR_MergeResults>>
+
+PR_Invariant ==
+  PR_Complete => GoodPRResolution
+
+THEOREM PR_Spec => []PR_Invariant
+
 =============================================================================