Skip to content

Commit 9ba4bba

Browse files
kumarakkumarak
committed
refactor patch and contract function implementations
1 parent 81374cd commit 9ba4bba

File tree

19 files changed

+1880
-496
lines changed

19 files changed

+1880
-496
lines changed

‎docs/GettingStarted/patch_specifications.md‎

Lines changed: 386 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,23 @@ meta_contracts: # Meta-contract configurations
103103

104104
```
105105

106+
## Contract Types
107+
108+
Patchestry supports two types of contracts:
109+
110+
1. **Runtime Contracts**: Implemented as C/C++ functions that are called at runtime to validate conditions
111+
2. **Static Contracts**: Declarative specifications attached as MLIR attributes for static analysis and verification
112+
113+
### Runtime vs Static Contracts
114+
115+
| Aspect | Runtime Contracts | Static Contracts |
116+
|--------|------------------|------------------|
117+
| **Implementation** | C/C++ function code | Declarative predicates in YAML |
118+
| **Verification** | Runtime checks during execution | Static analysis at compile time |
119+
| **Performance** | Runtime overhead | No runtime overhead |
120+
| **Expressiveness** | Full programming language | Limited to supported predicates |
121+
| **Use Cases** | Complex validations, security checks | Type constraints, null checks, range checks |
122+
106123
## Field Descriptions
107124

108125
### Top-Level Fields
@@ -550,6 +567,375 @@ action:
550567
index: "1"
551568
```
552569

570+
## Contract Library Specification
571+
572+
Contract libraries are separate YAML files that define reusable contracts. They can be referenced by multiple deployment specifications.
573+
574+
### Contract Library Structure
575+
576+
```yaml
577+
apiVersion: patchestry.io/v1
578+
579+
metadata:
580+
name: "contract-library-name"
581+
version: "1.0.0"
582+
description: "Description of contract library"
583+
author: "Author Name"
584+
created: "YYYY-MM-DD"
585+
586+
contracts:
587+
- name: "contract_name"
588+
id: "CONTRACT-ID-001"
589+
description: "Contract description"
590+
category: "validation_category"
591+
severity: "critical|high|medium|low"
592+
type: "STATIC|RUNTIME"
593+
594+
# For STATIC contracts
595+
preconditions: [...]
596+
postconditions: [...]
597+
598+
# For RUNTIME contracts
599+
implementation: {...}
600+
contract_module: "path/to/module"
601+
```
602+
603+
### Contract Library Fields
604+
605+
| Field | Description | Required | Example |
606+
|-------|-------------|----------|---------|
607+
| `apiVersion` | API version | Yes | `"patchestry.io/v1"` |
608+
| `metadata` | Library metadata | Yes | See metadata fields |
609+
| `contracts` | List of contract specifications | Yes | See contract spec fields |
610+
611+
### Contract Specification Fields
612+
613+
| Field | Description | Required | Type | Example |
614+
|-------|-------------|----------|------|---------|
615+
| `name` | Contract identifier | Yes | All | `"usb_validation_contract"` |
616+
| `id` | Unique contract ID | Yes | All | `"USB-CONTRACT-001"` |
617+
| `description` | Contract description | No | All | `"Validates USB parameters"` |
618+
| `category` | Contract category | No | All | `"validation"`, `"security"` |
619+
| `severity` | Severity level | No | All | `"critical"`, `"high"`, `"medium"`, `"low"` |
620+
| `type` | Contract type | Yes | All | `"STATIC"` or `"RUNTIME"` |
621+
| `preconditions` | Static preconditions | STATIC only | STATIC | List of precondition specs |
622+
| `postconditions` | Static postconditions | STATIC only | STATIC | List of postcondition specs |
623+
| `implementation` | Runtime implementation | RUNTIME only | RUNTIME | Implementation details |
624+
| `contract_module` | Path to contract module | RUNTIME only | RUNTIME | `"contracts/security.o"` |
625+
626+
### Static Contract Predicates
627+
628+
Static contracts use declarative predicates that are attached as MLIR attributes. Each predicate specifies a condition that must hold.
629+
630+
#### Predicate Structure
631+
632+
```yaml
633+
preconditions:
634+
- id: "precondition_1"
635+
description: "Description of the precondition"
636+
pred:
637+
kind: "nonnull|relation|alignment|expr|range"
638+
# Fields depend on kind - see "Predicate Kind Requirements" below
639+
target: "arg0|arg1|...|return_value|symbol" # Required for: nonnull, relation, range
640+
relation: "eq|neq|lt|lte|gt|gte|none" # Required for: relation
641+
value: "constant_value" # Required for: relation
642+
symbol: "symbol_name" # Optional: descriptive symbol name
643+
align: "alignment_bytes" # Required for: alignment
644+
expr: "expression_string" # Required for: expr
645+
range: # Required for: range
646+
min: "min_value"
647+
max: "max_value"
648+
649+
postconditions:
650+
- id: "postcondition_1"
651+
description: "Description of the postcondition"
652+
pred:
653+
# Same structure as preconditions
654+
```
655+
656+
#### Static Contract Predicate Fields
657+
658+
| Field | Description | Required | Example |
659+
|-------|-------------|----------|---------|
660+
| `id` | Unique identifier for the condition | Yes | `"precondition_1"` |
661+
| `description` | Human-readable description | No | `"Ensure pointer is non-null"` |
662+
| `pred` | Predicate specification | Yes | See predicate fields below |
663+
664+
#### Predicate Fields
665+
666+
| Field | Description | Required | Valid Values | Example |
667+
|-------|-------------|----------|--------------|---------|
668+
| `kind` | Type of predicate | Yes | `nonnull`, `relation`, `alignment`, `expr`, `range` | `"relation"` |
669+
| `target` | What the predicate applies to | `nonnull`, `relation`, `range` | `arg0`, `arg1`, ..., `return_value`, `symbol` | `"arg0"` |
670+
| `relation` | Comparison relation | `relation` only | `eq`, `neq`, `lt`, `lte`, `gt`, `gte`, `none` | `"neq"` |
671+
| `value` | Constant value for comparison | `relation` only | String representation of value | `"0"`, `"NULL"` |
672+
| `symbol` | Symbol name reference (descriptive) | If target is symbol | Symbol name | `"usb_device"` |
673+
| `align` | Alignment requirement in bytes | `alignment` only | String representation of bytes | `"4"`, `"8"` |
674+
| `expr` | Expression string | `expr` only | Expression string | `"usb_device != NULL"` |
675+
| `range` | Range constraint | `range` only | Range object | See range fields |
676+
677+
#### Range Fields
678+
679+
| Field | Description | Example |
680+
|-------|-------------|---------|
681+
| `min` | Minimum value (inclusive) | `"0"` |
682+
| `max` | Maximum value (inclusive) | `"USB_MAX_PACKET_SIZE"` |
683+
684+
#### Predicate Kinds and Required Fields
685+
686+
Each predicate kind requires specific fields. **Only include the fields listed for each kind** to avoid parser errors:
687+
688+
| Kind | Description | Required Fields | Optional Fields | Example Use Case |
689+
|------|-------------|-----------------|-----------------|------------------|
690+
| `nonnull` | Verify target is not null | `kind`, `target` (arg or return_value) | `symbol` | Pointer validation |
691+
| `relation` | Compare target against a value | `kind`, `target` (arg, return_value, or symbol), `relation`, `value` | `symbol` | Bounds checking, comparisons |
692+
| `alignment` | Verify memory alignment | `kind`, `target`, `align` | `symbol` | Memory alignment requirements |
693+
| `expr` | Free-form expression | `kind`, `expr` | `target`, `symbol` | Complex conditions |
694+
| `range` | Verify value is within range | `kind`, `target` (arg, return_value, or symbol), `range` (with `min` and `max`) | `symbol` | Input validation, bounds |
695+
696+
#### Quick Reference: Field Requirements by Predicate Kind
697+
698+
| Predicate Kind | `kind` | `target` | `relation` | `value` | `align` | `expr` | `range` | `symbol` |
699+
|----------------|--------|----------|------------|---------|---------|--------|---------|----------|
700+
| **nonnull** | ✓ | ✓ | ✗ | ✗ | ✗ | ✗ | ✗ | Optional |
701+
| **relation** | ✓ | ✓ | ✓ | ✓ | ✗ | ✗ | ✗ | Optional |
702+
| **alignment** | ✓ | ✓ | ✗ | ✗ | ✓ | ✗ | ✗ | Optional |
703+
| **expr** | ✓ | Optional | ✗ | ✗ | ✗ | ✓ | ✗ | ✗ |
704+
| **range** | ✓ | ✓ | ✗ | ✗ | ✗ | ✗ | ✓ | Optional |
705+
706+
**Legend**: ✓ = Required, ✗ = Not allowed/Not used, Optional = May be included
707+
708+
**Important Notes:**
709+
- **`nonnull`**: Only set `target` to an argument (e.g., `arg0`) or `return_value`. The `symbol` field is optional for documentation purposes.
710+
- **`relation`**: Must specify `target`, `relation` operator, and `value` to compare against. Target can be an argument, return value, or symbol reference.
711+
- **`alignment`**: Must specify `target` and `align` (alignment in bytes). Typically used with pointer arguments.
712+
- **`expr`**: Only requires the `expr` field with a free-form expression string. Target and symbol are optional for context.
713+
- **`range`**: Must specify `target` and a `range` object with both `min` and `max` values.
714+
- **`symbol`**: This field is always optional and serves as a descriptive reference to document what variable or symbol the predicate refers to.
715+
716+
#### Target Specification
717+
718+
The `target` field specifies what the predicate applies to:
719+
720+
- **`arg0`, `arg1`, etc.**: Function arguments (0-indexed)
721+
- **`return_value`**: Return value of the function
722+
- **`symbol`**: A named symbol (requires `symbol` field)
723+
724+
#### Relation Types
725+
726+
For `relation` kind predicates:
727+
728+
| Relation | Operators | Description |
729+
|----------|-----------|-------------|
730+
| `eq` | `==` | Equal to |
731+
| `neq` | `!=` | Not equal to |
732+
| `lt` | `<` | Less than |
733+
| `lte` | `<=` | Less than or equal to |
734+
| `gt` | `>` | Greater than |
735+
| `gte` | `>=` | Greater than or equal to |
736+
| `none` | - | No relation (for existence checks) |
737+
738+
### Static Contract Examples
739+
740+
#### Example 1: Non-null Pointer Check (nonnull)
741+
742+
```yaml
743+
preconditions:
744+
- id: "ptr_nonnull"
745+
description: "USB device pointer must not be null"
746+
pred:
747+
kind: "nonnull"
748+
target: "arg0"
749+
symbol: "usb_device" # Optional: for documentation
750+
```
751+
752+
**Required fields for `nonnull`**: `kind`, `target`
753+
754+
#### Example 2: Range Validation (range)
755+
756+
```yaml
757+
preconditions:
758+
- id: "size_range"
759+
description: "Buffer size must be within valid range"
760+
pred:
761+
kind: "range"
762+
target: "arg1"
763+
range:
764+
min: "0"
765+
max: "USB_MAX_PACKET_SIZE"
766+
symbol: "buffer_size" # Optional: for documentation
767+
```
768+
769+
**Required fields for `range`**: `kind`, `target`, `range` (with `min` and `max`)
770+
771+
#### Example 3: Comparison Relation (relation)
772+
773+
```yaml
774+
preconditions:
775+
- id: "size_positive"
776+
description: "Size must be greater than zero"
777+
pred:
778+
kind: "relation"
779+
target: "arg1"
780+
relation: "gt"
781+
value: "0"
782+
symbol: "size" # Optional: for documentation
783+
```
784+
785+
**Required fields for `relation`**: `kind`, `target`, `relation`, `value`
786+
787+
#### Example 4: Memory Alignment (alignment)
788+
789+
```yaml
790+
preconditions:
791+
- id: "buffer_aligned"
792+
description: "Buffer must be 4-byte aligned"
793+
pred:
794+
kind: "alignment"
795+
target: "arg0"
796+
align: "4"
797+
symbol: "buffer" # Optional: for documentation
798+
```
799+
800+
**Required fields for `alignment`**: `kind`, `target`, `align`
801+
802+
#### Example 5: Complex Expression (expr)
803+
804+
```yaml
805+
preconditions:
806+
- id: "device_valid"
807+
description: "USB device must be in configured state"
808+
pred:
809+
kind: "expr"
810+
expr: "usb_device->state == USB_STATE_CONFIGURED"
811+
```
812+
813+
**Required fields for `expr`**: `kind`, `expr`
814+
**Optional fields**: `target`, `symbol` (for documentation)
815+
816+
#### Example 6: Return Value Check (relation)
817+
818+
```yaml
819+
postconditions:
820+
- id: "success_return"
821+
description: "Function must return success code"
822+
pred:
823+
kind: "relation"
824+
target: "return_value"
825+
relation: "eq"
826+
value: "0"
827+
```
828+
829+
**Required fields for `relation` on return value**: `kind`, `target` (set to `return_value`), `relation`, `value`
830+
831+
### Complete Static Contract Example
832+
833+
This example demonstrates all predicate kinds with correct field usage:
834+
835+
```yaml
836+
apiVersion: patchestry.io/v1
837+
838+
metadata:
839+
name: "usb-security-contracts"
840+
version: "1.0.0"
841+
description: "USB security contracts for medical devices"
842+
author: "Security Team"
843+
created: "2025-01-15"
844+
845+
contracts:
846+
- name: "usb_endpoint_write_validation"
847+
id: "USB-CONTRACT-STATIC-001"
848+
description: "Validate USB endpoint write parameters"
849+
category: "write_validation"
850+
severity: "critical"
851+
type: "STATIC"
852+
853+
preconditions:
854+
# Example 1: nonnull predicate
855+
- id: "device_nonnull"
856+
description: "USB device pointer must not be null"
857+
pred:
858+
kind: "nonnull"
859+
symbol: "usb_device" # Optional
860+
861+
# Example 2: nonnull predicate
862+
- id: "buffer_nonnull"
863+
description: "Buffer pointer must not be null"
864+
pred:
865+
kind: "nonnull"
866+
symbol: "buffer" # Optional
867+
868+
# Example 3: range predicate
869+
- id: "size_range"
870+
description: "Write size must be within valid range"
871+
pred:
872+
kind: "range"
873+
target: "arg2"
874+
range:
875+
min: "1"
876+
max: "USB_MAX_PACKET_SIZE"
877+
878+
# Example 4: alignment predicate
879+
- id: "buffer_aligned"
880+
description: "Buffer must be properly aligned"
881+
pred:
882+
kind: "alignment"
883+
target: "arg1"
884+
align: "4"
885+
886+
postconditions:
887+
# Example 5: relation predicate on return value
888+
- id: "return_success"
889+
description: "Function must return success or error code"
890+
pred:
891+
kind: "relation"
892+
target: "return_value"
893+
relation: "gte"
894+
value: "-1"
895+
896+
# Example 6: expr predicate
897+
- id: "state_valid"
898+
description: "Device state must remain valid"
899+
pred:
900+
kind: "expr"
901+
expr: "usb_device->state != USB_STATE_ERROR"
902+
# Note: target and symbol are optional for expr predicates
903+
```
904+
905+
**Summary of field usage by predicate kind:**
906+
- **nonnull**: `kind` + `target` (`arg<N>`, `return_value`, or `symbol`)
907+
- **relation**: `kind` + `target` + `relation` + `value` (`arg<N>`, `return_value`, or `symbol`)
908+
- **alignment**: `kind` + `target` + `align` (`arg<N>`, `return_value`, or `symbol`)
909+
- **expr**: `kind` + `expr`
910+
- **range**: `kind` + `target` + `range` (with `min`/`max`) (`arg<N>`, `return_value`, or `symbol`)
911+
912+
### Runtime Contract Implementation
913+
914+
For runtime contracts, specify the implementation details:
915+
916+
```yaml
917+
contracts:
918+
- name: "usb_endpoint_write_contract"
919+
id: "USB-CONTRACT-001"
920+
description: "Runtime validation for USB endpoint write"
921+
type: "RUNTIME"
922+
923+
implementation:
924+
language: "C"
925+
code_file: "contracts/usb_validation.c"
926+
function_name: "contract::usb_endpoint_write_validation"
927+
parameters:
928+
- name: "usb_device"
929+
type: "usb_device_t*"
930+
description: "USB device context"
931+
- name: "buffer"
932+
type: "const void*"
933+
description: "Data buffer"
934+
- name: "size"
935+
type: "uint32_t"
936+
description: "Buffer size"
937+
```
938+
553939
## Deployment Architecture
554940

555941
The meta-patch architecture allows for:

0 commit comments

Comments
 (0)